types.ml 54.1 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)