types.ml 48.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

end


101 102
type pair_kind = [ `Normal | `XML ]

103

104 105 106 107 108 109
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
110
  but a  bug (?) in OCaml 3.07 makes it impossible
111 112 113 114 115 116 117 118 119
*)
  type t = {
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
120
    abstract: Abstract.t;
121 122
    absent: bool
  }
123
  val empty: t
124 125 126 127 128 129 130 131 132 133 134 135 136 137 138
  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;
139
    abstract: Abstract.t;
140 141
    absent: bool
  }
142

143 144 145 146 147 148 149 150 151
  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
152

153 154 155 156 157 158 159 160
  let empty = { 
    times = BoolPair.empty; 
    xml   = BoolPair.empty; 
    arrow = BoolPair.empty; 
    record= BoolRec.empty;
    ints  = Intervals.empty;
    atoms = Atoms.empty;
    chars = Chars.empty;
161
    abstract = Abstract.empty;
162 163 164
    absent= false;
  }

165
  let equal a b =
166 167 168 169 170 171 172 173
    (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) &&
174
      (Abstract.equal a.abstract b.abstract) &&
175 176
      (a.absent == b.absent)
    )
177 178 179 180 181 182 183 184 185 186

  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
187
    else let c = Abstract.compare a.abstract b.abstract in if c <> 0 then c
188 189 190
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
191
      
192
  let hash a =
193 194 195 196 197 198 199 200 201 202
    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
203

204 205 206 207 208 209 210 211
  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;
212
    Abstract.check a.abstract;
213 214 215
    ()


216 217 218
end
and Node :
sig
219
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
220 221 222 223 224
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
225
  val mk: int -> Descr.t -> t
226
end =
227

228
struct
229
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
230
  let check n = ()
231
  let dump ppf n = Format.fprintf ppf "X%i" n.id
232
  let hash x = x.id + Compunit.hash x.cu
233
  let compare x y = 
234 235 236
    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 }
237 238
end

239 240 241 242 243 244 245 246 247 248 249 250
(* 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


251
(* It is also possible to use Boolean instead of Bool here;
252
   need to analyze when each one is more efficient *)
253
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
254
(*Bool.Simplify*)(Bool.Make)(Custom.Pair(NodeT)(NodeT))
255 256

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

259 260
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
261 262
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)
263

264 265 266
type descr = Descr.t
type node = Node.t
include Descr
267

268 269
let forward_print = ref (fun _ _ -> assert false)

270 271 272 273
let make () = 
  incr count; 
  Node.mk !count empty

274 275 276
(*
let hash_cons = DescrHash.create 17000  

277 278 279
let define n d = 
  DescrHash.add hash_cons d n; 
  n.Node.descr <- d
280

281 282 283 284
let cons d = 
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
285
    let n = Node.mk !count d in
286
    DescrHash.add hash_cons d n; n  
287 288 289 290 291 292 293 294 295
*)

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

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

296

297
let any =  {
298 299 300
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
301
  record= BoolRec.full; 
302 303 304
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
305
  abstract = Abstract.any;
306
  absent= false;
307
}
308

309

310
let non_constructed =
311 312
  { any with  
      times = empty.times; xml = empty.xml; record = empty.record }
313
     
314
let non_constructed_or_absent = 
315
  { non_constructed with absent = true }
316
	     
317 318 319 320
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) }
321
let record label t = 
322
  { empty with 
323
      record = BoolRec.atom (true,LabelMap.singleton label t) }
324
let record_fields (x : bool * node Ident.label_map) =
325 326 327 328
  { 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 }
329 330

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

372

373

374 375 376 377 378 379 380 381
(* 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) &&
382
  (BoolRec.trivially_disjoint a.record b.record) &&
383
  (Abstract.disjoint a.abstract b.abstract) &&
384
  (not (a.absent && b.absent))
385

386

387

388
let descr n = n.Node.descr
389
let internalize n = n
390
let id n = n.Node.id
391 392


393 394 395 396 397
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)
398
  | Xml (x,y) -> xml (const_node x) (const_node y)
399
  | Record x -> record_fields (false ,LabelMap.map const_node x)
400 401 402 403 404 405
  | 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)
406

407 408
let neg x = diff any x

409
let any_node = cons any
410
let empty_node = cons empty
411

412
module LabelS = Set.Make(Label)
413

414 415
let any_or_absent = { any with absent = true } 
let only_absent = { empty with absent = true }
416

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

    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
459
  List.map line (BoolRec.get r)
460
   
461

462

463 464 465 466 467 468 469


(* 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)
470
let cap_product any_left any_right l =
471 472
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
473
    (any_left,any_right)
474
    l
475
let any_pair = { empty with times = any.times }
476

477

478 479 480
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

481
exception NotEmpty
482

483 484 485 486 487 488 489 490 491 492 493 494
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) -> 
495
      if n.status == Maybe then (try f n with NotEmpty -> ());
496 497 498 499 500 501 502 503 504 505
      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;
506
  s.notify <- Nothing; 
507 508 509 510 511 512 513
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
514 515 516
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
517 518 519
	try 
	  f arg s;
	  if s.active then n.active <- true
520
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
521

522 523
let guard a f n =
  match a with
524
    | { status = Empty } -> ()
525 526 527
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
528
    | { status = NEmpty } -> f n
529

530 531 532 533 534 535

(* Fast approximation *)

module ClearlyEmpty = 
struct

536
let memo = DescrHash.create 8191
537 538 539 540 541 542
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
543
	  (Abstract.is_empty d.abstract) &&
544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628
	  (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) 

629 630
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

631
let memo = DescrHash.create 8191
632 633
let marks = ref [] 

634 635
let count_subtype = Stats.Counter.create "Subtyping internal loop" 

636 637
let complex = ref 0

638
let rec slot d =
639
  incr complex;
640
  Stats.Counter.incr count_subtype; 
641 642
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
643
	  (Chars.is_empty d.chars) &&
644
	  (Abstract.is_empty d.abstract) &&
645
	  (not d.absent)) then slot_not_empty 
646 647 648 649 650
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
651
       iter_s s check_times (BoolPair.get d.times);  
652
       iter_s s check_xml (BoolPair.get d.xml); 
653
       iter_s s check_arrow (BoolPair.get d.arrow);
654 655 656 657 658 659 660 661
       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
662 663
    | (n1,n2)::right ->
	let t1 = descr n1 and t2 = descr n2 in
664 665
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
666 667
	     aux accu1 accu2 right s )
	else (
668
          let accu1' = diff accu1 t1 in 
669
	  guard (slot accu1') (aux accu1' accu2 right) s;
670 671

          let accu2' = diff accu2 t2 in 
672
	  guard (slot accu2') (aux accu1 accu2' right) s  
673
	)
674 675
    | [] -> set s
  in
676
  let (accu1,accu2) = cap_product any any left in
677 678 679 680 681 682 683 684 685 686 687
  let rec check_trivial l s = match l with
    | [] -> aux accu1 accu2 right s
    | (n1,n2)::l ->
	let t1 = diff accu1 (descr n1) in
	if Descr.equal t1 empty then
	  let t2 = diff accu2 (descr n2) in
	  guard (slot t2) (check_trivial l) s
	else
	  check_trivial l s
  in
  guard (slot accu1) (guard (slot accu2) (check_trivial right)) s
688 689 690

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

          let accu2' = diff accu2 t2 in 
701
	  guard (slot accu2') (aux accu1 accu2' right) s  
702 703 704 705
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
706
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s 
707

708 709 710 711
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 ->
712
          let accu1' = diff_t accu1 t1 in 
713
	  guard (slot accu1') (aux accu1' accu2 left) s;
714 715

          let accu2' = cap_t  accu2 t2 in 
716
	  guard (slot accu2') (aux accu1 accu2' left) s
717 718 719
      | [] -> set s
    in
    let accu1 = descr s1 in
720
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
721 722
  in
  big_conj single_right right s
723

724
and check_record (labels,(oleft,left),rights) s =
725
  let rec aux left rights s = match rights with
726
    | [] -> set s
727
    | (oright,right)::rights ->
728
	let next =
729
	  (oleft && (not oright)) ||
730
	  exists (Array.length left)
731
	    (fun i -> trivially_disjoint left.(i) right.(i))
732
	in
733
	if next then aux left rights s
734 735
	else
	  for i = 0 to Array.length left - 1 do
736 737 738 739
	    let left' = Array.copy left in
	    let di = diff left.(i) right.(i) in
	    left'.(i) <- di;
	    guard (slot di) (aux left' rights) s;
740 741 742
	  done
  in
  let rec start i s =
743
    if (i < 0) then aux left rights s
744
    else
745
      guard (slot left.(i)) (start (i - 1)) s
746 747 748 749
  in
  start (Array.length left - 1) s


750

751
let timer_subtype = Stats.Timer.create "Types.is_empty"
752

753

754
let is_empty d =
755
  Stats.Timer.start timer_subtype; 
756 757
  let s = slot d in
  List.iter 
758 759
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
760 761
    !marks;
  marks := [];
762
  Stats.Timer.stop timer_subtype 
763
    (s.status == Empty)
764

765
(*
766
let is_empty d =
767 768 769 770 771 772 773
(*  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
*)  
774

775 776 777 778 779 780 781 782 783 784 785 786 787 788
(*
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
*)

789 790 791 792 793 794
let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

795 796 797
let disjoint d1 d2 =
  is_empty (cap d1 d2)

798 799
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)

800 801 802 803 804 805
module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
806 807
      | `Normal -> { d with times = empty.times }
      | `XML -> { d with xml = empty.xml }
808 809 810 811 812

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

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

813 814 815 816
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

817 818 819 820 821 822 823
    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*) 
824
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848
	      
	      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)

849
*)
850
  let get_aux any_right d =
851 852
    let accu = ref [] in
    let line (left,right) =
853
      let (d1,d2) = cap_product any any_right left in
854 855 856 857 858 859 860 861 862 863 864 865 866 867 868
      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
869
    List.iter line (BoolPair.get d);
870
    !accu
871 872 873
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
874

875

876 877
  let get ?(kind=`Normal) d = 
    match kind with
878 879
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
880 881 882

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
883 884 885 886
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
887 888

  let restrict_1 rects pi1 =