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

4
let count = ref 0
5
6
7
8
9
		
let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)

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
type const = 
20
  | Integer of Intervals.V.t
21
  | Atom of Atoms.V.t
22
  | Char of Chars.V.t
23
24
25
26
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const
27

28
29
30
module Const = struct
  type t = const

31
32
  let check _ = ()
  let dump ppf _ = Format.fprintf ppf "<Types.Const.t>"
33
34

  let rec compare c1 c2 = match (c1,c2) with
35
    | Integer x, Integer y -> Intervals.V.compare x y
36
37
    | Integer _, _ -> -1
    | _, Integer _ -> 1
38
    | Atom x, Atom y -> Atoms.V.compare x y
39
40
    | Atom _, _ -> -1
    | _, Atom _ -> 1
41
    | Char x, Char y -> Chars.V.compare x y
42
43
44
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
45
46
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
47
48
49
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
50
51
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
52
53
54
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
55
	LabelMap.compare compare x y
56
57
58
59
60
61
62
    | 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 *)
63
64
65
66
67
68
69
70
71
72
	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
73
      (* Note: improve hash for String *)
74

75
76
  let equal c1 c2 = compare c1 c2 = 0
end
77

78
79
module Abstract =
struct
80
  module T = Custom.String
81
82
83
84
85
86
87
88
89
90
  type abs = T.t

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

  include SortedList.FiniteCofinite(T)

  let print = function
91
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
92
93
94
95
96
    | Cofinite l ->       
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]
97

98
99
100
101
102
103
  let contains_sample s t = match s,t with
    | None, Cofinite _ -> true
    | None, Finite _ -> false
    | Some s, t -> contains s t
    

104
105
106
end


107
108
type pair_kind = [ `Normal | `XML ]

109

110
111
112
113
114
115
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
116
  but a  bug (?) in OCaml 3.07 makes it impossible
117
118
119
120
121
122
123
124
125
*)
  type t = {
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
126
    abstract: Abstract.t;
127
128
    absent: bool
  }
129
  val empty: t
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
end =
struct
  type t = {
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
145
    abstract: Abstract.t;
146
147
    absent: bool
  }
148

149
150
151
152
153
154
155
156
157
  let print_lst ppf =
    List.iter (fun f -> f ppf; Format.fprintf ppf " |")

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

159
160
161
162
163
164
165
166
  let empty = { 
    times = BoolPair.empty; 
    xml   = BoolPair.empty; 
    arrow = BoolPair.empty; 
    record= BoolRec.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    chars = Chars.empty;
167
    abstract = Abstract.empty;
168
169
170
    absent= false;
  }

171
  let equal a b =
172
173
174
175
176
177
178
179
    (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) &&
180
      (Abstract.equal a.abstract b.abstract) &&
181
182
      (a.absent == b.absent)
    )
183
184
185
186
187
188
189
190
191
192

  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
193
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
194
195
196
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
197
      
198
  let hash a =
199
200
201
202
203
204
205
206
207
208
    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
    let accu = 17 * accu + Abstract.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu
209

210
211
212
213
214
215
216
217
  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;
218
    Abstract.check a.abstract;
219
220
221
    ()


222
223
224
end
and Node :
sig
225
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
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
231
  val mk: int -> Descr.t -> t
232
end =
233

234
struct
235
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
236
  let check n = ()
237
  let dump ppf n = Format.fprintf ppf "X%i" n.id
238
  let hash x = x.id + Compunit.hash x.cu
239
  let compare x y = 
240
241
242
    let c = x.id - y.id in if c = 0 then Compunit.compare x.cu y.cu else c
  let equal x y = x==y || (x.id == y.id && (Compunit.equal x.cu y.cu))
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
243
244
end

245
246
247
248
249
250
251
252
253
254
255
256
(* 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
end


257
(* It is also possible to use Boolean instead of Bool here;
258
   need to analyze when each one is more efficient *)
259
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
260
(*Bool.Simplify*)(Bool.Make)(Custom.Pair(NodeT)(NodeT))
261
262

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

265
266
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
267
268
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
269

270
271
272
type descr = Descr.t
type node = Node.t
include Descr
273

274
275
let forward_print = ref (fun _ _ -> assert false)

276
277
278
279
let make () = 
  incr count; 
  Node.mk !count empty

280
281
282
(*
let hash_cons = DescrHash.create 17000  

283
284
285
let define n d = 
  DescrHash.add hash_cons d n; 
  n.Node.descr <- d
286

287
288
289
290
let cons d = 
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
291
    let n = Node.mk !count d in
292
    DescrHash.add hash_cons d n; n  
293
294
295
296
297
298
299
300
301
*)

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

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

302

303
let any =  {
304
305
306
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
307
  record= BoolRec.full; 
308
309
310
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
311
  abstract = Abstract.any;
312
  absent= false;
313
}
314

315

316
let non_constructed =
317
318
  { any with  
      times = empty.times; xml = empty.xml; record = empty.record }
319
     
320
let non_constructed_or_absent = 
321
  { non_constructed with absent = true }
322
	     
323
324
325
326
let interval i = { empty with ints = i }
let times x y = { empty with times = BoolPair.atom (x,y) }
let xml x y = { empty with xml = BoolPair.atom (x,y) }
let arrow x y = { empty with arrow = BoolPair.atom (x,y) }
327
let record label t = 
328
  { empty with 
329
      record = BoolRec.atom (true,LabelMap.singleton label t) }
330
let record_fields (x : bool * node Ident.label_map) =
331
332
333
334
  { empty with record = BoolRec.atom x }
let atom a = { empty with atoms = a }
let char c = { empty with chars = c }
let abstract a = { empty with abstract = a }
335
336

let get_abstract t = t.abstract
337
      
338
339
let cup x y = 
  if x == y then x else {
340
341
342
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
343
    record= BoolRec.cup x.record y.record;
344
345
346
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
347
    abstract = Abstract.cup x.abstract y.abstract;
348
    absent= x.absent || y.absent;
349
350
351
352
  }
    
let cap x y = 
  if x == y then x else {
353
354
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
355
    record= BoolRec.cap x.record y.record;
356
    arrow = BoolPair.cap x.arrow y.arrow;
357
358
359
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
360
    abstract = Abstract.cap x.abstract y.abstract;
361
    absent= x.absent && y.absent;
362
363
364
365
  }
    
let diff x y = 
  if x == y then empty else {
366
367
368
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
369
    record= BoolRec.diff x.record y.record;
370
371
372
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
373
    abstract = Abstract.diff x.abstract y.abstract;
374
    absent= x.absent && not y.absent;
375
376
  }
    
377

378

379

380
381
382
383
384
385
386
387
(* 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) &&
388
  (BoolRec.trivially_disjoint a.record b.record) &&
389
  (Abstract.disjoint a.abstract b.abstract) &&
390
  (not (a.absent && b.absent))
391

392

393

394
let descr n = n.Node.descr
395
let internalize n = n
396
let id n = n.Node.id
397
398


399
400
401
402
403
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)
404
  | Xml (x,y) -> xml (const_node x) (const_node y)
405
  | Record x -> record_fields (false ,LabelMap.map const_node x)
406
407
408
409
410
411
  | 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)
412

413
414
let neg x = diff any x

415
let any_node = cons any
416
let empty_node = cons empty
417

418
module LabelS = Set.Make(Label)
419

420
421
let any_or_absent = { any with absent = true } 
let only_absent = { empty with absent = true }
422

423
424
let get_record r =
  let labs accu (_,r) = 
425
426
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
427
  let extend descrs labs (o,r) =
428
429
430
431
432
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
433
	      | (l2,x)::r when l1 == l2 -> 
434
435
436
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
437
438
		  if not o then 
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
439
440
		  aux (i+1) labs r
    in
441
    aux 0 labs (LabelMap.get r);
442
443
444
445
    o
  in
  let line (p,n) =
    let labels = 
446
447
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
448
    let nlab = List.length labels in
449
    let mk () = Array.create nlab any_or_absent in
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464

    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
465
  List.map line (BoolRec.get r)
466
   
467

468

469
470
471
472
473
474
475


(* 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)
476
let cap_product any_left any_right l =
477
478
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
479
    (any_left,any_right)
480
    l
481
let any_pair = { empty with times = any.times }
482

483

484
485
486
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

487
exception NotEmpty
488

489
490
491
492
493
494
495
496
497
498
499
500
501
type witness =
  | WInt of Intervals.V.t
  | WAtom of Atoms.sample
  | WChar of Chars.V.t
  | WPair of witness * witness
  | WXml of witness * witness
  | WRecord of witness label_map * bool
  | WFun of (witness * witness option) list
  | WAbstract of Abstract.elem option
  | WAbsent

let eps_witness = WAtom (Atoms.sample (Atoms.atom (Atoms.V.mk_ascii "nil")))

502
503
504
type slot = { mutable status : status; 
	       mutable notify : notify;
	       mutable active : bool }
505
506
and status = Empty | NEmpty of witness | Maybe
and notify = Nothing | Do of slot * (witness -> unit) * notify
507
508

let slot_empty = { status = Empty; active = false; notify = Nothing }
509
510
511
512
let slot_nempty w = { status = NEmpty w;
		     active = false; notify = Nothing }
let slot_eps = slot_nempty eps_witness

513

514
let rec notify w = function
515
516
  | Nothing -> ()
  | Do (n,f,rem) -> 
517
518
      if n.status == Maybe then (try f w with NotEmpty -> ());
      notify w rem
519
520
521
522
523
524

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


525
526
527
let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
528
  s.notify <- Nothing; 
529
530
  raise NotEmpty

531
let rec big_conj f l n w =
532
  match l with
533
534
    | [] -> set n w
    | [arg] -> f w arg n
535
    | arg::rem ->
536
537
	let s = 
	  { status = Maybe; active = false; 
538
	    notify = Do (n,(big_conj f rem n), Nothing) } in
539
	try 
540
	  f w arg s;
541
	  if s.active then n.active <- true
542
	with NotEmpty when n.status == Empty || n.status == Maybe -> ()
543
544
545
546
547
548

(* Fast approximation *)

module ClearlyEmpty = 
struct

549
let memo = DescrHash.create 8191
550
551
552
553
554
555
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
556
	  (Abstract.is_empty d.abstract) &&
557
	  (not d.absent)) then slot_eps
558
559
560
561
562
563
564
565
566
567
568
569
570
571
  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

572
573
574
575
576
and guard n t f = match (slot t) with
  | { status = Empty } -> ()
  | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
  | { status = NEmpty v } -> f v

577
578
and check_times (left,right) s =
  let (accu1,accu2) = cap_product any any left in
579
  let single_right w (t1,t2) s =
580
    let t1 = descr t1 and t2 = descr t2 in
581
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s w
582
    else
583
584
585
586
      let accu1 = diff accu1 t1 in guard s accu1 (set s);
      let accu2 = diff accu2 t2 in guard s accu2 (set s) in
  guard s accu1 
    (fun _ -> guard s accu2 (big_conj single_right right s))
587
588
589

and check_xml (left,right) s =
  let (accu1,accu2) = cap_product any any_pair left in
590
  let single_right w (t1,t2) s =
591
    let t1 = descr t1 and t2 = descr t2 in
592
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s w
593
    else
594
595
596
597
      let accu1 = diff accu1 t1 in guard s accu1 (set s);
      let accu2 = diff accu2 t2 in guard s accu2 (set s) in
  guard s accu1
    (fun _ -> guard s accu2 (big_conj single_right right s))
598
599

and check_arrow (left,right) s =
600
  let single_right w (s1,s2) s =
601
    let accu1 = descr s1 and accu2 = neg (descr s2) in
602
603
604
    let single_left w (t1,t2) s =
      let accu1 = diff_t accu1 t1 in guard s accu1 (set s);
      let accu2 = cap_t  accu2 t2 in guard s accu2 (set s)
605
    in
606
    guard s accu1 (big_conj single_left left s)
607
  in
608
  big_conj single_right right s eps_witness
609
610

and check_record (labels,(oleft,left),rights) s =
611
  let rec single_right w (oright,right) s = 
612
613
614
615
616
    let next =
      (oleft && (not oright)) ||
      exists (Array.length left)
	(fun i -> trivially_disjoint left.(i) right.(i))
    in
617
    if next then set s w
618
619
    else
      for i = 0 to Array.length left - 1 do
620
	let di = diff left.(i) right.(i) in guard s di (set s)
621
622
      done
  in
623
624
625
  let rec start i s w =
    if (i < 0) then big_conj single_right rights s w
    else guard s left.(i) (start (i - 1) s)
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
  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) 

649
650
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

651
let memo = DescrHash.create 8191
652
653
let marks = ref [] 

654
655
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

656
657
let complex = ref 0

658
let rec slot d =
659
  incr complex;
660
  Stats.Counter.incr count_subtype; 
661
662
663
664
665
666
667
668
669
  if not (Intervals.is_empty d.ints) 
  then slot_nempty (WInt (Intervals.sample d.ints))
  else if not (Atoms.is_empty d.atoms) 
  then slot_nempty (WAtom (Atoms.sample d.atoms))
  else if not (Chars.is_empty d.chars) 
  then slot_nempty (WChar (Chars.sample d.chars))
  else if not (Abstract.is_empty d.abstract) 
  then slot_nempty (WAbstract (Abstract.sample d.abstract))
  else if d.absent then slot_nempty WAbsent
670
671
672
673
674
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
675
       iter_s s check_times (BoolPair.get d.times);  
676
       iter_s s check_xml (BoolPair.get d.xml); 
677
       iter_s s check_arrow (BoolPair.get d.arrow);
678
679
680
681
682
683
       iter_s s check_record (get_record d.record);
       if s.active then marks := s :: !marks else s.status <- Empty;
     with
	 NotEmpty -> ());
    s

684
685
686
687
688
and guard n t f = match (slot t) with
  | { status = Empty } -> ()
  | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
  | { status = NEmpty v } -> f v

689
and check_times (left,right) s =
690
  let rec aux w1 w2 accu1 accu2 right = match right with
691
692
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
693
	if trivially_disjoint accu1 t1 || 
694
695
	   trivially_disjoint accu2 t2 then
	     aux w1 w2 accu1 accu2 right
696
	else (
697
          let accu1' = diff accu1 t1 in 
698
	  guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 right);
699
700

          let accu2' = diff accu2 t2 in 
701
	  guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' right)
702
	)
703
    | [] -> set s (WPair (w1,w2))
704
  in
705
  let (accu1,accu2) = cap_product any any left in
706
707
  let rec check_trivial w1 w2 l = match l with
    | [] -> aux w1 w2 accu1 accu2 right
708
709
710
711
    | (n1,n2)::l ->
	let t1 = diff accu1 (descr n1) in
	if Descr.equal t1 empty then
	  let t2 = diff accu2 (descr n2) in
712
	  guard s t2 (fun _ -> check_trivial w1 w2 l)
713
	else
714
	  check_trivial w1 w2 l
715
  in
716
717
718
  guard s accu1 
    (fun w1 -> guard s accu2 
       (fun w2 -> check_trivial w1 w2 right))
719
720

and check_xml (left,right) s =
721
  let rec aux w1 w2 accu1 accu2 right = match right with
722
723
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
724
	if clearly_disjoint accu1 t1 || 
725
726
	   trivially_disjoint accu2 t2 then 
	     aux w1 w2 accu1 accu2 right
727
728
	else (
          let accu1' = diff accu1 t1 in 
729
	  guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 right);
730
731

          let accu2' = diff accu2 t2 in 
732
	  guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' right)  
733
	)
734
    | [] -> set s (WXml (w1,w2))
735
736
  in
  let (accu1,accu2) = cap_product any any_pair left in
737
738
739
740
  guard s accu1 
    (fun w1 -> 
       guard s accu2
	 (fun w2 -> aux w1 w2 accu1 accu2 right))
741

742
and check_arrow (left,right) s =
743
744
  let single_right f (s1,s2) s =
    let rec aux w1 w2 accu1 accu2 left = match left with
745
      | (t1,t2)::left ->
746
          let accu1' = diff_t accu1 t1 in 
747
	  guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);
748
749

          let accu2' = cap_t  accu2 t2 in 
750
751
752
	  guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
      | [] -> (match f with WFun l -> set s (WFun ((w1,w2)::l))
		 | _ -> assert false)
753
754
    in
    let accu1 = descr s1 in
755
    guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
756
  in
757
  big_conj single_right right s (WFun [])
758

759
and check_record (labels,(oleft,left),rights) s =
760
761
762
763
764
765
  let rec aux ws left rights = match rights with
    | [] -> 
	let rec aux w i = function
	  | [] -> assert (i == Array.length ws); w
	  | l::labs -> aux (LabelMap.add l ws.(i) w) (succ i) labs in
	set s (WRecord (aux LabelMap.empty 0 labels,oleft))
766
    | (oright,right)::rights ->
767
	let next =
768
	  (oleft && (not oright)) ||
769
	  exists (Array.length left)
770
	    (fun i -> trivially_disjoint left.(i) right.(i))
771
	in
772
	if next then aux ws left rights
773
774
	else
	  for i = 0 to Array.length left - 1 do
775
	    let di = diff left.(i) right.(i) in
776
777
778
779
	    guard s di (fun w -> 
			  let left' = Array.copy left in left'.(i) <- di;
			  let ws' = Array.copy ws in ws'.(i) <- w;
			  aux ws' left' rights);
780
781
	  done
  in
782
783
784
  let rec start wl i =
    if (i < 0) then aux (Array.of_list wl) left rights
    else guard s left.(i) (fun w -> start (w::wl) (i - 1))
785
  in
786
  start [] (Array.length left - 1)
787
788


789

790
let timer_subtype = Stats.Timer.create "Types.is_empty"
791

792

793
let is_empty d =
794
  Stats.Timer.start timer_subtype; 
795
796
  let s = slot d in
  List.iter 
797
798
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
799
800
    !marks;
  marks := [];
801
  Stats.Timer.stop timer_subtype 
802
    (s.status == Empty)
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
let rec print_witness ppf = function
  | WInt i ->
      Format.fprintf ppf "%a" Intervals.V.print i
  | WChar c ->
      Format.fprintf ppf "%a" Chars.V.print c
  | WAtom None ->
      Format.fprintf ppf "`#:#"
  | WAtom (Some (ns,None)) ->
      Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
  | WAtom (Some (_,Some t)) ->
      Format.fprintf ppf "`%a" Ns.Label.print_attr t
  | WPair (w1,w2) -> 
      Format.fprintf ppf "(%a,%a)" print_witness w1 print_witness w2
  | WXml (w1,w2) -> 
      Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
  | WRecord (ws,o) ->
      Format.fprintf ppf "{";
      LabelMap.iteri
	(fun l w -> Format.fprintf ppf " %a=%a" 
	   Label.print_attr l print_witness w)
	ws;
      if o then Format.fprintf ppf " ..";
      Format.fprintf ppf " }"
  | WFun f ->
      Format.fprintf ppf "{";
      List.iter (fun (x,y) ->
		   Format.fprintf ppf " %a->" print_witness x;
		   match y with
		     | None -> Format.fprintf ppf "#"
		     | Some y -> print_witness ppf y) f;
      Format.fprintf ppf " }"
  | WAbstract None ->
      Format.fprintf ppf "Abstract(..)"
  | WAbstract (Some s) ->
      Format.fprintf ppf "Abstract(%s)" s
  | WAbsent ->
      Format.fprintf ppf "Absent"


let witness t =
  if is_empty t then raise Not_found
  else match (slot t).status with NEmpty w -> w | _ -> assert false

847
(*
848
let is_empty d =
849
850
851
852
853
854
855
(*  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
*)  
856

857
858
859
860
861
862
863
864
865
866
867
868
869
870
(*
let is_empty d =
(*  Format.fprintf Format.std_formatter "complex=%i@."
	  !complex; *)
  if !complex = 0 then
    (let r = is_empty d in
     if !complex > 100 then
       (let c = !complex in
	Format.fprintf Format.std_formatter "is_empty (%i)@." c
	  (*Descr.dump (*!forward_print*) d*));
     complex := 0; r)
  else is_empty d
*)

871
872
873
874
875
876
let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

877
878
879
let disjoint d1 d2 =
  is_empty (cap d1 d2)

880
881
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

882
883
884
885
886
887
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
888
889
      | `Normal -> { d with times = empty.times }
      | `XML -> { d with xml = empty.xml }
890
891
892
893
894

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

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

895
896
897
898
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

899
900
901
902
903
904
905
    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*) 
906
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
	      
	      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)

931
*)
932
  let get_aux any_right d =
933
934
    let accu = ref [] in
    let line (left,right) =
935
      let (d1,d2) = cap_product any any_right left in
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
      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
951
    List.iter line (BoolPair.get d);
952
    !accu
953
954
955
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
956

957

958
959
  let get ?(kind=`Normal) d = 
    match kind with
960
961
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
962
963
964

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
965
966
967
968
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
969
970

  let restrict_1 rects pi1 =
971
972
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
973
974
975
976
    List.fold_left aux [] rects
  
  type normal = t

977
  module Memo = Map.Make(BoolPair)
978

979
980
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
981
  let memo = ref Memo.empty
982
  let normal_times d = 
983
984
985
    try Memo.find d !memo 
    with
	Not_found ->
986
	  let gd = get_aux any d in
987
	  let n = normal_aux gd in
988
989
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
990
991
	  memo := Memo.add d n !memo;
	  n