types.ml 52.9 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
  let close_serialize_ref = ref (fun () -> assert false)
27
      
28
  let depend = Inttbl.create ()
29
      
30
  let serialize t cu =
31
    if (cu != pervasives) && (cu != !current) then Inttbl.add depend cu ();
32
33
34
35
36
37
38
39
40
41
42
    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 []
		
43
44
  let enter i = 
    stack := !current :: !stack; current := i
45
46
47
48
49
50
51
52
53
54
55
		  
  let leave () =
    match !stack with
      | hd::tl -> current := hd; stack := tl
      | _ -> assert false


  let () = enter pervasives
end	  


56
type const = 
57
  | Integer of Intervals.V.t
58
  | Atom of Atoms.V.t 
59
  | Char of Chars.V.t
60
61
62
63
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
64

65
66
67
module Const = struct
  type t = const

68
69
70
71
72
73
74
75
76
77
78
  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>"

79
80
81
82
83
84
85
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
  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)
111
112
      | 2 ->
	  Char (Chars.V.deserialize s)
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
      | 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
131
    | Integer x, Integer y -> Intervals.V.compare x y
132
133
    | Integer _, _ -> -1
    | _, Integer _ -> 1
134
    | Atom x, Atom y -> Atoms.V.compare x y
135
136
    | Atom _, _ -> -1
    | _, Atom _ -> 1
137
    | Char x, Char y -> Chars.V.compare x y
138
139
140
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
141
142
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
143
144
145
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
146
147
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
148
149
150
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
151
	LabelMap.compare compare x y
152
153
154
155
156
157
158
    | 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 *)
159
160
161
162
163
164
165
166
167
168
	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
169
      (* Note: improve hash for String *)
170

171
172
  let equal c1 c2 = compare c1 c2 = 0
end
173

174
175
module Abstract =
struct
176
  module T = Custom.String
177
178
179
180
181
182
183
184
185
186
  type abs = T.t

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

  include SortedList.FiniteCofinite(T)

  let print = function
187
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
188
189
190
191
192
    | Cofinite l ->       
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
193
194
195
196

end


197
198
type pair_kind = [ `Normal | `XML ]

199

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

243
244
245
  let dump ppf _ =
    Format.fprintf ppf "<Types.Descr.t>"

246
247
248
249
250
251
252
253
254
  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;
255
    abstract = Abstract.empty;
256
257
258
    absent= false;
  }

259
  let equal a b =
260
261
262
263
264
265
266
267
    (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) &&
268
      (Abstract.equal a.abstract b.abstract) &&
269
270
      (a.absent == b.absent)
    )
271
272
273
274
275
276
277
278
279
280

  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
281
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
282
283
284
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
285
      
286
  let hash a =
287
288
289
290
291
292
293
294
    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
295
      let accu = 17 * accu + Abstract.hash a.abstract in
296
297
298
299
      let accu = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
300

301
302
303
304
305
306
307
308
  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;
309
    Abstract.check a.abstract;
310
311
312
    ()


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

355
struct
356
  type t = { id : int; comp_unit : CompUnit.t; mutable descr : Descr.t }
357
358
  let check n = ()
  let dump ppf n = failwith "Types.Node.dump"
359
360
361
362
  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
363
  let equal x y = x == y
364

365
366
367
368
369
370
371
372
  let serialize_memo = Inttbl.create ()
  let counter_serialize = ref 0

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

374
  let serialize t n = 
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
    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
390
    )
391
      
392

393
394
395
396
  let deserialize_memo = Inttbl.create ()

  let find_tbl id =
    try Inttbl.find deserialize_memo id
397
    with Not_found ->
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
      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

425
426
end

427
428
429
430
431
432
433
434
435
436
437
438
439
440
(* 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


441
(* It is also possible to use Boolean instead of Bool here;
442
   need to analyze when each one is more efficient *)
443
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
444
Bool.Make(Custom.Pair(NodeT)(NodeT))
445
446

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

449
450
451
452
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
453

454
455
456
type descr = Descr.t
type node = Node.t
include Descr
457

458
459
let forward_print = ref (fun _ _ -> assert false)

460
461
let hash_cons = DescrHash.create 17000  

462
463
464
465
466
467
468
469
470
471
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

472
473
474
475
476
477
478
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; 
479
    let n = Node.mk !count d in
480
481
    DescrHash.add hash_cons d n; n  

482
let any =  {
483
  hash = 0;
484
485
486
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
487
  record= BoolRec.full; 
488
489
490
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
491
  abstract = Abstract.any;
492
  absent= false;
493
}
494

495

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

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

562

563

564
565
566
567
568
569
570
571
(* 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) &&
572
  (BoolRec.trivially_disjoint a.record b.record) &&
573
  (Abstract.disjoint a.abstract b.abstract) &&
574
  (not (a.absent && b.absent))
575

576

577

578
let descr n = n.Node.descr
579
let internalize n = n
580
let id n = n.Node.id
581
582


583
584
585
586
587
588
589
590
591
592
593
594
595
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)
596

597
598
let neg x = diff any x

599
let any_node = cons any
600
let empty_node = cons empty
601

602
module LabelS = Set.Make(LabelPool)
603

604
605
606
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

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

    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
649
  List.map line (BoolRec.get r)
650
   
651

652

653
654
655
656
657
658
659


(* 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)
660
let cap_product any_left any_right l =
661
662
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
663
    (any_left,any_right)
664
    l
665
let any_pair = { empty with hash = 0; times = any.times }
666

667

668
669
670
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

671
exception NotEmpty
672

673
674
675
676
677
678
679
680
681
682
683
684
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) -> 
685
      if n.status == Maybe then (try f n with NotEmpty -> ());
686
687
688
689
690
691
692
693
694
695
      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;
696
  s.notify <- Nothing; 
697
698
699
700
701
702
703
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
704
705
706
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
707
708
709
	try 
	  f arg s;
	  if s.active then n.active <- true
710
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
711

712
713
let guard a f n =
  match a with
714
    | { status = Empty } -> ()
715
716
717
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
718
    | { status = NEmpty } -> f n
719

720
721
722
723
724
725
726
727
728
729
730
731
732

(* 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) &&
733
	  (Abstract.is_empty d.abstract) &&
734
735
736
737
738
739
740
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
	  (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) 

819
820
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

821
822
823
let memo = DescrHash.create 33000
let marks = ref [] 

824
825
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

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

          let accu2' = diff accu2 t2 in 
859
	  guard (slot accu2') (aux accu1 accu2' right) s  
860
	)
861
862
    | [] -> set s
  in
863
  let (accu1,accu2) = cap_product any any left in
864
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
865
866
867
868
869

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
870
	if clearly_disjoint accu1 t1 || 
871
872
873
874
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
875
	  guard (slot accu1') (aux accu1' accu2 right) s;
876
877

          let accu2' = diff accu2 t2 in 
878
	  guard (slot accu2') (aux accu1 accu2' right) s  
879
880
881
882
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
883
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
884

885
886
887
888
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 ->
889
          let accu1' = diff_t accu1 t1 in 
890
	  guard (slot accu1') (aux accu1' accu2 left) s;
891
892

          let accu2' = cap_t  accu2 t2 in 
893
	  guard (slot accu2') (aux accu1 accu2' left) s
894
895
896
      | [] -> set s
    in
    let accu1 = descr s1 in
897
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
898
899
  in
  big_conj single_right right s
900

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


927

928
let timer_subtype = Stats.Timer.create "Types.is_empty"
929

930

931
let is_empty d =
932
  Stats.Timer.start timer_subtype; 
933
934
  let s = slot d in
  List.iter 
935
936
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
937
938
    !marks;
  marks := [];
939
  Stats.Timer.stop timer_subtype 
940
    (s.status == Empty)
941

942
(*
943
let is_empty d =
944
945
946
947
948
949
950
(*  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
*)  
951
952
953
954
955
956
957

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

958
959
960
let disjoint d1 d2 =
  is_empty (cap d1 d2)

961
962
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

963
964
965
966
967
968
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
969
970
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
971
972
973
974
975

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

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

976
977
978
979
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

980
981
982
983
984
985
986
    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*) 
987
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
988
989
990
991
992
993
994
995
996
997
998
999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
	      
	      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)

1012
*)
1013
  let get_aux any_right d =
1014
1015
    let accu = ref [] in
    let line (left,right) =
1016
      let (d1,d2) = cap_product any any_right left in
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
      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
1032
    List.iter line (BoolPair.get d);
1033
    !accu
1034
1035
1036
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
1037

1038

1039
1040
  let get ?(kind=`Normal) d = 
    match kind with
1041
1042
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
1043
1044
1045

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
1046
1047
1048
1049
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
1050
1051

  let restrict_1 rects pi1 =
1052
1053
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
1054
1055
1056
1057
    List.fold_left aux [] rects
  
  type normal = t

1058
  module Memo = Map.Make(BoolPair)
1059

1060
1061
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
1062
  let memo = ref Memo.empty
1063
  let normal_times d = 
1064
1065
1066
    try Memo.find d !memo 
    with
	Not_found ->
1067
	  let gd = get_aux any d in
1068
	  let n = normal_aux gd in
1069
1070
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
1071
1072
	  memo := Memo.add d n !memo;
	  n
1073

1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
  let memo_xml = ref Memo.empty
  let normal_xml d = 
    try Memo.find d !memo_xml
    with
	Not_found ->
	  let gd = get_aux any_pair d in
	  let n = normal_aux gd in
	  memo_xml := Memo.add d n !memo_xml;
	  n

  let normal ?(kind=`Normal) d =
    match kind with 
      | `Normal -> normal_times d.times 
      | `XML -> normal_xml d.xml


1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
  let merge_same_2 r =
    let r = 
      List.fold_left 
	(fun accu (t1,t2) ->
	   let t = try DescrMap.find t2 accu with Not_found -> empty in
	   DescrMap.add t2 (cup t t1) accu
	) DescrMap.empty r in
    DescrMap.fold (fun t2 t1 accu -> (t1,t2)::accu) r []
	 

1100
1101
1102
1103
1104
1105
1106
  let constraint_on_2 n t1 =
    List.fold_left 
      (fun accu (d1,d2) ->
	 if is_empty (cap d1 t1) then accu else cap accu d2)
      any
      n

1107
1108
1109
1110
1111
1112
1113
1114
1115

  let clean_normal l =
    let rec aux accu (t1,t2) =
      match accu with
	| [] -> [ (t1,t2) ]
	| (s1,s2) :: rem when equiv t2 s2 -> (cup s1 t1, s2) :: rem
	| (s1,s2) :: rem -> (s1,s2) :: (aux rem (t1,t2)) in
    List.fold_left aux [] l

1116
1117