types.ml 37.7 KB
Newer Older
1 2
open Recursive
open Printf
3
open Ident
4

5 6 7 8 9 10 11 12 13 14 15 16 17 18
(* IDEAS for optimizations:

  * optimize lines of dnf for products and record;
    instead of
      (t1,s1) & ... & (tn,sn) \ ....
    use:
      (t1 & ... & tn, s1 & ... & sn) \ ....

    ---> more compact representation, more sharing, ...
 
  * re-consider using BDD-like representation instead of dnf
*)


19 20 21 22 23 24
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
25 26


27 28 29 30
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
31

32 33 34 35 36 37 38 39 40 41 42 43 44 45 46
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

47 48
let equal_const c1 c2 = compare_const c1 c2 = 0

49 50
type pair_kind = [ `Normal | `XML ]

51 52 53 54
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
55 56 57
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
58 59 60 61 62 63 64
    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 

65 66 67
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
68 69
  let dump ppf (o,r) = ()

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 98 99 100 101 102 103
  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

104 105
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
106

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

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

194
let equal_descr a b =
195 196 197
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
198 199 200
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
201
  (BoolRec.equal a.record b.record) &&
202
  (a.absent == b.absent)
203 204

let compare_descr a b =
205 206
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
207 208
  else let c = compare a.chars b.chars in if c <> 0 then c
  else let c = compare a.ints b.ints in if c <> 0 then c
209 210 211
  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
212
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
213 214
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
215 216
  else 0

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

228

229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246
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)

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)
247

248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266
let hash_cons = DescrHash.create 17000

let count = ref 0
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




267 268
let print_descr = ref (fun _ _  -> assert false)

269 270
let neg x = diff any x

271 272
let any_node = cons any

273
module LabelS = Set.Make(LabelPool)
274 275 276

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

    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
317
  List.map line (BoolRec.get r)
318
   
319

320

321 322 323 324 325 326 327 328 329 330 331 332


(* 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
333 334 335 336 337
let cup_product l =
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cup_t d1 t1, cup_t d2 t2))
    (empty,empty)
    l
338

339 340 341
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

342
let trivially_empty d = equal_descr d empty
343

344
exception NotEmpty
345

346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371
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) -> 
      if n.status = Maybe then (try f n with NotEmpty -> ());
      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;
372
  s.notify <- Nothing; 
373 374 375 376 377 378 379 380 381 382 383 384 385 386
  raise NotEmpty

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

let rec guard a f n =
387 388
  match slot a with
    | { status = Empty } -> ()
389
    | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
390
    | { status = NEmpty } -> f n
391 392 393 394

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
395 396
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
397 398
  else try DescrHash.find memo d
  with Not_found ->
399
(*    Format.fprintf Format.std_formatter "Empty:%a@\n" !print_descr d; *)
400 401 402
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
403 404 405
       iter_s s check_times (BoolPair.get d.times);
       iter_s s check_times (BoolPair.get d.xml);
       iter_s s check_arrow (BoolPair.get d.arrow);
406 407 408 409 410 411 412
       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 =
413
(*  Printf.eprintf "[%i]" (List.length right);
414
  flush stderr;  *)
415 416 417
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	if trivially_empty (cap_t accu1 t1) || 
418 419 420
	   trivially_empty (cap_t accu2 t2) then (
	     aux accu1 accu2 right s )
	else (
421
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
422
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
423
	)
424 425
    | [] -> set s
  in
426 427 428 429 430 431 432 433 434
(*
  if List.length right > 6 then (
    Printf.eprintf "HEURISTIC\n"; flush stderr;
    let (n1,n2) = cup_product right in
    let n1 = diff accu1 n1 and n2 = diff accu2 n2 in
    guard n1 set s;
    guard n2 set s;
    Printf.eprintf "HEURISTIC failed\n"; flush stderr;
  ); *)
435 436
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
437

438 439 440 441 442 443 444 445 446 447 448 449
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 ->
          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
      | [] -> set s
    in
    let accu1 = descr s1 in
    guard accu1 (aux accu1 (neg (descr s2)) left) s
  in
  big_conj single_right right s
450

451
and check_record (labels,(oleft,left),rights) s =
452 453
  let rec aux rights s = match rights with
    | [] -> set s
454
    | (oright,right)::rights ->
455
	let next =
456
	  (oleft && (not oright)) || (* ggg... why ???  check this line *)
457 458
	  exists (Array.length left)
	    (fun i ->
459
	       trivially_empty (cap left.(i) right.(i)))
460 461 462 463 464 465
	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
466 467 468 469 470
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
471 472 473 474 475
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
476
      guard left.(i) (start (i - 1)) s
477 478 479 480 481
  in
  start (Array.length left - 1) s


let is_empty d =
482
(*  Printf.eprintf "is_empty: start\n"; flush stderr; *)
483 484 485 486 487
  let s = slot d in
  List.iter 
    (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
488
(*  Printf.eprintf "is_empty: done\n"; flush stderr; *)
489 490 491
  s.status = Empty
  

492
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
493 494
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
495

496
let rec empty_rec d =
497
  if not (Intervals.is_empty d.ints) then false
498 499
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
500
  else if d.absent then false
501 502
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
503 504
  else (
    let backup = !memo in
505
    memo := Assumptions.add d backup;
506
    if 
507 508 509
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
510 511 512 513
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
514
      DescrHash.add cache_false d ();
515 516 517 518 519 520 521 522 523 524
      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 ->
525 526
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
527 528 529 530 531
	  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
532
	  if not (empty_rec accu2') then aux accu1 accu2' right
533 534 535 536 537
    | [] -> 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)
538

539 540 541 542 543 544 545 546 547

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
548
          if not (empty_rec accu1') then aux accu1' accu2 left;
549
          let accu2' = cap_t accu2 t2 in
550
          if not (empty_rec accu2') then aux accu1 accu2' left
551 552 553 554 555 556 557 558
      | [] -> 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

559
and empty_rec_record_aux (labels,(oleft,left),rights) =
560 561
  let rec aux = function
    | [] -> raise NotEmpty
562
    | (oright,right)::rights ->
563 564 565 566
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
567
	       trivially_empty (cap left.(i) right.(i)))
568 569 570 571 572 573
	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
574
	    if not (empty_rec di) then (
575 576 577 578 579 580 581
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
582
    (fun i -> empty_rec left.(i))
583 584 585 586
  ||
  (try aux rights; true with NotEmpty -> false)
	    

587
and empty_rec_record c =
588
  List.for_all empty_rec_record_aux (get_record c)
589

590 591
(*
let is_empty d =
592
  empty_rec d
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

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

  let normal_aux d =
    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*) 
622
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639
	      
	      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

640
(*
641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668
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)

669
*)
670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688
  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
689
    List.iter line (BoolPair.get d);
690
    !accu
691 692 693
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
694

695

696 697
  let get ?(kind=`Normal) d = 
    match kind with
698 699
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
700 701 702

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
703 704 705 706
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
707 708

  let restrict_1 rects pi1 =
709 710
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
711 712 713 714
    List.fold_left aux [] rects
  
  type normal = t

715
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
716 717 718 719 720 721 722 723


  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 ->
724
	  let gd = get_aux d in
725
	  let n = normal_aux gd in
726 727
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
728 729
	  memo := Memo.add d n !memo;
	  n
730

731 732 733 734
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
735

736 737
module Print = 
struct
738 739 740 741 742 743 744
  let rec print_union ppf = function
    | [] -> Format.fprintf ppf "Empty"
    | [h] -> h ppf
    | h::t -> Format.fprintf ppf "@[%t |@ %a@]" h print_union t

  let print_tag ppf a =
    match Atoms.is_atom a with
745 746
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
747

748
  let print_const ppf = function
749 750 751
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
752

753 754 755
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
756 757 758 759 760 761 762 763 764 765

  let marks = DescrHash.create 63
  let wh = ref []
  let count_name = ref 0
  let name () =
    incr count_name;
    "X" ^ (string_of_int !count_name)
(* TODO: 
   check that these generated names does not conflict with declared types *)

766
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
767
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
768 769

  let worth_abbrev d = 
770 771
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
772 773 774

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
775
    if not (DescrMap.mem d !named) then
776 777 778 779 780 781 782 783
      try 
	let r = DescrHash.find marks d in
	if (!r = None) && (worth_abbrev d) then 
	  let na = name () in 
	  r := Some na;
	  wh := (na,d) :: !wh
      with Not_found -> 
	DescrHash.add marks d (ref None);
784 785
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
786 787
	  (fun (n1,n2) -> mark n1; mark n2
(*
788 789 790
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
791 792 793
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
794
		  let l = get_record d1.record in
795 796 797 798 799
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
800 801
	       )
	       (Product.normal (descr n2))
802
*)
803
	  ) d.xml;
804
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
805 806 807
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
808 809 810 811 812

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
813
      let name = DescrMap.find d !named in
814 815 816 817 818 819 820
      Format.fprintf ppf "%s" name
    with Not_found ->
      try
      	match !(DescrHash.find marks d) with
      	  | Some n -> Format.fprintf ppf "%s" n
      	  | None -> real_print_descr ppf d
      with
821
	  Not_found -> assert false
822 823
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
824 825 826 827 828 829 830 831 832
      (
	if d.absent then Format.fprintf ppf "?";
	print_union ppf 
	  (Intervals.print d.ints @
	   Chars.print d.chars @
	   Atoms.print d.atoms @
	   BoolPair.print "Pair" print_times d.times @
	   BoolPair.print "XML" print_xml d.xml @
	   BoolPair.print "Arrow" print_arrow d.arrow @
833
	   BoolRec.print "Record" print_record d.record
834 835
	  )
      )
836 837
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
838
  and print_xml ppf (t1,t2) =
839 840
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
841 842 843 844 845 846 847 848 849
    let l = Product.normal (descr t2) in
    let l = List.map
	      (fun (d1,d2) ppf ->
		 Format.fprintf ppf "@[<><%a%a>%a@]" 
		   print_tag (descr t1).atoms
		   print_attribs d1.record 
		   print_descr d2) l
    in
    print_union ppf l
850
*)
851 852
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
853 854 855 856
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
857
    List.iter (fun (l,t) ->
858
		 let sep = if !first then (first := false; "") else ";" in
859 860
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
861
	      ) (LabelMap.get r);
862 863
    Format.fprintf ppf " %s}@]" o
(*
864 865 866 867 868 869 870 871 872 873 874 875 876 877 878 879 880
  and print_attribs ppf r =
    let l = get_record r in
    if l <> [ [] ] then 
    let l = List.map 
      (fun att ppf ->
	 let first = ref true in
	 Format.fprintf ppf "{" ;
	 List.iter (fun (l,(o,d)) ->
		      Format.fprintf ppf "%s%s=%s%a" 
		        (if !first then "" else " ")
		        (LabelPool.value l) (if o then "?" else "")
		        print_descr d; 
		      first := false
		   ) att;
	   Format.fprintf ppf "}"
      ) l in
    print_union ppf l
881
*)
882 883 884

	  
  let end_print ppf =
885
    Format.fprintf ppf "@]";
886 887 888 889 890 891 892 893 894 895
    (match List.rev !wh with
       | [] -> ()
       | (na,d)::t ->
	   Format.fprintf ppf " where@ @[%s = %a" na real_print_descr d;
	   List.iter 
	     (fun (na,d) -> 
		Format.fprintf ppf " and@ %s = %a" na real_print_descr d)
	     t;
	   Format.fprintf ppf "@]"
    );
896
(*    Format.fprintf ppf "@]"; *)
897 898 899 900 901 902 903 904 905 906 907 908 909
    count_name := 0;
    wh := [];
    DescrHash.clear marks

  let print_descr ppf d =
    mark_descr d;
    Format.fprintf ppf "@[%a" print_descr d;
    end_print ppf

   let print ppf n = print_descr ppf (descr n)

end

910
let () = print_descr := Print.print_descr
911

912 913
module Positive =
struct
914
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
915
  and v = { mutable def : rhs; mutable node : node option }
916 917


918 919 920 921 922 923 924 925 926
  let rec make_descr seen v =
    if List.memq v seen then empty
    else
      let seen = v :: seen in
      match v.def with
	| `Type d -> d
	| `Cup vl -> 
	    List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
	| `Times (v1,v2) -> times (make_node v1) (make_node v2)
927
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
928

929 930 931 932 933 934 935 936 937
  and make_node v =
    match v.node with
      | Some n -> n
      | None ->
	  let n = make () in
	  v.node <- Some n;
	  let d = make_descr [] v in
	  define n d;
	  n
938

939 940 941 942 943 944
  let forward () = { def = `Cup []; node = None }
  let def v d = v.def <- d
  let cons d = let v = forward () in def v d; v
  let ty d = cons (`Type d)
  let cup vl = cons (`Cup vl)
  let times d1 d2 = cons (`Times (d1,d2))
945
  let xml d1 d2 = cons (`Xml (d1,d2))
946
  let define v1 v2 = def v1 (`Cup [v2]) 
947

948 949
  let solve v = internalize (make_node v)
end
950

951

952

953

954 955 956
(* Sample value *)
module Sample =
struct
957

958

959 960 961 962 963
let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
964 965 966
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
967 968
  | Pair of (t * t)
  | Xml of (t * t)
969
  | Record of (bool * (label * t) list)
970
  | Fun of (node * node) list
971
  | Other
972
 exception FoundSampleRecord of bool * (label * t) list
973 974 975 976