types.ml 54.5 KB
Newer Older
1
open Ident
2
open Encodings
3

4
5
6
7
8
9
10
11
let caml_mode = ref false

let count = State.ref "Types.count" 0
		
let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)

12
13
14
15
16
(* TODO:
   - I store hash in types to avoid computing it several times.
     Does not seem to help a lot.
*)

17
18
19
20
21
22
23
24
25
26
(*
To be sure not to use generic comparison ...
*)
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1


27
28
29
module CompUnit = struct   
  include Pool.Make(Utf8)
  module Tbl = Inttbl
30

31
  let pervasives = mk (U.mk "Pervasives") 
32
  let current = ref dummy_min
33
34
35
36
  let get_current () =
    assert (!current != dummy_min);
    !current

37
38
  let print ppf t = Format.fprintf ppf "%a" U.print (value t)

39
40
41
  let print_qual ppf t =
    if (t != !current) && (t != pervasives) then
      Format.fprintf ppf "%a." U.print (value t)
42
      
43
  let close_serialize_ref = ref (fun () -> assert false)
44
      
45
  let depend = Inttbl.create ()
46
      
47
  let serialize t cu =
48
    if (cu != pervasives) && (cu != !current) then Inttbl.add depend cu ();
49
50
51
52
53
54
55
56
57
58
59
    serialize t cu

  let close_serialize () =
    !close_serialize_ref ();
    let deps = Inttbl.fold depend (fun cu () l -> cu :: l) [] in
    Inttbl.clear depend;
    deps


  let stack = ref []
		
60
  let enter i = 
61
62
(*    Format.fprintf Format.std_formatter "Types.CompUnit.enter: %a@." 
      U.print (value i); *)
63
    stack := !current :: !stack; current := i
64
65
66
67
68
69
70
71
72
73
74
		  
  let leave () =
    match !stack with
      | hd::tl -> current := hd; stack := tl
      | _ -> assert false


  let () = enter pervasives
end	  


75
type const = 
76
  | Integer of Intervals.V.t
77
  | Atom of Atoms.V.t 
78
  | Char of Chars.V.t
79
80
81
82
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
83

84
85
86
module Const = struct
  type t = const

87
88
89
90
91
92
93
94
95
96
97
  let rec check = function
    | Integer i -> Intervals.V.check i
    | Atom i -> Atoms.V.check i
    | Char i -> Chars.V.check i
    | Pair (x,y) | Xml (x,y) -> check x; check y
    | Record l -> LabelMap.iter check l
    | String (i,j,s,q) -> U.check s; check q

  let dump ppf _ =
    Format.fprintf ppf "<Types.Const.t>"

98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
  let rec serialize s = function
    | Integer x ->
	Serialize.Put.bits 3 s 0;
	Intervals.V.serialize s x
    | Atom x ->
	Serialize.Put.bits 3 s 1;
	Atoms.V.serialize s x
    | Char x ->
	Serialize.Put.bits 3 s 2;
	Chars.V.serialize s x
    | Pair (x,y) ->
	Serialize.Put.bits 3 s 3;
	serialize s x;
	serialize s y
    | Xml (x,y) ->
	Serialize.Put.bits 3 s 4;
	serialize s x;
	serialize s y
    | Record r ->
	Serialize.Put.bits 3 s 5;
	LabelMap.serialize serialize s r
    | String (i,j,st,q) ->
	Serialize.Put.bits 3 s 6;
	U.serialize_sub s st i j;
	serialize s q

  let rec deserialize s =
    match Serialize.Get.bits 3 s with
      | 0 ->
	  Integer (Intervals.V.deserialize s)
      | 1 ->
	  Atom (Atoms.V.deserialize s)
130
131
      | 2 ->
	  Char (Chars.V.deserialize s)
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
      | 3 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  Pair (x,y)
      | 4 ->
	  let x = deserialize s in
	  let y = deserialize s in
	  Xml (x,y)
      | 5 ->
	  Record (LabelMap.deserialize deserialize s)
      | 6 ->
	  let st = U.deserialize s in
	  let q = deserialize s in
	  String (U.start_index st, U.end_index st, st, q)
      | _ ->
	  assert false

  let rec compare c1 c2 = match (c1,c2) with
150
    | Integer x, Integer y -> Intervals.V.compare x y
151
152
    | Integer _, _ -> -1
    | _, Integer _ -> 1
153
    | Atom x, Atom y -> Atoms.V.compare x y
154
155
    | Atom _, _ -> -1
    | _, Atom _ -> 1
156
    | Char x, Char y -> Chars.V.compare x y
157
158
159
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
160
161
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
162
163
164
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
165
166
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
167
168
169
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
170
	LabelMap.compare compare x y
171
172
173
174
175
176
177
    | Record _, _ -> -1
    | _, Record _ -> 1
    | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
	let c = Pervasives.compare i1 i2 in if c <> 0 then c 
	else let c = Pervasives.compare j1 j2 in if c <> 0 then c
	else let c = U.compare s1 s2 in if c <> 0 then c (* Should compare
							    only the substring *)
178
179
180
181
182
183
184
185
186
187
	else compare r1 r2

  let rec hash = function
    | Integer x -> 1 + 17 * (Intervals.V.hash x)
    | Atom x -> 2 + 17 * (Atoms.V.hash x)
    | Char x -> 3 + 17 * (Chars.V.hash x)
    | Pair (x,y) -> 4 + 17 * (hash x) + 257 * (hash y)
    | Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
    | Record x -> 6 + 17 * (LabelMap.hash hash x)
    | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
188
      (* Note: improve hash for String *)
189

190
191
  let equal c1 c2 = compare c1 c2 = 0
end
192

193
194
module Abstract =
struct
195
  module T = Custom.String
196
197
198
199
200
201
202
203
204
205
  type abs = T.t

  module V =
  struct
    type t = abs * Obj.t
  end

  include SortedList.FiniteCofinite(T)

  let print = function
206
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
207
208
209
210
211
    | Cofinite l ->       
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
212
213
214
215

end


216
217
type pair_kind = [ `Normal | `XML ]

218

219
220
221
222
223
224
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
225
  but a  bug (?) in OCaml 3.07 makes it impossible
226
227
*)
  type t = {
228
    mutable hash: int;
229
230
231
232
233
234
235
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
236
    abstract: Abstract.t;
237
238
    absent: bool
  }
239
  val empty: t
240
241
242
243
244
245
246
247
248
249
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
  val serialize: t Serialize.Put.f
  val deserialize: t Serialize.Get.f
end =
struct
  type t = {
250
    mutable hash: int;
251
252
253
254
255
256
257
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
258
    abstract: Abstract.t;
259
260
    absent: bool
  }
261

262
263
264
265
266
267
268
269
270
  let print_lst ppf =
    List.iter (fun f -> f ppf; Format.fprintf ppf " |")

  let dump ppf d =
    Format.fprintf ppf "<types atoms(%a) times(%a) record(%a) xml(%a)>"
      print_lst (Atoms.print d.atoms)
      BoolPair.dump d.times
      BoolRec.dump d.record
      BoolPair.dump d.xml
271

272
273
274
275
276
277
278
279
280
  let empty = { 
    hash = 0;
    times = BoolPair.empty; 
    xml   = BoolPair.empty; 
    arrow = BoolPair.empty; 
    record= BoolRec.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    chars = Chars.empty;
281
    abstract = Abstract.empty;
282
283
284
    absent= false;
  }

285
  let equal a b =
286
287
288
289
290
291
292
293
    (a == b) || (
      (Atoms.equal a.atoms b.atoms) &&
      (Chars.equal a.chars b.chars) &&
      (Intervals.equal a.ints  b.ints) &&
      (BoolPair.equal a.times b.times) &&
      (BoolPair.equal a.xml b.xml) &&
      (BoolPair.equal a.arrow b.arrow) &&
      (BoolRec.equal a.record b.record) &&
294
      (Abstract.equal a.abstract b.abstract) &&
295
296
      (a.absent == b.absent)
    )
297
298
299
300
301
302
303
304
305
306

  let compare a b =
    if a == b then 0 
    else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = Chars.compare a.chars b.chars in if c <> 0 then c
    else let c = Intervals.compare a.ints b.ints in if c <> 0 then c
    else let c = BoolPair.compare a.times b.times in if c <> 0 then c
    else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
    else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
    else let c = BoolRec.compare a.record b.record in if c <> 0 then c
307
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
308
309
310
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
311
      
312
  let hash a =
313
314
315
316
317
318
319
320
    if a.hash <> 0 then a.hash else (
      let accu = Chars.hash a.chars in
      let accu = 17 * accu + Intervals.hash a.ints in
      let accu = 17 * accu + Atoms.hash a.atoms in
      let accu = 17 * accu + BoolPair.hash a.times in
      let accu = 17 * accu + BoolPair.hash a.xml in
      let accu = 17 * accu + BoolPair.hash a.arrow in
      let accu = 17 * accu + BoolRec.hash a.record in
321
      let accu = 17 * accu + Abstract.hash a.abstract in
322
323
324
325
      let accu = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
326

327
328
329
330
331
332
333
334
  let check a =
    Chars.check a.chars;
    Intervals.check a.ints;
    Atoms.check a.atoms;
    BoolPair.check a.times;
    BoolPair.check a.xml;
    BoolPair.check a.arrow;
    BoolRec.check a.record;
335
    Abstract.check a.abstract;
336
337
338
    ()


339
340
341
342
343
344
345
346
  let serialize t a =
    Chars.serialize t a.chars;
    Intervals.serialize t a.ints;
    Atoms.serialize t a.atoms;
    BoolPair.serialize t a.times;
    BoolPair.serialize t a.xml;
    BoolPair.serialize t a.arrow;
    BoolRec.serialize t a.record;
347
    Abstract.serialize t a.abstract;
348
349
350
351
352
353
354
355
356
357
    Serialize.Put.bool t a.absent 

  let deserialize t =
    let chars = Chars.deserialize t in
    let ints = Intervals.deserialize t in
    let atoms = Atoms.deserialize t in
    let times = BoolPair.deserialize t in
    let xml = BoolPair.deserialize t in
    let arrow = BoolPair.deserialize t in
    let record = BoolRec.deserialize t in
358
    let abstract = Abstract.deserialize t in
359
    let absent = Serialize.Get.bool t in
360
    let d = { hash=0; 
361
      chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
362
      arrow = arrow; record = record; abstract = abstract; absent = absent } in
363
364
    check d;
    d
365
366
   
    
367
368
369
end
and Node :
sig
370
  type t = { id : int; comp_unit: CompUnit.t; mutable descr : Descr.t }
371
372
373
374
375
376
377
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
  val serialize: t Serialize.Put.f
  val deserialize: t Serialize.Get.f
378
  val mk: int -> Descr.t -> t
379
  val clear_deserialize_table: unit -> unit
380
end =
381

382
struct
383
  type t = { id : int; comp_unit : CompUnit.t; mutable descr : Descr.t }
384
  let check n = ()
385
  let dump ppf n = Format.fprintf ppf "X%i" n.id
386
387
  let hash x = x.id + 17 * x.comp_unit
  let compare x y = 
388
    assert(x.id != y.id || x.comp_unit != y.comp_unit || x == y);
389
390
    let c = x.id - y.id in
    if c = 0 then x.comp_unit - y.comp_unit else c
391
  let equal x y = x == y
392

393
394
395
396
397
398
  let serialize_memo = Inttbl.create ()
  let counter_serialize = ref 0

  let () =
    CompUnit.close_serialize_ref := 
    (fun () ->
399
(*       Format.fprintf Format.std_formatter "Close_serialize@."; *)
400
401
       Inttbl.clear serialize_memo;
       counter_serialize := 0)
402

403
  let serialize t n = 
404
405
406
407
    if n.comp_unit == !CompUnit.current then (
      Serialize.Put.bool t true;
      try 
	let i = Inttbl.find serialize_memo n.id in
408
409
410
(*	Format.fprintf Format.std_formatter 
	  "serialize node (memo) id=%i i=%i@."
	  n.id i;  *)
411
412
413
414
	Serialize.Put.int t i
      with Not_found ->
	let i = !counter_serialize in
	incr counter_serialize;
415
416
(*	Format.fprintf Format.std_formatter "serialize node id=%i i=%i@."
	  n.id i;  *)
417
418
419
420
421
422
423
	Inttbl.add serialize_memo n.id i;
	Serialize.Put.int t i;
	Descr.serialize t n.descr
    ) else (
      Serialize.Put.bool t false;
      CompUnit.serialize t n.comp_unit;
      Serialize.Put.int t n.id
424
    )
425
      
426

427
428
429
430
  let deserialize_memo = Inttbl.create ()

  let find_tbl id =
    try Inttbl.find deserialize_memo id
431
    with Not_found ->
432
433
434
435
      let tbl = Inttbl.create () in
      Inttbl.add deserialize_memo id tbl;
      tbl

436
437
438
  let clear_deserialize_table () =
    Inttbl.remove deserialize_memo !CompUnit.current

439
  let mk id d =
440
441
(*    Format.fprintf Format.std_formatter "mk cu=%a i=%i@." 
      CompUnit.print !CompUnit.current id; *)
442
443
444
445
446
447
448
449
    let n = { id = id; comp_unit = !CompUnit.current; descr = d } in
    if !CompUnit.current == CompUnit.pervasives then
      Inttbl.add (find_tbl CompUnit.pervasives) n.id n;
    n

  let deserialize t = 
    if Serialize.Get.bool t then
      let i = Serialize.Get.int t in
450
(*      Format.fprintf Format.std_formatter "deserialize i=%i@." i; *)
451
452
453
      let tbl = find_tbl !CompUnit.current in
      try Inttbl.find tbl i
      with Not_found ->
454
455
456
	let id = if !caml_mode then (incr count;!count) else i in
(*	Format.fprintf Format.std_formatter "... not found ==> %i@." id; *)
	let n = mk id Descr.empty in
457
458
459
460
461
462
	Inttbl.add tbl i n;
	n.descr <- Descr.deserialize t;
	n
    else
      let cu = CompUnit.deserialize t in
      let i = Serialize.Get.int t in
463
464
(*      Format.fprintf Format.std_formatter "deserialize cu=%a i=%i@." 
	CompUnit.print cu i; *)
465
466
467
      try Inttbl.find (Inttbl.find deserialize_memo cu) i 
      with Not_found -> assert false

468
469
end

470
471
472
473
474
475
476
477
478
479
480
481
482
483
(* See PR#2920 in OCaml BTS *)
and NodeT : Custom.T with type t = Node.t =
struct
  type t = Node.t
  let dump x = Node.dump x
  let check x = Node.check x
  let equal x = Node.equal x
  let hash x = Node.hash x
  let compare x = Node.compare x
  let serialize x = Node.serialize x
  let deserialize x = Node.deserialize x
end


484
(* It is also possible to use Boolean instead of Bool here;
485
   need to analyze when each one is more efficient *)
486
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
487
Bool.Simplify(Bool.Make)(Custom.Pair(NodeT)(NodeT))
488
489

and BoolRec : Bool.S with type elem = bool * Node.t label_map =
490
(*Bool.Simplify*)(Bool.Make)(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(NodeT)))
491

492
493
494
495
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
496

497
498
499
type descr = Descr.t
type node = Node.t
include Descr
500

501
502
503
let clear_deserialize_table = Node.clear_deserialize_table


504
505
let forward_print = ref (fun _ _ -> assert false)

506
507
508
509
let make () = 
  incr count; 
  Node.mk !count empty

510
511
512
(*
let hash_cons = DescrHash.create 17000  

513
514
515
let define n d = 
  DescrHash.add hash_cons d n; 
  n.Node.descr <- d
516

517
518
519
520
let cons d = 
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
521
    let n = Node.mk !count d in
522
    DescrHash.add hash_cons d n; n  
523
524
525
526
527
528
529
530
531
*)

let define n d = 
  n.Node.descr <- d

let cons d = 
  incr count; 
  Node.mk !count d

532

533
let any =  {
534
  hash = 0;
535
536
537
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
538
  record= BoolRec.full; 
539
540
541
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
542
  abstract = Abstract.any;
543
  absent= false;
544
}
545

546

547
let non_constructed =
548
549
550
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
551
     
552
553
let non_constructed_or_absent = 
  { non_constructed with hash = 0; absent = true }
554
	     
555
556
557
558
let interval i = { empty with hash = 0; ints = i }
let times x y = { empty with hash = 0; times = BoolPair.atom (x,y) }
let xml x y = { empty with hash = 0; xml = BoolPair.atom (x,y) }
let arrow x y = { empty with hash = 0; arrow = BoolPair.atom (x,y) }
559
let record label t = 
560
561
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
562
let record_fields (x : bool * node Ident.label_map) =
563
564
565
  { empty with hash = 0; record = BoolRec.atom x }
let atom a = { empty with hash = 0; atoms = a }
let char c = { empty with hash = 0; chars = c }
566
567
568
let abstract a = { empty with hash = 0; abstract = a }

let get_abstract t = t.abstract
569
      
570
571
let cup x y = 
  if x == y then x else {
572
    hash = 0;
573
574
575
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
576
    record= BoolRec.cup x.record y.record;
577
578
579
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
580
    abstract = Abstract.cup x.abstract y.abstract;
581
    absent= x.absent || y.absent;
582
583
584
585
  }
    
let cap x y = 
  if x == y then x else {
586
    hash = 0;
587
588
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
589
    record= BoolRec.cap x.record y.record;
590
    arrow = BoolPair.cap x.arrow y.arrow;
591
592
593
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
594
    abstract = Abstract.cap x.abstract y.abstract;
595
    absent= x.absent && y.absent;
596
597
598
599
  }
    
let diff x y = 
  if x == y then empty else {
600
    hash = 0;
601
602
603
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
604
    record= BoolRec.diff x.record y.record;
605
606
607
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
608
    abstract = Abstract.diff x.abstract y.abstract;
609
    absent= x.absent && not y.absent;
610
611
  }
    
612

613

614

615
616
617
618
619
620
621
622
(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
  (Chars.disjoint a.chars b.chars) &&
  (Intervals.disjoint a.ints b.ints) &&
  (Atoms.disjoint a.atoms b.atoms) &&
  (BoolPair.trivially_disjoint a.times b.times) &&
  (BoolPair.trivially_disjoint a.xml b.xml) &&
  (BoolPair.trivially_disjoint a.arrow b.arrow) &&
623
  (BoolRec.trivially_disjoint a.record b.record) &&
624
  (Abstract.disjoint a.abstract b.abstract) &&
625
  (not (a.absent && b.absent))
626

627

628

629
let descr n = n.Node.descr
630
let internalize n = n
631
let id n = n.Node.id
632
633


634
635
636
637
638
let rec constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
  | Pair (x,y) -> times (const_node x) (const_node y)
639
  | Xml (x,y) -> xml (const_node x) (const_node y)
640
  | Record x -> record_fields (false ,LabelMap.map const_node x)
641
642
643
644
645
646
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
      else 
	let (ch,i') = U.next s i in
	constant (Pair (Char (Chars.V.mk_int ch), String (i',j,s,c)))
and const_node c = cons (constant c)
647

648
649
let neg x = diff any x

650
let any_node = cons any
651
let empty_node = cons empty
652

653
module LabelS = Set.Make(LabelPool)
654

655
656
657
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

658
659
let get_record r =
  let labs accu (_,r) = 
660
661
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
662
  let extend descrs labs (o,r) =
663
664
665
666
667
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
668
	      | (l2,x)::r when l1 == l2 -> 
669
670
671
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
672
673
		  if not o then 
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
674
675
		  aux (i+1) labs r
    in
676
    aux 0 labs (LabelMap.get r);
677
678
679
680
    o
  in
  let line (p,n) =
    let labels = 
681
682
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
683
    let nlab = List.length labels in
684
    let mk () = Array.create nlab any_or_absent in
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699

    let pos = mk () in
    let opos = List.fold_left 
		 (fun accu x -> 
		    (extend pos labels x) && accu)
		 true p in
    let p = (opos, pos) in

    let n = List.map (fun x ->
			let neg = mk () in
			let o = extend neg labels x in
			(o,neg)
		     ) n in
    (labels,p,n)
  in
700
  List.map line (BoolRec.get r)
701
   
702

703

704
705
706
707
708
709
710


(* Subtyping algorithm *)

let diff_t d t = diff d (descr t)
let cap_t d t = cap d (descr t)
let cup_t d t = cup d (descr t)
711
let cap_product any_left any_right l =
712
713
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
714
    (any_left,any_right)
715
    l
716
let any_pair = { empty with hash = 0; times = any.times }
717

718

719
720
721
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

722
exception NotEmpty
723

724
725
726
727
728
729
730
731
732
733
734
735
type slot = { mutable status : status; 
	       mutable notify : notify;
	       mutable active : bool }
and status = Empty | NEmpty | Maybe
and notify = Nothing | Do of slot * (slot -> unit) * notify

let slot_empty = { status = Empty; active = false; notify = Nothing }
let slot_not_empty = { status = NEmpty; active = false; notify = Nothing }

let rec notify = function
  | Nothing -> ()
  | Do (n,f,rem) -> 
736
      if n.status == Maybe then (try f n with NotEmpty -> ());
737
738
739
740
741
742
743
744
745
746
      notify rem

let rec iter_s s f = function
  | [] -> ()
  | arg::rem -> f arg s; iter_s s f rem


let set s =
  s.status <- NEmpty;
  notify s.notify;
747
  s.notify <- Nothing; 
748
749
750
751
752
753
754
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
755
756
757
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
758
759
760
	try 
	  f arg s;
	  if s.active then n.active <- true
761
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
762

763
764
let guard a f n =
  match a with
765
    | { status = Empty } -> ()
766
767
768
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
769
    | { status = NEmpty } -> f n
770

771
772
773
774
775
776

(* Fast approximation *)

module ClearlyEmpty = 
struct

777
let memo = DescrHash.create 8191
778
779
780
781
782
783
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
784
	  (Abstract.is_empty d.abstract) &&
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
	  (not d.absent)) then slot_not_empty 
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_xml (BoolPair.get d.xml); 
       iter_s s check_arrow (BoolPair.get d.arrow);
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

and check_times (left,right) s =
  let (accu1,accu2) = cap_product any any left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_xml (left,right) s =
  let (accu1,accu2) = cap_product any any_pair left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_arrow (left,right) s =
  let single_right (s1,s2) s =
    let accu1 = descr s1 and accu2 = neg (descr s2) in
    let single_left (t1,t2) s =
      let accu1 = diff_t accu1 t1 in guard (slot accu1) set s;
      let accu2 = cap_t  accu2 t2 in guard (slot accu2) set s
    in
    guard (slot accu1) (big_conj single_left left) s
  in
  big_conj single_right right s

and check_record (labels,(oleft,left),rights) s =
  let rec single_right (oright,right) s = 
    let next =
      (oleft && (not oright)) ||
      exists (Array.length left)
	(fun i -> trivially_disjoint left.(i) right.(i))
    in
    if next then set s
    else
      for i = 0 to Array.length left - 1 do
	let di = diff left.(i) right.(i) in guard (slot di) set s
      done
  in
  let rec start i s =
    if (i < 0) then big_conj single_right rights s
    else guard (slot left.(i)) (start (i - 1)) s
  in
  start (Array.length left - 1) s


let is_empty d =
  let s = slot d in
  List.iter 
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
  s.status == Empty
end

let clearly_disjoint t1 t2 =
(*
  if trivially_disjoint t1 t2 then true
  else
    if ClearlyEmpty.is_empty (cap t1 t2) then
      (Printf.eprintf "!\n"; true) else false
*)
  trivially_disjoint t1 t2 || ClearlyEmpty.is_empty (cap t1 t2) 

870
871
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

872
let memo = DescrHash.create 8191
873
874
let marks = ref [] 

875
876
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

877
878
let complex = ref 0

879
let rec slot d =
880
  incr complex;
881
  Stats.Counter.incr count_subtype; 
882
883
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
884
	  (Chars.is_empty d.chars) &&
885
	  (Abstract.is_empty d.abstract) &&
886
	  (not d.absent)) then slot_not_empty 
887
888
889
890
891
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
892
       iter_s s check_times (BoolPair.get d.times);  
893
       iter_s s check_xml (BoolPair.get d.xml); 
894
       iter_s s check_arrow (BoolPair.get d.arrow);
895
896
897
898
899
900
901
902
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

and check_times (left,right) s =
  let rec aux accu1 accu2 right s = match right with
903
904
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
905
906
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
907
908
	     aux accu1 accu2 right s )
	else (
909
          let accu1' = diff accu1 t1 in 
910
	  guard (slot accu1') (aux accu1' accu2 right) s;
911
912

          let accu2' = diff accu2 t2 in 
913
	  guard (slot accu2') (aux accu1 accu2' right) s  
914
	)
915
916
    | [] -> set s
  in
917
  let (accu1,accu2) = cap_product any any left in
918
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
919
920
921

and check_xml (left,right) s =
  let rec aux accu1 accu2 right s = match right with
922
923
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
924
	if clearly_disjoint accu1 t1 || 
925
926
927
928
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
929
	  guard (slot accu1') (aux accu1' accu2 right) s;
930
931

          let accu2' = diff accu2 t2 in 
932
	  guard (slot accu2') (aux accu1 accu2' right) s  
933
934
935
936
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
937
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
938

939
940
941
942
and check_arrow (left,right) s =
  let single_right (s1,s2) s =
    let rec aux accu1 accu2 left s = match left with
      | (t1,t2)::left ->
943
          let accu1' = diff_t accu1 t1 in 
944
	  guard (slot accu1') (aux accu1' accu2 left) s;
945
946

          let accu2' = cap_t  accu2 t2 in 
947
	  guard (slot accu2') (aux accu1 accu2' left) s
948
949
950
      | [] -> set s
    in
    let accu1 = descr s1 in
951
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
952
953
  in
  big_conj single_right right s
954

955
and check_record (labels,(oleft,left),rights) s =
956
  let rec aux left rights s = match rights with
957
    | [] -> set s
958
    | (oright,right)::rights ->
959
	let next =
960
	  (oleft && (not oright)) ||
961
	  exists (Array.length left)
962
	    (fun i -> trivially_disjoint left.(i) right.(i))
963
	in
964
	if next then aux left rights s
965
966
	else
	  for i = 0 to Array.length left - 1 do
967
968
969
970
	    let left' = Array.copy left in
	    let di = diff left.(i) right.(i) in
	    left'.(i) <- di;
	    guard (slot di) (aux left' rights) s;
971
972
973
	  done
  in
  let rec start i s =
974
    if (i < 0) then aux left rights s
975
    else
976
      guard (slot left.(i)) (start (i - 1)) s
977
978
979
980
  in
  start (Array.length left - 1) s


981

982
let timer_subtype = Stats.Timer.create "Types.is_empty"
983

984

985
let is_empty d =
986
  Stats.Timer.start timer_subtype; 
987
988
  let s = slot d in
  List.iter 
989
990
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
991
992
    !marks;
  marks := [];
993
  Stats.Timer.stop timer_subtype 
994
    (s.status == Empty)
995

996
(*
997
let is_empty d =
998
999
1000
1001
1002
1003
1004
(*  let b1 = ClearlyEmpty.is_empty d in
  let b2 = is_empty d in
  assert (b2 || not b1);
  Printf.eprintf "b1 = %b; b2 = %b\n" b1 b2;
  b2  *)
  if ClearlyEmpty.is_empty d then (Printf.eprintf "!\n"; true) else is_empty d
*)  
1005

1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
(*
let is_empty d =
(*  Format.fprintf Format.std_formatter "complex=%i@."
	  !complex; *)
  if !complex = 0 then
    (let r = is_empty d in
     if !complex > 100 then
       (let c = !complex in
	Format.fprintf Format.std_formatter "is_empty (%i)@." c
	  (*Descr.dump (*!forward_print*) d*));
     complex := 0; r)
  else is_empty d
*)

1020
1021
1022
1023
1024
1025
let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

1026
1027
1028
let disjoint d1 d2 =
  is_empty (cap d1 d2)

1029
1030
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

1031
1032
1033
1034
1035
1036
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
1037
1038
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
1039
1040
1041
1042
1043

  let is_product ?kind d = is_empty (other ?kind d)

  let need_second = function _::_::_ -> true | _ -> false

1044
1045
1046
1047
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

1048
1049
1050
1051
1052
1053
1054
    let res = ref [] in

    let add (t1,t2) =
      let rec loop t1 t2 = function
	| [] -> res := (ref (t1,t2)) :: !res
	| ({contents = (d1,d2)} as r)::l ->
	    (*OPT*) 
1055
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
	      
	      let i = cap t1 d1 in
	      if is_empty i then loop t1 t2 l
	      else (
		r := (i, cup t2 d2);
		let k = diff d1 t1 in 
		if non_empty k then res := (ref (k,d2)) :: !res;
		
		let j = diff t1 d1 in 
		if non_empty j then loop j t2 l
	      )
      in
      loop t1 t2 !res
    in
    List.iter add d;
    List.map (!) !res


(* Partitioning:

(t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
=
(t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)

1080
*)
Pietro Abate's avatar