types.ml 54.3 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.Make(Custom.Pair(NodeT)(NodeT))
488
489

and BoolRec : Bool.S with type elem = bool * Node.t label_map =
490
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
let hash_cons = DescrHash.create 17000  

508
509
510
511
512
      
let make () = 
  incr count; 
  Node.mk !count empty

513
514
515
516
517
518
519
let define n d = 
  DescrHash.add hash_cons d n; 
  n.Node.descr <- d
let cons d = 
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
520
    let n = Node.mk !count d in
521
522
    DescrHash.add hash_cons d n; n  

523
let any =  {
524
  hash = 0;
525
526
527
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
528
  record= BoolRec.full; 
529
530
531
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
532
  abstract = Abstract.any;
533
  absent= false;
534
}
535

536

537
let non_constructed =
538
539
540
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
541
     
542
543
let non_constructed_or_absent = 
  { non_constructed with hash = 0; absent = true }
544
	     
545
546
547
548
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) }
549
let record label t = 
550
551
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
552
let record_fields (x : bool * node Ident.label_map) =
553
554
555
  { 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 }
556
557
558
let abstract a = { empty with hash = 0; abstract = a }

let get_abstract t = t.abstract
559
      
560
561
let cup x y = 
  if x == y then x else {
562
    hash = 0;
563
564
565
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
566
    record= BoolRec.cup x.record y.record;
567
568
569
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
570
    abstract = Abstract.cup x.abstract y.abstract;
571
    absent= x.absent || y.absent;
572
573
574
575
  }
    
let cap x y = 
  if x == y then x else {
576
    hash = 0;
577
578
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
579
    record= BoolRec.cap x.record y.record;
580
    arrow = BoolPair.cap x.arrow y.arrow;
581
582
583
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
584
    abstract = Abstract.cap x.abstract y.abstract;
585
    absent= x.absent && y.absent;
586
587
588
589
  }
    
let diff x y = 
  if x == y then empty else {
590
    hash = 0;
591
592
593
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
594
    record= BoolRec.diff x.record y.record;
595
596
597
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
598
    abstract = Abstract.diff x.abstract y.abstract;
599
    absent= x.absent && not y.absent;
600
601
  }
    
602

603

604

605
606
607
608
609
610
611
612
(* 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) &&
613
  (BoolRec.trivially_disjoint a.record b.record) &&
614
  (Abstract.disjoint a.abstract b.abstract) &&
615
  (not (a.absent && b.absent))
616

617

618

619
let descr n = n.Node.descr
620
let internalize n = n
621
let id n = n.Node.id
622
623


624
625
626
627
628
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)
629
  | Xml (x,y) -> xml (const_node x) (const_node y)
630
  | Record x -> record_fields (false ,LabelMap.map const_node x)
631
632
633
634
635
636
  | 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)
637

638
639
let neg x = diff any x

640
let any_node = cons any
641
let empty_node = cons empty
642

643
module LabelS = Set.Make(LabelPool)
644

645
646
647
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

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

    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
690
  List.map line (BoolRec.get r)
691
   
692

693

694
695
696
697
698
699
700


(* 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)
701
let cap_product any_left any_right l =
702
703
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
704
    (any_left,any_right)
705
    l
706
let any_pair = { empty with hash = 0; times = any.times }
707

708

709
710
711
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

712
exception NotEmpty
713

714
715
716
717
718
719
720
721
722
723
724
725
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) -> 
726
      if n.status == Maybe then (try f n with NotEmpty -> ());
727
728
729
730
731
732
733
734
735
736
      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;
737
  s.notify <- Nothing; 
738
739
740
741
742
743
744
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
745
746
747
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
748
749
750
	try 
	  f arg s;
	  if s.active then n.active <- true
751
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
752

753
754
let guard a f n =
  match a with
755
    | { status = Empty } -> ()
756
757
758
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
759
    | { status = NEmpty } -> f n
760

761
762
763
764
765
766
767
768
769
770
771
772
773

(* Fast approximation *)

module ClearlyEmpty = 
struct

let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
774
	  (Abstract.is_empty d.abstract) &&
775
776
777
778
779
780
781
782
783
784
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
	  (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) 

860
861
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

862
863
864
let memo = DescrHash.create 33000
let marks = ref [] 

865
866
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

867
868
let complex = ref 0

869
let rec slot d =
870
  incr complex;
871
  Stats.Counter.incr count_subtype; 
872
873
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
874
	  (Chars.is_empty d.chars) &&
875
	  (Abstract.is_empty d.abstract) &&
876
	  (not d.absent)) then slot_not_empty 
877
878
879
880
881
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
882
       iter_s s check_times (BoolPair.get d.times);  
883
       iter_s s check_xml (BoolPair.get d.xml); 
884
       iter_s s check_arrow (BoolPair.get d.arrow);
885
886
887
888
889
890
891
892
       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
893
894
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
895
896
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
897
898
	     aux accu1 accu2 right s )
	else (
899
          let accu1' = diff accu1 t1 in 
900
	  guard (slot accu1') (aux accu1' accu2 right) s;
901
902

          let accu2' = diff accu2 t2 in 
903
	  guard (slot accu2') (aux accu1 accu2' right) s  
904
	)
905
906
    | [] -> set s
  in
907
  let (accu1,accu2) = cap_product any any left in
908
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
909
910
911

and check_xml (left,right) s =
  let rec aux accu1 accu2 right s = match right with
912
913
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
914
	if clearly_disjoint accu1 t1 || 
915
916
917
918
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
919
	  guard (slot accu1') (aux accu1' accu2 right) s;
920
921

          let accu2' = diff accu2 t2 in 
922
	  guard (slot accu2') (aux accu1 accu2' right) s  
923
924
925
926
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
927
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
928

929
930
931
932
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 ->
933
          let accu1' = diff_t accu1 t1 in 
934
	  guard (slot accu1') (aux accu1' accu2 left) s;
935
936

          let accu2' = cap_t  accu2 t2 in 
937
	  guard (slot accu2') (aux accu1 accu2' left) s
938
939
940
      | [] -> set s
    in
    let accu1 = descr s1 in
941
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
942
943
  in
  big_conj single_right right s
944

945
and check_record (labels,(oleft,left),rights) s =
946
  let rec aux left rights s = match rights with
947
    | [] -> set s
948
    | (oright,right)::rights ->
949
	let next =
950
	  (oleft && (not oright)) ||
951
	  exists (Array.length left)
952
	    (fun i -> trivially_disjoint left.(i) right.(i))
953
	in
954
	if next then aux left rights s
955
956
	else
	  for i = 0 to Array.length left - 1 do
957
958
959
960
	    let left' = Array.copy left in
	    let di = diff left.(i) right.(i) in
	    left'.(i) <- di;
	    guard (slot di) (aux left' rights) s;
961
962
963
	  done
  in
  let rec start i s =
964
    if (i < 0) then aux left rights s
965
    else
966
      guard (slot left.(i)) (start (i - 1)) s
967
968
969
970
  in
  start (Array.length left - 1) s


971

972
let timer_subtype = Stats.Timer.create "Types.is_empty"
973

974

975
let is_empty d =
976
  Stats.Timer.start timer_subtype; 
977
978
  let s = slot d in
  List.iter 
979
980
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
981
982
    !marks;
  marks := [];
983
  Stats.Timer.stop timer_subtype 
984
    (s.status == Empty)
985

986
(*
987
let is_empty d =
988
989
990
991
992
993
994
(*  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
*)  
995

996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
(*
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
*)

1010
1011
1012
1013
1014
1015
let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

1016
1017
1018
let disjoint d1 d2 =
  is_empty (cap d1 d2)

1019
1020
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

1021
1022
1023
1024
1025
1026
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
1027
1028
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
1029
1030
1031
1032
1033

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

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

1034
1035
1036
1037
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

1038
1039
1040
1041
1042
1043
1044
    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*)