types.ml

open Ident
open Encodings

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


module HashedString = 
struct 
  type t = string 
  let hash = Hashtbl.hash
  let equal = (=)
end


type const = 
  | Integer of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v

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

let equal_const c1 c2 = compare_const c1 c2 = 0

type pair_kind = [ `Normal | `XML ]

type 'a node0 = { id : int; mutable descr : 'a }

module NodePair = struct
  type 'a t = 'a node0 * 'a node0
  let dump ppf (x,y) =
    Format.fprintf ppf "(%i,%i)" x.id y.id
  let compare (y1,x1) (y2,x2) =
    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 

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

  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

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

type descr = {
  atoms : Atoms.t;
  ints  : Intervals.t;
  chars : Chars.t;
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
  record: descr BoolRec.t;
  absent: bool
} and node = descr node0

	       
let empty = { 
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
  record= BoolRec.empty;
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
  absent= false;
}
	      
let any =  {
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
  record= BoolRec.full; 
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
  absent= false;
}

let non_constructed =
  { any with times = empty.times; xml = empty.xml; record = empty.record }
     
	     
let interval i = { empty with ints = i }
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) }
let record label t = 
  { empty with record = BoolRec.atom (true,LabelMap.singleton label t) }
let record' (x : bool * node Ident.label_map) =
  { empty with record = BoolRec.atom x }
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)
      
let cup x y = 
  if x == y then x else {
    times = BoolPair.cup x.times y.times;
    xml   = BoolPair.cup x.xml y.xml;
    arrow = BoolPair.cup x.arrow y.arrow;
    record= BoolRec.cup x.record y.record;
    ints  = Intervals.cup x.ints  y.ints;
    atoms = Atoms.cup x.atoms y.atoms;
    chars = Chars.cup x.chars y.chars;
    absent= x.absent || y.absent;
  }
    
let cap x y = 
  if x == y then x else {
    times = BoolPair.cap x.times y.times;
    xml   = BoolPair.cap x.xml y.xml;
    record= BoolRec.cap x.record y.record;
    arrow = BoolPair.cap x.arrow y.arrow;
    ints  = Intervals.cap x.ints  y.ints;
    atoms = Atoms.cap x.atoms y.atoms;
    chars = Chars.cap x.chars y.chars;
    absent= x.absent && y.absent;
  }
    
let diff x y = 
  if x == y then empty else {
    times = BoolPair.diff x.times y.times;
    xml   = BoolPair.diff x.xml y.xml;
    arrow = BoolPair.diff x.arrow y.arrow;
    record= BoolRec.diff x.record y.record;
    ints  = Intervals.diff x.ints  y.ints;
    atoms = Atoms.diff x.atoms y.atoms;
    chars = Chars.diff x.chars y.chars;
    absent= x.absent && not y.absent;
  }
    

let equal_descr a b =
  (Atoms.equal a.atoms b.atoms) &&
  (Chars.equal a.chars b.chars) &&
  (Intervals.equal a.ints  b.ints) &&
  (BoolPair.equal a.times b.times) &&
  (BoolPair.equal a.xml b.xml) &&
  (BoolPair.equal a.arrow b.arrow) &&
  (BoolRec.equal a.record b.record) &&
  (a.absent == b.absent)

let compare_descr a b =
  if a == b then 0 
  else let c = Atoms.compare a.atoms b.atoms in if c <> 0 then c
  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
  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
  else let c = BoolRec.compare a.record b.record in if c <> 0 then c
  else if a.absent && not b.absent then -1
  else if b.absent && not a.absent then 1
  else 0

let hash_descr a =
  let accu = Chars.hash 1 a.chars in
  let accu = Intervals.hash accu a.ints in
  let accu = Atoms.hash accu a.atoms in
  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
  let accu = 17 * accu + BoolRec.hash a.record in
  let accu = if a.absent then accu+5 else accu in
  accu

(* 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) &&
  (BoolRec.trivially_disjoint a.record b.record) &&
  (not (a.absent && b.absent))


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 DescrSet = Set.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)

(* let hash_cons = DescrHash.create 17000 *)

let count = State.ref "Types.count" 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




let neg x = diff any x

let any_node = cons any

module LabelS = Set.Make(LabelPool)

let get_record r =
  let labs accu (_,r) = 
    List.fold_left 
      (fun accu (l,_) -> LabelS.add l accu) accu (LabelMap.get r) in
  let extend descrs labs (o,r) =
    let rec aux i labs r =
      match labs with
	| [] -> ()
	| l1::labs ->
	    match r with
	      | (l2,x)::r when l1 == l2 -> 
		  descrs.(i) <- cap descrs.(i) (descr x);
		  aux (i+1) labs r
	      | r ->
		  if not o then descrs.(i) <- 
		    cap descrs.(i) { empty with absent = true }; (* TODO:OPT *)
		  aux (i+1) labs r
    in
    aux 0 labs (LabelMap.get r);
    o
  in
  let line (p,n) =
    let labels = 
      List.fold_left labs (List.fold_left labs LabelS.empty p) n in
    let labels = LabelS.elements labels in
    let nlab = List.length labels in
    let mk () = Array.create nlab { any with absent = true } in

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




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


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

exception NotEmpty

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) -> 
      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;
  s.notify <- Nothing; 
  raise NotEmpty

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

let guard a f n =
  match a with
    | { status = Empty } -> ()
    | { status = Maybe } as s -> 
	n.active <- true; 
	s.notify <- Do (n,f,s.notify)
    | { status = NEmpty } -> f n


(* 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 =
  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 rec aux accu1 accu2 right s = match right with
    | (t1,t2)::right ->
	let t1 = descr t1 and t2 = descr t2 in
	if trivially_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
	  guard (slot accu1') (aux accu1' accu2 right) s;

          let accu2' = diff accu2 t2 in 
	  guard (slot accu2') (aux accu1 accu2' right) s  
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any left in
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s

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
	if clearly_disjoint accu1 t1 || 
	   trivially_disjoint accu2 t2 then (
	     aux accu1 accu2 right s )
	else (
          let accu1' = diff accu1 t1 in 
	  guard (slot accu1') (aux accu1' accu2 right) s;

          let accu2' = diff accu2 t2 in 
	  guard (slot accu2') (aux accu1 accu2' right) s  
	)
    | [] -> set s
  in
  let (accu1,accu2) = cap_product any any_pair left in
  guard (slot accu1) (guard (slot accu2) (aux accu1 accu2 right)) s

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 (slot accu1') (aux accu1' accu2 left) s;

          let accu2' = cap_t  accu2 t2 in 
	  guard (slot accu2') (aux accu1 accu2' left) s
      | [] -> set s
    in
    let accu1 = descr s1 in
    guard (slot accu1) (aux accu1 (neg (descr s2)) left) s
  in
  big_conj single_right right s

and check_record (labels,(oleft,left),rights) s =
  let rec aux rights s = match rights with
    | [] -> set s
    | (oright,right)::rights ->
	let next =
	  (oleft && (not oright)) ||
	  exists (Array.length left)
	    (fun i -> trivially_disjoint left.(i) right.(i))
	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
	    guard (slot di) (fun s ->
			left.(i) <- di;
			aux rights s;
			left.(i) <- back;
		     ) s
(* TODO: are side effects correct ? *)
	  done
  in
  let rec start i s =
    if (i < 0) then aux 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

(*
let is_empty d =
(*  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
*)  

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 = function
    | ([] | [ _ ]) as d -> d
    | 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*) 
(*	    if equal_descr d1 t1 then r := (d1,cup d2 t2) else*)
	      
	      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)

*)
  let get_aux any_right d =
    let accu = ref [] in
    let line (left,right) =
      let (d1,d2) = cap_product any any_right 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
    List.iter line (BoolPair.get d);
    !accu
(* Maybe, can improve this function with:
     (t,s) \ (t1,s1) = (t&t',s\s') | (t\t',s),
   don't call normal_aux *)


  let get ?(kind=`Normal) d = 
    match kind with
      | `Normal -> get_aux any d.times
      | `XML -> get_aux any_pair d.xml

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

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

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

  (* TODO: try with an hashtable *)
  (* Also, avoid lookup for simple products (t1,t2) *)
  let memo = ref Memo.empty
  let normal_times d = 
    try Memo.find d !memo 
    with
	Not_found ->
	  let gd = get_aux any d in
	  let n = normal_aux gd in
(* Could optimize this call to normal_aux because one already
   know that each line is normalized ... *)
	  memo := Memo.add d n !memo;
	  n

  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


  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 []
	 

  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

  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d == []
end

module Record = 
struct
  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)

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

  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 
	  (fun accu (t1,t2) -> 
	     let x = (t1.absent, { t1 with absent = false }) in
	     aux ((l,x)::r) accu t2)
	  accu
	  (split d l)
    in
    aux [] [] d
end


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

  let nil_atom = Atoms.mk_ascii "nil"
  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

  module S = struct
  type t = { id : int; 
	     mutable def : d list; 
	     mutable state : [ `Expand | `None | `Marked | `Named of U.t ] }
  and  d =
    | Name of U.t
    | Regexp of t Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of t * t
    | Char of Chars.v
    | Xml of [ `Tag of (Format.formatter -> unit) | `Type of t ] * t * t
    | Record of (bool * t) label_map * bool * bool
    | Arrows of (t * t) list * (t * t) list
    | Neg of t
  let compare x y = x.id - y.id
  end
  module Decompile = Pretty.Decompile(DescrHash)(S)
  open S

  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
  let register_global (name : U.t) d = 
    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
	| _ -> ());
    named := DescrMap.add d name !named

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

  let count_name = ref 0
  let name () =
    incr count_name;
    U.mk ("X" ^ (string_of_int !count_name))

  let to_print = ref []

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

  let trivial_pair b = b == BoolPair.empty || b == BoolPair.full

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

  let worth_complement d =
    let aux f x y = if f x y = 0 then 1 else 0 in
    let n = 
      aux Atoms.compare d.atoms any.atoms +
      aux Chars.compare d.chars any.chars +
      aux Intervals.compare d.ints any.ints +
      aux BoolPair.compare d.times any.times +
      aux BoolPair.compare d.xml any.xml +
      aux BoolPair.compare d.arrow any.arrow +
      aux BoolRec.compare d.record any.record in
    n >= 4

  let rec prepare d =
    try DescrHash.find memo d
    with Not_found ->
      try 
	let n = DescrMap.find d !named in
	let s = alloc [] in
	s.state <- `Named n;
	DescrHash.add memo d s;
	s
      with Not_found ->
	if worth_complement d then 
	  alloc [Neg (prepare (neg d))]
	else
	let slot = alloc [] in
	if not (worth_abbrev d) then slot.state <- `Expand;
	DescrHash.add memo d slot;
	let (seq,not_seq) =
	  if (subtype { empty with times = d.times } seqs_descr) then
	    (cap d seqs_descr, diff d seqs_descr)
	  else
	    (empty, d) in

	let add u = slot.def <- u :: slot.def in
	if (non_empty seq) then
	  add (Regexp (decompile seq));  
	List.iter
	  (fun (t1,t2) -> add (Pair (prepare t1, prepare t2)))
	  (Product.get not_seq);
	List.iter
	  (fun (t1,t2) ->
	     try 
	       let n = DescrPairMap.find (t1,t2) !named_xml in
	       add (Name n)
	     with
		 Not_found ->
	     let tag = 
	       match Atoms.print_tag t1.atoms with
		 | Some a when is_empty { t1 with atoms = Atoms.empty } -> `Tag a
		 | _ -> `Type (prepare t1) in
	     assert (equal_descr { t2 with times = empty.times } empty);
	     List.iter
	       (fun (ta,tb) -> add (Xml (tag, prepare ta, prepare tb)))
	       (Product.get t2)
	  )
	  ((*Product.merge_same_2*) (Product.get ~kind:`XML not_seq));
	List.iter
	  (fun (r,some,none) -> 
	     let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
	     add (Record (r,some,none)))
	  (Record.get not_seq);
	(match Chars.is_char not_seq.chars with
	  | Some c -> add (Char c)
	  | None ->
	      List.iter (fun x -> add (Atomic x)) (Chars.print not_seq.chars));
	List.iter (fun x -> add (Atomic x)) (Intervals.print not_seq.ints);
	List.iter (fun x -> add (Atomic x)) (Atoms.print not_seq.atoms);
	List.iter
	  (fun (p,n) ->
	     let aux (t,s) = prepare (descr t), prepare (descr s) in
	     let p = List.map aux p and n = List.map aux n in
	     add (Arrows (p,n)))
	  (BoolPair.get not_seq.arrow);
	slot.def <- List.rev slot.def;
	slot
	

  and decompile d =
    Decompile.decompile 
      (fun t -> 
	 let tr = Product.get t in
	 let tr = List.map (fun (l,t) -> prepare l, t) tr in
	 tr, Atoms.contains nil_atom t.atoms)
      d

  let gen = ref 0

  let rec assign_name s =
    incr gen;
    match s.state with
      | `None ->  
	  let g = !gen in
	  s.state <- `Marked; 
	  List.iter assign_name_rec s.def;
	  if (s.state == `Marked) && (!gen == g) then s.state <- `None
      | `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print
      | _ -> ()
  and assign_name_rec = function
    | Neg t -> assign_name t
    | Name _ | Char _ | Atomic _ -> ()
    | Regexp r -> assign_name_regexp r
    | Pair (t1,t2) -> assign_name t1; assign_name t2
    | Xml (tag,t2,t3) -> 
	(match tag with `Type t -> assign_name t | _ -> ());
	assign_name t2;
	assign_name t3
    | Record (r,_,_) ->
	List.iter (fun (_,(_,t)) -> assign_name t) (LabelMap.get r)
    | Arrows (p,n) ->
	List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) p;
	List.iter (fun (t1,t2) -> assign_name t1; assign_name t2) n
  and assign_name_regexp = function
    | Pretty.Epsilon | Pretty.Empty -> ()
    | Pretty.Alt (r1,r2) 
    | Pretty.Seq (r1,r2) -> assign_name_regexp r1; assign_name_regexp r2
    | Pretty.Star r | Pretty.Plus r -> assign_name_regexp r
    | Pretty.Trans t -> assign_name t

  let rec do_print_slot pri ppf s =
    match s.state with
      | `Named n -> Format.fprintf ppf "%a" U.print n
      | _ -> do_print_slot_real pri ppf s.def
  and do_print_slot_real pri ppf def =
    let rec aux ppf = function
      | [] -> Format.fprintf ppf "Empty"
      | [ h ] -> do_print ppf h
      | h :: t -> Format.fprintf ppf "%a |@ %a" do_print h aux t
    in
    if (pri >= 2) && (List.length def >= 2) 
    then Format.fprintf ppf "@[(%a)@]" aux def
    else aux ppf def
  and do_print ppf = function
    | Neg t -> Format.fprintf ppf "Any \\ (@[%a@])" (do_print_slot 0) t
    | Name n -> Format.fprintf ppf "%a" U.print n
    | Char c -> Chars.print_v ppf c
    | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp 0) r
    | Atomic a -> a ppf
    | Pair (t1,t2) -> 
	Format.fprintf ppf "@[(%a,%a)@]" 
	  (do_print_slot 0) t1 
	  (do_print_slot 0) t2
    | Xml (tag,attr,t) -> 
	Format.fprintf ppf "<%a%a>%a" 
	  do_print_tag tag
	  do_print_attr attr
	  (do_print_slot 0) t
    | Record (r,some,none) ->
	if some then Format.fprintf ppf "@[{"
	else Format.fprintf ppf "@[{|";
	do_print_record ppf r;
	if not none then  Format.fprintf ppf ";@ ...";
	if some then Format.fprintf ppf " }@]"
	else Format.fprintf ppf " |}@]"
    | Arrows (p,n) ->
	(match p with
	   | [] -> Format.fprintf ppf "Arrow"
	   | (t,s)::l ->
	       Format.fprintf ppf "%a" do_print_arrow (t,s);
	       List.iter 
		 (fun (t,s) ->
		    Format.fprintf ppf " &@ %a" do_print_arrow (t,s)
		 ) l);
	List.iter 
	  (fun (t,s) ->
	     Format.fprintf ppf " \\@ %a" do_print_arrow (t,s)
	  ) n
  and do_print_arrow ppf (t,s) =
    Format.fprintf ppf "%a -> %a"
      (do_print_slot 0) t
      (do_print_slot 0) s
  and do_print_tag ppf = function
    | `Tag s -> s ppf
    | `Type t -> Format.fprintf ppf "(%a)" (do_print_slot 0) t
  and do_print_attr ppf = function
    | { state = `Marked|`Expand; 
	def = [ Record (r,true,true) ] } -> do_print_record ppf r