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

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

let rec hash_const = 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_const x) + 257 * (hash_const y)
  | Xml (x,y) -> 5 + 17 * (hash_const x) + 257 * (hash_const y)
  | Record x -> 6 + 17 * (LabelMap.hash hash_const x)
  | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash_const r
      (* Note: improve hash for String *)
70

71 72
let equal_const c1 c2 = compare_const c1 c2 = 0

73 74
type pair_kind = [ `Normal | `XML ]

75 76 77 78 79 80 81 82 83
module rec Descr : 
sig
(*
  Want to write:
    type s = { ... }
    include Custom.T with type t = s
  but a  bug in OCaml 3.07+beta 2 makes it impossible
*)
  type t = {
84
    mutable hash: int;
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    absent: bool
  }
  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
  include Custom.Dummy
  type t = {
105
    mutable hash: int;
106 107 108 109 110 111 112 113 114 115
    atoms : Atoms.t;
    ints  : Intervals.t;
    chars : Chars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    absent: bool
  }
  let equal a b =
116 117 118 119 120 121 122 123 124 125
    (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) &&
      (a.absent == b.absent)
    )
126 127 128 129 130 131 132 133 134 135 136 137 138

  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
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0
139
      
140
  let hash a =
141 142 143 144 145 146 147 148 149 150 151 152
    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
      let accu = if a.absent then accu+5 else accu in
      a.hash <- accu;
      accu
    )
153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172

  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;
    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
    let absent = Serialize.Get.bool t in
173 174
    { hash=0; 
      chars = chars; ints = ints; atoms = atoms; times = times; xml = xml;
175 176 177
      arrow = arrow; record = record; absent = absent }
   
    
178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195
end
and Node :
sig
  type t = { id : int; mutable descr : Descr.t }
  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 = { id : int; mutable descr : Descr.t }
  include Custom.Dummy
  let hash x = x.id
  let compare x y = Pervasives.compare x.id y.id
  let equal x y = x == y
196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212

  let buffer = Serialize.Put.mk_property (fun t -> ref [])
  let serialize t n = 
    let l = Serialize.Put.get_property buffer t in
    Printf.eprintf "Node.serialize %i\n" n.id;
    Serialize.Put.int t n.id;
    if not (List.memq n.id !l) then
      (
	Printf.eprintf "Recurs\n";
	l := n.id :: !l;
	Descr.serialize t n.descr
      )

  let deserialize t = 
    let id = Serialize.Get.int t in
    Printf.eprintf "Node.deserialize %i\n" id;
    failwith "deserialize"
213 214
end

215 216
(* It is also possible to use Boolean insteand of Bool here;
   need to analyze when each one is more efficient *)
217 218 219 220 221 222
and BoolPair : Bool.S with type elem = Node.t * Node.t = 
Bool.Make(Custom.Pair(Node)(Node))

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

223

224 225 226
type descr = Descr.t
type node = Node.t
include Descr
227
	       
228
let empty = { 
229
  hash = 0;
230 231 232
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
233
  record= BoolRec.empty;
234 235 236
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
237
  absent= false;
238 239 240
}
	      
let any =  {
241
  hash = 0;
242 243 244
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
245
  record= BoolRec.full; 
246 247 248
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
249
  absent= false;
250
}
251 252

let non_constructed =
253 254 255
  { any with  
      hash = 0;
      times = empty.times; xml = empty.xml; record = empty.record }
256
     
257
	     
258 259 260 261
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) }
262
let record label t = 
263 264
  { empty with hash = 0; 
      record = BoolRec.atom (true,LabelMap.singleton label t) }
265
let record' (x : bool * node Ident.label_map) =
266 267 268
  { 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 }
269
      
270 271
let cup x y = 
  if x == y then x else {
272
    hash = 0;
273 274 275
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
276
    record= BoolRec.cup x.record y.record;
277 278 279
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
280
    absent= x.absent || y.absent;
281 282 283 284
  }
    
let cap x y = 
  if x == y then x else {
285
    hash = 0;
286 287
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
288
    record= BoolRec.cap x.record y.record;
289
    arrow = BoolPair.cap x.arrow y.arrow;
290 291 292
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
293
    absent= x.absent && y.absent;
294 295 296 297
  }
    
let diff x y = 
  if x == y then empty else {
298
    hash = 0;
299 300 301
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
302
    record= BoolRec.diff x.record y.record;
303 304 305
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
306
    absent= x.absent && not y.absent;
307 308
  }
    
309

310

311

312 313 314 315 316 317 318 319
(* 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) &&
320 321
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
322

323

324 325
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
326
module DescrSet = Set.Make(Descr)
327
module DescrSList = SortedList.Make(Descr)
328

329
let hash_cons = DescrHash.create 17000  
330

331
let count = State.ref "Types.count" 0
332 333 334 335 336

let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)

337
let make () = incr count; { Node.id = !count; Node.descr = empty }
338
let define n d = 
339
  DescrHash.add hash_cons d n; 
340
  n.Node.descr <- d
341
let cons d = 
342 343 344 345 346 347 348
  try DescrHash.find hash_cons d 
  with Not_found ->
    incr count; 
    let n = { Node.id = !count; Node.descr = d } in
    DescrHash.add hash_cons d n; n  


349
let descr n = n.Node.descr
350
let internalize n = n
351
let id n = n.Node.id
352 353


354 355 356 357 358 359 360 361 362 363 364 365 366
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)
367

368 369
let neg x = diff any x

370 371
let any_node = cons any

372
module LabelS = Set.Make(LabelPool)
373

374 375 376
let any_or_absent = { any with hash=0; absent = true } 
let only_absent = { empty with hash=0; absent = true }

377 378
let get_record r =
  let labs accu (_,r) = 
379 380
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
381
  let extend descrs labs (o,r) =
382 383 384 385 386
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
387
	      | (l2,x)::r when l1 == l2 -> 
388 389 390
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
391 392
		  if not o then 
		    descrs.(i) <- cap descrs.(i) only_absent; (* TODO:OPT *)
393 394
		  aux (i+1) labs r
    in
395
    aux 0 labs (LabelMap.get r);
396 397 398 399
    o
  in
  let line (p,n) =
    let labels = 
400 401
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
402
    let nlab = List.length labels in
403
    let mk () = Array.create nlab any_or_absent in
404 405 406 407 408 409 410 411 412 413 414 415 416 417 418

    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
419
  List.map line (BoolRec.get r)
420
   
421

422

423 424 425 426 427 428 429


(* 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)
430
let cap_product any_left any_right l =
431 432
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
433
    (any_left,any_right)
434
    l
435
let any_pair = { empty with hash = 0; times = any.times }
436

437

438 439 440
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

441
exception NotEmpty
442

443 444 445 446 447 448 449 450 451 452 453 454
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) -> 
455
      if n.status == Maybe then (try f n with NotEmpty -> ());
456 457 458 459 460 461 462 463 464 465
      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;
466
  s.notify <- Nothing; 
467 468 469 470 471 472 473
  raise NotEmpty

let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
474 475 476
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
477 478 479
	try 
	  f arg s;
	  if s.active then n.active <- true
480
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
481

482 483
let guard a f n =
  match a with
484
    | { status = Empty } -> ()
485 486 487
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
488
    | { status = NEmpty } -> f n
489

490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 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

(* 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) &&
	  (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) 

588 589
(* TODO: need to invesigate when ClearEmpty is a good thing... *)

590 591 592 593
let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
594 595
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
596 597
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
598 599 600 601 602
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
603
       iter_s s check_times (BoolPair.get d.times);  
604
       iter_s s check_xml (BoolPair.get d.xml); 
605
       iter_s s check_arrow (BoolPair.get d.arrow);
606 607 608 609 610 611 612 613 614
       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 ->
615 616 617
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
618 619
	     aux accu1 accu2 right s )
	else (
620
          let accu1' = diff accu1 t1 in 
621
	  guard (slot accu1') (aux accu1' accu2 right) s;
622 623

          let accu2' = diff accu2 t2 in 
624
	  guard (slot accu2') (aux accu1 accu2' right) s  
625
	)
626 627
    | [] -> set s
  in
628
  let (accu1,accu2) = cap_product any any left in
629
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
630 631 632 633 634

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
635
	if clearly_disjoint accu1 t1 || 
636 637 638 639
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
640
	  guard (slot accu1') (aux accu1' accu2 right) s;
641 642

          let accu2' = diff accu2 t2 in 
643
	  guard (slot accu2') (aux accu1 accu2' right) s  
644 645 646 647
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
648
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
649

650 651 652 653
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 ->
654
          let accu1' = diff_t accu1 t1 in 
655
	  guard (slot accu1') (aux accu1' accu2 left) s;
656 657

          let accu2' = cap_t  accu2 t2 in 
658
	  guard (slot accu2') (aux accu1 accu2' left) s
659 660 661
      | [] -> set s
    in
    let accu1 = descr s1 in
662
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
663 664
  in
  big_conj single_right right s
665

666
and check_record (labels,(oleft,left),rights) s =
667 668
  let rec aux rights s = match rights with
    | [] -> set s
669
    | (oright,right)::rights ->
670
	let next =
671
	  (oleft && (not oright)) ||
672
	  exists (Array.length left)
673
	    (fun i -> trivially_disjoint left.(i) right.(i))
674 675 676 677 678 679
	in
	if next then aux rights s
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let di = diff back right.(i) in
680 681
	    guard (slot di) (fun s ->
			left.(i) <- di;
682 683 684
			aux rights s;
			left.(i) <- back;
		     ) s
685
(* TODO: are side effects correct ? *)
686 687 688 689 690
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
691
      guard (slot left.(i)) (start (i - 1)) s
692 693 694 695
  in
  start (Array.length left - 1) s


696 697
let timer_subtype = Stats.Timer.create "Types.is_empty"

698
let is_empty d =
699
  Stats.Timer.start timer_subtype;
700 701
  let s = slot d in
  List.iter 
702 703
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
704 705
    !marks;
  marks := [];
706
  Stats.Timer.stop timer_subtype;
707
  s.status == Empty
708

709
(*
710
let is_empty d =
711 712 713 714 715 716 717
(*  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
*)  
718 719 720 721 722 723 724 725 726 727 728 729 730

let non_empty d = 
  not (is_empty d)

let subtype d1 d2 =
  is_empty (diff d1 d2)

module Product =
struct
  type t = (descr * descr) list

  let other ?(kind=`Normal) d = 
    match kind with
731 732
      | `Normal -> { d with hash = 0; times = empty.times }
      | `XML -> { d with hash = 0; xml = empty.xml }
733 734 735 736 737

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

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

738 739 740 741
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

742 743 744 745 746 747 748
    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*) 
749
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773
	      
	      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)

774
*)
775
  let get_aux any_right d =
776 777
    let accu = ref [] in
    let line (left,right) =
778
      let (d1,d2) = cap_product any any_right left in
779 780 781 782 783 784 785 786 787 788 789 790 791 792 793
      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
794
    List.iter line (BoolPair.get d);
795
    !accu
796 797 798
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
799

800

801 802
  let get ?(kind=`Normal) d = 
    match kind with
803 804
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml
805 806 807

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
808 809 810 811
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
812 813

  let restrict_1 rects pi1 =
814 815
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
816 817 818 819
    List.fold_left aux [] rects
  
  type normal = t

820
  module Memo = Map.Make(BoolPair)
821

822 823
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
824
  let memo = ref Memo.empty
825
  let normal_times d = 
826 827 828
    try Memo.find d !memo 
    with
	Not_found ->
829
	  let gd = get_aux any d in
830
	  let n = normal_aux gd in
831 832
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
833 834
	  memo := Memo.add d n !memo;
	  n
835

836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851
  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


852 853 854 855 856 857 858 859 860 861
  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 []
	 

862 863 864 865 866 867 868
  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

869 870
  let any = { empty with hash = 0; times = any.times }
  and any_xml = { empty with hash = 0; xml = any.xml }
871
  let is_empty d = d == []
872
end
873

874
module Record = 
875
struct
876 877
  let has_record d = not (is_empty { empty with hash= 0; record = d.record })
  let or_absent d = { d with hash = 0; absent = true }
878 879 880
  let any_or_absent = or_absent any
  let has_absent d = d.absent

881
  let only_absent = {empty with hash = 0; absent = true}
882 883 884 885 886 887 888 889 890 891 892 893 894
  let only_absent_node = cons only_absent

  module T = struct
    type t = descr
    let any = any_or_absent
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module R = struct
    type t = descr
895
    let any = { empty with hash = 0; record = any.record }
896 897 898 899 900 901 902 903
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module TR = Normal.Make(T)(R)

904
  let any_record = { empty with hash = 0; record = BoolRec.full }
905 906 907

  let atom o l = 
    if o && LabelMap.is_empty l then any_record else
908
    { empty with hash = 0; record = BoolRec.atom (o,l) }
909 910 911 912 913 914 915 916 917 918 919

  type zor = Pair of descr * descr | Any

  let aux_split d l=
    let f (o,r) =
      try
	let (lt,rem) = LabelMap.assoc_remove l r in
	Pair (descr lt, atom o rem)
      with Not_found -> 
	if o then
	  if LabelMap.is_empty r then Any else
920
	    Pair (any_or_absent, { empty with hash=0; record = BoolRec.atom (o,r) })
921 922
	else
	  Pair (only_absent,
923
		{ empty with hash = 0; record = BoolRec.atom (o,r) })
924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948 949 950 951 952 953 954 955 956
    in
    List.fold_left 
      (fun b (p,n) ->
	 let rec aux_p accu = function
	   | x::p -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
		  | Any -> aux_p accu p)
	   | [] -> aux_n accu [] n
	 and aux_n p accu = function
	   | x::n -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
		  | Any -> b)
	   | [] -> (p,accu) :: b in
	 aux_p [] p)
      []
      (BoolRec.get d.record)

  let split (d : descr) l =
    TR.boolean (aux_split d l)

  let split_normal d l =
    TR.boolean_normal (aux_split d l)


  let project d l =
    let t = TR.pi1 (split d l) in
    if t.absent then raise Not_found;
    t

  let project_opt d l =
    let t = TR.pi1 (split d l) in
957
    { t with hash = 0; absent = false }
958 959 960

  let condition d l t =
    TR.pi2_restricted t (split d l)
961

962 963 964 965 966
(* TODO: eliminate this cap ... (reord l only_absent_node) when
   not necessary. eg. {| ..... |} \ l *)

  let remove_field d l = 
    cap (TR.pi2 (split d l)) (record l only_absent_node)
967

968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019
  let first_label d =
    let min = ref LabelPool.dummy_max in
    let aux (_,r) = 
      match LabelMap.get r with
	  (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
    BoolRec.iter aux d.record;
    !min

  let empty_cases d =
    let x = BoolRec.compute
	      ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
	      ~diff:(fun a b -> a land lnot b)
	      ~atom:(function (o,r) ->
		       assert (LabelMap.get r == []);
		       if o then 3 else 1
		    )
	      d.record in
    (x land 2 <> 0, x land 1 <> 0)

  let has_empty_record d =
    BoolRec.compute
      ~empty:false ~full:true ~cup:(||) ~cap:(&&)
      ~diff:(fun a b -> a && not b)
      ~atom:(function (o,r) ->
	       List.for_all 
	         (fun (l,t) -> (descr t).absent)
	         (LabelMap.get r)
	    )
      d.record
    

(*TODO: optimize merge
   - pre-compute the sequence of labels
   - remove empty or full { l = t }
*)

  let merge d1 d2 = 
    let res = ref empty in