types.ml 37.6 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
type pair_kind = [ `Normal | `XML ]

49 50 51 52
type 'a node0 = { id : int; mutable descr : 'a }

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

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

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

102 103
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
104

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

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

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

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

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

226

227 228 229 230 231 232 233 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)

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

246 247 248 249 250 251 252 253 254 255 256 257 258 259 260 261 262 263 264
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




265 266
let print_descr = ref (fun _ _  -> assert false)

267 268
let neg x = diff any x

269 270
let any_node = cons any

271
module LabelS = Set.Make(LabelPool)
272 273 274

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

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

318

319 320 321 322 323 324 325 326 327 328 329 330


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

337 338 339
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

340
let trivially_empty d = equal_descr d empty
341

342
exception NotEmpty
343

344 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
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;
370
  s.notify <- Nothing; 
371 372 373 374 375 376 377 378 379 380 381 382 383 384
  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 =
385 386
  match slot a with
    | { status = Empty } -> ()
387
    | { status = Maybe } as s -> n.active <- true; s.notify <- Do (n,f,s.notify)
388
    | { status = NEmpty } -> f n
389 390 391 392

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

436 437 438 439 440 441 442 443 444 445 446 447
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
448

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


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

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

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

537 538 539 540 541 542 543 544 545

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

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

585
and empty_rec_record c =
586
  List.for_all empty_rec_record_aux (get_record c)
587

588 589
(*
let is_empty d =
590
  empty_rec d
591
  *)
592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619

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

638
(*
639 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
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)

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

693

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

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

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

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


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

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

734 735
module Print = 
struct
736 737 738 739 740 741 742
  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
743 744
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
745

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

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

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

764
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
765
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
766 767

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

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
773
    if not (DescrMap.mem d !named) then
774 775 776 777 778 779 780 781
      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);
782 783
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
784 785
	  (fun (n1,n2) -> mark n1; mark n2
(*
786 787 788
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
789 790 791
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
792
		  let l = get_record d1.record in
793 794 795 796 797
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
798 799
	       )
	       (Product.normal (descr n2))
800
*)
801
	  ) d.xml;
802
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
803 804 805
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
806 807 808 809 810

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
811
      let name = DescrMap.find d !named in
812 813 814 815 816 817 818
      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
819
	  Not_found -> assert false
820 821
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
822 823 824 825 826 827 828 829 830
      (
	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 @
831
	   BoolRec.print "Record" print_record d.record
832 833
	  )
      )
834 835
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
836
  and print_xml ppf (t1,t2) =
837 838
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
839 840 841 842 843 844 845 846 847
    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
848
*)
849 850
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
851 852 853 854
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
855
    List.iter (fun (l,t) ->
856
		 let sep = if !first then (first := false; "") else ";" in
857 858
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
859
	      ) (LabelMap.get r);
860 861
    Format.fprintf ppf " %s}@]" o
(*
862 863 864 865 866 867 868 869 870 871 872 873 874 875 876 877 878
  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
879
*)
880 881 882

	  
  let end_print ppf =
883
    Format.fprintf ppf "@]";
884 885 886 887 888 889 890 891 892 893
    (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 "@]"
    );
894
(*    Format.fprintf ppf "@]"; *)
895 896 897 898 899 900 901 902 903 904 905 906 907
    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

908
let () = print_descr := Print.print_descr
909

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


916 917 918 919 920 921 922 923 924
  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)
925
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
926

927 928 929 930 931 932 933 934 935
  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
936

937 938 939 940 941 942
  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))
943
  let xml d1 d2 = cons (`Xml (d1,d2))
944
  let define v1 v2 = def v1 (`Cup [v2]) 
945

946 947
  let solve v = internalize (make_node v)
end
948

949

950

951

952 953 954
(* Sample value *)
module Sample =
struct
955

956

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

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

let rec sample_rec memo d =
  if (Assumptions.mem d memo) || (is_empty d) then raise Not_found 
  else 
    try Int (Intervals.sample d.ints) with Not_found ->