viewcvs.cgi/types/types.ml

open Recursive
open Printf


let map_sort f l =
  SortedList.from_list (List.map f l)

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

module LabelPool = Pool.Make(SortedList.String)
module X = SortedList.Make(SortedList.Lift(LabelPool))

type label = LabelPool.t

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

type pair_kind = [ `Normal | `XML ]

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 

module BoolPair = Boolean.Make(NodePair)

type descr = {
  atoms : Atoms.t;
  ints  : Intervals.t;
  chars : Chars.t;
  times : descr BoolPair.t;
  xml   : descr BoolPair.t;
  arrow : descr BoolPair.t;
  record: (bool * (label, node) SortedMap.t) Boolean.t;
  absent: bool
} and node = descr node0

               
let empty = { 
  times = BoolPair.empty; 
  xml   = BoolPair.empty; 
  arrow = BoolPair.empty; 
  record= Boolean.empty;
  ints  = Intervals.empty;
  atoms = Atoms.empty;
  chars = Chars.empty;
  absent= false;
}
              
let any =  {
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
  record= Boolean.full; 
  ints  = Intervals.any;
  atoms = Atoms.any;
  chars = Chars.any;
  absent= false;
}
             
             
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 = Boolean.atom (true,[label,t]) }
let record' x =
  { empty with record = Boolean.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= Boolean.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= Boolean.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= Boolean.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 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

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 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
             
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 rec equal_rec_list l1 l2  =
  (l1 == l2) ||
  match (l1,l2) with
    | (o1,r1)::l1, (o2,r2)::l2 ->
        (o1 == o2) &&
        (equal_rec r1 r2) && (equal_rec_list l1 l2)
    | _ -> 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 =
  (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) &&
  (equal_rec_bool a.record b.record) &&
  (a.absent == b.absent)

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
  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 = compare_rec_bool 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 compare_descr a b =
  let c = compare_descr a b in
  assert (c = compare a b);
  c
*)


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
  | (l,x)::rem ->
      hash_rec (257 * accu + 17 * (LabelPool.hash l) + x.id) rem
  | [] -> accu + 5
      
let rec hash_rec_list accu = function
  | (o,r)::l ->
      hash_rec_list (hash_rec (if o then accu*3 else accu) r) l
  | [] -> 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 =
  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 = hash_rec_bool accu a.record in
  let accu = if a.absent then accu+5 else accu in
  accu

module DescrHash = 
  Hashtbl.Make(
    struct 
      type t = descr
      let hash = hash_descr
      let equal = equal_descr
    end
  )

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

let neg x = diff any x

let any_node = cons any

module LabelSet = Set.Make(LabelPool)

let get_record r =
  let labs accu (_,r) = 
    List.fold_left (fun accu (l,_) -> LabelSet.add l accu) accu 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 };
                  aux (i+1) labs r
    in
    aux 0 labs r;
    o
  in
  let line (p,n) =
    let labels = 
      List.fold_left labs (List.fold_left labs LabelSet.empty p) n in
    let labels = LabelSet.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 r
   

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

let check d =
  BoolPair.check d.times;
  BoolPair.check d.xml;
  BoolPair.check d.arrow;
  Boolean.check d.record;
  ()


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

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

let trivially_empty d = equal_descr d empty

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 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;
  raise NotEmpty

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


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

and 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_times (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 ->
        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;
          let accu2' = diff_t accu2 t2 in guard accu2' (aux accu1 accu2' right) s 
    | [] -> set s
  in
  let (accu1,accu2) = cap_product left in
  guard accu1 (guard 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 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

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)) || (* ggg... why ???  check this line *)
          exists (Array.length left)
            (fun i ->
               trivially_empty (cap 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 di (fun s ->
                        left.(i) <- diff back right.(i);
                        aux rights s;
                        left.(i) <- back;
                     ) s
          done
  in
  let rec start i s =
    if (i < 0) then aux rights s
    else
      guard 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
  

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

let rec empty_rec d =
  if not (Intervals.is_empty d.ints) then false
  else if not (Atoms.is_empty d.atoms) then false
  else if not (Chars.is_empty d.chars) then false
  else if d.absent then false
  else if DescrHash.mem cache_false d then false 
  else if Assumptions.mem d !memo then true
  else (
    let backup = !memo in
    memo := Assumptions.add d backup;
    if 
      (empty_rec_times (BoolPair.get d.times)) &&
      (empty_rec_times (BoolPair.get d.xml)) &&
      (empty_rec_arrow (BoolPair.get d.arrow)) &&
      (empty_rec_record d.record) 
    then true
    else (
      memo := backup;
      DescrHash.add cache_false d ();
      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 ->
        if trivially_empty (cap_t accu1 t1) || 
           trivially_empty (cap_t accu2 t2) then
          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
          if not (empty_rec accu2') then aux accu1 accu2' right
    | [] -> 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)


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
          if not (empty_rec accu1') then aux accu1' accu2 left;
          let accu2' = cap_t accu2 t2 in
          if not (empty_rec accu2') then aux accu1 accu2' left
      | [] -> 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

and empty_rec_record_aux (labels,(oleft,left),rights) =
  let rec aux = function
    | [] -> raise NotEmpty
    | (oright,right)::rights ->
        let next =
          (oleft && (not oright)) ||
          exists (Array.length left)
            (fun i ->
               trivially_empty (cap left.(i) right.(i)))
        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
            if not (empty_rec di) then (
              left.(i) <- diff back right.(i);
              aux rights;
              left.(i) <- back;
            )
          done
  in
  exists (Array.length left) 
    (fun i -> empty_rec left.(i))
  ||
  (try aux rights; true with NotEmpty -> false)
            

and empty_rec_record c =
  List.for_all empty_rec_record_aux (get_record c)

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

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

*)
  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
    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 d.times
      | `XML -> get_aux 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)


  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 ->
          let gd = get_aux 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 any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d = []
end

module Print = 
struct
  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
      | Some a -> Format.fprintf ppf "%s" (Atoms.value a)
      | None -> Format.fprintf ppf "(%a)" print_union (Atoms.print a)

  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 named = State.ref "Types.Printf.named" DescrMap.empty
  let register_global name d = 
    named := DescrMap.add d name !named

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

  let trivial b = b = Boolean.empty || b = Boolean.full
  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 d.record) 

  let rec mark n = mark_descr (descr n)
  and mark_descr d =
    if not (DescrMap.mem d !named) then
      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);
        BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.times;
        BoolPair.iter 
          (fun (n1,n2) -> mark n1; mark n2
(*
             List.iter
               (fun (d1,d2) ->
                  mark_descr d2;
                  bool_iter 
                    (fun (o,l) -> List.iter (fun (l,(o,n)) -> mark n) l) 
                    d1.record
                  let l = get_record d1.record in
                  List.iter (fun labs,(_,(_,p)),ns ->
                               Array.iter mark_descr p;
                               List.iter (fun (_,(_,n)) -> 
                                            Array.iter mark_descr n) ns
                            ) l
               )
               (Product.normal (descr n2))
*)
          ) d.xml;
        BoolPair.iter (fun (n1,n2) -> mark n1; mark n2) d.arrow;
        Boolean.iter (fun (o,l) -> List.iter (fun (l,n) -> mark n) l) d.record

    
  let rec print ppf n = print_descr ppf (descr n)
  and print_descr ppf d = 
    try 
      let name = DescrMap.find d !named in
      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
          Not_found -> assert false
  and real_print_descr ppf d = 
    if d = any then Format.fprintf ppf "Any" else
      (
        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 @
           Boolean.print "Record" print_record d.record
          )
      )
  and print_times ppf (t1,t2) =
    Format.fprintf ppf "@[(%a,%a)@]" print t1 print t2
  and print_xml ppf (t1,t2) =
    Format.fprintf ppf "@[XML(%a,%a)@]" print t1 print t2
(*
    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
*)
  and print_arrow ppf (t1,t2) =
    Format.fprintf ppf "@[(%a -> %a)@]" print t1 print t2
  and print_record ppf (o,r) =
    let o = if o then "" else "|" in
    Format.fprintf ppf "@[{%s" o;
    let first = ref true in
    List.iter (fun (l,t) ->
                 let sep = if !first then (first := false; "") else ";" in
                 Format.fprintf ppf "%s@ @[%s =@] %a" sep
                   (LabelPool.value l) print t
              ) r;
    Format.fprintf ppf " %s}@]" o
(*
  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
*)

          
  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

let () = print_descr := Print.print_descr

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 }


  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)

  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

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

  let solve v = internalize (make_node v)
end


(* Sample value *)
module Sample =
struct


let rec find f = function
  | [] -> raise Not_found
  | x::r -> try f x with Not_found -> find f r

type t =
  | Int of Intervals.v
  | Atom of Atoms.v
  | Char of Chars.v
  | Pair of (t * t)
  | Xml of (t * t)
  | Record of (label * t) list
  | Fun of (node * node) list
  | Other
  exception FoundSampleRecord of (label * t) list

let rec sample_rec memo d =
  if (Assumptions.mem d memo) || (is_empty d) then raise Not_found 
  else 
    try Int (Intervals.sample d.ints) with Not_found ->
    try Atom (Atoms.sample d.atoms) with 
        Not_found ->
(* Here: could create a fresh atom ... *)
    try Char (Chars.sample d.chars) with Not_found ->
    try sample_rec_arrow (BoolPair.get d.arrow) with Not_found ->

    let memo = Assumptions.add d memo in
    try Pair (sample_rec_times memo (BoolPair.get d.times)) with Not_found ->
    try Xml (sample_rec_times memo (BoolPair.get d.xml)) with Not_found ->
    try sample_rec_record memo d.record with Not_found -> 
    raise Not_found


and sample_rec_times memo c = 
  find (sample_rec_times_aux memo) c

and sample_rec_times_aux memo (left,right) =
  let rec aux accu1 accu2 = function
    | (t1,t2)::right ->
(*TODO: check: is this correct ?  non_empty could return true
  but because of coinduction, the call to aux may raise Not_found, no ? *)
        let accu1' = diff_t accu1 t1 in
        if non_empty accu1' then aux accu1' accu2 right else
          let accu2' = diff_t accu2 t2 in
          if non_empty accu2' then aux accu1 accu2' right else
            raise Not_found
    | [] -> (sample_rec memo accu1, sample_rec memo accu2)
  in
  let (accu1,accu2) = cap_product left in
  if (is_empty accu1) || (is_empty accu2) then raise Not_found;
  aux accu1 accu2 right

and sample_rec_arrow c =
  find sample_rec_arrow_aux c

and check_empty_simple_arrow_line left (s1,s2) = 
  let rec aux accu1 accu2 = function
    | (t1,t2)::left ->
        let accu1' = diff_t accu1 t1 in
        if non_empty accu1' then aux accu1 accu2 left;
        let accu2' = cap_t accu2 t2 in
        if non_empty accu2' then aux accu1 accu2 left
    | [] -> raise NotEmpty
  in
  let accu1 = descr s1 in
  (is_empty accu1) ||
  (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)

and check_empty_arrow_line left right = 
  List.exists (check_empty_simple_arrow_line left) right

and sample_rec_arrow_aux (left,right) =
  if (check_empty_arrow_line left right) then raise Not_found
  else Fun left


and sample_rec_record memo c =
  Record (find (sample_rec_record_aux memo) (get_record c))

and sample_rec_record_aux memo (labels,(oleft,left),rights) =
  let rec aux = function
    | [] -> 
        let l = ref labels and fields = ref [] in
        for i = 0 to Array.length left - 1 do
          fields := (List.hd !l, sample_rec memo left.(i))::!fields;
          l := List.tl !l
        done;
        raise (FoundSampleRecord (List.rev !fields))
    | (oright,right)::rights ->
        let next = (oleft && (not oright)) 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
            if not (is_empty di) then (
              left.(i) <- diff back right.(i);
              aux rights;
              left.(i) <- back;
            )
          done
  in
  if exists (Array.length left) 
    (fun i -> is_empty left.(i)) then raise Not_found;
  try aux rights; raise Not_found
  with FoundSampleRecord r -> r

            
let get x = try sample_rec Assumptions.empty x with Not_found -> Other

  let rec print_sep f sep ppf = function
    | [] -> ()
    | [x] -> f ppf x
    | x::rem -> f ppf x; Format.fprintf ppf "%s" sep; print_sep f sep ppf rem


  let rec print ppf = function
    | Int i -> Intervals.print_v ppf i
    | Atom a -> Atoms.print_v ppf a
    | Char c -> Chars.print_v ppf c
    | Pair (x1,x2) -> Format.fprintf ppf "(%a,%a)" print x1 print x2
    | Xml (x1,x2) -> Format.fprintf ppf "XML(%a,%a)" print x1 print x2
    | Record r ->
        Format.fprintf ppf "{ %a }"
          (print_sep 
             (fun ppf (l,x) -> 
                Format.fprintf ppf "%s = %a"
                (LabelPool.value l)
                print x
             )
             " ; "
          ) r
    | Fun iface ->
        Format.fprintf ppf "(fun ( %a ) x -> ...)"
          (print_sep
             (fun ppf (t1,t2) ->
                Format.fprintf ppf "%a -> %a; "
                Print.print t1 Print.print t2
             )
             " ; "
          ) iface
    | Other ->
        Format.fprintf ppf "[cannot determine value]"
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

  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 atom = function
    | (true,[]) -> { empty with record = Boolean.full }
    | (o,l) -> { empty with record = Boolean.atom (o,l) }

  let aux d l=
    Boolean.compute_bool
      (fun ((o,r) as x) ->
         try
           let lt = List.assoc l r in
           Boolean.atom (descr lt, atom (o, SortedMap.diff r [l]))
         with Not_found -> 
           if o then Boolean.atom (or_absent any, atom x) 
           else Boolean.empty
      )
      d.record

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

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


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

  let first_label d =
    let min = ref LabelPool.dummy_max in
    let aux = 
      function _,(l,_)::_ -> if (l:int) < !min then min := l | _ -> () in
    Boolean.iter aux d.record;
    !min

  let empty_cases d =
    let x = Boolean.compute
              ~empty:0 ~full:3 ~cup:(lor) ~cap:(land)
              ~diff:(fun a b -> a land lnot b)
              ~atom:(function (true,[]) -> 3 | (false,[]) -> 1 
                       | _ -> assert false) d.record in
    (x land 2 <> 0, x land 1 <> 0)
    

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


let memo_normalize = ref DescrMap.empty


let rec rec_normalize d =
  try DescrMap.find d !memo_normalize
  with Not_found ->
    let n = make () in
    memo_normalize := DescrMap.add d n !memo_normalize;
    let times = 
      List.fold_left 
        (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
        BoolPair.empty (Product.normal d)
    in
    let xml = 
      List.fold_left 
        (fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (rec_normalize d1, rec_normalize d2)))
        BoolPair.empty (Product.normal ~kind:`XML d)
    in
    let record = d.record
(*
      map_sort
        (fun f -> map_sort (fun (l,(o,d)) -> (l,o,rec_normalize d)) f, [])
        (Record.get d)
*)
    in
    define n { d with times = times; xml = xml; record = record };
    n

let normalize n =
  descr (internalize (rec_normalize n))

module Arrow =
struct
  let check_simple left s1 s2 =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
          if non_empty accu1' then aux accu1 accu2 left;
          let accu2' = cap_t accu2 t2 in
          if non_empty accu2' then aux accu1 accu2 left
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (is_empty accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)
      
  let check_strenghten t s =
    let left = match (BoolPair.get t.arrow) with [ (p,[]) ] -> p | _ -> assert false in
    let rec aux = function
      | [] -> raise Not_found
      | (p,n) :: rem ->
          if (List.for_all (fun (a,b) -> check_simple left a b) p) &&
            (List.for_all (fun (a,b) -> not (check_simple left a b)) n) then
              { empty with arrow = Obj.magic [ (SortedList.cup left p, n) ] }  (* rework this ! *)
          else aux rem
    in
    aux (BoolPair.get s.arrow)

  let check_simple_iface left s1 s2 =
    let rec aux accu1 accu2 = function
      | (t1,t2)::left ->
          let accu1' = diff accu1 t1 in
          if non_empty accu1' then aux accu1 accu2 left;
          let accu2' = cap accu2 t2 in
          if non_empty accu2' then aux accu1 accu2 left
      | [] -> raise NotEmpty
    in
    let accu1 = descr s1 in
    (is_empty accu1) ||
    (try aux accu1 (diff any (descr s2)) left; true with NotEmpty -> false)

  let check_iface iface s =
    let rec aux = function
      | [] -> false
      | (p,n) :: rem ->
          ((List.for_all (fun (a,b) -> check_simple_iface iface a b) p) &&
           (List.for_all (fun (a,b) -> not (check_simple_iface iface a b)) n))
          || (aux rem)
    in
    aux (BoolPair.get s.arrow)

  type t = descr * (descr * descr) list list

  let get t =
    List.fold_left
      (fun ((dom,arr) as accu) (left,right) ->
         if Sample.check_empty_arrow_line left right 
         then accu
         else (
           let left =
             List.map 
               (fun (t,s) -> (descr t, descr s)) left in
           let d = List.fold_left (fun d (t,_) -> cup d t) empty left in
           (cap dom d, left :: arr)
         )
      )
      (any, [])
      (BoolPair.get t.arrow)

  let domain (dom,_) = dom

  let apply_simple t result left = 
    let rec aux result accu1 accu2 = function
      | (t1,s1)::left ->
          let result = 
            let accu1 = diff accu1 t1 in
            if non_empty accu1 then aux result accu1 accu2 left
            else result in
          let result =
            let accu2 = cap accu2 s1 in
            aux result accu1 accu2 left in
          result
      | [] -> 
          if subtype accu2 result 
          then result
          else cup result accu2
    in
    aux result t any left
      
  let apply (_,arr) t =
    List.fold_left (apply_simple t) empty arr

  let need_arg (dom, arr) =
    List.exists (function [_] -> false | _ -> true) arr

  let apply_noarg (_,arr) =
    List.fold_left 
      (fun accu -> 
         function 
           | [(t,s)] -> cup accu s
           | _ -> assert false
      )
      empty arr

  let any = { empty with arrow = any.arrow }
  let is_empty (_,arr) = arr = []
end
  

module Int = struct
  let has_int d i = Intervals.contains i d.ints

  let get d = d.ints
  let put i = { empty with ints = i }
  let is_int d = is_empty { d with ints = Intervals.empty }
  let any = { empty with ints = Intervals.any }
end

module Atom = struct
  let has_atom d a = Atoms.contains a d.atoms
end

module Char = struct
  let has_char d c = Chars.contains c d.chars
  let any = { empty with chars = Chars.any }
end

let print_stat ppf =
(*  Format.fprintf ppf "nb_rec = %i@." !nb_rec;
  Format.fprintf ppf "nb_norec = %i@." !nb_norec;
*)
  ()

(*
let rec print_normal_record ppf = function
  | Success -> Format.fprintf ppf "Yes"
  | Fail -> Format.fprintf ppf "No"
  | FirstLabel (l,present,absent) ->
      Format.fprintf ppf "%s?@[<v>@\n" (label_name l);
      List.iter
        (fun (t,n) ->
           Format.fprintf ppf "(%a)=>@[%a@]@\n" 
             Print.print_descr t
             print_normal_record n
        ) present;
      if absent <> Fail then
        Format.fprintf ppf "(absent)=>@[%a@]@\n" print_normal_record absent;
      Format.fprintf ppf "@]" 
*)


(* 
let pr s = Types.Print.print Format.std_formatter (Syntax.make_type (Syntax.parse s));;

let pr' s = Types.Print.print Format.std_formatter 
   (Types.normalize (Syntax.make_type (Syntax.parse s)));;

BUG:
pr "'a | 'b where 'a = ('a , 'a) and 'b= ('b , 'b)";;
*)


(*
  let nr s =
    let t = Types.descr (Syntax.make_type (Syntax.parse s)) in
    let n = Types.normal_record' t.Types.record in
    Types.print_normal_record Format.std_formatter n;;
*)