types.ml 53.7 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
  let dump ppf _ =
    Format.fprintf ppf "<Types.Descr.t>"

265
266
267
268
269
270
271
272
273
  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;
274
    abstract = Abstract.empty;
275
276
277
    absent= false;
  }

278
  let equal a b =
279
280
281
282
283
284
285
286
    (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) &&
287
      (Abstract.equal a.abstract b.abstract) &&
288
289
      (a.absent == b.absent)
    )
290
291
292
293
294
295
296
297
298
299

  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
300
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
301
302
303
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
304
      
305
  let hash a =
306
307
308
309
310
311
312
313
    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
314
      let accu = 17 * accu + Abstract.hash a.abstract in
315
316
317
318
      let accu = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
319

320
321
322
323
324
325
326
327
  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;
328
    Abstract.check a.abstract;
329
330
331
    ()


332
333
334
335
336
337
338
339
  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;
340
    Abstract.serialize t a.abstract;
341
342
343
344
345
346
347
348
349
350
    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
351
    let abstract = Abstract.deserialize t in
352
    let absent = Serialize.Get.bool t in
353
    let d = { hash=0; 
354
      chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
355
      arrow = arrow; record = record; abstract = abstract; absent = absent } in
356
357
    check d;
    d
358
359
   
    
360
361
362
end
and Node :
sig
363
  type t = { id : int; comp_unit: CompUnit.t; mutable descr : Descr.t }
364
365
366
367
368
369
370
  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
371
  val mk: int -> Descr.t -> t
372
  val clear_deserialize_table: unit -> unit
373
end =
374

375
struct
376
  type t = { id : int; comp_unit : CompUnit.t; mutable descr : Descr.t }
377
378
  let check n = ()
  let dump ppf n = failwith "Types.Node.dump"
379
380
  let hash x = x.id + 17 * x.comp_unit
  let compare x y = 
381
    assert(x.id != y.id || x.comp_unit != y.comp_unit || x == y);
382
383
    let c = x.id - y.id in
    if c = 0 then x.comp_unit - y.comp_unit else c
384
  let equal x y = x == y
385

386
387
388
389
390
391
  let serialize_memo = Inttbl.create ()
  let counter_serialize = ref 0

  let () =
    CompUnit.close_serialize_ref := 
    (fun () ->
392
(*       Format.fprintf Format.std_formatter "Close_serialize@."; *)
393
394
       Inttbl.clear serialize_memo;
       counter_serialize := 0)
395

396
  let serialize t n = 
397
398
399
400
    if n.comp_unit == !CompUnit.current then (
      Serialize.Put.bool t true;
      try 
	let i = Inttbl.find serialize_memo n.id in
401
402
403
(*	Format.fprintf Format.std_formatter 
	  "serialize node (memo) id=%i i=%i@."
	  n.id i;  *)
404
405
406
407
	Serialize.Put.int t i
      with Not_found ->
	let i = !counter_serialize in
	incr counter_serialize;
408
409
(*	Format.fprintf Format.std_formatter "serialize node id=%i i=%i@."
	  n.id i;  *)
410
411
412
413
414
415
416
	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
417
    )
418
      
419

420
421
422
423
  let deserialize_memo = Inttbl.create ()

  let find_tbl id =
    try Inttbl.find deserialize_memo id
424
    with Not_found ->
425
426
427
428
      let tbl = Inttbl.create () in
      Inttbl.add deserialize_memo id tbl;
      tbl

429
430
431
  let clear_deserialize_table () =
    Inttbl.remove deserialize_memo !CompUnit.current

432
  let mk id d =
433
434
(*    Format.fprintf Format.std_formatter "mk cu=%a i=%i@." 
      CompUnit.print !CompUnit.current id; *)
435
436
437
438
439
440
441
442
    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
443
(*      Format.fprintf Format.std_formatter "deserialize i=%i@." i; *)
444
445
446
      let tbl = find_tbl !CompUnit.current in
      try Inttbl.find tbl i
      with Not_found ->
447
448
449
	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
450
451
452
453
454
455
	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
456
457
(*      Format.fprintf Format.std_formatter "deserialize cu=%a i=%i@." 
	CompUnit.print cu i; *)
458
459
460
      try Inttbl.find (Inttbl.find deserialize_memo cu) i 
      with Not_found -> assert false

461
462
end

463
464
465
466
467
468
469
470
471
472
473
474
475
476
(* 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


477
(* It is also possible to use Boolean instead of Bool here;
478
   need to analyze when each one is more efficient *)
479
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
480
Bool.Make(Custom.Pair(NodeT)(NodeT))
481
482

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

485
486
487
488
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
489

490
491
492
type descr = Descr.t
type node = Node.t
include Descr
493

494
495
496
let clear_deserialize_table = Node.clear_deserialize_table


497
498
let forward_print = ref (fun _ _ -> assert false)

499
500
let hash_cons = DescrHash.create 17000  

501
502
503
504
505
      
let make () = 
  incr count; 
  Node.mk !count empty

506
507
508
509
510
511
512
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; 
513
    let n = Node.mk !count d in
514
515
    DescrHash.add hash_cons d n; n  

516
let any =  {
517
  hash = 0;
518
519
520
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
521
  record= BoolRec.full; 
522
523
524
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
525
  abstract = Abstract.any;
526
  absent= false;
527
}
528

529

530
let non_constructed =
531
532
533
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
534
     
535
536
let non_constructed_or_absent = 
  { non_constructed with hash = 0; absent = true }
537
	     
538
539
540
541
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) }
542
let record label t = 
543
544
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
545
let record' (x : bool * node Ident.label_map) =
546
547
548
  { 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 }
549
550
551
let abstract a = { empty with hash = 0; abstract = a }

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

596

597

598
599
600
601
602
603
604
605
(* 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) &&
606
  (BoolRec.trivially_disjoint a.record b.record) &&
607
  (Abstract.disjoint a.abstract b.abstract) &&
608
  (not (a.absent && b.absent))
609

610

611

612
let descr n = n.Node.descr
613
let internalize n = n
614
let id n = n.Node.id
615
616


617
618
619
620
621
622
623
624
625
626
627
628
629
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)
  | Xml (x,y) -> times (const_node x) (const_node y)
  | Record x -> record' (false ,LabelMap.map const_node x)
  | 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)
630

631
632
let neg x = diff any x

633
let any_node = cons any
634
let empty_node = cons empty
635

636
module LabelS = Set.Make(LabelPool)
637

638
639
640
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

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

    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
683
  List.map line (BoolRec.get r)
684
   
685

686

687
688
689
690
691
692
693


(* 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)
694
let cap_product any_left any_right l =
695
696
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
697
    (any_left,any_right)
698
    l
699
let any_pair = { empty with hash = 0; times = any.times }
700

701

702
703
704
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

705
exception NotEmpty
706

707
708
709
710
711
712
713
714
715
716
717
718
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) -> 
719
      if n.status == Maybe then (try f n with NotEmpty -> ());
720
721
722
723
724
725
726
727
728
729
      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;
730
  s.notify <- Nothing; 
731
732
733
734
735
736
737
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
738
739
740
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
741
742
743
	try 
	  f arg s;
	  if s.active then n.active <- true
744
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
745

746
747
let guard a f n =
  match a with
748
    | { status = Empty } -> ()
749
750
751
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
752
    | { status = NEmpty } -> f n
753

754
755
756
757
758
759
760
761
762
763
764
765
766

(* 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) &&
767
	  (Abstract.is_empty d.abstract) &&
768
769
770
771
772
773
774
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
	  (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) 

853
854
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

855
856
857
let memo = DescrHash.create 33000
let marks = ref [] 

858
859
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

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

          let accu2' = diff accu2 t2 in 
893
	  guard (slot accu2') (aux accu1 accu2' right) s  
894
	)
895
896
    | [] -> set s
  in
897
  let (accu1,accu2) = cap_product any any left in
898
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
899
900
901
902
903

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

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

919
920
921
922
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 ->
923
          let accu1' = diff_t accu1 t1 in 
924
	  guard (slot accu1') (aux accu1' accu2 left) s;
925
926

          let accu2' = cap_t  accu2 t2 in 
927
	  guard (slot accu2') (aux accu1 accu2' left) s
928
929
930
      | [] -> set s
    in
    let accu1 = descr s1 in
931
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
932
933
  in
  big_conj single_right right s
934

935
and check_record (labels,(oleft,left),rights) s =
936
  let rec aux left rights s = match rights with
937
    | [] -> set s
938
    | (oright,right)::rights ->
939
	let next =
940
	  (oleft && (not oright)) ||
941
	  exists (Array.length left)
942
	    (fun i -> trivially_disjoint left.(i) right.(i))
943
	in
944
	if next then aux left rights s
945
946
	else
	  for i = 0 to Array.length left - 1 do
947
948
949
950
	    let left' = Array.copy left in
	    let di = diff left.(i) right.(i) in
	    left'.(i) <- di;
	    guard (slot di) (aux left' rights) s;
951
952
953
	  done
  in
  let rec start i s =
954
    if (i < 0) then aux left rights s
955
    else
956
      guard (slot left.(i)) (start (i - 1)) s
957
958
959
960
  in
  start (Array.length left - 1) s


961

962
let timer_subtype = Stats.Timer.create "Types.is_empty"
963

964

965
let is_empty d =
966
  Stats.Timer.start timer_subtype; 
967
968
  let s = slot d in
  List.iter 
969
970
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
971
972
    !marks;
  marks := [];
973
  Stats.Timer.stop timer_subtype 
974
    (s.status == Empty)
975

976
(*
977
let is_empty d =
978
979
980
981
982
983
984
(*  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
*)  
985
986
987
988
989
990
991

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

992
993
994
let disjoint d1 d2 =
  is_empty (cap d1 d2)

995
996
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

997
998
999
1000
1001
1002
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
1003
1004
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
1005
1006
1007
1008
1009

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

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

1010
1011
1012
1013
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

1014
1015
1016
1017
1018
1019
1020
    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*) 
1021
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
	      
	      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)

1046
*)
1047
  let get_aux any_right d =
1048
1049
    let accu = ref [] in
    let line (left,right) =
1050
      let (d1,d2) = cap_product any any_right left in
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
      if (non_empty d1) && (non_empty d2) then
	let right = List.map (fun (t1,t2) -> descr t1, descr t2) right in
	let right = normal_aux right in
	let resid1 = ref d1 in
	let () = 
	  List.iter
	    (fun (