types.ml 41.3 KB
Newer Older
1
open Ident
2
open Encodings
3

4 5 6 7 8 9 10 11 12 13
(*
To be sure not to use generic comparison ...
*)
let (=) : int -> int -> bool = (==)
let (<) : int -> int -> bool = (<)
let (<=) : int -> int -> bool = (<=)
let (<>) : int -> int -> bool = (<>)
let compare = 1


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


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

27 28 29 30 31 32 33 34 35 36 37 38 39 40 41
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

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

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

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

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

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

65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98
  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

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

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

115
	       
116
let empty = { 
117 118 119
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
120
  record= BoolRec.empty;
121 122 123
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
124
  absent= false;
125 126 127
}
	      
let any =  {
128 129 130
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
131
  record= BoolRec.full; 
132 133 134
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
135
  absent= false;
136
}
137 138 139 140

let non_constructed =
  { any with times = empty.times; xml = empty.xml; record = empty.record }
     
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 = Chars.compare a.chars b.chars in if c <> 0 then c
  else let c = Intervals.compare a.ints b.ints in if c <> 0 then c
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
(* 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) &&
236 237
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))
238

239

240 241 242 243 244 245 246 247 248
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)
249
module DescrSet = Set.Make(Descr)
250 251 252 253 254 255 256 257 258

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

260
(* let hash_cons = DescrHash.create 17000 *)
261

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




279 280
let neg x = diff any x

281 282
let any_node = cons any

283
module LabelS = Set.Make(LabelPool)
284 285 286

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

    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
327
  List.map line (BoolRec.get r)
328
   
329

330

331 332 333 334 335 336 337


(* 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)
338
let cap_product any_left any_right l =
339 340
  List.fold_left 
    (fun (d1,d2) (t1,t2) -> (cap_t d1 t1, cap_t d2 t2))
341
    (any_left,any_right)
342
    l
343 344
let any_pair = { empty with times = any.times }

345

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

349
exception NotEmpty
350

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

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

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

398 399 400 401 402 403 404 405 406 407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432 433 434 435 436 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 464 465 466 467 468 469 470 471 472 473 474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499

(* Fast approximation *)

module ClearlyEmpty = 
struct

let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
       iter_s s check_times (BoolPair.get d.times);  
       iter_s s check_xml (BoolPair.get d.xml); 
       iter_s s check_arrow (BoolPair.get d.arrow);
       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 (accu1,accu2) = cap_product any any left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_xml (left,right) s =
  let (accu1,accu2) = cap_product any any_pair left in
  let single_right (t1,t2) s =
    let t1 = descr t1 and t2 = descr t2 in
    if trivially_disjoint accu1 t1 || trivially_disjoint accu2 t2 then set s 
    else
      let accu1 = diff accu1 t1 in guard (slot accu1) set s;
      let accu2 = diff accu2 t2 in guard (slot accu2) set s in
  guard (slot accu1) (guard (slot accu2) (big_conj single_right right)) s

and check_arrow (left,right) s =
  let single_right (s1,s2) s =
    let accu1 = descr s1 and accu2 = neg (descr s2) in
    let single_left (t1,t2) s =
      let accu1 = diff_t accu1 t1 in guard (slot accu1) set s;
      let accu2 = cap_t  accu2 t2 in guard (slot accu2) set s
    in
    guard (slot accu1) (big_conj single_left left) s
  in
  big_conj single_right right s

and check_record (labels,(oleft,left),rights) s =
  let rec single_right (oright,right) s = 
    let next =
      (oleft && (not oright)) ||
      exists (Array.length left)
	(fun i -> trivially_disjoint left.(i) right.(i))
    in
    if next then set s
    else
      for i = 0 to Array.length left - 1 do
	let di = diff left.(i) right.(i) in guard (slot di) set s
      done
  in
  let rec start i s =
    if (i < 0) then big_conj single_right rights s
    else guard (slot left.(i)) (start (i - 1)) s
  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
end

let clearly_disjoint t1 t2 =
(*
  if trivially_disjoint t1 t2 then true
  else
    if ClearlyEmpty.is_empty (cap t1 t2) then
      (Printf.eprintf "!\n"; true) else false
*)
  trivially_disjoint t1 t2 || ClearlyEmpty.is_empty (cap t1 t2) 

let memo = DescrHash.create 33000
let marks = ref [] 

let rec slot d =
500 501
  if not ((Intervals.is_empty d.ints) && 
	  (Atoms.is_empty d.atoms) &&
502 503
	  (Chars.is_empty d.chars) &&
	  (not d.absent)) then slot_not_empty 
504 505 506 507 508
  else try DescrHash.find memo d
  with Not_found ->
    let s = { status = Maybe; active = false; notify = Nothing } in
    DescrHash.add memo d s;
    (try
509
       iter_s s check_times (BoolPair.get d.times);  
510
       iter_s s check_xml (BoolPair.get d.xml); 
511
       iter_s s check_arrow (BoolPair.get d.arrow);
512 513 514 515 516 517 518 519 520
       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 ->
521 522 523
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
524 525
	     aux accu1 accu2 right s )
	else (
526
          let accu1' = diff accu1 t1 in 
527
	  guard (slot accu1') (aux accu1' accu2 right) s;
528 529

          let accu2' = diff accu2 t2 in 
530
	  guard (slot accu2') (aux accu1 accu2' right) s  
531
	)
532 533
    | [] -> set s
  in
534
  let (accu1,accu2) = cap_product any any left in
535
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
536 537 538 539 540

and check_xml (left,right) s =
  let rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	let t1 = descr t1 and t2 = descr t2 in
541
	if clearly_disjoint accu1 t1 || 
542 543 544 545
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
546
	  guard (slot accu1') (aux accu1' accu2 right) s;
547 548

          let accu2' = diff accu2 t2 in 
549
	  guard (slot accu2') (aux accu1 accu2' right) s  
550 551 552 553
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
554
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s
555

556 557 558 559
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 ->
560
          let accu1' = diff_t accu1 t1 in 
561
	  guard (slot accu1') (aux accu1' accu2 left) s;
562 563

          let accu2' = cap_t  accu2 t2 in 
564
	  guard (slot accu2') (aux accu1 accu2' left) s
565 566 567
      | [] -> set s
    in
    let accu1 = descr s1 in
568
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
569 570
  in
  big_conj single_right right s
571

572
and check_record (labels,(oleft,left),rights) s =
573 574
  let rec aux rights s = match rights with
    | [] -> set s
575
    | (oright,right)::rights ->
576
	let next =
577
	  (oleft && (not oright)) ||
578
	  exists (Array.length left)
579
	    (fun i -> trivially_disjoint left.(i) right.(i))
580 581 582 583 584 585
	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
586 587
	    guard (slot di) (fun s ->
			left.(i) <- di;
588 589 590
			aux rights s;
			left.(i) <- back;
		     ) s
591
(* TODO: are side effects correct ? *)
592 593 594 595 596
	  done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
597
      guard (slot left.(i)) (start (i - 1)) s
598 599 600 601 602 603 604
  in
  start (Array.length left - 1) s


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

611
(*
612
let is_empty d =
613 614 615 616 617 618 619
(*  let b1 = ClearlyEmpty.is_empty d in
  let b2 = is_empty d in
  assert (b2 || not b1);
  Printf.eprintf "b1 = %b; b2 = %b\n" b1 b2;
  b2  *)
  if ClearlyEmpty.is_empty d then (Printf.eprintf "!\n"; true) else is_empty d
*)  
620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639

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

640 641 642 643
  let normal_aux = function
    | ([] | [ _ ]) as d -> d
    | d ->

644 645 646 647 648 649 650
    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*) 
651
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675
	      
	      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


(* Partitioning:

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

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

702

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

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

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

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

724 725
  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
726
  let memo = ref Memo.empty
727
  let normal_times d = 
728 729 730
    try Memo.find d !memo 
    with
	Not_found ->
731
	  let gd = get_aux any d in
732
	  let n = normal_aux gd in
733 734
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
735 736
	  memo := Memo.add d n !memo;
	  n
737

738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753
  let memo_xml = ref Memo.empty
  let normal_xml d = 
    try Memo.find d !memo_xml
    with
	Not_found ->
	  let gd = get_aux any_pair d in
	  let n = normal_aux gd in
	  memo_xml := Memo.add d n !memo_xml;
	  n

  let normal ?(kind=`Normal) d =
    match kind with 
      | `Normal -> normal_times d.times 
      | `XML -> normal_xml d.xml


754 755 756 757 758 759 760 761 762 763
  let merge_same_2 r =
    let r = 
      List.fold_left 
	(fun accu (t1,t2) ->
	   let t = try DescrMap.find t2 accu with Not_found -> empty in
	   DescrMap.add t2 (cup t t1) accu
	) DescrMap.empty r in
    DescrMap.fold (fun t2 t1 accu -> (t1,t2)::accu) r []
	 

764 765 766 767 768 769 770
  let constraint_on_2 n t1 =
    List.fold_left 
      (fun accu (d1,d2) ->
	 if is_empty (cap d1 t1) then accu else cap accu d2)
      any
      n

771 772
  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
773
  let is_empty d = d == []
774
end
775

776
module Record = 
777
struct
778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862
  let has_record d = not (is_empty { empty with record = d.record })
  let or_absent d = { d with absent = true }
  let any_or_absent = or_absent any
  let has_absent d = d.absent

  let only_absent = {empty with absent = true}
  let only_absent_node = cons only_absent

  module T = struct
    type t = descr
    let any = any_or_absent
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module R = struct
    type t = descr
    let any = { empty with record = any.record }
    let cap = cap
    let cup = cup
    let diff = diff
    let is_empty = is_empty
    let empty = empty
  end
  module TR = Normal.Make(T)(R)

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

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

  type zor = Pair of descr * descr | Any

  let aux_split d l=
    let f (o,r) =
      try
	let (lt,rem) = LabelMap.assoc_remove l r in
	Pair (descr lt, atom o rem)
      with Not_found -> 
	if o then
	  if LabelMap.is_empty r then Any else
	    Pair (any_or_absent, { empty with record = BoolRec.atom (o,r) })
	else
	  Pair (only_absent,
		{ empty with record = BoolRec.atom (o,r) })
    in
    List.fold_left 
      (fun b (p,n) ->
	 let rec aux_p accu = function
	   | x::p -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_p ((t1,t2)::accu) p
		  | Any -> aux_p accu p)
	   | [] -> aux_n accu [] n
	 and aux_n p accu = function
	   | x::n -> 
	       (match f x with
		  | Pair (t1,t2) -> aux_n p ((t1,t2)::accu) n
		  | Any -> b)
	   | [] -> (p,accu) :: b in
	 aux_p [] p)
      []
      (BoolRec.get d.record)

  let split (d : descr) l =
    TR.boolean (aux_split d l)

  let split_normal d l =
    TR.boolean_normal (aux_split d l)


  let project d l =
    let t = TR.pi1 (split d l) in
    if t.absent then raise Not_found;
    t

  let project_opt d l =
    let t = TR.pi1 (split d l) in
    { t with absent = false }

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

864 865 866 867 868
(* TODO: eliminate this cap ... (reord l only_absent_node) when
   not necessary. eg. {| ..... |} \ l *)

  let remove_field d l = 
    cap (TR.pi2 (split d l)) (record l only_absent_node)
869

870 871 872 873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908 909 910 911 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942
  let first_label d =
    let min = ref LabelPool.dummy_max in
    let aux (_,r) = 
      match LabelMap.get r with
	  (l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
    BoolRec.iter aux d.record;
    !min

  let empty_cases d =
    let x = BoolRec.compute
	      ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
	      ~diff:(fun a b -> a land lnot b)
	      ~atom:(function (o,r) ->
		       assert (LabelMap.get r == []);
		       if o then 3 else 1
		    )
	      d.record in
    (x land 2 <> 0, x land 1 <> 0)

  let has_empty_record d =
    BoolRec.compute
      ~empty:false ~full:true ~cup:(||) ~cap:(&&)
      ~diff:(fun a b -> a && not b)
      ~atom:(function (o,r) ->
	       List.for_all 
	         (fun (l,t) -> (descr t).absent)
	         (LabelMap.get r)
	    )
      d.record
    

(*TODO: optimize merge
   - pre-compute the sequence of labels
   - remove empty or full { l = t }
*)

  let merge d1 d2 = 
    let res = ref empty in
    let rec aux accu d1 d2 =
      let l = min (first_label d1) (first_label d2) in
      if l = LabelPool.dummy_max then
	let (some1,none1) = empty_cases d1 
	and (some2,none2) = empty_cases d2 in
	let none = none1 && none2 and some = some1 || some2 in
	let accu = LabelMap.from_list (fun _ _ -> assert false) accu in
	(* approx for the case (some && not none) ... *)
	res := cup !res (record' (some, accu))
      else
	let l1 = split d1 l and l2 = split d2 l in
	let loop (t1,d1) (t2,d2) =
	  let t = 
	    if t2.absent 
	    then cup t1 { t2 with absent = false } 
	    else t2 
	  in
	  aux ((l,cons t)::accu) d1 d2
	in
	List.iter (fun x -> List.iter (loop x) l2) l1
	  
    in
    aux [] d1 d2;
    !res

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

  let get d =
    let rec aux r accu d =
      let l = first_label d in
      if l == LabelPool.dummy_max then
	let (o1,o2) = empty_cases d in 
	if o1 || o2 then (LabelMap.from_list_disj r,o1,o2)::accu else accu
      else
	List.fold_left 
943 944 945
	  (fun accu (t1,t2) -> 
	     let x = (t1.absent, { t1 with absent = false }) in
	     aux ((l,x)::r) accu t2)
946 947 948 949 950 951 952 953 954
	  accu
	  (split d l)
    in
    aux [] [] d
end


module Print = 
struct
955
  let print_const ppf = function
956 957 958
    | Integer i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
959

960
  let nil_atom = Atoms.mk_ascii "nil"
961 962 963 964 965 966 967 968 969
  let nil_type = atom (Atoms.atom nil_atom)
  let (seqs_node,seqs_descr) = 
    let n = make () in
    let d = cup nil_type (times any_node n) in
    define n d;
    (n, d)

  let is_regexp t = subtype t seqs_descr

970 971 972
  module S = struct
  type t = { id : int; 
	     mutable def : d list; 
973
	     mutable state : [ `Expand | `None | `Marked | `Named of U.t ] }
974
  and  d =
975
    | Name of U.t
976 977 978 979
    | Regexp of t Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of t * t
    | Char of Chars.v
980
    | Xml of [ `Tag of (Format.formatter -> unit) | `Type of t ] * t * t
981 982
    | Record of (bool * t) label_map * bool * bool
    | Arrows of (t * t) list * (t * t) list
983
    | Neg of t
984 985 986 987
  let compare x y = x.id - y.id
  end
  module Decompile = Pretty.Decompile(DescrHash)(S)
  open S
988 989 990 991 992 993 994 995 996 997 998 999

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

  let named = State.ref "Types.Print.named" DescrMap.empty
  let named_xml = State.ref "Types.Print.named_xml"  DescrPairMap.empty
1000
  let register_global (name : U.t) d = 
1001 1002 1003 1004 1005
    if equal_descr { d with xml = BoolPair.empty } empty then 
      (let l = (*Product.merge_same_2*) (Product.get ~kind:`XML d) in
      match l with
	| [(t1,t2)] -> named_xml := DescrPairMap.add (t1,t2) name !named_xml
	| _ -> ());
1006
    named := DescrMap.add d name !named
1007

1008
  let memo = DescrHash.create 63
1009 1010
  let counter = ref 0
  let alloc def = { id = (incr counter; !counter); def = def; state = `None }
1011

1012 1013 1014
  let count_name = ref 0
  let name () =
    incr count_name;
1015
    U.mk ("X" ^ (string_of_int !count_name))
1016

1017 1018
  let to_print = ref []

1019 1020 1021
  let trivial_rec b = 
    b == BoolRec.empty || 
    (is_empty { empty with record = BoolRec.diff BoolRec.full b})
1022

1023
  let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
1024 1025

  let worth_abbrev d = 
1026 1027
    not (trivial_pair d.times && trivial_pair d.xml && 
	 trivial_pair d.arrow && trivial_rec d.record) 
1028

1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039