types.ml 38.9 KB
Newer Older
1
open Ident
2

3 4 5 6 7 8
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
9 10


11 12 13 14
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
15

16 17 18 19 20 21 22 23 24 25 26 27 28 29 30
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

31 32
let equal_const c1 c2 = compare_const c1 c2 = 0

33 34
type pair_kind = [ `Normal | `XML ]

35 36 37 38
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
39 40 41
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
42 43 44 45 46 47 48
    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 

49 50 51
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
52 53
  let dump ppf (o,r) = ()

54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87
  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

88 89
module BoolPair = Bool.Make(NodePair)
module BoolRec = Bool.Make(RecArg)
90

91
type descr = {
92
  atoms : Atoms.t;
93 94
  ints  : Intervals.t;
  chars : Chars.t;
95 96 97
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
98
  record: descr BoolRec.t;
99
  absent: bool
100
} and node = descr node0
101

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

178
let equal_descr a b =
179 180 181
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
182 183 184
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
185
  (BoolRec.equal a.record b.record) &&
186
  (a.absent == b.absent)
187 188

let compare_descr a b =
189 190
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
191 192
  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
193 194 195
  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
196
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
197 198
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
199 200
  else 0

201
let hash_descr a =
202 203 204
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
205 206 207
  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
208
  let accu = 17 * accu + BoolRec.hash a.record in
209
  let accu = if a.absent then accu+5 else accu in
210
  accu
211

212 213 214 215 216 217 218 219
(* 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) &&
220 221
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
222

223

224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241
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)
242

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




262 263
let print_descr = ref (fun _ _  -> assert false)

264 265
let neg x = diff any x

266 267
let any_node = cons any

268
module LabelS = Set.Make(LabelPool)
269 270 271

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

    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
312
  List.map line (BoolRec.get r)
313
   
314

315

316 317 318 319 320 321 322 323 324 325 326 327


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

334 335 336
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

337
let trivially_empty d = equal_descr d empty
338

339
exception NotEmpty
340

341 342 343 344 345 346 347 348 349 350 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) -> 
      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;
367
  s.notify <- Nothing; 
368 369
  raise NotEmpty

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

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
391 392
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
393 394
  else try DescrHash.find memo d
  with Not_found ->
395 396
    (*    incr count_slot;
    Printf.eprintf "%i;" !count_slot; *)
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 404 405
(*       Format.fprintf Format.std_formatter "check_times_bool:@[%a@]@\n"
	 BoolPair.dump d.times;  *)
(*       check_times_bool any any d.times s; *)
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_times (BoolPair.get d.xml); 
406
       iter_s s check_arrow (BoolPair.get d.arrow);
407 408 409 410 411 412 413
       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 =
414
(*  Printf.eprintf "[%i]" (List.length right);
415
  flush stderr;  *)
416 417
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
418 419 420
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
421 422
	     aux accu1 accu2 right s )
	else (
423 424 425 426 427 428 429 430 431
          let accu1' = diff accu1 t1 in 
	  guard accu1' (aux accu1' accu2 right) s;

          let accu2' = diff accu2 t2 in 
	    guard accu2' (aux accu1 accu2' right) s  
(*	  let accu1 = cap accu1 t1 in (* TODO: approximation of cap ... *)
          let accu2' = diff accu2 t2 in 
	  guard accu1 (guard accu2' (aux accu1 accu2' right)) s *)

432
	)
433 434
    | [] -> set s
  in
435 436 437
  let (accu1,accu2) = cap_product left in
(*  if List.length right > 6 then (
    Printf.eprintf "HEURISTIC\n"; flush stderr; 
438 439 440 441
    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;
442 443
    Printf.eprintf "HEURISTIC failed\n"; flush stderr; 
  );  *)
444
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
445

446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463 464 465 466 467 468 469 470 471 472

(*
and check_times_bool accu1 accu2 b s =
  match b with
    | BoolPair.True -> guard accu1 (guard accu2 set) s
    | BoolPair.False -> ()
    | BoolPair.Split (_, (t1,t2), p,i,n) ->
	check_times_bool accu1 accu2 i s;
	let t1 = descr t1 and t2 = descr t2 in
	if (trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2)
	then check_times_bool accu1 accu2 n s else
	  (
	    if p <> BoolPair.False then
	      (let accu1 = cap accu1 t1 
	       and accu2 = cap accu2 t2 in
	       if not (trivially_empty accu1 || trivially_empty accu2) then
		 check_times_bool accu1 accu2 p s);
	    
	    if n <> BoolPair.False then
	      (let accu1' = diff accu1 t1 in 
	       check_times_bool accu1' accu2 n s;
               let accu2' = diff accu2 t2 in 
	       check_times_bool accu1 accu2' n s)
	  )
*)


473 474 475 476 477 478 479 480 481 482 483 484
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
485

486
and check_record (labels,(oleft,left),rights) s =
487 488
  let rec aux rights s = match rights with
    | [] -> set s
489
    | (oright,right)::rights ->
490
	let next =
491
	  (oleft && (not oright)) ||
492
	  exists (Array.length left)
493
	    (fun i -> trivially_disjoint left.(i) right.(i))
494 495 496 497 498 499
	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
500 501 502 503 504
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
505 506 507 508 509
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
510
      guard left.(i) (start (i - 1)) s
511 512 513 514 515
  in
  start (Array.length left - 1) s


let is_empty d =
516
(*  Printf.eprintf "is_empty: start\n"; flush stderr; *)
517 518 519 520 521
  let s = slot d in
  List.iter 
    (fun s' -> if s'.status = Maybe then s'.status <- Empty; s'.notify <- Nothing) 
    !marks;
  marks := [];
522
(*  Printf.eprintf "is_empty: done\n"; flush stderr; *)
523 524 525
  s.status = Empty
  

526
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
527 528
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
529

530
let rec empty_rec d =
531
  if not (Intervals.is_empty d.ints) then false
532 533
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
534
  else if d.absent then false
535 536
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
537 538
  else (
    let backup = !memo in
539
    memo := Assumptions.add d backup;
540
    if 
541 542 543
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
544 545 546 547
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
548
      DescrHash.add cache_false d ();
549 550 551 552 553 554 555 556 557 558
      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 ->
559 560
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
561 562 563 564 565
	  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
566
	  if not (empty_rec accu2') then aux accu1 accu2' right
567 568 569 570 571
    | [] -> 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)
572

573 574 575 576 577 578 579 580 581

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
582
          if not (empty_rec accu1') then aux accu1' accu2 left;
583
          let accu2' = cap_t accu2 t2 in
584
          if not (empty_rec accu2') then aux accu1 accu2' left
585 586 587 588 589 590 591 592
      | [] -> 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

593
and empty_rec_record_aux (labels,(oleft,left),rights) =
594 595
  let rec aux = function
    | [] -> raise NotEmpty
596
    | (oright,right)::rights ->
597 598 599 600
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
601
	       trivially_empty (cap left.(i) right.(i)))
602 603 604 605 606 607
	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
608
	    if not (empty_rec di) then (
609 610 611 612 613 614 615
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
616
    (fun i -> empty_rec left.(i))
617 618 619 620
  ||
  (try aux rights; true with NotEmpty -> false)
	    

621
and empty_rec_record c =
622
  List.for_all empty_rec_record_aux (get_record c)
623

624 625
(*
let is_empty d =
626
  empty_rec d
627
  *)
628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655

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*) 
656
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673
	      
	      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

674
(*
675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702
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)

703
*)
704 705 706 707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722
  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
723
    List.iter line (BoolPair.get d);
724
    !accu
725 726 727
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
728

729

730 731
  let get ?(kind=`Normal) d = 
    match kind with
732 733
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
734 735 736

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
737 738 739 740
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
741 742

  let restrict_1 rects pi1 =
743 744
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
745 746 747 748
    List.fold_left aux [] rects
  
  type normal = t

749
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
750 751 752 753 754 755 756 757


  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 ->
758
	  let gd = get_aux d in
759
	  let n = normal_aux gd in
760 761
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
762 763
	  memo := Memo.add d n !memo;
	  n
764

765 766 767 768
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
769

770 771
module Print = 
struct
772 773 774 775 776 777 778
  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
779 780
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
781

782
  let print_const ppf = function
783 784 785
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
786

787 788 789
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
790 791 792 793 794 795 796 797 798 799

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

800
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
801
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
802 803

  let worth_abbrev d = 
804 805
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
806 807 808

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
809
    if not (DescrMap.mem d !named) then
810 811 812 813 814 815 816 817
      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);
818 819
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
820 821
	  (fun (n1,n2) -> mark n1; mark n2
(*
822 823 824
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
825 826 827
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
828
		  let l = get_record d1.record in
829 830 831 832 833
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
834 835
	       )
	       (Product.normal (descr n2))
836
*)
837
	  ) d.xml;
838
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
839 840 841
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
842 843 844 845 846

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
847
      let name = DescrMap.find d !named in
848 849 850 851 852 853 854
      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
855
	  Not_found -> assert false
856 857
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
858 859 860 861 862 863 864 865 866
      (
	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 @
867
	   BoolRec.print "Record" print_record d.record
868 869
	  )
      )
870 871
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
872
  and print_xml ppf (t1,t2) =
873 874
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
875 876 877 878 879 880 881 882 883
    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
884
*)
885 886
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
887 888 889 890
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
891
    List.iter (fun (l,t) ->
892
		 let sep = if !first then (first := false; "") else ";" in
893 894
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
895
	      ) (LabelMap.get r);
896 897
    Format.fprintf ppf " %s}@]" o
(*
898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914
  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
915
*)
916 917 918

	  
  let end_print ppf =
919
    Format.fprintf ppf "@]";
920 921 922 923 924 925 926 927 928 929
    (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 "@]"
    );
930
(*    Format.fprintf ppf "@]"; *)
931 932 933 934 935 936 937 938 939 940 941 942 943
    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

944
let () = print_descr := Print.print_descr
945

946 947
module Positive =
struct
948
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v | `Xml of v * v ]
949
  and v = { mutable def : rhs; mutable node : node option }
950 951


952 953 954 955 956 957 958 959 960
  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)
961
	| `Xml (v1,v2) -> xml (make_node v1) (make_node v2)
962

963 964 965 966 967 968 969 970 971
  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
972

973 974 975 976 977 978
  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))
979
  let xml d1 d2 = cons (`Xml (d1,d2))
980
  let define v1 v2 = def v1 (`Cup [v2]) 
981

982 983
  let solve v = internalize (make_node v)
end
984

985

986