types.ml 44.2 KB
Newer Older
1
open Ident
2

3 4 5 6 7 8 9 10 11 12
(*
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


13 14 15 16 17 18
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
19 20


21 22 23 24
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
25

26 27 28 29 30 31 32 33 34 35 36 37 38 39 40
let compare_const c1 c2 =
  match (c1,c2) with
    | Integer x, Integer y -> Intervals.vcompare x y
    | Integer _, _ -> -1
    | _, Integer _ -> 1
    | Atom x, Atom y -> Atoms.vcompare x y
    | Atom _, _ -> -1
    | _, Atom _ -> 1
    | Char x, Char y -> Chars.vcompare x y

let hash_const = function
  | Integer x -> Intervals.vhash x
  | Atom x -> Atoms.vhash x
  | Char x -> Chars.vhash x

41 42
let equal_const c1 c2 = compare_const c1 c2 = 0

43 44
type pair_kind = [ `Normal | `XML ]

45 46 47 48
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
49 50 51
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
52 53 54 55 56 57 58
    if x1.id < x2.id then -1
    else if x1.id > x2.id then 1
    else y1.id - y2.id
  let equal (x1,y1) (x2,y2) = (x1==x2) && (y1==y2)
  let hash (x,y) = x.id + 17 * y.id
end 

59 60 61
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
62 63
  let dump ppf (o,r) = ()

64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97
  let rec compare_rec r1 r2 =
    if r1 == r2 then 0
    else match (r1,r2) with
      | (l1,x1)::r1,(l2,x2)::r2 ->
	  if ((l1:int) < l2) then -1 
	  else if (l1 > l2) then 1 
	  else if x1.id < x2.id then -1
	  else if x1.id > x2.id then 1
	  else compare_rec r1 r2
      | ([],_) -> -1
      | _ -> 1

  let compare (o1,r1) (o2,r2) =
    if o1 && not o2 then -1 
    else if o2 && not o1 then 1
    else compare_rec (LabelMap.get r1) (LabelMap.get r2)

  let rec equal_rec r1 r2 =
    (r1 == r2) ||
    match (r1,r2) with
      | (l1,x1)::r1,(l2,x2)::r2 ->
	  (x1.id == x2.id) && (l1 == l2) && (equal_rec r1 r2)
      | _ -> false

  let equal (o1,r1) (o2,r2) =
    (o1 == o2) && (equal_rec (LabelMap.get r1) (LabelMap.get r2))

  let rec hash_rec accu = function
    | (l,x)::rem -> hash_rec (257 * accu + 17 * l + x.id) rem
    | [] -> accu + 5
      
  let hash (o,r) = hash_rec (if o then 2 else 1) (LabelMap.get r)
end

98 99
(* It is also possible to use Boolean insteand of Bool here;
   need to analyze when each one is more efficient *)
100 101
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
102

103
type descr = {
104
  atoms : Atoms.t;
105 106
  ints  : Intervals.t;
  chars : Chars.t;
107 108 109
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
110
  record: descr BoolRec.t;
111
  absent: bool
112
} and node = descr node0
113

114
	       
115
let empty = { 
116 117 118
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
119
  record= BoolRec.empty;
120 121 122
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
123
  absent= false;
124 125 126
}
	      
let any =  {
127 128 129
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
130
  record= BoolRec.full; 
131 132 133
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
134
  absent= false;
135 136 137 138
}
	     
	     
let interval i = { empty with ints = i }
139 140 141
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) }
142
let record label t = 
143 144 145
  { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
let record' (x : bool * node Ident.label_map) =
  { empty with record = BoolRec.atom x }
146 147 148 149 150 151
let atom a = { empty with atoms = a }
let char c = { empty with chars = c }
let constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
152
      
153 154
let cup x y = 
  if x == y then x else {
155 156 157
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
158
    record= BoolRec.cup x.record y.record;
159 160 161
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
162
    absent= x.absent || y.absent;
163 164 165 166
  }
    
let cap x y = 
  if x == y then x else {
167 168
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
169
    record= BoolRec.cap x.record y.record;
170
    arrow = BoolPair.cap x.arrow y.arrow;
171 172 173
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
174
    absent= x.absent && y.absent;
175 176 177 178
  }
    
let diff x y = 
  if x == y then empty else {
179 180 181
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
182
    record= BoolRec.diff x.record y.record;
183 184 185
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
186
    absent= x.absent && not y.absent;
187 188
  }
    
189

190
let equal_descr a b =
191 192 193
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
194 195 196
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
197
  (BoolRec.equal a.record b.record) &&
198
  (a.absent == b.absent)
199 200

let compare_descr a b =
201 202
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
203 204
  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
205 206 207
  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
208
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
209 210
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
211 212
  else 0

213
let hash_descr a =
214 215 216
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
217 218 219
  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
220
  let accu = 17 * accu + BoolRec.hash a.record in
221
  let accu = if a.absent then accu+5 else accu in
222
  accu
223

224 225 226 227 228 229 230 231
(* 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) &&
232 233
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
234

235

236 237 238 239 240 241 242 243 244
module Descr =
struct 
  type t = descr
  let hash = hash_descr
  let equal = equal_descr
  let compare = compare_descr
end
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
245
module DescrSet = Set.Make(Descr)
246 247 248 249 250 251 252 253 254

module Descr1 =
struct 
  type 'a t = descr
  let hash = hash_descr
  let equal = equal_descr
  let compare = compare_descr
end
module DescrSList = SortedList.Make(Descr1)
255

256
(* let hash_cons = DescrHash.create 17000 *)
257

258
let count = State.ref "Types.count" 0
259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274
let make () = incr count; { id = !count; descr = empty }
let define n d = 
(*  DescrHash.add hash_cons d n; *)
  n.descr <- d
let cons d = 
  (* try DescrHash.find hash_cons d with Not_found ->
  incr count; let n = { id = !count; descr = d } in
  DescrHash.add hash_cons d n; n *)
  incr count; { id = !count; descr = d }
let descr n = n.descr
let internalize n = n
let id n = n.id




275 276
let neg x = diff any x

277 278
let any_node = cons any

279
module LabelS = Set.Make(LabelPool)
280 281 282

let get_record r =
  let labs accu (_,r) = 
283 284
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
285
  let extend descrs labs (o,r) =
286 287 288 289 290
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
291
	      | (l2,x)::r when l1 == l2 -> 
292 293 294
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
295
		  if not o then descrs.(i) <- 
296
		    cap descrs.(i) { empty with absent = true }; (* TODO:OPT *)
297 298
		  aux (i+1) labs r
    in
299
    aux 0 labs (LabelMap.get r);
300 301 302 303
    o
  in
  let line (p,n) =
    let labels = 
304 305
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
306
    let nlab = List.length labels in
307
    let mk () = Array.create nlab { any with absent = true } in
308 309 310 311 312 313 314 315 316 317 318 319 320 321 322

    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
323
  List.map line (BoolRec.get r)
324
   
325

326

327 328 329 330 331 332 333 334 335 336 337 338


(* 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)
let cap_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
    (any,any)
    l
339 340 341 342 343
let cup_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
    (empty,empty)
    l
344

345 346 347
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

348
let trivially_empty d = equal_descr d empty
349

350
exception NotEmpty
351

352 353 354 355 356 357 358 359 360 361 362 363 364 365 366
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 memo = DescrHash.create 33000

let marks = ref [] 
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) -> 
367
      if n.status == Maybe then (try f n with NotEmpty -> ());
368 369 370 371 372 373 374 375 376 377
      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;
378
  s.notify <- Nothing; 
379 380
  raise NotEmpty

381
let count_slot = ref 0
382 383 384 385 386
let rec big_conj f l n =
  match l with
    | [] -> set n
    | [arg] -> f arg n
    | arg::rem ->
387 388 389
	let s = 
	  { status = Maybe; active = false; 
	    notify = Do (n,(big_conj f rem), Nothing) } in
390 391 392
	try 
	  f arg s;
	  if s.active then n.active <- true
393
	with NotEmpty -> if n.status == NEmpty then raise NotEmpty
394 395

let rec guard a f n =
396 397
  match slot a with
    | { status = Empty } -> ()
398 399 400
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
401
    | { status = NEmpty } -> f n
402 403 404 405

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
406 407
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
408 409 410 411 412
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
413 414
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_times (BoolPair.get d.xml); 
415
       iter_s s check_arrow (BoolPair.get d.arrow);
416 417 418 419 420 421 422 423 424
       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 ->
425 426 427
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
428 429
	     aux accu1 accu2 right s )
	else (
430 431 432 433
          let accu1' = diff accu1 t1 in 
	  guard accu1' (aux accu1' accu2 right) s;

          let accu2' = diff accu2 t2 in 
434
	  guard accu2' (aux accu1 accu2' right) s  
435
	)
436 437
    | [] -> set s
  in
438
  let (accu1,accu2) = cap_product left in
439
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
440

441 442 443 444
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 ->
445 446 447 448 449
          let accu1' = diff_t accu1 t1 in 
	  guard accu1' (aux accu1' accu2 left) s;

          let accu2' = cap_t  accu2 t2 in 
	  guard accu2' (aux accu1 accu2' left) s
450 451 452 453 454 455
      | [] -> set s
    in
    let accu1 = descr s1 in
    guard accu1 (aux accu1 (neg (descr s2)) left) s
  in
  big_conj single_right right s
456

457
and check_record (labels,(oleft,left),rights) s =
458 459
  let rec aux rights s = match rights with
    | [] -> set s
460
    | (oright,right)::rights ->
461
	let next =
462
	  (oleft && (not oright)) ||
463
	  exists (Array.length left)
464
	    (fun i -> trivially_disjoint left.(i) right.(i))
465 466 467 468 469 470
	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
471 472 473 474 475
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
476 477 478 479 480
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
481
      guard left.(i) (start (i - 1)) s
482 483 484 485 486 487 488
  in
  start (Array.length left - 1) s


let is_empty d =
  let s = slot d in
  List.iter 
489 490
    (fun s' -> 
       if s'.status == Maybe then s'.status <- Empty; s'.notify <- Nothing) 
491 492
    !marks;
  marks := [];
493
  s.status == Empty
494 495
  

496 497 498 499
(*****************************************************************
 Old (backtracking) implementation of the subtyping algo:

let memo = ref DescrSet.empty
500
let cache_false = DescrHash.create 33000
501

502
let rec empty_rec d =
503
  if not (Intervals.is_empty d.ints) then false
504 505
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
506
  else if d.absent then false
507
  else if DescrHash.mem cache_false d then false 
508
  else if DescrSet.mem d !memo then true
509 510
  else (
    let backup = !memo in
511
    memo := DescrSet.add d backup;
512
    if 
513 514 515
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
516 517 518 519
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
520
      DescrHash.add cache_false d ();
521 522 523 524 525 526 527 528 529 530
      false
    )
  )

and empty_rec_times c =
  List.for_all empty_rec_times_aux c

and empty_rec_times_aux (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
531 532
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
533 534 535 536 537
	  aux accu1 accu2 right
	else
          let accu1' = diff_t accu1 t1 in
          if not (empty_rec accu1') then aux accu1' accu2 right;
          let accu2' = diff_t accu2 t2 in
538
	  if not (empty_rec accu2') then aux accu1 accu2' right
539 540 541 542 543
    | [] -> raise NotEmpty
  in
  let (accu1,accu2) = cap_product left in
  (empty_rec accu1) || (empty_rec accu2) ||
    (try aux accu1 accu2 right; true with NotEmpty -> false)
544

545 546 547 548 549 550 551 552 553

and empty_rec_arrow c =
  List.for_all empty_rec_arrow_aux c

and empty_rec_arrow_aux (left,right) =
  let single_right (s1,s2) =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
554
          if not (empty_rec accu1') then aux accu1' accu2 left;
555
          let accu2' = cap_t accu2 t2 in
556
          if not (empty_rec accu2') then aux accu1 accu2' left
557 558 559 560 561 562 563 564
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (empty_rec accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
  in
  List.exists single_right right

565
and empty_rec_record_aux (labels,(oleft,left),rights) =
566 567
  let rec aux = function
    | [] -> raise NotEmpty
568
    | (oright,right)::rights ->
569 570 571 572
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
573
	       trivially_empty (cap left.(i) right.(i)))
574 575 576 577 578 579
	in
	if next then aux rights 
	else
	  for i = 0 to Array.length left - 1 do
	    let back = left.(i) in
	    let di = diff back right.(i) in
580
	    if not (empty_rec di) then (
581 582 583 584 585 586 587
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
588
    (fun i -> empty_rec left.(i))
589 590 591 592
  ||
  (try aux rights; true with NotEmpty -> false)
	    

593
and empty_rec_record c =
594
  List.for_all empty_rec_record_aux (get_record c)
595

596
let is_empty d =
597
  empty_rec d
598 599
*******************************************************************)

600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619

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
      | `Normal -> { d with times = empty.times }
      | `XML -> { d with xml = empty.xml }

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

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

620 621 622 623
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

624 625 626 627 628 629 630
    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*) 
631
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648
	      
	      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

649
(*
650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677
This version explodes when dealing with
   Any - [ t1? t2? t3? ... tn? ]
==> need partitioning 
*)
  let get_aux d =
    let line accu (left,right) =
      let rec aux accu d1 d2 = function
	| (t1,t2)::right ->
	    let accu = 
	      let d1 = diff_t d1 t1 in
              if is_empty d1 then accu else aux accu d1 d2 right in
	    let accu =
              let d2 = diff_t d2 t2 in
              if is_empty d2 then accu else aux accu d1 d2 right in
	    accu
	| [] -> (d1,d2) :: accu
      in
      let (d1,d2) = cap_product left in
      if (is_empty d1) || (is_empty d2) then accu else aux accu d1 d2 right
    in
    List.fold_left line [] d

(* Partitioning:

(t,s) - ((t1,s1) | (t2,s2) | ... | (tn,sn))
=
(t & t1, s - s1) | ... | (t & tn, s - sn) | (t - (t1|...|tn), s)

678
*)
679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697
  let get_aux d =
    let accu = ref [] in
    let line (left,right) =
      let (d1,d2) = cap_product left in
      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
698
    List.iter line (BoolPair.get d);
699
    !accu
700 701 702
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
703

704

705 706
  let get ?(kind=`Normal) d = 
    match kind with
707 708
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
709 710 711

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
712 713 714 715
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
716 717

  let restrict_1 rects pi1 =
718 719
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
720 721 722 723
    List.fold_left aux [] rects
  
  type normal = t

724
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
725

726 727
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
728 729 730 731 732 733
  let memo = ref Memo.empty
  let normal ?(kind=`Normal) d = 
    let d = match kind with `Normal -> d.times | `XML -> d.xml in
    try Memo.find d !memo 
    with
	Not_found ->
734
	  let gd = get_aux d in
735
	  let n = normal_aux gd in
736 737
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
738 739
	  memo := Memo.add d n !memo;
	  n
740

741 742 743 744 745 746 747 748 749 750
  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 []
	 

751 752 753 754 755 756 757
  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

758 759
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
760
  let is_empty d = d == []
761
end
762

763
module Record = 
764
struct
765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 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 847 848 849
  let has_record d = not (is_empty { empty with record = d.record })
  let or_absent d = { d with absent = true }
  let any_or_absent = or_absent any
  let has_absent d = d.absent

  let only_absent = {empty with absent = true}
  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
    let any = { empty with record = any.record }
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module TR = Normal.Make(T)(R)

  let any_record = { empty with record = BoolRec.full }

  let atom o l = 
    if o && LabelMap.is_empty l then any_record else
    { empty with record = BoolRec.atom (o,l) }

  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
	    Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
	else
	  Pair (only_absent,
		{ empty with record = BoolRec.atom (o,r) })
    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
    { t with absent = false }

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

851 852 853 854 855
(* 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)
856

857 858 859 860 861 862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939
  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
    let rec aux accu d1 d2 =
      let l = min (first_label d1) (first_label d2) in
      if l = LabelPool.dummy_max then
	let (some1,none1) = empty_cases d1 
	and (some2,none2) = empty_cases d2 in
	let none = none1 && none2 and some = some1 || some2 in
	let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
	(* approx for the case (some && not none) ... *)
	res := cup !res (record' (some, accu))
      else
	let l1 = split d1 l and l2 = split d2 l in
	let loop (t1,d1) (t2,d2) =
	  let t = 
	    if t2.absent 
	    then cup t1 { t2 with absent = false } 
	    else t2 
	  in
	  aux ((l,cons t)::accu) d1 d2
	in
	List.iter (fun x -> List.iter (loop x) l2) l1
	  
    in
    aux [] d1 d2;
    !res

  let any = { empty with record = any.record }

  let get d =
    let rec aux r accu d =
      let l = first_label d in
      if l == LabelPool.dummy_max then
	let (o1,o2) = empty_cases d in 
	if o1 || o2 then (LabelMap.from_list_disj r,o1,o2)::accu else accu
      else
	List.fold_left 
	  (fun accu (t1,t2) -> aux ((l,t1)::r) accu t2)
	  accu
	  (split d l)
    in
    aux [] [] d
end


module Print = 
struct
940
  let print_const ppf = function
941 942 943
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
944

945 946 947 948 949 950 951 952 953 954
  let nil_atom = Atoms.mk "nil"
  let nil_type = atom (Atoms.atom nil_atom)
  let (seqs_node,seqs_descr) = 
    let n = make () in
    let d = cup nil_type (times any_node n) in
    define n d;
    (n, d)

  let is_regexp t = subtype t seqs_descr

955 956 957 958
  module S = struct
  type t = { id : int; 
	     mutable def : d list; 
	     mutable state : [ `Expand | `None | `Marked | `Named of string ] }
959 960 961 962 963 964 965 966 967
  and  d =
    | Name of string
    | Regexp of t Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of t * t
    | Char of Chars.v
    | Xml of [ `Tag of string | `Type of t ] * t * t
    | Record of (bool * t) label_map * bool * bool
    | Arrows of (t * t) list * (t * t) list
968
    | Neg of t
969 970 971 972
  let compare x y = x.id - y.id
  end
  module Decompile = Pretty.Decompile(DescrHash)(S)
  open S
973 974 975 976 977 978 979 980 981 982 983 984

  module DescrPairMap = 
    Map.Make(
      struct
	type t = descr * descr
	let compare (x1,y1) (x2,y2) =
	  let c = compare_descr x1 x2 in 
	  if c = 0 then compare_descr y1 y2 else c
      end)

  let named = State.ref "Types.Print.named" DescrMap.empty
  let named_xml = State.ref "Types.Print.named_xml"  DescrPairMap.empty
985
  let register_global name d = 
986 987 988 989 990
    if equal_descr { d with xml = BoolPair.empty } empty then 
      (let l = (*Product.merge_same_2*) (Product.get ~kind:`XML d) in
      match l with
	| [(t1,t2)] -> named_xml := DescrPairMap.add (t1,t2) name !named_xml
	| _ -> ());
991
    named := DescrMap.add d name !named
992

993
  let memo = DescrHash.create 63
994 995
  let counter = ref 0
  let alloc def = { id = (incr counter; !counter); def = def; state = `None }
996

997 998 999 1000 1001
  let count_name = ref 0
  let name () =
    incr count_name;
    "X" ^ (string_of_int !count_name)

1002 1003
  let to_print = ref []

1004 1005 1006
  let trivial_rec b = 
    b == BoolRec.empty || 
    (is_empty { empty with record = BoolRec.diff BoolRec.full b})
1007

1008
  let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
1009 1010

  let worth_abbrev d = 
1011 1012
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
1013

1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025
  let worth_complement d =
    let aux f x y = if f x y = 0 then 1 else 0 in
    let n = 
      aux Atoms.compare d.atoms any.atoms +
      aux Chars.compare d.chars any.chars +
      aux Intervals.compare d.ints any.ints +
      aux BoolPair.compare d.times any.times +
      aux BoolPair.compare d.xml any.xml +
      aux BoolPair.compare d.arrow any.arrow +
      aux BoolRec.compare d.record any.record in
    n >= 4

1026
  let rec prepare d =
1027
    try DescrHash.find memo d
1028
    with Not_found ->
1029 1030
      try 
	let n = DescrMap.find d !named in
1031 1032
	let s = alloc [] in
	s.state <- `Named n;
1033 1034 1035
	DescrHash.add memo d s;
	s
      with Not_found ->
1036
	if worth_complement d then 
1037
	  alloc [Neg (prepare (neg d))]
1038
	else
1039 1040 1041
	let slot = alloc [] in
	if not (worth_abbrev d) then slot