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

4
5
6
7
8
(* TODO:
   - I store hash in types to avoid computing it several times.
     Does not seem to help a lot.
*)

9
10
11
12
13
14
15
16
17
18
(*
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


19
20
21
module CompUnit = struct   
  include Pool.Make(Utf8)
  module Tbl = Inttbl
22

23
  let pervasives = mk (U.mk "Pervasives") 
24
  let current = ref dummy_min
25
26
27
28
29
30
31
  let get_current () =
    assert (!current != dummy_min);
    !current

  let print_qual ppf t =
    if (t != !current) && (t != pervasives) then
      Format.fprintf ppf "%a." U.print (value t)
32
      
33
  let close_serialize_ref = ref (fun () -> assert false)
34
      
35
  let depend = Inttbl.create ()
36
      
37
  let serialize t cu =
38
    if (cu != pervasives) && (cu != !current) then Inttbl.add depend cu ();
39
40
41
42
43
44
45
46
47
48
49
    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 []
		
50
51
  let enter i = 
    stack := !current :: !stack; current := i
52
53
54
55
56
57
58
59
60
61
62
		  
  let leave () =
    match !stack with
      | hd::tl -> current := hd; stack := tl
      | _ -> assert false


  let () = enter pervasives
end	  


63
type const = 
64
  | Integer of Intervals.V.t
65
  | Atom of Atoms.V.t 
66
  | Char of Chars.V.t
67
68
69
70
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
71

72
73
74
module Const = struct
  type t = const

75
76
77
78
79
80
81
82
83
84
85
  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>"

86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
  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)
118
119
      | 2 ->
	  Char (Chars.V.deserialize s)
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
      | 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
138
    | Integer x, Integer y -> Intervals.V.compare x y
139
140
    | Integer _, _ -> -1
    | _, Integer _ -> 1
141
    | Atom x, Atom y -> Atoms.V.compare x y
142
143
    | Atom _, _ -> -1
    | _, Atom _ -> 1
144
    | Char x, Char y -> Chars.V.compare x y
145
146
147
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
148
149
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
150
151
152
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
153
154
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
155
156
157
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
158
	LabelMap.compare compare x y
159
160
161
162
163
164
165
    | 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 *)
166
167
168
169
170
171
172
173
174
175
	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
176
      (* Note: improve hash for String *)
177

178
179
  let equal c1 c2 = compare c1 c2 = 0
end
180

181
182
module Abstract =
struct
183
  module T = Custom.String
184
185
186
187
188
189
190
191
192
193
  type abs = T.t

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

  include SortedList.FiniteCofinite(T)

  let print = function
194
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
195
196
197
198
199
    | Cofinite l ->       
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
200
201
202
203

end


204
205
type pair_kind = [ `Normal | `XML ]

206

207
208
209
210
211
212
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
213
  but a  bug (?) in OCaml 3.07 makes it impossible
214
215
*)
  type t = {
216
    mutable hash: int;
217
218
219
220
221
222
223
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
224
    abstract: Abstract.t;
225
226
    absent: bool
  }
227
  val empty: t
228
229
230
231
232
233
234
235
236
237
  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 = {
238
    mutable hash: int;
239
240
241
242
243
244
245
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
246
    abstract: Abstract.t;
247
248
    absent: bool
  }
249

250
251
252
  let dump ppf _ =
    Format.fprintf ppf "<Types.Descr.t>"

253
254
255
256
257
258
259
260
261
  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;
262
    abstract = Abstract.empty;
263
264
265
    absent= false;
  }

266
  let equal a b =
267
268
269
270
271
272
273
274
    (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) &&
275
      (Abstract.equal a.abstract b.abstract) &&
276
277
      (a.absent == b.absent)
    )
278
279
280
281
282
283
284
285
286
287

  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
288
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
289
290
291
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
292
      
293
  let hash a =
294
295
296
297
298
299
300
301
    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
302
      let accu = 17 * accu + Abstract.hash a.abstract in
303
304
305
306
      let accu = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
307

308
309
310
311
312
313
314
315
  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;
316
    Abstract.check a.abstract;
317
318
319
    ()


320
321
322
323
324
325
326
327
  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;
328
    Abstract.serialize t a.abstract;
329
330
331
332
333
334
335
336
337
338
    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
339
    let abstract = Abstract.deserialize t in
340
    let absent = Serialize.Get.bool t in
341
    let d = { hash=0; 
342
      chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
343
      arrow = arrow; record = record; abstract = abstract; absent = absent } in
344
345
    check d;
    d
346
347
   
    
348
349
350
end
and Node :
sig
351
  type t = { id : int; comp_unit: CompUnit.t; mutable descr : Descr.t }
352
353
354
355
356
357
358
  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
359
  val mk: int -> Descr.t -> t
360
end =
361

362
struct
363
  type t = { id : int; comp_unit : CompUnit.t; mutable descr : Descr.t }
364
365
  let check n = ()
  let dump ppf n = failwith "Types.Node.dump"
366
367
368
369
  let hash x = x.id + 17 * x.comp_unit
  let compare x y = 
    let c = x.id - y.id in
    if c = 0 then x.comp_unit - y.comp_unit else c
370
  let equal x y = x == y
371

372
373
374
375
376
377
378
379
  let serialize_memo = Inttbl.create ()
  let counter_serialize = ref 0

  let () =
    CompUnit.close_serialize_ref := 
    (fun () ->
       Inttbl.clear serialize_memo;
       counter_serialize := 0)
380

381
  let serialize t n = 
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
    if n.comp_unit == !CompUnit.current then (
      Serialize.Put.bool t true;
      try 
	let i = Inttbl.find serialize_memo n.id in
	Serialize.Put.int t i
      with Not_found ->
	let i = !counter_serialize in
	incr counter_serialize;
	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
397
    )
398
      
399

400
401
402
403
  let deserialize_memo = Inttbl.create ()

  let find_tbl id =
    try Inttbl.find deserialize_memo id
404
    with Not_found ->
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
      let tbl = Inttbl.create () in
      Inttbl.add deserialize_memo id tbl;
      tbl

  let mk id d =
    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
      let tbl = find_tbl !CompUnit.current in
      try Inttbl.find tbl i
      with Not_found ->
	let n = { id = i; comp_unit = !CompUnit.current;
		  descr = Descr.empty } in
	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
      try Inttbl.find (Inttbl.find deserialize_memo cu) i 
      with Not_found -> assert false

432
433
end

434
435
436
437
438
439
440
441
442
443
444
445
446
447
(* 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


448
(* It is also possible to use Boolean instead of Bool here;
449
   need to analyze when each one is more efficient *)
450
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
451
Bool.Make(Custom.Pair(NodeT)(NodeT))
452
453

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

456
457
458
459
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
460

461
462
463
type descr = Descr.t
type node = Node.t
include Descr
464

465
466
let forward_print = ref (fun _ _ -> assert false)

467
468
let hash_cons = DescrHash.create 17000  

469
470
471
472
473
474
475
476
477
478
let count = State.ref "Types.count" 0
		
let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)
      
let make () = 
  incr count; 
  Node.mk !count empty

479
480
481
482
483
484
485
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; 
486
    let n = Node.mk !count d in
487
488
    DescrHash.add hash_cons d n; n  

489
let any =  {
490
  hash = 0;
491
492
493
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
494
  record= BoolRec.full; 
495
496
497
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
498
  abstract = Abstract.any;
499
  absent= false;
500
}
501

502

503
let non_constructed =
504
505
506
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
507
     
508
509
let non_constructed_or_absent = 
  { non_constructed with hash = 0; absent = true }
510
	     
511
512
513
514
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) }
515
let record label t = 
516
517
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
518
let record' (x : bool * node Ident.label_map) =
519
520
521
  { 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 }
522
523
524
let abstract a = { empty with hash = 0; abstract = a }

let get_abstract t = t.abstract
525
      
526
527
let cup x y = 
  if x == y then x else {
528
    hash = 0;
529
530
531
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
532
    record= BoolRec.cup x.record y.record;
533
534
535
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
536
    abstract = Abstract.cup x.abstract y.abstract;
537
    absent= x.absent || y.absent;
538
539
540
541
  }
    
let cap x y = 
  if x == y then x else {
542
    hash = 0;
543
544
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
545
    record= BoolRec.cap x.record y.record;
546
    arrow = BoolPair.cap x.arrow y.arrow;
547
548
549
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
550
    abstract = Abstract.cap x.abstract y.abstract;
551
    absent= x.absent && y.absent;
552
553
554
555
  }
    
let diff x y = 
  if x == y then empty else {
556
    hash = 0;
557
558
559
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
560
    record= BoolRec.diff x.record y.record;
561
562
563
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
564
    abstract = Abstract.diff x.abstract y.abstract;
565
    absent= x.absent && not y.absent;
566
567
  }
    
568

569

570

571
572
573
574
575
576
577
578
(* 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) &&
579
  (BoolRec.trivially_disjoint a.record b.record) &&
580
  (Abstract.disjoint a.abstract b.abstract) &&
581
  (not (a.absent && b.absent))
582

583

584

585
let descr n = n.Node.descr
586
let internalize n = n
587
let id n = n.Node.id
588
589


590
591
592
593
594
595
596
597
598
599
600
601
602
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)
603

604
605
let neg x = diff any x

606
let any_node = cons any
607
let empty_node = cons empty
608

609
module LabelS = Set.Make(LabelPool)
610

611
612
613
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

614
615
let get_record r =
  let labs accu (_,r) = 
616
617
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
618
  let extend descrs labs (o,r) =
619
620
621
622
623
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
624
	      | (l2,x)::r when l1 == l2 -> 
625
626
627
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
628
629
		  if not o then 
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
630
631
		  aux (i+1) labs r
    in
632
    aux 0 labs (LabelMap.get r);
633
634
635
636
    o
  in
  let line (p,n) =
    let labels = 
637
638
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
639
    let nlab = List.length labels in
640
    let mk () = Array.create nlab any_or_absent in
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655

    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
656
  List.map line (BoolRec.get r)
657
   
658

659

660
661
662
663
664
665
666


(* 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)
667
let cap_product any_left any_right l =
668
669
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
670
    (any_left,any_right)
671
    l
672
let any_pair = { empty with hash = 0; times = any.times }
673

674

675
676
677
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

678
exception NotEmpty
679

680
681
682
683
684
685
686
687
688
689
690
691
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) -> 
692
      if n.status == Maybe then (try f n with NotEmpty -> ());
693
694
695
696
697
698
699
700
701
702
      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;
703
  s.notify <- Nothing; 
704
705
706
707
708
709
710
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
711
712
713
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
714
715
716
	try 
	  f arg s;
	  if s.active then n.active <- true
717
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
718

719
720
let guard a f n =
  match a with
721
    | { status = Empty } -> ()
722
723
724
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
725
    | { status = NEmpty } -> f n
726

727
728
729
730
731
732
733
734
735
736
737
738
739

(* 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) &&
740
	  (Abstract.is_empty d.abstract) &&
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
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
	  (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) 

826
827
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

828
829
830
let memo = DescrHash.create 33000
let marks = ref [] 

831
832
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

833
let rec slot d =
834
  Stats.Counter.incr count_subtype; 
835
836
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
837
	  (Chars.is_empty d.chars) &&
838
	  (Abstract.is_empty d.abstract) &&
839
	  (not d.absent)) then slot_not_empty 
840
841
842
843
844
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
845
       iter_s s check_times (BoolPair.get d.times);  
846
       iter_s s check_xml (BoolPair.get d.xml); 
847
       iter_s s check_arrow (BoolPair.get d.arrow);
848
849
850
851
852
853
854
855
856
       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 ->
857
858
859
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
860
861
	     aux accu1 accu2 right s )
	else (
862
          let accu1' = diff accu1 t1 in 
863
	  guard (slot accu1') (aux accu1' accu2 right) s;
864
865

          let accu2' = diff accu2 t2 in 
866
	  guard (slot accu2') (aux accu1 accu2' right) s  
867
	)
868
869
    | [] -> set s
  in
870
  let (accu1,accu2) = cap_product any any left in
871
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
872
873
874
875
876

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
877
	if clearly_disjoint accu1 t1 || 
878
879
880
881
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
882
	  guard (slot accu1') (aux accu1' accu2 right) s;
883
884

          let accu2' = diff accu2 t2 in 
885
	  guard (slot accu2') (aux accu1 accu2' right) s  
886
887
888
889
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
890
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
891

892
893
894
895
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 ->
896
          let accu1' = diff_t accu1 t1 in 
897
	  guard (slot accu1') (aux accu1' accu2 left) s;
898
899

          let accu2' = cap_t  accu2 t2 in 
900
	  guard (slot accu2') (aux accu1 accu2' left) s
901
902
903
      | [] -> set s
    in
    let accu1 = descr s1 in
904
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
905
906
  in
  big_conj single_right right s
907

908
and check_record (labels,(oleft,left),rights) s =
909
  let rec aux left rights s = match rights with
910
    | [] -> set s
911
    | (oright,right)::rights ->
912
	let next =
913
	  (oleft && (not oright)) ||
914
	  exists (Array.length left)
915
	    (fun i -> trivially_disjoint left.(i) right.(i))
916
	in
917
	if next then aux left rights s
918
919
	else
	  for i = 0 to Array.length left - 1 do
920
921
922
923
	    let left' = Array.copy left in
	    let di = diff left.(i) right.(i) in
	    left'.(i) <- di;
	    guard (slot di) (aux left' rights) s;
924
925
926
	  done
  in
  let rec start i s =
927
    if (i < 0) then aux left rights s
928
    else
929
      guard (slot left.(i)) (start (i - 1)) s
930
931
932
933
  in
  start (Array.length left - 1) s


934

935
let timer_subtype = Stats.Timer.create "Types.is_empty"
936

937

938
let is_empty d =
939
  Stats.Timer.start timer_subtype; 
940
941
  let s = slot d in
  List.iter 
942
943
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
944
945
    !marks;
  marks := [];
946
  Stats.Timer.stop timer_subtype 
947
    (s.status == Empty)
948

949
(*
950
let is_empty d =
951
952
953
954
955
956
957
(*  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
*)  
958
959
960
961
962
963
964

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

965
966
967
let disjoint d1 d2 =
  is_empty (cap d1 d2)

968
969
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

970
971
972
973
974
975
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
976
977
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
978
979
980
981
982

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

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

983
984
985
986
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

987
988
989
990
991
992
993
    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*) 
994
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
	      
	      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)

1019
*)
1020
  let get_aux any_right d =
1021
1022
    let accu = ref [] in
    let line (left,right) =
1023
      let (d1,d2) = cap_product any any_right left in
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
      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 (t1,t2) ->
	       let t1 = cap d1 t1 in
	       if (non_empty t1) then
		 let () = resid1 := diff !resid1 t1 in
		 let t2 = diff d2 t2 in
		 if (non_empty t2) then accu := (t1,t2) :: !accu
	    ) right in
	if non_empty !resid1 then accu := (!resid1, d2) :: !accu 
    in
1039
    List.iter line (BoolPair.get d);
1040
    !accu
1041
1042
1043
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
1044

1045

1046
1047
  let get ?(kind=`Normal) d = 
    match kind with
1048
1049
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
1050
1051
1052

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
1053
1054
1055
1056
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
1057
1058

  let restrict_1 rects pi1 =
1059
1060
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
1061
1062
1063
1064
    List.fold_left aux [] rects
  
  type normal = t

1065
  module Memo = Map.Make(BoolPair)
1066

1067
1068
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
1069
  let memo = ref Memo.empty
1070
  let normal_times d = 
1071
1072
1073
    try Memo.find d !memo 
    with
	Not_found ->
1074
	  let gd = get_aux any d in