types.ml 40.2 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
let map_sort f l =
  SortedList.from_list (List.map f l)
21

22 23 24 25 26 27
module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end
28 29


30 31 32 33
type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
34

35 36
type pair_kind = [ `Normal | `XML ]

37 38 39 40 41 42 43 44 45 46 47 48
type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
  let compare (x1,y1) (x2,y2) =
    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 52 53 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
module RecArg = struct
  type 'a t = bool * 'a node0 label_map
  
  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

86
module BoolPair = Boolean.Make(NodePair)
87
module BoolRec = Boolean.Make(RecArg)
88

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

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

let rec compare_rec r1 r2 =
  if r1 == r2 then 0
  else match (r1,r2) with
186
    | (l1,x1)::r1,(l2,x2)::r2 ->
187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236
	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 rec compare_rec_list l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
	if o2 && not o1 then -1
	else if o1 && not o2 then 1
	else let c = compare_rec r1 r2 in if c <> 0 then c 
	else compare_rec_list l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_rec_bool l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 ->
	let c = compare_rec_list p1 p2 in if c <> 0 then c 
	else let c = compare_rec_list n1 n2 in if c <> 0 then c 
	else compare_rec_bool l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_times_list l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (x1,y1)::l1, (x2,y2)::l2 ->
	if (x1.id < x2.id) then -1
	else if (x1.id > x2.id) then 1 
	else if (y1.id < y2.id) then -1
	else if (y1.id > y2.id) then 1 
	else compare_times_list l1 l2
    | ([],_) -> -1
    | _ -> 1

let rec compare_times_bool l1 l2  =
  if l1 == l2 then 0 
  else match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 ->
	let c = compare_times_list p1 p2 in if c <> 0 then c 
	else let c = compare_times_list n1 n2 in if c <> 0 then c 
	else compare_times_bool l1 l2
    | ([],_) -> -1
    | _ -> 1
237 238 239 240
	     
let rec equal_rec r1 r2 =
  (r1 == r2) ||
  match (r1,r2) with
241 242
    | (l1,x1)::r1,(l2,x2)::r2 ->
	(x1.id = x2.id) && (l1 == l2) && (equal_rec r1 r2)
243
    | _ -> false
244 245 246 247 248
	
let rec equal_rec_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
249 250
	(o1 == o2) &&
	(equal_rec r1 r2) && (equal_rec_list l1 l2)
251 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280
    | _ -> false
	
let rec equal_rec_bool l1 l2 =
  (l1 == l2) ||
  match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 -> 
	(equal_rec_list p1 p2) &&
	(equal_rec_list n1 n2) &&
        (equal_rec_bool l1 l2)
    | _ -> false
	
let rec equal_times_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (x1,y1)::l1, (x2,y2)::l2 -> 
	(x1.id = x2.id) &&
	(y1.id = y2.id) &&
	(equal_times_list l1 l2)
    | _ -> false
	
let rec equal_times_bool l1 l2 =
  (l1 == l2) ||
  match (l1,l2) with
    | (p1,n1)::l1, (p2,n2)::l2 -> 
	(equal_times_list p1 p2) &&
	(equal_times_list n1 n2) &&
        (equal_times_bool l1 l2)
    | _ -> false
	
let equal_descr a b =
281 282 283
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
284 285 286
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
287
  (BoolRec.equal a.record b.record) &&
288
  (a.absent == b.absent)
289 290 291 292 293

let compare_descr a b =
  let c = compare a.atoms b.atoms in if c <> 0 then c
  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
294 295 296
  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
297
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
298 299
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
300 301 302 303 304 305 306 307 308 309
  else 0

(*
let compare_descr a b =
  let c = compare_descr a b in
  assert (c = compare a b);
  c
*)


310 311 312 313 314 315 316 317 318 319 320
let rec hash_times_list accu = function
  | (x,y)::l ->
      hash_times_list (accu * 257 + x.id * 17 + y.id) l
  | [] -> accu + 17
      
let rec hash_times_bool accu = function
  | (p,n)::l -> 
      hash_times_bool (hash_times_list (hash_times_list accu p) n) l
  | [] -> accu + 3
      
let rec hash_rec accu = function
321
  | (l,x)::rem ->
322 323 324 325 326
      hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
  | [] -> accu + 5
      
let rec hash_rec_list accu = function
  | (o,r)::l ->
327
      hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
328 329 330 331 332 333 334 335 336
  | [] -> accu + 17
      
let rec hash_rec_bool accu = function
  | (p,n)::l -> 
      hash_rec_bool (hash_rec_list (hash_rec_list accu p) n) l
  | [] -> accu + 3
      
      
let hash_descr a =
337 338 339
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
340 341 342
  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
343
  let accu = 17 * accu + BoolRec.hash a.record in
344
  let accu = if a.absent then accu+5 else accu in
345
  accu
346

347 348 349 350 351 352 353 354 355
module DescrHash = 
  Hashtbl.Make(
    struct 
      type t = descr
      let hash = hash_descr
      let equal = equal_descr
    end
  )

356 357
let print_descr = ref (fun _ _  -> assert false)

358 359
let neg x = diff any x

360 361
let any_node = cons any

362
module LabelS = Set.Make(LabelPool)
363 364 365

let get_record r =
  let labs accu (_,r) = 
366 367
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
368
  let extend descrs labs (o,r) =
369 370 371 372 373
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
374
	      | (l2,x)::r when l1 == l2 -> 
375 376 377
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
378 379
		  if not o then descrs.(i) <- 
		    cap descrs.(i) { empty with absent = true };
380 381
		  aux (i+1) labs r
    in
382
    aux 0 labs (LabelMap.get r);
383 384 385 386
    o
  in
  let line (p,n) =
    let labels = 
387 388
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
389
    let nlab = List.length labels in
390
    let mk () = Array.create nlab { any with absent = true } in
391 392 393 394 395 396 397 398 399 400 401 402 403 404 405

    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
406
  List.map line (BoolRec.get r)
407
   
408

409
module DescrMap = Map.Make(struct type t = descr let compare = compare end)
410

411
let check d =
412 413 414
  BoolPair.check d.times;
  BoolPair.check d.xml;
  BoolPair.check d.arrow;
415
  BoolRec.check d.record;
416
  ()
417

418 419 420 421 422 423 424 425 426 427 428 429 430


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

431 432 433
let rec exists max f =
  (max > 0) && (f (max - 1) || exists (max - 1) f)

434
let trivially_empty d = equal_descr d empty
435

436
exception NotEmpty
437

438 439 440 441 442 443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463
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;
464
(*  s.notify <- Nothing; *)
465 466 467 468 469 470 471 472 473 474 475 476 477
  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

478

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

and slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
488 489
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
490 491 492 493 494
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
495 496 497
       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);
498 499 500 501 502 503 504 505 506 507 508 509 510 511
       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 ->
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
	     aux accu1 accu2 right s
	else
          let accu1' = diff_t accu1 t1 in guard accu1' (aux accu1' accu2 right) s;
512
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
513 514 515 516
    | [] -> set s
  in
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard accu2 (aux accu1 accu2 right)) s
517

518 519 520 521 522 523 524 525 526 527 528 529
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
530

531
and check_record (labels,(oleft,left),rights) s =
532 533
  let rec aux rights s = match rights with
    | [] -> set s
534
    | (oright,right)::rights ->
535
	let next =
536
	  (oleft && (not oright)) || (* ggg... why ???  check this line *)
537 538
	  exists (Array.length left)
	    (fun i ->
539
	       trivially_empty (cap left.(i) right.(i)))
540 541 542 543 544 545
	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
546 547 548 549 550
	    guard di (fun s ->
			left.(i) <- diff back right.(i);
			aux rights s;
			left.(i) <- back;
		     ) s
551 552 553 554 555
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
556
      guard left.(i) (start (i - 1)) s
557 558 559 560 561 562 563 564 565 566 567 568 569
  in
  start (Array.length left - 1) s


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

570
module Assumptions = Set.Make(struct type t = descr let compare = compare_descr end)
571 572
let memo = ref Assumptions.empty
let cache_false = DescrHash.create 33000
573

574
let rec empty_rec d =
575
  if not (Intervals.is_empty d.ints) then false
576 577
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
578
  else if d.absent then false
579 580
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
581 582
  else (
    let backup = !memo in
583
    memo := Assumptions.add d backup;
584
    if 
585 586 587
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
588 589 590 591
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
592
      DescrHash.add cache_false d ();
593 594 595 596 597 598 599 600 601 602
      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 ->
603 604
	if trivially_empty (cap_t accu1 t1) || 
	   trivially_empty (cap_t accu2 t2) then
605 606 607 608 609
	  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
610
	  if not (empty_rec accu2') then aux accu1 accu2' right
611 612 613 614 615
    | [] -> 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)
616

617 618 619 620 621 622 623 624 625

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
626
          if not (empty_rec accu1') then aux accu1' accu2 left;
627
          let accu2' = cap_t accu2 t2 in
628
          if not (empty_rec accu2') then aux accu1 accu2' left
629 630 631 632 633 634 635 636
      | [] -> 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

637
and empty_rec_record_aux (labels,(oleft,left),rights) =
638 639
  let rec aux = function
    | [] -> raise NotEmpty
640
    | (oright,right)::rights ->
641 642 643 644
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i ->
645
	       trivially_empty (cap left.(i) right.(i)))
646 647 648 649 650 651
	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
652
	    if not (empty_rec di) then (
653 654 655 656 657 658 659
	      left.(i) <- diff back right.(i);
	      aux rights;
	      left.(i) <- back;
	    )
	  done
  in
  exists (Array.length left) 
660
    (fun i -> empty_rec left.(i))
661 662 663 664
  ||
  (try aux rights; true with NotEmpty -> false)
	    

665
and empty_rec_record c =
666
  List.for_all empty_rec_record_aux (get_record c)
667

668 669
(*
let is_empty d =
670
  empty_rec d
671
  *)
672 673 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

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*) 
700
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
701 702 703 704 705 706 707 708 709 710 711 712 713 714 715 716 717
	      
	      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

718
(*
719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746
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)

747
*)
748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766
  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
767
    List.iter line (BoolPair.get d);
768
    !accu
769 770 771
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)
772

773

774 775
  let get ?(kind=`Normal) d = 
    match kind with
776 777
      | `Normal -> get_aux d.times
      | `XML -> get_aux d.xml
778 779 780

  let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
  let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
781 782 783 784
  let pi2_restricted restr = 
    List.fold_left (fun acc (t1,t2) -> 
		      if is_empty (cap t1 restr) then acc
		      else cup acc t2) empty
785 786

  let restrict_1 rects pi1 =
787 788
    let aux acc (t1,t2) = 
      let t1 = cap t1 pi1 in if is_empty t1 then acc else (t1,t2)::acc in
789 790 791 792
    List.fold_left aux [] rects
  
  type normal = t

793
  module Memo = Map.Make(struct type t = descr BoolPair.t let compare = BoolPair.compare end)
794 795 796 797 798 799 800 801


  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 ->
802
	  let gd = get_aux d in
803
	  let n = normal_aux gd in
804 805
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
806 807
	  memo := Memo.add d n !memo;
	  n
808

809 810 811 812
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end
813

814 815
module Print = 
struct
816 817 818 819 820 821 822
  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
823 824
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)
825

826
  let print_const ppf = function
827 828 829
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
830

831 832 833
  let named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named
834 835 836 837 838 839 840 841 842 843

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

844
  let trivial_rec b = b = BoolRec.empty || b = BoolRec.full
845
  let trivial_pair b = b = BoolPair.empty || b = BoolPair.full
846 847

  let worth_abbrev d = 
848 849
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
850 851 852

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
853
    if not (DescrMap.mem d !named) then
854 855 856 857 858 859 860 861
      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);
862 863
    	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
    	BoolPair.iter 
864 865
	  (fun (n1,n2) -> mark n1; mark n2
(*
866 867 868
	     List.iter
	       (fun (d1,d2) ->
		  mark_descr d2;
869 870 871
    		  bool_iter 
		    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
		    d1.record
872
		  let l = get_record d1.record in
873 874 875 876 877
		  List.iter (fun labs,(_,(_,p)),ns ->
			       Array.iter mark_descr p;
			       List.iter (fun (_,(_,n)) -> 
					    Array.iter mark_descr n) ns
			    ) l
878 879
	       )
	       (Product.normal (descr n2))
880
*)
881
	  ) d.xml;
882
	BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
883 884 885
    	BoolRec.iter 
	  (fun (o,l) -> List.iter (fun (l,n) -> mark n) (LabelMap.get l)) 
	  d.record
886 887 888 889 890

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
891
      let name = DescrMap.find d !named in
892 893 894 895 896 897 898
      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
899
	  Not_found -> assert false
900 901
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
902 903 904 905 906 907 908 909 910
      (
	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 @
911
	   BoolRec.print "Record" print_record d.record
912 913
	  )
      )
914 915
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
916
  and print_xml ppf (t1,t2) =
917 918
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
919 920 921 922 923 924 925 926 927
    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
928
*)
929 930
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
931 932 933 934
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
935
    List.iter (fun (l,t) ->
936
		 let sep = if !first then (first := false; "") else ";" in
937 938
		 Format.fprintf ppf "%s@ @[%s =@] %a" sep
		   (LabelPool.value l) print t
939
	      ) (LabelMap.get r);
940 941
    Format.fprintf ppf " %s}@]" o
(*
942 943 944 945 946 947 948 949 950 951 952 953 954 955 956 957 958
  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
959
*)
960 961 962 963 964 965 966 967 968 969 970 971 972 973 974 975 976 977 978 979 980 981 982 983 984 985 986

	  
  let end_print ppf =
    (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 "@]"
    );
    Format.fprintf ppf "@]";
    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

987
let () = print_descr := Print.print_descr
988

989 990 991 992
module Positive =
struct
  type rhs = [ `Type of descr | `Cup of v list | `Times of v * v ]
  and v = { mutable def : rhs; mutable node : node option }
993 994


995 996 997 998 999 1000 1001 1002 1003
  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)
1004

1005 1006 1007 1008 1009 1010 1011 1012 1013
  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
1014

1015 1016 1017 1018 1019 1020 1021
  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))
  let define v1 v2 = def v1 (`Cup [v2]) 
1022

1023 1024
  let solve v = internalize (make_node v)
end
1025

1026

1027

1028

1029 1030 1031
(* Sample value *)
module Sample =
struct
1032