open Ident
open Encodings

let (@@) f a = f a

let count = ref 0

let () =
  Stats.register Stats.Summary
    (fun ppf -> Format.fprintf ppf "Allocated type nodes:%i@\n" !count)

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

type const =
  | Integer of Intervals.V.t
  | Atom of Atoms.V.t
  | Char of Chars.V.t
  | Pair of const * const
  | Xml of const * const
  | Record of const label_map
  | String of U.uindex * U.uindex * U.t * const

type service_params =
  | TProd of service_params * service_params
  | TOption of service_params
  | TList of string * service_params
  | TSet of service_params
  | TSum of service_params * service_params
  | TString of string
  | TInt of string
  | TInt32 of string
  | TInt64 of string
  | TFloat of string
  | TBool of string
  | TFile of string
      (* | TUserType of string * (string -> 'a) * ('a -> string) *)
  | TCoord of string
  | TCoordv of service_params * string
  | TESuffix of string
  | TESuffixs of string
      (*  | TESuffixu of (string * (string -> 'a) * ('a -> string)) *)
  | TSuffix of (bool * service_params)
  | TUnit
  | TAny
  | TConst of string;;

module Const = struct
  type t = const

  let check _ = ()
  let dump ppf _ = Format.fprintf ppf "<Types.Const.t>"

  let rec compare c1 c2 = match (c1,c2) with
    | Integer x, Integer y -> Intervals.V.compare x y
    | Integer _, _ -> -1
    | _, Integer _ -> 1
    | Atom x, Atom y -> Atoms.V.compare x y
    | Atom _, _ -> -1
    | _, Atom _ -> 1

    | Char x, Char y -> Chars.V.compare x y
    | Char _, _ -> -1
    | _, Char _ -> 1
    | Pair (x1,x2), Pair (y1,y2) ->
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
    | Pair (_,_), _ -> -1
    | _, Pair (_,_) -> 1
    | Xml (x1,x2), Xml (y1,y2) ->
	let c = compare x1 y1 in
	if c <> 0 then c else compare x2 y2
    | Xml (_,_), _ -> -1
    | _, Xml (_,_) -> 1
    | Record x, Record y ->
	LabelMap.compare compare x y
    | Record _, _ -> -1
    | _, Record _ -> 1
    | String (i1,j1,s1,r1), String (i2,j2,s2,r2) ->
	let c = Pervasives.compare i1 i2 in if c <> 0 then c
	else let c = Pervasives.compare j1 j2 in if c <> 0 then c
	else let c = U.compare s1 s2 in if c <> 0 then c (* Should compare
							    only the substring *)
	else compare r1 r2

  let rec hash = function
    | Integer x -> 1 + 17 * (Intervals.V.hash x)
    | Atom x -> 2 + 17 * (Atoms.V.hash x)
    | Char x -> 3 + 17 * (Chars.V.hash x)
    | Pair (x,y) -> 4 + 17 * (hash x) + 257 * (hash y)
    | Xml (x,y) -> 5 + 17 * (hash x) + 257 * (hash y)
    | Record x -> 6 + 17 * (LabelMap.hash hash x)
    | String (i,j,s,r) -> 7 + 17 * (U.hash s) + 257 * hash r
      (* Note: improve hash for String *)

  let equal c1 c2 = compare c1 c2 = 0
end

module Abstracts = struct
  module T = Custom.String
  type abs = T.t

  module V = struct type t = abs * Obj.t end

  include SortedList.FiniteCofinite(T)
  let full = any

  let print = function
    | Finite l -> List.map (fun x ppf -> Format.fprintf ppf "!%s" x) l
    | Cofinite l ->
	[ fun ppf ->
	  Format.fprintf ppf "@[Abstract";
	  List.iter (fun x -> Format.fprintf ppf " \\@ !%s" x) l;
	  Format.fprintf ppf "@]" ]

  let contains_sample s t = match s,t with
    | None, Cofinite _ -> true
    | None, Finite _ -> false
    | Some s, t -> contains s t

end

type pair_kind = [ `Normal | `XML ]

module BoolAtoms : BoolVar.S with
  type s = Atoms.t = BoolVar.Make(Atoms)
module BoolIntervals : BoolVar.S with
  type s = Intervals.t = BoolVar.Make(Intervals)
module BoolChars : BoolVar.S with
  type s = Chars.t = BoolVar.Make(Chars)
module BoolAbstracts : BoolVar.S with
  type s = Abstracts.t = BoolVar.Make(Abstracts)

(* module TLV = struct *)

(*   module Set = struct *)
(*     include Set.Make( *)
(*       struct *)
(*         type t = (Var.var * bool) *)
(*         let compare (v1,p1) (v2,p2) = *)
(*           let c = Var.compare v1 v2 in *)
(*           if c == 0 then *)
(*             if p1 == p2 then 0 *)
(*             else if p1 then 1 else -1 *)
(*           else c *)
(*       end) *)
(*     let pp_aux ppf pp_elem s = *)
(*       let f ppf = function *)
(*         |(v,true) -> Format.fprintf ppf "%a" pp_elem v *)
(*         |(v,false) -> Format.fprintf ppf "~ %a" pp_elem v *)
(*       in *)
(*       Utils.pp_list ~sep:";" ~delim:("{","}") f ppf (elements s) *)
(*     let dump ppf s = pp_aux ppf Var.dump s *)
(*     let pp ppf s = pp_aux ppf Var.pp s *)

(*     let printf = pp Format.std_formatter *)
(*   end *)

(*   (\* tlv : top level variables *)
(*    * fv : all free variables in the subtree *\) *)
(*   type t =  { tlv : Set.t ; fv : Var.Set.t; isvar : bool } *)

(*   let empty = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)
(*   let any = { tlv = Set.empty ; fv = Var.Set.empty; isvar = false } *)

(*   let singleton (v,p) = { tlv = Set.singleton (v,p); fv = Var.Set.singleton v; isvar = true } *)

(*   (\* return the max of top level variables *\) *)
(*   let max x = Set.max_elt x.tlv *)

(*   let pair x y = { *)
(*     tlv = Set.empty ; *)
(*     fv = Var.Set.union x.fv y.fv ; *)
(*     isvar = false *)
(*   } *)

(*   let record x = { *)
(*     tlv = Set.empty ; *)
(*     fv = x.fv ; *)
(*     isvar = false *)
(*   } *)

(*   (\* true if it contains only one variable *\) *)
(*   let is_single t = t.isvar && (Var.Set.cardinal t.fv = 1) && (Set.cardinal t.tlv = 1) *)

(*   let no_variables t = (Var.Set.cardinal t.fv = 0) && (Set.cardinal t.tlv = 0) *)

(*   let has_toplevel t = Set.cardinal t.tlv > 0 *)

(*   let pp ppf x = Set.pp ppf x.tlv *)
(*   let dump ppf x = Format.fprintf ppf "<fv = %a ; tlv = %a>" Var.Set.dump x.fv Set.dump x.tlv *)
(*   let printf = pp Format.std_formatter *)

(*   let mem v x = Set.mem v x.tlv *)

(* end *)

module rec Descr :
sig
  (* each kind is represented as a union of itersection of types
   * the type is a union of all kinds
   *
   * we add a new field that contains only variables.
   * Inv :
     * if the bdd of ANY kind is composed only of variables,
       the we move it in vars:
     * From a bdd we move all variables to vars: that belong to
     * to a path in the bdd that contains only variables and end in
     * true
     * A bdd never contains a path that ends in 1 and contains only variables
     *
     * (t1 v a ) ^ ( t2 v b )
     * we need to distribute variables for the intersection
     * (t1 ^ t2) v (t1 ^ b) v (t2 ^ a) v (a ^ b)
     * before we were doing only t1 ^ t2
   *)
  type s = {
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    abstract: BoolAbstracts.t;
    (* this is used in record to flag the fact that the type of a label is
     * absent . It is used for optional arguments in functions as ?Int
     * is the union of Int ^ undef where undef is a type with absent : true *)
    absent: bool;
  }
  include Custom.T with type t = s
  val empty: t
  val any : t
  val is_empty : t -> bool
end =
struct
  type s = {
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    abstract: BoolAbstracts.t;
    absent: bool;
  }
  type t = s

  let dump ppf d =
    Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>\n"
      BoolAtoms.dump d.atoms
      BoolIntervals.dump d.ints
      BoolChars.dump d.chars
      BoolPair.dump d.times
      BoolPair.dump d.arrow
      BoolRec.dump d.record
      BoolPair.dump d.xml
      BoolAbstracts.dump d.abstract
      d.absent

  let empty = {
    times = BoolPair.empty;
    xml   = BoolPair.empty;
    arrow = BoolPair.empty;
    record= BoolRec.empty;
    ints  = BoolIntervals.empty;
    atoms = BoolAtoms.empty;
    chars = BoolChars.empty;
    abstract = BoolAbstracts.empty;
    absent = false;
  }

  (*
   * Two representations possible. Either all fields (except vars) are full, OR
   * the field vars is full.
   *)
  let any =  {
    times = BoolPair.full;
    xml   = BoolPair.full;
    arrow = BoolPair.full;
    record= BoolRec.full;
    ints  = BoolIntervals.full;
    atoms = BoolAtoms.full;
    chars = BoolChars.full;
    abstract = BoolAbstracts.full;
    absent= false;
  }

  let check a =
    BoolChars.check a.chars;
    BoolIntervals.check a.ints;
    BoolAtoms.check a.atoms;
    BoolPair.check a.times;
    BoolPair.check a.xml;
    BoolPair.check a.arrow;
    BoolRec.check a.record;
    BoolAbstracts.check a.abstract;
    ()

  let equal a b =
    (a == b) || (
      (BoolAtoms.equal a.atoms b.atoms) &&
      (BoolChars.equal a.chars b.chars) &&
      (BoolIntervals.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) &&
      (BoolAbstracts.equal a.abstract b.abstract) &&
      (a.absent == b.absent)
    )

  let is_empty a =
    (BoolAtoms.is_empty a.atoms) &&
      (BoolChars.is_empty a.chars) &&
      (BoolIntervals.is_empty a.ints) &&
      (BoolPair.is_empty a.times) &&
      (BoolPair.is_empty a.xml) &&
      (BoolPair.is_empty a.arrow) &&
      (BoolRec.is_empty a.record) &&
      (BoolAbstracts.is_empty a.abstract)

  let compare a b =
    if a == b then 0
    else let c = BoolAtoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = BoolChars.compare a.chars b.chars in if c <> 0 then c
    else let c = BoolIntervals.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 let c = BoolAbstracts.compare a.abstract b.abstract 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 a =
    let accu = BoolChars.hash a.chars in
    let accu = 17 * accu + BoolIntervals.hash a.ints in
    let accu = 17 * accu + BoolAtoms.hash 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 = 17 * accu + BoolAbstracts.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu

end
and Node :
sig
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
  val dump: Format.formatter -> t -> unit
  val check: t -> unit
  val equal: t -> t -> bool
  val hash: t -> int
  val compare:t -> t -> int
  val mk: int -> Descr.t -> t
end =

struct
  type t = { id : int; cu: Compunit.t; mutable descr : Descr.t }
  let check n = ()
  let dump ppf n = Format.fprintf ppf "X%i" n.id
  let hash x = x.id + Compunit.hash x.cu
  let compare x y =
    let c = x.id - y.id in if c = 0 then Compunit.compare x.cu y.cu else c
  let equal x y = x==y || (x.id == y.id && (Compunit.equal x.cu y.cu))
  let mk id d = { id = id; cu = Compunit.current (); descr = d }
end

and Pair : Bool.S with type elem = (Node.t * Node.t) =
  Bool.Make(Custom.Pair(Node)(Node))
and BoolPair : BoolVar.S with type s = Pair.t =
  BoolVar.Make(Pair)

(* bool = true means that the record is open that is, that
 * the labels that are not in the domain of the map are
 * equal to "any" *)
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
  Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
and BoolRec : BoolVar.S with
  type s = Rec.t = BoolVar.Make(Rec)

module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr)
module DescrSList = SortedList.Make(Descr)

type descr = Descr.t
type node = Node.t
include Descr

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

let make () =
  incr count;
  Node.mk !count empty

let define n d =
  n.Node.descr <- d

let cons d =
  incr count;
  Node.mk !count d

let descr n = n.Node.descr
let internalize n = n
let id n = n.Node.id

let non_constructed =
  { any with
      times = empty.times; xml = empty.xml; record = empty.record }

let non_constructed_or_absent =
  { non_constructed with absent = true }

(* Descr.t type constructors *)
let times x y = { empty with times = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolPair.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolPair.atom (`Atm (Pair.atom (x,y))) }

let record label t =
  { empty with record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }

let record_fields x =
  { empty with record = BoolRec.atom (`Atm (Rec.atom x)) }

let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }

(* Atm = Any ^ a *)
let var a =  {
  times = BoolPair.vars a;
  xml   = BoolPair.vars a;
  arrow = BoolPair.vars a;
  record= BoolRec.vars a;
  ints  = BoolIntervals.vars a;
  atoms = BoolAtoms.vars a;
  chars = BoolChars.vars a;
  abstract = BoolAbstracts.vars a;
  absent = false;
}

let char c = { empty with chars = BoolChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) }


module type BVS =
sig
    type elem
    type t
    val get : t -> (elem list* elem list) list
end


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  = BoolIntervals.cup x.ints  y.ints;
      atoms = BoolAtoms.cup x.atoms y.atoms;
      chars = BoolChars.cup x.chars y.chars;
      abstract = BoolAbstracts.cup x.abstract y.abstract;
      absent = x.absent || y.absent;
    }

let cap x y =
  if x == y then x else
    {
      ints  = BoolIntervals.cap x.ints y.ints;
      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;
      atoms = BoolAtoms.cap x.atoms y.atoms;
      chars = BoolChars.cap x.chars y.chars;
      abstract = BoolAbstracts.cap x.abstract y.abstract;
      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  = BoolIntervals.diff x.ints y.ints;
      atoms = BoolAtoms.diff x.atoms y.atoms;
      chars = BoolChars.diff x.chars y.chars;
      abstract = BoolAbstracts.diff x.abstract y.abstract;
      absent= x.absent && not y.absent;
    }

(* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b =
  (BoolChars.trivially_disjoint a.chars b.chars) &&
  (BoolIntervals.trivially_disjoint a.ints b.ints) &&
  (BoolAtoms.trivially_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) &&
  (BoolAbstracts.trivially_disjoint a.abstract b.abstract) &&
  (not (a.absent && b.absent))

let rec constant = function
  | Integer i -> interval (Intervals.atom i)
  | Atom a -> atom (Atoms.atom a)
  | Char c -> char (Chars.atom c)
  | Pair (x,y) -> times (const_node x) (const_node y)
  | Xml (x,y) -> xml (const_node x) (const_node y)
  | Record x -> record_fields (false ,LabelMap.map const_node x)
  | String (i,j,s,c) ->
      if U.equal_index i j then constant c
      else
	let (ch,i') = U.next s i in
	constant (Pair (Char (Chars.V.mk_int ch), String (i',j,s,c)))
and const_node c = cons (constant c)

let neg x = diff any x

let any_node = cons any
let empty_node = cons empty

module LabelS = Set.Make(Label)

let any_or_absent = { any with absent = true }
let only_absent = { empty with absent = true }

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) only_absent; (* 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_or_absent 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 (Rec.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

module Witness = struct

  module NodeSet = Set.Make(Node)

  type witness =
    | WInt of Intervals.V.t
    | WAtom of Atoms.sample
    | WChar of Chars.V.t
    | WAbsent
    | WAbstract of Abstracts.elem option

    | WPair of witness * witness * witness_slot
    | WXml of witness * witness * witness_slot
    | WRecord of witness label_map * bool * witness_slot
	(* Invariant: WAbsent cannot actually appear *)

    | WFun of (witness * witness option) list * witness_slot
  and witness_slot =
      { mutable wnodes_in: NodeSet.t;
	mutable wnodes_out: NodeSet.t;
	mutable wuid: int }

  module WHash = Hashtbl.Make(
    struct
      type t = witness
      let hash_small = function
	| WInt i -> 17 * Intervals.V.hash i
	| WChar c -> 1 + 17 * Chars.V.hash c
	| WAtom None -> 2
	| WAtom (Some (ns,None)) -> 3 + 17 * Ns.Uri.hash ns
	| WAtom (Some (_,Some t)) -> 4 + 17 * Ns.Label.hash t
	| WAbsent -> 5
	| WAbstract None -> 6
	| WAbstract (Some t) -> 7 + 17 * Abstracts.T.hash t
	| WPair (_,_,s)
	| WXml (_,_,s)
	| WRecord (_,_,s)
	| WFun (_,s) -> 8 + 17 * s.wuid
      let hash = function
	| WPair (p1,p2,_) -> 257 * hash_small p1 + 65537 * hash_small p2
	| WXml (p1,p2,_) -> 1 + 257 * hash_small p1 + 65537 * hash_small p2
	| WRecord (r,o,_) ->
	    (if o then 2 else 3) + 257 * LabelMap.hash hash_small r
	| WFun (f,_) ->
	    4 + 257 *
	      (Hashtbl.hash
		 (List.map
		    (function (x,None) -> 17 * hash_small x
		       | (x,Some y) ->
			   1 + 17 * hash_small x + 257 * hash_small y)
		    f)
	      )
	| _ -> assert false

      let equal_small w1 w2 = match w1,w2 with
	| WInt i1, WInt i2 -> Intervals.V.equal i1 i2
	| WChar c1, WChar c2 -> Chars.V.equal c1 c2
	| WAtom None, WAtom None -> true
	| WAtom (Some (ns1,None)), WAtom (Some (ns2,None)) ->
	    Ns.Uri.equal ns1 ns2
	| WAtom (Some (_,Some t1)), WAtom (Some (_,Some t2)) ->
	    Ns.Label.equal t1 t2
	| WAbsent, WAbsent -> true
	| WAbstract None, WAbstract None -> false
	| WAbstract (Some t1), WAbstract (Some t2) -> Abstracts.T.equal t1 t2
	| _ -> w1 == w2

      let equal w1 w2 = match w1,w2 with
	| WPair (p1,q1,_), WPair (p2,q2,_)
	| WXml (p1,q1,_), WXml (p2,q2,_) ->
	    equal_small p1 p2 && equal_small q1 q2
	| WRecord (r1,o1,_), WRecord (r2,o2,_) ->
	    o1 == o2 && (LabelMap.equal equal_small r1 r2)
	| WFun (f1,_), WFun (f2,_) ->
	    List.length f1 = List.length f2 &&
		List.for_all2
		(fun (x1,y1) (x2,y2) ->
		   equal_small x1 x2 && (match y1,y2 with
					   | Some y1, Some y2 ->
					       equal_small y1 y2
					   | None, None -> true
					   | _ -> false)
		) f1 f2
	| _ -> false
    end)

  let wmemo = WHash.create 1024
  let wuid = ref 0
  let wslot () = { wuid = !wuid; wnodes_in = NodeSet.empty;
		   wnodes_out = NodeSet.empty }

  let () =
    Stats.register Stats.Summary
      (fun ppf -> Format.fprintf ppf "Allocated witnesses:%i@\n" !wuid)

  let rec pp ppf = function
    | WInt i ->
	Format.fprintf ppf "%a" Intervals.V.print i
    | WChar c ->
	Format.fprintf ppf "%a" Chars.V.print c
    | WAtom None ->
	Format.fprintf ppf "`#:#"
    | WAtom (Some (ns,None)) ->
	Format.fprintf ppf "`%a" Ns.InternalPrinter.print_any_ns ns
    | WAtom (Some (_,Some t)) ->
	Format.fprintf ppf "`%a" Ns.Label.print_attr t
    | WPair (w1,w2,_) ->
	Format.fprintf ppf "(%a,%a)" pp w1 pp w2
    | WXml (w1,w2,_) ->
	Format.fprintf ppf "XML(%a,%a)" pp w1 pp w2
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
	  (fun l w -> Format.fprintf ppf " %a=%a"
	     Label.print_attr l pp w)
	  ws;
	if o then Format.fprintf ppf " ..";
	Format.fprintf ppf " }"
    | WFun (f,_) ->
	Format.fprintf ppf "FUN{";
	List.iter (fun (x,y) ->
		     Format.fprintf ppf " %a->" pp x;
		     match y with
		       | None -> Format.fprintf ppf "#"
		       | Some y -> pp ppf y) f;
	Format.fprintf ppf " }"
    | WAbstract None ->
	Format.fprintf ppf "Abstract(..)"
    | WAbstract (Some s) ->
	Format.fprintf ppf "Abstract(%s)" s
    | WAbsent ->
	Format.fprintf ppf "Absent"

  let printf = pp Format.std_formatter

  let wmk w =  (* incr wuid; w *)  (* hash-consing disabled *)
    try WHash.find wmemo w
    with Not_found ->
      incr wuid;
      WHash.add wmemo w w;
(*      Format.fprintf Format.std_formatter "W:%a@."
	pp w; *)
      w

  let wpair p1 p2 = wmk (WPair (p1,p2, wslot()))
  let wxml p1 p2 = wmk (WXml (p1,p2, wslot()))
  let wrecord r o = wmk (WRecord (r,o, wslot()))
  let wfun f = wmk (WFun (f, wslot()))

  let bool_pair f =
    Pair.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
      ~atom:f

  let bool_rec f =
    Rec.compute
      ~empty:false ~full:true
      ~cup:(||) ~cap:(&&) ~diff:(fun x y -> x && not y)
      ~atom:f

  let rec node_has n = function
    | WXml (_,_,s) | WPair (_,_,s) | WFun (_,s) | WRecord (_,_,s) as w ->
	if NodeSet.mem n s.wnodes_in then true
	else if NodeSet.mem n s.wnodes_out then false
	else (let r = type_has (descr n) w in
	      if r then s.wnodes_in <- NodeSet.add n s.wnodes_in
	      else s.wnodes_out <- NodeSet.add n s.wnodes_out;
	      r)
    | w -> type_has (descr n) w

  (* type_has checks if a witness is contained in the union of
   * the leafs of a bdd, ignoring all variables. *)
  and type_has t = function
    | WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints)
    | WChar c -> Chars.contains c (BoolChars.leafconj t.chars)
    | WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms)
    | WPair (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
	  (BoolPair.leafconj t.times)
    | WXml (w1,w2,_) ->
	bool_pair
	  (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
	  (BoolPair.leafconj t.xml)
    | WFun (f,_) ->
	bool_pair
	  (fun (n1,n2) ->
	     List.for_all
	       (fun (x,y) ->
		  not (node_has n1 x) ||
		    (match y with None -> false
		       | Some y -> node_has n2 y))
	       f)
	  (BoolPair.leafconj t.arrow)
    | WRecord (f,o,_) ->
	bool_rec
	  (fun (o',f') ->
	     ((not o) || o') && (
	       let checked = ref 0 in
	       try
		 LabelMap.iteri
		   (fun l n ->
		      let w =
			try let w = LabelMap.assoc l f in incr checked; w
			with Not_found -> WAbsent in
		      if not (node_has n w) then raise Exit
		   ) f';
		 o' || (LabelMap.length f == !checked)
		   (* All the remaining fields cannot be WAbsent
		      because of an invariant. Otherwise, we must
		      check that all are WAbsent here. *)
	       with Exit -> false))
	  (BoolRec.leafconj t.record)
    | WAbsent -> t.absent
    | WAbstract a -> Abstracts.contains_sample a (BoolAbstracts.leafconj t.abstract)
end

type slot = { mutable status : status;
	       mutable notify : notify;
	       mutable active : bool }
and status = Empty | NEmpty of Witness.witness | Maybe
and notify = Nothing | Do of slot * (Witness.witness -> unit) * notify

let slot_empty = { status = Empty; active = false; notify = Nothing }
let slot_nempty w = { status = NEmpty w;
		     active = false; notify = Nothing }

let rec notify w = function
  | Nothing -> ()
  | Do (n,f,rem) ->
      if n.status == Maybe then (try f w with NotEmpty -> ());
      notify w rem

let rec iter_s s f = function
  | [] -> ()
  | arg::rem -> f arg s; iter_s s f rem

let set s w =
  s.status <- NEmpty w;
  notify w s.notify;
  s.notify <- Nothing;
  raise NotEmpty

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

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

let count_subtype = Stats.Counter.create "Subtyping internal loop"

let complex = ref 0

let rec slot d =
  incr complex;
  Stats.Counter.incr count_subtype;
  (* XXX here I call leafconj a zilliontime. REWRITE !!! *)
  if d.absent then slot_nempty Witness.WAbsent
  else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints))
  then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints)))
  else if not (Atoms.is_empty (BoolAtoms.leafconj d.atoms))
  then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms)))
  else if not (Chars.is_empty (BoolChars.leafconj d.chars))
  then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars)))
  else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract))
  then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract)))
  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 (Pair.get (BoolPair.leafconj d.times));
       iter_s s check_xml (Pair.get (BoolPair.leafconj d.xml));
       iter_s s check_arrow (Pair.get (BoolPair.leafconj d.arrow));
       iter_s s check_record (get_record (BoolRec.leafconj d.record));
       if s.active then marks := s :: !marks else s.status <- Empty;
     with NotEmpty -> ());
    s

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

and check_times (left,right) s =
  let rec aux w1 w2 accu1 accu2 seen = function
    (* Find a product in right which contains (w1,w2) *)
    | [] -> (* no such product: the current witness is in the difference. *)
	set s (Witness.wpair w1 w2)
    | (n1,n2) :: rest
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
	let accu2' = diff accu2 (descr n2) in
	guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
	let accu1' = diff accu1 (descr n1) in
	guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
  in
  let (t1,t2) = cap_product any any left in
  guard s t1 (fun w1 -> guard s t2 (fun w2 -> aux w1 w2 t1 t2 [] right))

and check_xml (left,right) s =
  let rec aux w1 w2 accu1 accu2 seen = function
    (* Find a product in right which contains (w1,w2) *)
    | [] -> (* no such product: the current witness is in the difference. *)
	set s (Witness.wxml w1 w2)
    | (n1,n2) :: rest
	when (Witness.node_has n1 w1) && (Witness.node_has n2 w2) ->
	let right = seen @ rest in
	let accu2' = diff accu2 (descr n2) in
	guard s accu2' (fun w2 -> aux w1 w2 accu1 accu2' [] right);
	let accu1' = diff accu1 (descr n1) in
	guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 [] right)
    | k :: rest -> aux w1 w2 accu1 accu2 (k::seen) rest
  in
  let (t1,t2) = cap_product any any_pair left in
  guard s t1 (fun w1 -> guard s t2 (fun w2 -> aux w1 w2 t1 t2 [] right))

and check_arrow (left,right) s =
  let single_right f (s1,s2) s =
    let rec aux w1 w2 accu1 accu2 left = match left with
      | (t1,t2)::left ->
          let accu1' = diff_t accu1 t1 in
          guard s accu1' (fun w1 -> aux w1 w2 accu1' accu2 left);

          let accu2' = cap_t  accu2 t2 in
          guard s accu2' (fun w2 -> aux w1 (Some w2) accu1 accu2' left)
      | [] ->
	  let f = match f with Witness.WFun (f,_) -> f | _ -> assert false in
	  set s (Witness.wfun ((w1,w2)::f))
    in
    let accu1 = descr s1 in
    guard s accu1 (fun w1 -> aux w1 None accu1 (neg (descr s2)) left)
  in
  big_conj single_right right s (Witness.wfun [])

and check_record (labels,(oleft,left),rights) s =
  let rec aux ws accus seen = function
    | [] ->
	let rec aux w i = function
	  | [] -> assert (i == Array.length ws); w
	  | l::labs ->
	      let w = match ws.(i) with
              | Witness.WAbsent -> w
              | wl -> LabelMap.add l wl w
            in
	      aux w (succ i) labs
      in
	set s (Witness.wrecord (aux LabelMap.empty 0 labels) oleft)
    | (false,_) :: rest when oleft -> aux ws accus seen rest
    | (_,f) :: rest
	when not (exists (Array.length left)
		    (fun i -> not (Witness.type_has f.(i) ws.(i)))) ->
	(* TODO: a version f get_record which keeps nodes in neg records. *)
	let right = seen @ rest in
	for i = 0 to Array.length left - 1 do
	  let di = diff accus.(i) f.(i) in
	  guard s di (fun wi ->
			let accus' = Array.copy accus in accus'.(i) <- di;
			let ws' = Array.copy ws in ws'.(i) <- wi;
			aux ws' accus' [] right);
	done
    | k :: rest -> aux ws accus (k::seen) rest
  in
  let rec start wl i =
    if (i < 0) then aux (Array.of_list wl) left [] rights
    else guard s left.(i) (fun w -> start (w::wl) (i - 1))
  in
  start [] (Array.length left - 1)

let timer_subtype = Stats.Timer.create "Types.is_empty"

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

let getwit t = match (slot t).status with NEmpty w -> w | _ -> assert false
  (* Assumes that is_empty has been called on t before. *)

let witness t = if is_empty t then raise Not_found else getwit t

let non_empty d = not (is_empty d)

let disjoint d1 d2 = is_empty (cap d1 d2)

let subtype d1 d2 = is_empty (diff d1 d2)

let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)


(* functions on variables need the subtyping relation *)
let get_variables =
  let memo_descr = DescrHash.create 17 in
  fun t ->
  let get_vars_conj get_atom pos acc l =
    List.fold_left (fun acc e ->
      get_atom pos acc e) acc l
  in
  let get_vars_bdd (type s) (type e)
      (module BV : BVS with type elem = e and type t = s)
      get_atom _pos acc bdd
      =
    List.fold_left (fun ((tlvp, tlvn, vars) as acc) (p, n) ->
      let acc' = get_vars_conj get_atom true acc p in
      get_vars_conj  get_atom false acc' n
    ) acc (BV.get bdd)
  in
  let get_vars_boolvar get_atom pos (tlvp, tlvn, vars) = function
    | (`Var v ) as x when pos -> Var.Set.add x tlvp, tlvn, Var.Set.add x vars
    | (`Var v ) as x -> tlvp, Var.Set.add x tlvn,  Var.Set.add x vars
    | `Atm x ->
      let _, _, vars' = get_atom pos (Var.Set.empty, Var.Set.empty, vars) x
      in
      tlvp, tlvn, vars'
  in
  let get_nothing _ acc _ = acc in
  let rec get_pair pos acc (t1, t2) =
    let acc1 = get_variables pos acc (descr t1) in
    get_variables pos acc1 (descr t2)
  and get_record pos acc (_, lmap) =
    LabelMap.fold (fun _ t acc -> get_variables pos acc (descr t)) lmap acc
  and get_bdd_pair pos = get_vars_bdd (module Pair) (get_pair) pos
  and get_bdd_record pos = get_vars_bdd (module Rec) (get_record) pos
  and get_bv_pairs pos = get_vars_bdd (module BoolPair)
    (get_vars_boolvar get_bdd_pair) pos
  and get_bv_recs pos = get_vars_bdd (module BoolRec)
    (get_vars_boolvar get_bdd_record) pos
  and get_variables pos (tvpos,tvneg,vars) t =
    let tpos, tneg, tvars =
      try
        let r = DescrHash.find memo_descr t in
        r
      with
        Not_found ->
          let acc = Var.Set.(empty,empty,empty) in
          DescrHash.add memo_descr t acc;
          let acc = get_vars_bdd (module BoolIntervals)
            (get_vars_boolvar get_nothing) pos acc t.ints in
          let acc = get_vars_bdd (module BoolChars)
            (get_vars_boolvar get_nothing) pos acc t.chars in
          let acc = get_vars_bdd (module BoolAtoms)
            (get_vars_boolvar get_nothing) pos acc t.atoms in
          let acc = get_vars_bdd (module BoolAbstracts)
            (get_vars_boolvar get_nothing) pos acc t.abstract in
          let acc = get_bv_pairs pos acc t.times in
          let acc = get_bv_pairs pos acc t.xml in
          let acc = get_bv_pairs pos acc t.arrow in
          let acc = get_bv_recs pos acc t.record in
          DescrHash.replace memo_descr t acc;
          acc
    in
    (Var.Set.union tvpos tpos,
     Var.Set.union tvneg tneg,
     Var.Set.union tvars vars)
  in
  try
    DescrHash.find memo_descr t
  with
    Not_found ->
      let res = get_variables true Var.Set.(empty,empty,empty) t in
      DescrHash.add memo_descr t res;
      res

let check_var =
  let aux t =
    let tvpos, tvneg, tvars = get_variables t in
    match Var.Set.(cardinal tvpos, cardinal tvneg, cardinal tvars) with
      1, 0, 1 -> let v = Var.Set.choose tvpos in
                if equiv (var v) t then `Pos v else `NotVar
    | 0, 1, 1 -> let v = Var.Set.choose tvneg in
                if equiv (diff any (var v)) t then `Neg v else `NotVar
    | _ -> `NotVar
  in
  let memo_descr = DescrHash.create 17 in
  fun t -> try DescrHash.find memo_descr t with
    Not_found ->
      let res = aux t in
      DescrHash.add memo_descr t res;
      res

let is_var t = match check_var t with `NotVar -> false | _ -> true
let no_var t =
  let _, _, s = get_variables t in Var.Set.is_empty s

let has_tlv t =
  let p, n, _ = get_variables t in
  not Var.Set.(is_empty p && is_empty n)

let all_vars t =
  let _, _, s = get_variables t in s

let all_tlv t =
  let p , n, _ = get_variables t in Var.Set.union p n

let is_closed delta t =
  Var.Set.(is_empty (diff (all_vars t) delta))

let extract_variable t =
  match check_var t with
    `Pos v -> v, true
  | `Neg v -> v, false
  | _ -> assert false



module Cache = struct

  type 'a cache =
    | Empty
    | Type of t * 'a
    | Split of Witness.witness * 'a cache * 'a cache

  let rec find f t = function
    | Empty ->
	let r = f t in Type (t,r), r
    | Split (w,yes,no) ->
	if Witness.type_has t w
	then let yes,r = find f t yes in Split (w,yes,no), r
	else let no,r = find f t no in Split (w,yes,no), r
    | Type (s,rs) as c ->
	let f1 ()=
	  let w = witness (diff t s) in
	  let rt = f t in
	  Split (w, Type (t,rt), c), rt
	and f2 () =
	  let w = witness (diff s t) in
	  let rt = f t in
	  Split (w, c, Type (t,rt)), rt in

	if Random.int 2 = 0 then
	  try f1 () with Not_found -> try f2 () with Not_found -> c, rs
	else
	  try f2 () with Not_found -> try f1 () with Not_found -> c, rs

  let rec lookup t = function
    | Empty -> None
    | Split (w,yes,no) -> lookup t (if Witness.type_has t w then yes else no)
    | Type (s,rs) -> if equiv s t then Some rs else None

  let emp = Empty


  let rec dump_cache f ppf = function
    | Empty -> Format.fprintf ppf "Empty"
    | Type (_,s) -> Format.fprintf ppf "*%a" f s
    | Split (w,c1,c2) -> Format.fprintf ppf "?(%a,%a)"
	(*Witness.pp w *)(dump_cache f) c1 (dump_cache f) c2

  let memo f =
    let c = ref emp in
    fun t ->
       let c',r = find f t !c in
       c := c';
       r

end

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 partition 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 (Pair.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 -> partition any (BoolPair.leafconj d.times)
    | `XML -> partition any_pair (BoolPair.leafconj 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 disjoint 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(Pair)

  (* 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 = partition 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 = partition 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 (BoolPair.leafconj d.times)
      | `XML -> normal_xml (BoolPair.leafconj 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 disjoint d1 t1 then accu else cap accu d2)
      any
      n

  let merge_same_first tr =
    let trs = ref [] in
    let _ =
      List.fold_left
	(fun memo (t1,t2) ->
	   let memo',l =
	     Cache.find
	       (fun t1 -> let l = ref empty in trs := (t1,l) :: !trs; l)
	       t1 memo in
	   l := cup t2 !l;
	   memo')
	Cache.emp tr in
    List.map (fun (t1,l) -> (t1,!l)) !trs

  (* same on second component: use the same implem? *)
  let clean_normal l =
    let rec aux accu (t1,t2) =
      match accu with
	| [] -> [ (t1,t2) ]
	| (s1,s2) :: rem when equiv t2 s2 -> (cup s1 t1, s2) :: rem
	| (s1,s2) :: rem -> (s1,s2) :: (aux rem (t1,t2)) in
    List.fold_left aux [] l

  let any = { empty with times = any.times }
  and any_xml = { empty with xml = any.xml }
  let is_empty d = d == []
  let any_of = function `XML -> any_xml | `Normal -> any
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 absent = or_absent empty
  let any_or_absent = or_absent any
  let any_or_absent_node = cons any_or_absent
  let has_absent d = d.absent

  let absent_node = cons 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
      record_fields (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, record_fields (o,r))
	else
	  Pair (absent,record_fields (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)
      []
      (Rec.get (BoolRec.leafconj 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 pi l d = TR.pi1 (split d l)

  let project d l =
    let t = pi l d in
    if t.absent then raise Not_found;
    t

  let project_opt d l =
    let t = pi l d in
    { t with absent = false }

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

(* TODO: eliminate this cap ... (record l absent_node) when
   not necessary. eg. { ..... } \ l *)

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

  let all_labels d =
    let res = ref LabelSet.empty in
    let aux (_,r) =
      let ls = LabelMap.domain r in
      res := LabelSet.cup ls !res in
    (* XXX every times I use BoolRec.leafconj I'm trowing away all variables ! *)
    Rec.iter aux (BoolRec.leafconj d.record);
    !res

  let first_label d =
    let min = ref Label.dummy in
    let aux (_,r) = match LabelMap.get r with
	(l,_)::_ -> min := Label.min l !min | _ -> () in
    Rec.iter aux (BoolRec.leafconj d.record);
    !min

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

  let has_empty_record d =
    Rec.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)
	    )
      (BoolRec.leafconj 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 = Label.min (first_label d1) (first_label d2) in
      if l == Label.dummy 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_fields (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 == Label.dummy 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


  type t = TR.t
  let focus = split_normal
  let get_this r = { (TR.pi1 r) with absent = false }
  let need_others = function _::_::_ -> true | _ -> false
  let constraint_on_others r t1 =
    List.fold_left
      (fun accu (d1,d2) -> if disjoint d1 t1 then accu else cap accu d2)
      any_record
      r
end

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_line_non_empty (left,right) =
    not (List.exists (check_simple left) right)

  let sample t =
    let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
    List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
      { empty with arrow = any.arrow } left

  let check_strenghten t s =
    if subtype t s then t else raise Not_found

  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
    (* considering only arrows here and not poly variables is correct as
     * the iface is just an intersection of arrows *)
    aux (Pair.get (BoolPair.leafconj s.arrow))

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

  let get t =
    List.fold_left
      (fun ((dom,arr) as accu) (left,right) ->
	 if check_line_non_empty (left,right)
	 then
	   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)
	 else accu
      )
      (any, [])
      (Pair.get (BoolPair.leafconj 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 (BoolIntervals.leafconj d.ints)
  let get d = d.ints
  let any = { empty with ints = any.ints }
(*  let any = { empty with ints = BoolIntervals.full } *)
end

module Atom = struct
  let has_atom d a = Atoms.contains a (BoolAtoms.leafconj d.atoms)
  let get d = d.atoms
  let any = { empty with atoms = any.atoms }
end

module OldChar = Char
module Char = struct
  let has_char d c = Chars.contains c (BoolChars.leafconj d.chars)
  let is_empty d = Chars.is_empty (BoolChars.leafconj d.chars)
  let get d = d.chars
  let any = { empty with chars = any.chars }
end

module Abstract = struct
  let has_abstract d a = Abstracts.contains a (BoolAbstracts.leafconj d.abstract)
  let get d = d.abstract
  let any = { empty with abstract = any.abstract }
end

module Print =
struct
  let rec pp_const ppf = function
    | Integer i -> Intervals.V.print ppf i
    | Atom a -> Atoms.V.print_quote ppf a
    | Char c -> Chars.V.print ppf c
    | Pair (x,y) -> Format.fprintf ppf "(%a,%a)" pp_const x pp_const y
    | Xml (x,y) -> Format.fprintf ppf "XML(%a,%a)" pp_const x pp_const y
    | Record r ->
        let pp ppf =
          LabelMap.iteri (fun l c ->
            Format.fprintf ppf "%a : %a; " Label.print_attr l pp_const c)
        in
        Format.fprintf ppf "Record{%a}" pp r
    | String (i,j,s,c) ->
	Format.fprintf ppf "\"%a\" %a"
	U.print (U.mk (U.get_substr s i j))
	pp_const c

  let nil_atom = Atoms.V.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

  type gname = string * Ns.QName.t

  type nd = {
    id : int;
    mutable def : d list;
    mutable state :[
      | `Expand
      | `None
      | `Marked
      | `GlobalName of gname
      | `Named of U.t ]
  }
  and  d =
    | Name of gname
    | Regexp of nd Pretty.regexp
    | Atomic of (Format.formatter -> unit)
    | Pair of nd * nd
    | Char of Chars.V.t
    | Xml of [ `Tag of (Format.formatter -> unit) | `Type of nd ] * nd * nd
    | Record of (bool * nd) label_map * bool * bool
    | Arrows of (nd * nd) list * (nd * nd) list
    | Intersection of nd list
    | Diff of nd * nd
    | Neg of nd
    | Abs of nd


  module Key = struct
    include Custom.Pair(Var.Set)(Var.Set)
    let empty = Var.Set.(empty,empty)
    let is_empty (v1, v2) = Var.Set.(is_empty v1 && is_empty v2)
  end
  module VarTable = Hashtbl.Make(Key)
  module KeySet = Set.Make(Key)

  let compare x y = x.id - y.id

  module S = struct
    type t = nd
    let compare x y = x.id - y.id
    let hash x = x.id
    let equal x y = x.id = y.id
  end
  module Decompile = Pretty.Decompile(DescrHash)(S)

  module DescrPairMap = Map.Make(Custom.Pair(Descr)(Descr))

  let memo = ref Cache.emp

  let uniq t =
    let c',r = Cache.find (fun t -> t) t !memo in
    memo := c';
    r

  let lookup t = match Cache.lookup t !memo with Some t -> t | None -> t

  let named = ref DescrMap.empty
  let named_xml = ref DescrPairMap.empty
  let register_global cu (name : Ns.QName.t) d =
    let d = uniq d in
    if equal { d with xml = BoolPair.empty } empty then
      (let l = (*Product.merge_same_2*) (Product.get ~kind:`XML d) in
       match l with
	 | [(t1,t2)] ->
	     if DescrPairMap.mem (t1,t2) !named_xml then ()
	     else
	       named_xml := DescrPairMap.add (t1,t2) (cu,name) !named_xml
	 | _ -> ());
    if DescrMap.mem d !named then ()
    else named := DescrMap.add d (cu,name) !named

  let unregister_global d =
    let d = uniq d in
    if equal { d with xml = BoolPair.empty } empty then
      (let l = Product.get ~kind:`XML d in
      match l with
	 | [(t1,t2)] ->
	     named_xml := DescrPairMap.remove (t1,t2) !named_xml
	 | _ -> ());
    named := DescrMap.remove d !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 BoolAtoms.compare d.atoms any.atoms +
      aux BoolChars.compare d.chars any.chars +
      aux BoolIntervals.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 +
      aux BoolAbstracts.compare d.abstract any.abstract
    in
    n >= 5

  let rec prepare d =
    let d = lookup d in
    try DescrHash.find memo d
    with Not_found ->
      try begin
        let n = DescrMap.find d !named in
        let s = alloc [] in
        s.state <- `GlobalName n;
        DescrHash.add memo d s;
        s
      end with Not_found ->
        if d.absent then
          alloc [Abs (prepare ({d with absent=false}))]
        else 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;

        (* Given a bdd
           \/_i (p_i & pvar_i, n_i& nvar_i)
           we fill a table appropriately where the entries are the (pvar_i,nvar_i)
           and the data the variable-less bdd (p_i \ n_i)
        *)

        let split_var_atom op init l =
          List.fold_left (fun (acc_v, acc_a) e ->
            match e with
              `Atm _ -> (acc_v, op e acc_a)
            | `Var _ as x -> (Var.Set.add x acc_v, acc_a)
          ) (Var.Set.empty, init) l
        in
        let fill_line (type s)
            (module BV : BoolVar.S with type t = s) table get set t =
          List.iter (fun (p, n) ->
            let v1, a1 = split_var_atom (fun a b -> BV.(cap (atom a) b)) BV.full p in
            let v2, a2 = split_var_atom (fun a b -> BV.(cup (atom a) b)) BV.empty n in
            let a = BV.diff a1 a2 in
            let key = v1, v2 in
            let old_t = try VarTable.find table key with Not_found -> {empty with absent = t.absent } in
            let new_a = BV.cup a (get old_t) in
            VarTable.replace table key (set old_t new_a)) (BV.get (get t))
        in
        let h = VarTable.create 17 in
        fill_line (module BoolIntervals) h (fun t -> t.ints) (fun t u -> {t with ints = u }) d;
        fill_line (module BoolChars) h (fun t -> t.chars) (fun t u -> {t with chars = u }) d;
        fill_line (module BoolAtoms) h (fun t -> t.atoms) (fun t u -> {t with atoms = u }) d;
        fill_line (module BoolPair) h (fun t -> t.times) (fun t u -> {t with times = u }) d;
        fill_line (module BoolPair) h (fun t -> t.xml) (fun t u -> {t with xml = u }) d;
        fill_line (module BoolPair) h (fun t -> t.arrow) (fun t u -> {t with arrow = u }) d;
        fill_line (module BoolRec) h (fun t -> t.record) (fun t u -> {t with record = u }) d;
        fill_line (module BoolAbstracts) h (fun t -> t.abstract) (fun t u -> {t with abstract = u }) d;
        let h =
          try
            let no_var = VarTable.find h Key.empty in
            let update_field (type s) (module BV : BoolVar.S with type t = s) get set d1 d2 =
              let bdd = get d1 in
              if BV.(is_empty (diff full bdd)) then set d2 bdd else d2
            in
            let h' = VarTable.create 17 in
            VarTable.iter (fun ((v1, v2) as k) t ->
              let t =
              if Var.Set.(is_empty v1 && is_empty v2) then t
              else
                let t = update_field (module BoolIntervals) (fun t -> t.ints) (fun t u -> {t with ints = u }) no_var t in
                let t = update_field (module BoolChars) (fun t -> t.chars) (fun t u -> {t with chars = u }) no_var t in
                let t = update_field (module BoolAtoms) (fun t -> t.atoms) (fun t u -> {t with atoms = u }) no_var t in
                let t = update_field (module BoolPair) (fun t -> t.times) (fun t u -> {t with times = u }) no_var t in
                let t = update_field (module BoolPair) (fun t -> t.xml) (fun t u -> {t with xml = u }) no_var t in
                let t = update_field (module BoolPair) (fun t -> t.arrow) (fun t u -> {t with arrow = u }) no_var t in
                let t = update_field (module BoolRec) (fun t -> t.record) (fun t u -> {t with record = u }) no_var t in
                let t = update_field (module BoolAbstracts) (fun t -> t.abstract) (fun t u -> {t with abstract = u }) no_var t in t
              in
              VarTable.replace h' k t
            ) h; h'
          with Not_found -> h
        in
        let found_any, all_descrs =
          try
            let res =
              VarTable.fold (fun ((v1, v2) as k) tt acc ->
                if Var.Set.(not (is_empty (inter v1 v2))) || is_empty tt then acc
                else if Key.is_empty k && subtype any tt then raise Not_found
                else
                  (k, tt) :: acc
              ) h []
            in
            false, res
          with Not_found -> true, [ Key.empty , any ]
        in
        if found_any then (slot.def <- [Neg (alloc [])];slot)
        else
          let merge_column_with (v1,t1) l =
            List.fold_left  (fun (accv, accl) ((v2,t2) as x) ->
              if equal t1 t2 then (v2::accv, accl) else (accv,x::accl))
              ([ v1 ],[]) l
          in
          let merge_variables l =
            match l with
              [] -> (Var.Set.empty, Var.Set.empty), []
            | i :: ll ->
              let factp, factn =
                List.fold_left (fun (accp, accn) (vp, vn) ->
                  Var.Set.(inter accp vp, inter accn vn))
                  i ll
              in
              let nl =
                List.fold_left (fun acc (vp, vn) ->
                  let nvp = Var.Set.diff vp factp in
                  let nvn = Var.Set.diff vn factn in
                  if Var.Set.(is_empty nvp && is_empty nvn) then acc
                else (nvp, nvn) :: acc
                ) [] l
              in
              (factp, factn), nl
          in
          let rec merge_columns acc l =
            match l with
              [] -> acc
            | ((_, t) as e) :: ll ->
              let vars, nll = merge_column_with e ll in
              let factv,remv = merge_variables vars in
              merge_columns ((factv, remv,t)::acc) nll
          in
          let all_descrs = merge_columns [] all_descrs in
          let inter_d l =
            match l with
              [] -> Neg (alloc [])
            | [ p ] -> p
            | [ p ; Neg { def = [] } ] -> p
            | _ -> Intersection (List.map (fun x -> alloc [x]) l)
          in
          let inter_nd l =
            match l with
              [] -> Neg (alloc [])
            | [ { def = [ p ] }  ] -> p
            | _ -> Intersection l
          in
          let prepare_boolvar get print bdd acc =
            (* there should not be any toplevel variable left *)
            match get bdd with
              [ ] -> acc
            | [ ([`Atm bdd], []) ] ->  (print bdd) @ acc
            | _ -> assert false
          in
          let print_vars l =
            Var.Set.fold
              (fun acc v -> (Atomic (fun ppf -> Var.pp ppf v)) :: acc) [] l
          in
          let print_pnvars l =
            List.fold_left (fun acc (p,n) ->
              let pneg = print_vars n in
              let ppos = print_vars p in
              match  List.rev ppos,  List.rev pneg with
                [],[] -> acc
              | [],l -> Neg(alloc l) :: acc
              | l, [] -> (inter_d l) :: acc
              | l1,l2  -> (Diff (alloc [inter_d l1], alloc l2)) :: acc
            ) [] l
          in
          let print_descr (pvars,nvars) lvars tt =
            if is_empty tt then [] else
              let print_topvars pos rem =
                let rem = List.rev rem in
                let printed_nvars = List.rev (print_vars nvars) in
                let negative_part = printed_nvars @ (if pos then [] else rem) in
                let printed_lvars = print_pnvars lvars in
                let positive_part2 = printed_lvars @ (if pos then rem else []) in
                let positive_part =
                  (List.rev_map (fun e -> alloc [e]) (print_vars pvars))
                  @ (if positive_part2 == []
                    then [] else [ alloc positive_part2 ])
                in
                match positive_part, negative_part with
                  [], [] -> []
                | [], l  -> [ Neg (alloc l) ]
                | l,  []  -> [ inter_nd l ]
                | l1, l2  -> [ Diff (alloc [inter_nd l1], alloc l2) ]
              in
              if subtype any tt then print_topvars true [] else
                let tt, positive =
                  if worth_complement tt then
                    diff any tt, false
                  else tt , true
                in
              (* sequence type. We do not want to split types such as
                 Any into Any \ [ Any *] | Any, and likewise, write
                 Atom \ [] | [].

              *)
                let finite_atoms =
                  try
                    match BoolAtoms.get tt.atoms with
                      [ ( [ `Atm bdd ], [] ) ] -> let res =
                                                   match Atoms.sample bdd with
                                                     None -> false
                                                   | _ -> true
                                                 in res
                    | _ -> false
                  with Not_found -> true
                in
                let u_acc, tt =
	          if subtype { empty with times = tt.times } seqs_descr
                  then
                    let seq = cap tt seqs_descr in
                    if is_empty seq || (is_empty { empty with times = seq.times }
                                       && not finite_atoms)
                    then [], tt
                    else [ (Regexp (decompile seq)) ],
                         (let d = diff tt seqs_descr in
                          if finite_atoms then d else
                            cup d (cap tt nil_type))
	          else
	            [], tt
                in
              (* base types *)
                let u_acc = prepare_boolvar BoolChars.get (fun bdd ->
                  match Chars.is_char bdd with
                  | Some c -> [Char c]
                  | None ->
                   List.map (fun x -> (Atomic x)) (Chars.print bdd)
                ) tt.chars u_acc
                in

                let u_acc = prepare_boolvar BoolIntervals.get (fun bdd ->
                  let l = Intervals.print bdd in
                  List.map (fun x -> (Atomic x)) l
                )  tt.ints u_acc
                in

                let bool =
                  Atoms.cup
                    (Atoms.atom (Atoms.V.mk_ascii "false"))
                    (Atoms.atom (Atoms.V.mk_ascii "true"))
                in
                let u_acc = prepare_boolvar BoolAtoms.get  (fun bdd ->
                  match Atoms.print bdd with
                  | [ x ] when (Atoms.equal bool bdd) ->
                    [Atomic (fun ppf -> Format.fprintf ppf "Bool")]
                  | l -> List.map (fun x -> (Atomic x)) l
                )  tt.atoms u_acc
                in

              (* pairs *)
                let u_acc = prepare_boolvar BoolPair.get (fun x ->
                  List.rev_map (fun (t1,t2) ->
                    Pair (prepare t1, prepare t2)
                  ) (Product.partition any x)
                )  tt.times u_acc
                in

              (* xml pairs *)
                let u_acc = prepare_boolvar BoolPair.get (fun x ->
                  List.flatten (
                    List.map (fun (t1,t2) ->
                      try let n = DescrPairMap.find (t1,t2) !named_xml in [(Name n)]
                      with Not_found ->
                        let tag =
                          match Atoms.print_tag (BoolAtoms.leafconj t1.atoms) with
                          | Some a when is_empty { t1 with atoms = BoolAtoms.empty } -> `Tag a
                          | _ -> `Type (prepare t1)
                        in
                        assert (equal { t2 with times = empty.times } empty);
                        List.rev_map (fun (ta,tb) ->
                          (Xml (tag, prepare ta, prepare tb))
                        ) (Product.get t2);
                    ) (Product.partition any_pair x)
                  )
                )  tt.xml u_acc
                in

              (* arrows *)
                let u_acc = prepare_boolvar BoolPair.get  (fun x ->
                  List.map (fun (p,n) ->
                    let p = List.fold_left (fun acc (t,s) ->
                      if is_empty (descr t) then acc else
                        (prepare (descr t), prepare (descr s)) :: acc) [] p
                    in
                    let n = List.rev_map (fun (t,s) ->
                      (prepare (descr t), prepare (descr s))) n
                    in
                    (Arrows (p,n))
                  ) (Pair.get x))  tt.arrow u_acc
                in

              (* records *)
                let u_acc = prepare_boolvar BoolRec.get  (fun x ->
                  List.map (fun (r,some,none) ->
                    let r = LabelMap.map (fun (o,t) -> (o, prepare t)) r in
                    (Record (r,some,none))
                  ) (Record.get { empty with record = BoolRec.atom (`Atm x) }))  tt.record u_acc
                in

                let u_acc = prepare_boolvar BoolAbstracts.get (fun bdd ->
                  let l = Abstracts.print bdd in
                  List.map (fun x -> (Atomic x)) l
                )  tt.abstract u_acc
                in

                let u_acc =
                  if tt.absent then (Atomic (fun ppf -> Format.fprintf ppf "#ABSENT")) :: u_acc
                  else u_acc
                in
                print_topvars positive u_acc
          in
          let all_printed =
            List.fold_left (fun acc (factvars,lvars,t) ->
              (print_descr factvars lvars t) @ acc
            ) slot.def all_descrs
          in
          slot.def <- all_printed;
          slot
  and decompile d =
    let aux t =
      let tr = Product.get t in
      let tr = Product.merge_same_first tr in
      let tr = Product.clean_normal tr in

      let eps = Atoms.contains nil_atom (BoolAtoms.leafconj t.atoms) in
      let tr_cons = List.map (fun (li,ti) -> (cons li, cons ti)) tr in

      try
       let (l0,t0) = List.find
         (fun ((l0,t0) as tr0) ->
           let t'' =
           List.fold_left
             (fun accu ((li,ti) as tri) ->
               if tr0 == tri then accu
               else cup accu (times li ti)
             )
             (if eps then nil_type else empty)
             tr_cons
           in
           equiv (descr t0) t'' ) tr_cons in
       `Eps (prepare (descr l0), descr t0)
      with Not_found ->
       let tr = List.map (fun (l,t) -> prepare l, t) tr in
       `T (tr, eps)
    in
    Decompile.decompile aux 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;
          (* + 8 allows to disable sharing for small subtrees *)
	  if (s.state == `Marked) && (!gen < g + 8) then s.state <- `None
      | `Marked -> s.state <- `Named (name ()); to_print := s :: !to_print
      | _ -> ()
  and assign_name_rec = function
    | Neg t -> assign_name t
    | Abs t -> assign_name t
    | Name _ | Char _ | Atomic _ -> ()
    | Regexp r -> assign_name_regexp r
    | Pair (t1,t2) -> assign_name t1; assign_name t2
    | Intersection l -> List.iter assign_name l
    | Diff (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 print_gname ppf (cu,n) =
    Format.fprintf ppf "%s%a" cu Ns.QName.print n

(* operator precedences:
   20 names, constants, ...
   10 : <t1 >
   9 : star plus ?
   8 : seq
   7 : \ left of \
   6 : \
   5 : &
   4 : | alt
   3 : should be xml but for compatibility xml is stronger than & | \
   2 : arrow left of arrow
   1 : arrow
   0
   We use a private type to force the use of a symbolic name
 *)
  module Level : sig
    type t = private int
    val make : int -> t
  end
    = struct
      type t = int
      let make x = x
    end

  let lv_min = Level.make 0
  let lv_arrow = Level.make 1
  let lv_larrow = Level.make 2
  let _dummy_lv = Level.make 3
  let lv_alt = Level.make 4
  let lv_and = Level.make 5
  let lv_diff = Level.make 6
  let lv_ldiff = Level.make 7
  let lv_seq = Level.make 8
  let lv_post = Level.make 9
  let lv_xml = Level.make 10
  let lv_max = Level.make 20

  let opar ppf ~level (pri : Level.t) =
    if Pervasives.(level < pri) then Format.fprintf ppf "@[("

  let cpar ppf ~level (pri : Level.t) =
    if Pervasives.(level < pri) then Format.fprintf ppf ")@]"

  let  do_print_list empty pri op pri_op pr_e ppf l =
    let rec loop l =
      match l with
        [] -> ()
      | [ h ] -> (pr_e pri_op) ppf h
      | h :: t -> Format.fprintf ppf "%a %s@ " (pr_e pri_op) h op; loop t
    in
    match l with
      [] -> Format.fprintf ppf "%s" empty
    | [ h ] -> (pr_e pri) ppf h
    | _ ->
      opar ppf ~level:pri_op pri;
      loop l;
      cpar ppf ~level:pri_op pri


  let rec do_print_slot (pri : Level.t) ppf s =
    match s.state with
      | `Named n -> U.print ppf n
      | `GlobalName n -> print_gname ppf n
      | _ -> do_print_slot_real pri ppf s.def

  and do_print_slot_real pri ppf def =
      do_print_list "Empty" pri "|" lv_alt do_print ppf def
  and do_print pri ppf =
    function
    | Neg { def = [] } -> Format.fprintf ppf "Any"
    | Neg t -> Format.fprintf ppf "Any \\ @[%a@]" (do_print_slot lv_diff) t
    | Abs t -> Format.fprintf ppf "?(@[%a@])" (do_print_slot lv_min) t
    | Name n -> print_gname ppf n
    | Char c -> Chars.V.print ppf c
    | Regexp r -> Format.fprintf ppf "@[[ %a ]@]" (do_print_regexp lv_min) r
    | Atomic a -> a ppf
    | Diff (a, b) ->
      opar ppf ~level:lv_diff pri;
      Format.fprintf ppf "@[%a@] \\ @[%a@]" (do_print_slot lv_ldiff) a
        (do_print_slot lv_diff) b;
      cpar ppf ~level:lv_diff pri
    | Intersection [] -> ()
    | Intersection [ p ] -> do_print_slot pri ppf p
    | Intersection a -> do_print_list "Any" pri "&" lv_and do_print_slot ppf a
    | Pair (t1,t2) ->
	Format.fprintf ppf "@[(%a,%a)@]"
	  (do_print_slot lv_min) t1
	  (do_print_slot lv_min) t2
    | Xml (tag,attr,t) ->
        opar ppf ~level:lv_xml pri;
	Format.fprintf ppf "<%a%a>%a"
	  do_print_tag tag
	  do_print_attr attr
	  (do_print_slot lv_xml) t;
        cpar ppf ~level:lv_xml pri;
    | Record (r,some,none) ->
	Format.fprintf ppf "@[{";
	do_print_record ppf (r,some,none);
	Format.fprintf ppf " }@]"
    | Arrows (p,[]) ->
      do_print_list "Arrow" pri "&" lv_and do_print_arrow ppf p
    | Arrows (p, n) ->
      opar ppf ~level:lv_diff pri;
      do_print_list "Arrow" lv_diff "&" lv_and do_print_arrow ppf p;
      Format.fprintf ppf " \\@ ";
      do_print_list "##ERROR" lv_diff "|" lv_alt do_print_arrow ppf n;
      cpar ppf ~level:lv_diff pri
  and do_print_arrow pri ppf (t,s) =
    opar ppf ~level:lv_arrow pri;
    Format.fprintf ppf "%a -> %a"
      (do_print_slot lv_larrow) t
      (do_print_slot lv_arrow) s;
    cpar ppf ~level:lv_arrow pri
  and do_print_tag ppf = function
    | `Tag s -> s ppf
    | `Type t -> Format.fprintf ppf "(%a)" (do_print_slot lv_min) t
  and do_print_attr ppf = function
    | { state = `Marked|`Expand|`None;
	def = [ Record (r,some,none) ] } -> do_print_record ppf (r,some,none)
    | t -> Format.fprintf ppf " (%a)" (do_print_slot lv_min) t
  and do_print_record ppf (r,some,none) =
    List.iter
      (fun (l,(o,t)) ->
	 let opt = if o then "?" else "" in
	 Format.fprintf ppf "@ @[%a=%s@]%a"
	   Label.print_attr l opt (do_print_slot lv_min) t
      ) (LabelMap.get r);
    if not none then Format.fprintf ppf "@ (+others)";
    if some then Format.fprintf ppf " ..";
  and do_print_regexp pri ppf = function
    | Pretty.Empty ->  Format.fprintf ppf "Empty" (*assert false *)
    | Pretty.Epsilon -> ()
    | Pretty.Seq (Pretty.Trans { def = [ Char _ ] }, _) as r->
	(match extract_string [] r with
	  | s, None ->
	      Format.fprintf ppf "'";
	      List.iter (Chars.V.print_in_string ppf) s;
	      Format.fprintf ppf "'"
	  | s, Some r ->
            opar ppf ~level:lv_seq pri;
	    Format.fprintf ppf "'";
	    List.iter (Chars.V.print_in_string ppf) s;
	    Format.fprintf ppf "' %a" (do_print_regexp lv_seq) r;
	    cpar ppf ~level:lv_seq pri)
    | Pretty.Seq (r1,r2) ->
      opar ppf ~level:lv_seq pri;
      Format.fprintf ppf "%a@ %a"
	(do_print_regexp lv_seq) r1
	(do_print_regexp lv_seq) r2;
      cpar ppf ~level:lv_seq pri
    | Pretty.Alt (r,Pretty.Epsilon) | Pretty.Alt (Pretty.Epsilon,r) ->
	Format.fprintf ppf "@[%a@]?" (do_print_regexp lv_post) r
    | Pretty.Alt (r1,r2) ->
      opar ppf ~level:lv_alt pri;
      Format.fprintf ppf "%a |@ %a"
	(do_print_regexp lv_alt) r1
	(do_print_regexp lv_alt) r2;
      cpar ppf ~level:lv_alt pri
    | Pretty.Star r ->
	Format.fprintf ppf "@[%a@]*" (do_print_regexp lv_post) r
    | Pretty.Plus r ->
	Format.fprintf ppf "@[%a@]+" (do_print_regexp lv_post) r
    | Pretty.Trans t ->
	do_print_slot pri ppf t
  and extract_string accu = function
    | Pretty.Seq (Pretty.Trans { def = [ Char c ] }, r) ->
	extract_string (c :: accu) r
    | Pretty.Trans { def = [ Char c ] } ->
	(List.rev (c :: accu), None)
    | r -> (List.rev accu,Some r)


  let get_name = function
      | { state = `Named n } -> n
    | _ -> assert false

  let pp_type ppf t =
    let t = uniq t in
    let t = prepare t in
    assign_name t;
    Format.fprintf ppf "@[@[%a@]" (do_print_slot lv_min) t;
    (match List.rev !to_print with
       | [] -> ()
       | s::t ->
	   Format.fprintf ppf
	     " where@ @[<v>%a = @[%a@]" U.print (get_name s)
	   (do_print_slot_real lv_min) s.def;
	   List.iter
	     (fun s ->
		Format.fprintf ppf " and@ %a = @[%a@]"  U.print
		  (get_name s) (do_print_slot_real lv_min) s.def)
	     t;
	   Format.fprintf ppf "@]"
    );
    Format.fprintf ppf "@]";
    count_name := 0;
    to_print := [];
    DescrHash.clear memo

  let pp_noname ppf t =
    let old_named = !named in
    let old_named_xml = !named_xml in
    unregister_global t;
    pp_type ppf t;
    named := old_named;
    named_xml := old_named_xml

  let pp_node ppf n = pp_type ppf (descr n)

  let () = forward_print := pp_type

  let string_of_type t = Utils.string_of_formatter pp_type t
  let string_of_node t = Utils.string_of_formatter pp_node t
  let printf = pp_type Format.std_formatter

end

module Service =
struct
  type service_attributs = {
    mutable const : bool;
    mutable end_suffix : bool;
    mutable file : bool
  }
  let prepare t =
    let t = Print.uniq t in
    let t = Print.prepare t in
    Print.assign_name t;
    t;;

  let trace msg =
    (* output_string stderr (msg ^ "\n");
	flush stderr *)
    ();;

  let print_to_string f =
    let b = Buffer.create 1024 in
    let ppf = Format.formatter_of_buffer b in
    f ppf;
    Format.pp_print_flush ppf ();
    Buffer.contents b

  let get_gname (cu,n) =
    Ns.QName.to_string n;;

  let get_gtype t =
    get_gname t;;

(* from ns:atom, returns :atom. *)
  let strip_namespace tagname =
    let len = String.length tagname in
    let cur = ref len in
    for i = 0 to (len - 1) do
      let c = String.get tagname i in
      match c with
	| ':' -> cur := i
	| _ -> ()
    done;
    if !cur = len then
      tagname
    else
      String.sub tagname !cur (len - !cur);;

  let convert_gtype t name =
    match t with
      | "Int" -> TInt(name)
      | "String" -> TString(name)
      | "Float" -> TFloat(name)
      | "Bool" -> TBool(name)
      | _ -> assert false;;

  let rec convert (s : Print.nd) name =
    trace ("debug:convert: " ^ name);
    match s.Print.state with
      | `Named n -> trace ("debug:convert " ^ (U.to_string n)) ;
	  convert_real name s.Print.def
      | `GlobalName n ->
	  let t = get_gtype n in
	  trace("debug:convert:globalname: " ^ t);
	  (match t with
	    | "Int" | "String" | "Float" | "Bool"
		-> convert_gtype t name
	    | _ -> convert_real name s.Print.def)
      | _ -> convert_real name s.Print.def
  and convert_real name def =
    let rec aux = function
      | [] -> trace ("debug:convert_real:" ^ name); assert false
      | [ h ] -> convert_expr name h
      | h :: t -> assert false
    in
    aux def
  and convert_expr name = function
    | Print.Neg { Print.def = [] } -> assert false
    | Print.Neg t -> convert t name
    | Print.Abs t -> convert t name
    | Print.Name n -> assert false
    | Print.Char c -> assert false
    | Print.Regexp r -> convert_regexp name r
    | Print.Xml (tag,attr,t) ->
      let flags = { const = false; end_suffix = false; file = false } in
	(convert_attrs flags attr;
	let tagname = convert_tag tag in
	let tagname = strip_namespace tagname in
	match tagname with
	  | ":suffix" -> TSuffix(true,(convert t tagname))
	  | ":any" -> TAny
	  | _ -> (if flags.const then
	      TConst tagname
	    else
	      if flags.end_suffix then
		TESuffix tagname
	      else
		if flags.file then
		  TFile tagname
		else
		  convert t tagname)
	)
    | _ -> assert false
  and convert_regexp name = function
    | Pretty.Seq (r1,r2) ->
	TProd((convert_regexp name r1),(convert_regexp name r2))
    | Pretty.Alt (r,Pretty.Epsilon) | Pretty.Alt (Pretty.Epsilon,r) ->
	  TOption((convert_regexp name r))
    | Pretty.Alt (r1,r2) ->
	TSum((convert_regexp name r1), (convert_regexp name r2))
    | Pretty.Star r -> TList(name,(convert_regexp name r))
    | Pretty.Plus r -> TList(name,(convert_regexp name r))
    | Pretty.Trans t -> convert t name
    | Pretty.Epsilon | Pretty.Empty -> TUnit
  and convert_tag =
    function
      | `Tag s -> print_to_string s
      | `Type t -> assert false
  and convert_attrs flags =
    trace "convert_attrs";
    function
      | { Print.state = `Marked|`Expand|`None;
	def = [ Print.Record (r,some,none) ] } ->
	  convert_record flags (r,some,none)
      | { Print.state = `Named n;
	def = [ Print.Record (r,some,none) ] } ->
	  trace ("debug:convert_attrs:Named "
	  ^ (U.to_string n));
	  convert_record flags (r,some,none)
	    (*	  convert_real name s.Print.def *)
	    (*      | `GlobalName n -> get_gtype n name *)
      | _ -> trace "convert_attrs:_"; ()
  and convert_record flags (r,some,none) =
    List.iter
      (fun (l,(o,t)) ->
	(*	let opt = if o then "?" else "" in *)
	let attr_label = Label.string_of_attr l in
	trace ("convert_record:" ^ attr_label);
	match attr_label with
	  | "const" -> flags.const <- true
	  | "end_suffix" -> flags.end_suffix <- true
	  | "file" -> flags.file <- true
	  | _ -> output_string stderr
	      ("Bad attribute name:" ^ attr_label ^ "\n")
	  (*	  Label.print_attr l opt (do_print_slot 0) t *)
      ) (LabelMap.get r);
    if not none then output_string stderr " (+others)";
    if some then output_string stderr " ..";;

  let clear () =
    Print.count_name := 0;
    Print.to_print := [];
    DescrHash.clear Print.memo;;

  let to_service_params t =
    Print.unregister_global t;
    let s = prepare t in
    let ret = convert s "" in
    clear ();
    ret;;

  let to_string t =
    let bool_to_string = function
      | true -> "true"
      | false -> "false"
    in
    let rec aux = function
      | TInt n -> "TInt(" ^ n ^ ")"
      | TFloat n -> "TFloat(" ^ n ^ ")"
      | TBool n -> "TBool(" ^ n ^ ")"
      | TString n -> "TString(" ^ n ^ ")"
      | TConst n -> "TConst(" ^ n ^ ")"
      | TProd (e1, e2) -> "TProd(" ^ (aux e1) ^ "," ^ (aux e2) ^ ")"
      | TOption e -> "TOption(" ^ (aux e) ^ ")"
      | TSet e -> "TSet(" ^ (aux e) ^ ")"
      | TList (n,e) -> "TList(" ^ n ^ "," ^ (aux e) ^ ")"
      | TUnit -> "TUnit()"
      | TSum (e1, e2) -> "TSum(" ^ (aux e1) ^ "," ^ (aux e2) ^ ")"
      | TSuffix (b,e) -> "TSuffix(" ^ (bool_to_string b) ^ "," ^ (aux e) ^ ")"
      | TESuffix n -> "TESuffix(" ^ n ^ ")"
      | TFile n -> "TFile(" ^ n ^ ")"
      | TAny -> "TAny"
      | _ -> " unknown "
    in aux t;;
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 (`Atm (Pair.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 (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
	BoolPair.empty (Product.normal ~kind:`XML d)
    in
    let record = d.record
    in
    define n { d with times = times; xml = xml; record = record };
    n

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

let rec tuple = function
  | [t1;t2] -> times t1 t2
  | t::tl -> times t (cons (tuple tl))
  | _ -> assert false

let rec_of_list o l =
  let map =
    LabelMap.from_list (fun _ _ -> assert false)
      (List.map
	 (fun (opt,qname,typ) ->
	    qname, cons (if opt then Record.or_absent typ else typ))
	 l)
  in
  record_fields (o,map)

let empty_closed_record = rec_of_list false []
let empty_open_record = rec_of_list true []

let cond_partition univ qs =
  let rec add accu (t,s) =
    let t = if subtype t s then t else cap t s in
    if (subtype s t) || (is_empty t) then accu else
      let rec aux accu u =
	let c = cap u t in
	if (is_empty c) || (subtype (cap u s) t) then u::accu
	else c::(diff u t)::accu
      in
      List.fold_left aux [] accu
  in
  List.fold_left add [ univ ] qs

module Positive = struct
  module T = struct
    type t = descr
    let any = any
    let empty = empty
    let cup = cup
    let cap = cap
    let any = any
    let diff = diff
    let arrow = arrow
    let times = times
    let abstract = abstract
    let cons = cons
  end

  type rhs = [
    |`Type of descr
    |`Variable of Var.var
    |`Neg of v
    |`Cup of v list
    |`Cap of v list
    |`Arrow of v * v
    |`Times of v * v
    |`Xml of v * v
    |`Record of bool * (bool * Ns.Label.t * v) list
  ]
  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
      |`Variable d -> var d
	|`Cup vl -> List.fold_left (fun acc v -> cup acc (make_descr seen v)) empty vl
	|`Cap vl -> List.fold_left (fun acc v -> cap acc (make_descr seen v)) any vl
	|`Times (v1,v2) -> times (make_node v1) (make_node v2)
	|`Arrow (v1,v2) -> arrow (make_node v1) (make_node v2)
	|`Xml (v1,v2) -> xml (make_node v1) (make_node v2)
      |`Record (b, flst) -> rec_of_list b (List.map (fun (b,l,v) -> (b,l,make_descr seen v)) flst)
      |`Neg v -> neg (make_descr seen v)

  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

(* We shadow the corresponding definitions in the outer module *)
  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 var d = cons (`Variable d)
  let neg v = cons (`Neg v)
  let cup = function [ v ] -> v | vl -> cons (`Cup vl)
  let cap vl = cons (`Cap vl)
  let times v1 v2 = cons (`Times (v1,v2))
  let arrow v1 v2 = cons (`Arrow (v1,v2))
  let xml v1 v2 = cons (`Xml (v1,v2))
  let interval i = ty (interval i)
  let char c = ty (char c)
  let atom a = ty (atom a)
  let abstract a = ty (abstract a)
  let record b vlst = cons (`Record (b, vlst))
  let define v1 v2 = def v1 (`Cup [v2])

  let decompose t =
    let memo = DescrHash.create 17 in
    let decompose_conj f_atom sign ilist acc =
      List.fold_left (fun acc e ->
        let ne = f_atom e in
        (sign ne) :: acc) acc ilist
    in
    let decompose_dnf t_any f_atom dnf acc =
      List.fold_left (fun acc (ipos, ineg) ->
        match
          decompose_conj f_atom neg ineg
          @@ decompose_conj f_atom (fun x -> x) ipos [t_any]
        with
        | [v] -> v::acc
        | l -> (cap l) :: acc) acc dnf
    in
    let or_var f = function
      |(`Var _) as v -> var v
      |`Atm a -> f a
    in
    let decompose_kind any make dnf acc =
      decompose_dnf (ty any) (or_var make) dnf acc
    in
    let rec decompose_bdd any make dnf acc =
      decompose_kind any (fun bdd ->
        cup (decompose_dnf (ty any) (fun (x,y) ->
          let x = descr x
          and y = descr y in
          make
            (decompose_type x)
            (decompose_type y)
        ) (Pair.get bdd) [])) dnf acc
    and format_rec b acc = function
      | (l, t) :: rest -> format_rec b (acc @ [b, l, decompose_type (descr t)]) rest
      | [] -> acc
    and decompose_rec any make dnf acc =
      decompose_kind any (fun bdd ->
        cup (decompose_dnf (ty any) (fun (b, l) ->
	  make b (format_rec b [] (LabelMap.get l))) (Rec.get bdd) [])) dnf acc
    and decompose_type t =
      try
        DescrHash.find memo t
      with
        Not_found ->
          let node_t = forward () in
          if no_var t then ty t
          else
            let () = DescrHash.add memo t node_t in
            let descr_t =
              decompose_kind Atom.any atom (BoolAtoms.get t.atoms)
              @@ decompose_kind Int.any interval (BoolIntervals.get t.ints)
              @@ decompose_kind Char.any char (BoolChars.get t.chars)
              @@ decompose_bdd Product.any times (BoolPair.get t.times)
              @@ decompose_bdd Product.any_xml xml (BoolPair.get t.xml)
              @@ decompose_bdd Arrow.any arrow (BoolPair.get t.arrow)
              @@ decompose_rec Record.any record (BoolRec.get t.record)
              @@ decompose_kind Abstract.any abstract (BoolAbstracts.get t.abstract) []
            in
            node_t.def <- (cup descr_t).def; node_t
    in
    decompose_type t

  let solve v = internalize (make_node v)
  module MemoHash = Hashtbl.Make(
    struct
      type t = v
      let hash = Hashtbl.hash
      let equal u v = u == v
    end )

  let substitute_aux delta v subst =
    let memo = MemoHash.create 17 in
    let rec aux v subst =
      try
        MemoHash.find memo v
      with
        Not_found -> begin
          let node_v = forward () in
          MemoHash.add memo v node_v;
          let new_v =
            match v.def with
            |`Type d -> `Type d
            |`Variable d when Var.Set.mem d delta -> v.def
            |`Variable d -> (subst d).def
            |`Cup vl -> `Cup (List.map (fun v -> aux v subst) vl)
            |`Cap vl -> `Cap (List.map (fun v -> aux v subst) vl)
            |`Times (v1,v2) -> `Times (aux v1 subst, aux v2 subst)
            |`Arrow (v1,v2) -> `Arrow (aux v1 subst, aux v2 subst)
            |`Xml (v1,v2) -> `Xml (aux v1 subst, aux v2 subst)
            |`Record (b, flst) ->
              `Record (b, List.map (fun (b,l,v) -> (b,l,aux v subst)) flst)
            |`Neg v -> `Neg (aux v subst)
          in
          node_v.def <- new_v;
          node_v
        end
    in
    aux v subst

  let pp ppf v =
    let id = ref 0 in
    let memo = MemoHash.create 17 in
    let rec aux ppf v =
      try
        let s = MemoHash.find memo v in
        Format.fprintf ppf "%s" s
      with Not_found -> begin
        let node_name = Printf.sprintf "X_%i" !id in
        incr id;
        MemoHash.add memo v node_name;
        match v.def with
        |`Type d -> Format.fprintf ppf "`Type(%a)" Print.pp_type d
        |`Variable d -> Format.fprintf ppf "`Var(%a)" Var.pp d
        |`Cup vl -> Format.fprintf ppf "`Cup(%a)" (Utils.pp_list aux) vl
        |`Cap vl -> Format.fprintf ppf "`Cap(%a)" (Utils.pp_list aux) vl
        |`Times (v1,v2) -> Format.fprintf ppf "`Times(%a,%a)" aux v1 aux v2
        |`Arrow (v1,v2) -> Format.fprintf ppf "`Arrow(%a,%a)" aux v1 aux v2
        |`Xml (v1,v2) -> Format.fprintf ppf "`Xml(%a,%a)" aux v1 aux v2
        |`Record _ -> Format.fprintf ppf "`Record"
        |`Neg v -> Format.fprintf ppf "`Neg(%a)" aux v
      end
    in
    aux ppf v

  let printf = pp Format.std_formatter
  let dump ppf t = pp ppf (decompose t)

  (* returns a recursive type where all occurrences of alpha n t
   * are substituted with a recursive variable X *)
  let substituterec t alpha =
    let subst x d =
      if Var.equal d alpha then x
      else var d
    in
    if no_var t then t
    else begin
      let x = forward () in
      define x (substitute_aux Var.Set.empty (decompose t) (subst x));
      descr(solve x)
    end

  (* Pre-condition : alpha \not\in \delta *)
  let substitute t (alpha,s) =
    if no_var t then t
    else begin
      let subst s d = if Var.equal d alpha then s else var d in
      let new_t = (substitute_aux Var.Set.empty (decompose t) (subst (ty s))) in
      descr (solve new_t)
    end

  let substitutefree delta =
    let idx = ref 0 in
    fun t -> if no_var t then t else
    let h = Hashtbl.create 17 in
    let subst h d =
      try Hashtbl.find h d
      with Not_found -> begin
        let id = Printf.sprintf "_%s_%d" (Var.id d) !idx in
        let x = var (Var.mk ~repr:(Var.id d) id) in
        incr idx;
        Hashtbl.add h d x ;
        x
      end
    in
    let dec = decompose t in
    let new_t = substitute_aux delta dec (subst h) in
    descr (solve new_t)

  (* We cannot use the variance annotation of variables to simplify them,
     since variables are shared amongst types. If we have two types
     A -> A and (A,A) (produced by the algorithm) then we can still simplify the
     latter but the variance annotation tells us that A is invariant.  *)
  let collect_variables delta v =
    (* we memoize based on the pair (pos, v), since v can occur both
       positively and negatively.  and we want to manage the variables
       differently in both cases. We do not need to memoize on delta as
       the memoization is local and delta does not change *)
    let module Memo =
      Hashtbl.Make (struct
        type t = bool * v
        let hash = Hashtbl.hash
        let equal (a,b) (c,d) = a == c && b == d
      end)
    in
    let rec freshvar idx =
      let rec pretty i acc =
        let ni,nm = i/26, i mod 26 in
        let acc = acc ^ (String.make 1 (OldChar.chr (OldChar.code 'a' + nm))) in
        if ni == 0 then acc else pretty ni acc
      in
      let x = Var.mk (pretty !idx "") in
      if Var.Set.mem x delta then (incr idx; freshvar idx) else x
    in
    let vars = Hashtbl.create 17 in
    let memo = Memo.create 17 in
    let t_emp = cup [] in
    let t_any = cap [] in
    let idx = ref 0 in
    let rec aux pos v =
      if not (Memo.mem memo (pos, v)) then
        let () = Memo.add memo (pos,v) () in
        match v.def with
        |`Type d -> ()
        |`Variable d when Var.Set.mem d delta || (not (Var.is_internal d) && not pos) -> Hashtbl.replace vars d v
        |`Variable d ->
          begin try
            let td = Hashtbl.find vars d in
            (* polarity conflict, replace the binding by a new, pretty-printed variable *)
            if ((td == t_emp) && not pos) || ((td == t_any) && pos)
            then Hashtbl.replace vars d (var(freshvar idx))
          (* first time we see a variable, set to empty for covariant and
             any for contravariant *)
          with Not_found -> Hashtbl.add vars d (if pos then t_emp else t_any) end
        |`Cup vl | `Cap vl -> List.iter (fun v -> aux pos v) vl
        |`Times (v1,v2) | `Xml (v1, v2) ->  (aux pos v1); (aux pos v2)
        |`Arrow (v1,v2) ->  (aux (not pos) v1); (aux pos v2)
        |`Record (_, flst) -> List.iter (fun (_,_,v) -> aux pos v) flst
        |`Neg v -> (aux (not pos) v)
    in
    aux true v;
    vars

  let clean_variables delta t =
    if no_var t then t
    else begin
      let dec = decompose t in
      let h = collect_variables delta dec in
      let new_t =
        substitute_aux delta dec (fun d ->
          try Hashtbl.find h d
          with Not_found -> assert false
        )
      in
      descr (solve new_t)
    end

  let clean_type delta t =
    if no_var t then t else
      clean_variables delta t


end

module Tallying = struct

  type constr =
    |Pos of (Var.var * s) (** alpha <= t | alpha \in P *)
    |Neg of (s * Var.var) (** t <= alpha | alpha \in N *)

  exception UnSatConstr of string

  module CS = struct

    (* we require that types are semantically equivalent and not structurally
     * equivalent *)
    let semantic_compare t1 t2 =
      if Descr.equal t1 t2 then 0
      else if equiv t1 t2 then 0
      else Descr.compare t1 t2

    (* constraint set : map to store constraints of the form (s <= alpha <= t) *)
    module M = struct

      module Key = struct
        type t = Var.var
        let compare v1 v2 = Var.compare v1 v2
      end
      type key = Key.t
      module VarMap =  Map.Make(Key)
      type t = (Descr.s * Descr.s) VarMap.t
      let singleton = VarMap.singleton
      let cardinal = VarMap.cardinal

      (* a set of constraints m1 subsumes a set of constraints m2,
         that is the solutions for m1 contains all the solutions for
         m2 if:
         forall i1 <= v <= s1 in m1,
         there exists i2 <= v <= s2 in m2 such that i1 <= i2 <= v <= s2 <= s1
      *)
      let subsumes map1 map2 =
        VarMap.for_all (fun v (i1, s1) ->
          try let i2, s2 = VarMap.find v map2 in
              subtype i1 i2 && subtype s2 s1
          with Not_found -> false
        ) map1

      let pp ppf map =
        Utils.pp_list ~delim:("{","}") (fun ppf (v, (i,s)) ->
          Format.fprintf ppf "%a <= %a <= %a" Print.pp_type i Var.pp v Print.pp_type s
        ) ppf (VarMap.bindings map)

      let compare map1 map2 =
        VarMap.compare (fun (i1,s1) (i2,s2) ->
          let c = semantic_compare i1 i2 in
          if c == 0 then semantic_compare s1 s2
          else c) map1 map2

      let add delta v (inf, sup) map =
        let new_i, new_s =
          try
            let old_i, old_s = VarMap.find v map in
            cup old_i inf,
            cap old_s sup
          with
            Not_found -> inf, sup
        in
        if Var.Set.mem v delta then map
          (* if ((equal inf empty) && (equal sup any)) ||
             (equal (var v) inf && equal (var v) sup) then
               map
          else
            raise (UnSatConstr (Format.sprintf "%s is a monomorphic variable" (Utils.string_of_formatter Var.pp v)))
          *)
        else
          VarMap.add v (new_i, new_s) map

      let inter delta map1 map2 = VarMap.fold (add delta) map1 map2
      let fold = VarMap.fold
      let empty = VarMap.empty

    end

    (* equation set : (s < alpha < t) stored as
     * { alpha -> ((s v beta) ^ t) } with beta fresh *)
    module E = struct
      include Map.Make(struct
        type t = Var.var
        let compare = Var.compare
      end)

      let pp ppf e =
          Utils.pp_list ~delim:("{","}") (fun ppf -> fun (v,t) ->
            Format.fprintf ppf "%a = %a@," Var.pp v Print.pp_type t
          ) ppf (bindings e)

    end

    (* Set of equation sets *)
    module ES = struct
      include Set.Make(struct
        type t = Descr.s E.t
        let compare = E.compare semantic_compare
      end)

      let pp ppf s = Utils.pp_list ~delim:("{","}") E.pp ppf (elements s)
    end

    (* Set of constraint sets *)
    module S = struct
      (* A set of constraint-sets is just a list of constraint-sets,
         that are pairwise "non-subsumable"
      *)

      type t = M.t list

      let elements t = t

      let empty = []

      let add m l =
        let rec loop m l acc =
          match l with
            [] -> m :: acc
          | mm :: ll ->
            if M.subsumes m mm then List.rev_append ll (m::acc)
            else if M.subsumes mm m then List.rev_append ll (mm::acc)
            else loop m ll (mm::acc)
        in
        loop m l []

      let singleton m = add m empty

      let pp ppf s = Utils.pp_list ~delim:("{","}") M.pp ppf s

      let fold f l a = List.fold_left (fun e a -> f a e) a l

      let is_empty l = l == []

      (* Square union : *)
      let union s1 s2 =
        match s1, s2 with
          [], _ -> s2
        | _, [] -> s1
        | _ ->
          (* Invariant: all elements of s1 (resp s2) are pairwise
             incomparable (they don't subsume one another)
             let e1 be an element of s1:
             - if e1 subsumes no element of s2, add e1 to the result
             - if e1 subsumes an element e2 of s2, add e1 to the
             result and remove e2 from s2

             - if an element e2 of s2 subsumes e1, add e2 to the
             result and remove e2 from s2 (and discard e1)

             once we are done for all e1, add the remaining elements from
             s2 to the result.
          *)

          let append e1 s2 result =
            let rec loop s2 accs2 =
              match s2 with
                [] -> accs2, e1::result
              | e2 :: ss2 ->
                if M.subsumes e1 e2 then List.rev_append ss2 accs2, e1::result
                else if M.subsumes e2 e1 then List.rev_append ss2 accs2, e2::result
                else loop ss2 (e2::accs2)
            in
            loop s2 []
          in
          let rec loop s1 s2 result =
            match s1 with
              [] -> List.rev_append s2 result
            | e1 :: ss1 ->
              let new_s2, new_result = append e1 s2 result in
              loop ss1 new_s2 new_result
          in
          loop s1 s2 []

      (* Square intersection *)
      let inter delta s1 s2 =
        match s1,s2 with
          [], _ | _, [] -> []
        | _ ->
          (* Perform the cartesian product. For each constraint m1 in s1,
             m2 in s2, we add M.inter m1 m2 to the result.
             Optimisations:
             - we use add to ensure that we do not add something that subsumes
               a constraint set that is already in the result
             - if m1 subsumes m2, it means that whenever m2 holds, so does m1, so
             we only add m2 (note that the condition is reversed w.r.t. union).
          *)
          fold (fun m1 acc1 ->
            fold (fun m2 acc2 ->
              let merged = if M.subsumes m1 m2 then m2
                else if M.subsumes m2 m1 then m1
                else M.inter delta m1 m2
              in
              add merged acc2
            )
              s2 acc1) s1 []

    end

    type s = S.t
    type m = M.t
    type es = ES.t
    type sigma = Descr.s E.t
    module SUB = SortedList.FiniteCofinite(struct
      type t = Descr.s E.t
      let compare = E.compare compare
      let equal = E.equal equal
      let hash = Hashtbl.hash
      let dump = E.pp
      let check _ = ()
    end)

    type sl = sigma list

    let singleton delta c =
      let constr, do_check, t1, t2 =
        match c with
        |Pos (v,s) ->
          if Var.Set.mem v delta then M.empty, true, (var v), s
          else M.singleton v (empty,s), false, empty, empty
        |Neg (s,v) ->
          if Var.Set.mem v delta then M.empty, true, s, (var v)
          else M.singleton v (s,any), false, empty, empty
      in
      let res = S.singleton constr in
      if do_check then
          if subtype t1 t2 then res
          else
            raise (UnSatConstr
                     (Format.sprintf
                        "Constraint (%s) <= (%s) on monomorphic variable failed"
                        (Utils.string_of_formatter Print.pp_type t1)
                        (Utils.string_of_formatter Print.pp_type t2)
                     ))
      else res

    let pp_s = S.pp
    let pp_m = M.pp
    let pp_e = E.pp
    let pp_sl ppf ll = Utils.pp_list ~delim:("{","}") E.pp ppf ll

    let sat = S.singleton M.empty
    let unsat = S.empty

    let union = S.union
    let prod delta = S.inter delta
    let merge delta = M.inter delta
  end

  let normatoms (t,_,_) = if Atoms.is_empty t then CS.sat else CS.unsat
  let normchars (t,_,_) = if Chars.is_empty t then CS.sat else CS.unsat
  let normints (t,_,_) = if Intervals.is_empty t then CS.sat else CS.unsat
  let normabstract (t,_,_) = if Abstracts.is_empty t then CS.sat else CS.unsat

  let single_aux constr (b,v,p,n) =
    let aux f constr l =
      List.fold_left (fun acc ->
        function
          |`Var a -> cap acc (f(var (`Var a)))
          |`Atm a -> cap acc (f(constr a))
      ) any l
    in
    let id = (fun x -> x) in
    let t = cap (aux id constr p) (aux neg constr n) in
    (* t = bigdisj ... alpha \in P --> alpha <= neg t *)
    (* t = bigdisj ... alpha \in N --> t <= alpha *)
    if b then (neg t) else t

  let single_atoms = single_aux atom

  let single_abstract = single_aux abstract

  let single_chars = single_aux char

  let single_ints = single_aux interval

  let single_times = single_aux (fun p -> { empty with times = BoolPair.atom (`Atm p) })

  let single_xml = single_aux (fun p -> { empty with xml = BoolPair.atom (`Atm p) })

  let single_record = single_aux (fun p -> { empty with record = BoolRec.atom (`Atm p) })

  let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })

  (* check if there exists a toplevel varaible : fun (pos,neg) *)
  let toplevel delta single norm_rec mem p n = match (p,n) with
    |([],(`Var x)::neg) ->
        let t = single (false,x,[],neg) in
        CS.singleton delta (Neg (t,`Var x))

    |((`Var x)::pos,[]) ->
        let t = single (true,x,pos,[]) in
        CS.singleton delta (Pos (`Var x,t))

    |((`Var x)::pos, (`Var y)::neg) ->
        if Var.compare (`Var x) (`Var y) < 0 then
          let t = single (true,x,pos,n) in
          CS.singleton delta (Pos (`Var x,t))
        else
          let t = single (false,y,p,neg) in
          CS.singleton delta (Neg (t,`Var y))

    |([`Atm a], (`Var x)::neg) ->
        let t = single (false,x,p,neg) in
        CS.singleton delta (Neg (t,`Var x))

    |([`Atm t], []) -> norm_rec (t,delta,mem)
    |_,_ -> assert false

  let big_prod delta f acc l =
    List.fold_left (fun acc (pos,neg) ->
      (* if CS.S.is_empty acc then acc else *)
        CS.prod delta acc (f pos neg)
    ) acc l

  (* norm generates a constraint set for the costraint t <= 0 *)
  let rec norm (t,delta,mem) =
    (* if we already evaluated it, it is sat *)
    if DescrSet.mem t mem || is_empty t then begin
      (*Format.printf "Sat for type %a\n%!" Print.print t; *)
      CS.sat end
    else begin
      (* if there is only one variable then is it A <= 0 or 1 <= A *)
      if is_var t then
        let (v,p) = extract_variable t in
        if Var.Set.mem v delta then CS.unsat
        else
          let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
          CS.singleton delta s
      (* if there are no vars, and it is not empty then unsat *)
      else if no_var t then CS.unsat
      else begin
        let mem = DescrSet.add t mem in
        let aux single norm_aux acc l = big_prod delta (toplevel delta single norm_aux mem) acc l in

        let acc = aux single_atoms normatoms CS.sat (BoolAtoms.get t.atoms) in
        let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
        let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
        let acc = aux single_times normpair acc (BoolPair.get t.times) in
        let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
        let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
        let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
        (* XXX normrec is not tested at all !!! *)
        aux single_record normrec acc (BoolRec.get t.record)
      end
    end

  (* (t1,t2) = intersection of all (fst pos,snd pos) \in P
   * (s1,s2) \in N
   * [t1] v [t2] v ( [t1 \ s1] ^ [t2 \ s2] ^
   * [t1 \ s1 \ s1_1] ^ [t2 \ s2 \ s2_1 ] ^
   * [t1 \ s1 \ s1_1 \ s1_2] ^ [t2 \ s2 \ s2_1 \ s2_2 ] ^ ... )
   *
   * prod(p,n) = [t1] v [t2] v prod'(t1,t2,n)
   * prod'(t1,t2,{s1,s2} v n) = ([t1\s1] v prod'(t1\s1,t2,n)) ^
   *                            ([t2\s2] v prod'(t1,t2\s2,n))
   * *)
  and normpair (t,delta,mem) =
    let norm_prod pos neg =
      let rec aux t1 t2 = function
        |[] -> CS.unsat
        |(s1,s2) :: rest -> begin
            let z1 = diff t1 (descr s1) in
            let z2 = diff t2 (descr s2) in
            let con1 = norm (z1, delta, mem) in
            let con2 = norm (z2, delta, mem) in
            let con10 = aux z1 t2 rest in
            let con20 = aux t1 z2 rest in
            let con11 = CS.union con1 con10 in
            let con22 = CS.union con2 con20 in
            CS.prod delta con11 con22
        end
      in
      (* cap_product return the intersection of all (fst pos,snd pos) *)
      let (t1,t2) = cap_product any any pos in
      let con1 = norm (t1, delta, mem) in
      let con2 = norm (t2, delta, mem) in
      let con0 = aux t1 t2 neg in
      CS.union (CS.union con1 con2) con0
    in
    big_prod delta norm_prod CS.sat (Pair.get t)

  and normrec (t,delta,mem) =
    let norm_rec ((oleft,left),rights) =
      let rec aux accus seen = function
        |[] -> CS.sat
        |(false,_) :: rest when oleft -> aux accus seen rest
        |(b,field) :: rest ->
            let right = seen @ rest in
            snd (Array.fold_left (fun (i,acc) t ->
              let di = diff accus.(i) t in
              let accus' = Array.copy accus in accus'.(i) <- di ;
              (i+1,CS.prod delta acc (CS.prod delta (norm (di,delta,mem)) (aux accus' [] right)))
            ) (0,CS.sat) field
            )
      in
      let c = Array.fold_left (fun acc t -> CS.union (norm (t,delta,mem)) acc) CS.sat left in
      CS.prod delta (aux left [] rights) c
    in
    List.fold_left (fun acc (_,p,n) ->
      if CS.S.is_empty acc then acc else CS.prod delta acc (norm_rec (p,n))
    ) CS.sat (get_record t)

  (* arrow(p,{t1 -> t2}) = [t1] v arrow'(t1,any \ t2,p)
   * arrow'(t1,acc,{s1 -> s2} v p) =
       ([t1\s1] v arrow'(t1\s1,acc,p)) ^
       ([acc ^ {s2}] v arrow'(t1,acc ^ {s2},p))

     t1 -> t2 \ s1 -> s2 =
       [t1] v (([t1\s1] v {[]}) ^ ([t2\s2] v {[]}))

     Bool -> Bool \ Int -> A =
       [Bool] v (([Bool\Int] v {[]}) ^ ([Bool\A] v {[]})

     P(Q v {a}) = {a} v P(Q) v {X v {a} | X \in P(Q) }
   *)
  and normarrow (t,delta,mem) =
    let rec norm_arrow pos neg =
      match neg with
      |[] -> CS.unsat
      |(t1,t2) :: n ->
          let con1 = norm (descr t1, delta, mem) in (* [t1] *)
          let con2 = aux (descr t1) (diff any (descr t2)) pos in
          let con0 = norm_arrow pos n in
          CS.union (CS.union con1 con2) con0
    and aux t1 acc = function
      |[] -> CS.unsat
      |(s1,s2) :: p ->
          let t1s1 = diff t1 (descr s1) in
          let acc1 = cap acc (descr s2) in
          let con1 = norm (t1s1, delta, mem) in (* [t1 \ s1] *)
          let con2 = norm (acc1, delta, mem) in (* [(Any \ t2) ^ s2] *)
          let con10 = aux t1s1 acc p in
          let con20 = aux t1 acc1 p in
          let con11 = CS.union con1 con10 in
          let con22 = CS.union con2 con20 in
          CS.prod delta con11 con22
    in
    big_prod delta norm_arrow CS.sat (Pair.get t)

  module NormMemoHash = Hashtbl.Make(
    struct
      type t = (Descr.t * Var.Set.t)
      let hash (v,d) = Descr.hash v + Var.Set.hash d
      let equal (v1,d1) (v2,d2) = Descr.equal v1 v2 && Var.Set.equal d1 d2
    end )

  let memo_norm = NormMemoHash.create 17
  let norm delta t =
    try NormMemoHash.find memo_norm (t,delta)
    with Not_found -> begin
      let res = norm (t,delta,DescrSet.empty) in
      NormMemoHash.add memo_norm (t,delta) res; res
    end

  (* merge needs delta because it calls norm recursively *)
  let rec merge (m,delta,mem) =
    let res =
      CS.M.fold (fun v (inf, sup) acc ->
        (* no need to add new constraints *)
        if subtype inf sup then acc
        else
          let x = diff inf sup in
          if DescrHash.mem mem x then acc
          else begin
            DescrHash.add mem x ();
            let n =
              let n = norm delta x in if CS.S.is_empty n then raise (UnSatConstr "merge2") else n
            in
            let c1 = CS.prod delta (CS.S.singleton m) n in
            let c2 = CS.S.fold (fun m1 acc -> CS.union acc (merge (m1,delta,mem))) c1 CS.S.empty in
            CS.union c2 acc
          end) m CS.S.empty
    in
    if CS.S.is_empty res then CS.S.singleton m else res

  let merge delta m = merge (m,delta,DescrHash.create 17)

  (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)
  let solve s =
    let aux ((`Var v) as alpha) (s,t) acc =
      (* we cannot solve twice the same variable *)
      assert(not(CS.E.mem alpha acc));
      let pre = Printf.sprintf "#fr_%s_" (Var.id alpha) in
      let b = var (Var.fresh ~pre ()) in
      (* s <= alpha <= t --> alpha = ( s v fresh ) ^ t *)
      CS.E.add alpha (cap (cup s b) t) acc
    in
    let aux1 m =
      let cache = Hashtbl.create 17 in
      CS.M.fold (fun alpha (s,t) acc ->
        if Hashtbl.mem cache alpha then acc else begin
          Hashtbl.add cache alpha ();
              (* if t containts only a toplevel variable and nothing else
               * means that the constraint is of the form (alpha,beta). *)
          if is_var t then begin
            let (beta,_) = extract_variable t in
            let acc1 = aux beta (empty,any) acc in
                (* alpha <= beta --> { empty <= alpha <= beta ; empty <= beta <= any } *)
            aux alpha (s,t) acc1
          end else
            (* alpha = ( s v fresh) ^ t *)
            aux alpha (s,t) acc;
        end
      ) m CS.E.empty
    in
    CS.S.fold (fun m acc -> CS.ES.add (aux1 m) acc) s CS.ES.empty

  let unify e =
    let rec aux sol e =
      (* Format.printf "e = %a\n" CS.print_e e; *)
      if CS.E.is_empty e then sol
      else begin
        let (alpha,t) = CS.E.min_binding e in
        (* Format.printf "Unify -> %a = %a\n" Var.pp alpha Print.pp_type t; *)
        let e1 = CS.E.remove alpha e in
        (* Format.printf "e1 = %a\n" CS.print_e e1; *)
        (* remove from E \ { (alpha,t) } every occurrences of alpha
         * by mu X . (t{X/alpha}) with X fresh . X is a recursion variale *)
        (* substituterec remove also all previously introduced fresh variables *)
        let x = Positive.substituterec t alpha in
        (* Format.printf "X = %a %a %a\n" Var.pp alpha Print.print x dump t; *)
        let es =
          CS.E.fold (fun beta s acc ->
            CS.E.add beta (Positive.substitute s (alpha,x)) acc
          ) e1 CS.E.empty
        in
        (* Format.printf "es = %a\n" CS.print_e es; *)
        aux ((CS.E.add alpha x sol)) es
      end
    in
    (* Format.printf "Begin e = %a\n" CS.print_e e; *)
    let r = aux CS.E.empty e in
    (* Format.printf "r = %a\n" CS.print_e r; *)
    r

  exception Step1Fail
  exception Step2Fail

  let tallying delta l =
    let n =
      List.fold_left (fun acc (s,t) ->
        let d = diff s t in
        if is_empty d then CS.sat
        else if no_var d then CS.unsat
        else CS.prod delta acc (norm delta d)
      ) CS.sat l
    in
    if Pervasives.(n = CS.unsat) then raise Step1Fail else
    let m =
      CS.S.fold (fun c acc ->
        try CS.ES.union (solve (merge delta c)) acc
        with UnSatConstr _ -> acc
      ) n CS.ES.empty
    in
    if CS.ES.is_empty m then raise Step2Fail else
    let el =
      let dom e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
      CS.ES.fold (fun e acc ->
        let si = unify e in
        (* XXX maybe we can eliminate solution earlier. Is it safe to do it here ? *)
        (* it is a solution only if (dom(si) /\ delta = emptyset) *)
        if Var.Set.is_empty (Var.Set.inter (dom(si)) delta) then
          CS.ES.add si acc
        else acc
      ) m CS.ES.empty
    in
    (CS.ES.elements el)

  (* apply sigma to t *)
  let ($$) t si = CS.E.fold (fun v sub acc -> Positive.substitute acc (v,sub)) si t

  type symsubst = I | S of CS.sigma | A of (symsubst * symsubst)

  let rec dom = function
    |I -> Var.Set.empty
    |S si -> CS.E.fold (fun v _ acc -> Var.Set.add v acc) si Var.Set.empty
    |A (si,sj) -> Var.Set.union (dom si) (dom sj)

  (* composition of two symbolic substitution sets sigmaI, sigmaJ .
     Cartesian product *)
  let (++) sI sJ =
    let bind m f = List.flatten(List.map f m) in
    bind sI (fun si ->
      bind sJ (fun sj ->
        [A(si,sj)]
      )
    )

  (* apply a symbolic substitution si to a type t *)
  let (@@) t si =
    let vst = ref Var.Set.empty in
    let vsi = ref Var.Set.empty in
    let get e = CS.E.fold (fun v _ acc -> Var.Set.add v acc) e Var.Set.empty in
    let filter t si =
      vsi := get si;
      vst := all_vars t;
      not(Var.Set.is_empty (Var.Set.inter !vst !vsi))
    in
    let filterdiff t si sj =
      let vsj = get sj in
      not(Var.Set.is_empty (Var.Set.inter !vst (Var.Set.diff !vsi vsj)))
    in
    let rec aux t = function
      |I -> t
      |S si -> t $$ si
      |A (S si,_) when filter t si -> t $$ si
      |A (S si,S sj) when filterdiff t si sj -> (t $$ sj) $$ si
      |A (si,sj) -> aux (aux t sj) si
    in
    aux t si

  let domain sl =
    List.fold_left (fun acc si ->
      CS.E.fold (fun v _ acc ->
        Var.Set.add v acc
      ) si acc
    ) Var.Set.empty sl

  let codomain ll =
    List.fold_left (fun acc e ->
      CS.E.fold (fun _ v acc ->
        Var.Set.union (all_vars v) acc
      ) e acc
    ) Var.Set.empty ll

  let is_identity = List.for_all (CS.E.is_empty)

end

let set a i v =
  let len = Array.length !a in
  if i <  len then (!a).(i) <- v
  else begin
    let b = Array.make (2*len+1) empty in
    Array.blit !a 0 b 0 len;
    b.(i) <- v;
    a := b
  end
let get a i = if i < 0 then any else (!a).(i)

exception FoundSquareSub of Tallying.CS.sl

let squaresubtype delta s t =
  Tallying.NormMemoHash.clear Tallying.memo_norm;
  let ai = ref [| |] in
  let tallying i =
    try
      let s = get ai i in
      let sl = Tallying.tallying delta [ (s,t) ] in
      raise (FoundSquareSub sl)
    with
      Tallying.Step1Fail -> (assert (i == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
    | Tallying.Step2Fail -> () (* continue *)
  in
  let rec loop i =
    try
      let ss =
        if i = 0 then s
        else (cap (Positive.substitutefree delta s) (get ai (i-1)))
      in
      set ai i ss;
      tallying i;
      loop (i+1)
    with FoundSquareSub sl -> sl
  in
  loop 0

let is_squaresubtype delta s t =
  try ignore(squaresubtype delta s t);true with Tallying.UnSatConstr _ -> false

exception FoundApply of t * int * int * Tallying.CS.sl

(** find two sets of type substitutions I,J such that
    s @@ sigma_i < t @@ sigma_j for all i \in I, j \in J *)
let apply_raw delta s t =
  Tallying.NormMemoHash.clear Tallying.memo_norm;
  let gamma = var (Var.mk "Gamma") in
  let cgamma = cons gamma in
  (* cell i of ai contains /\k<=i s_k, cell j of aj contains /\k<=j t_k *)
  let ai = ref [| |]
  and aj = ref [| |] in
  let tallying i j  =
    try
      let s = get ai i in
      let t = arrow (cons (get aj j)) cgamma in
      let sl = Tallying.tallying delta [ (s,t) ] in
      let new_res =
        Positive.clean_type delta (
          List.fold_left (fun tacc si ->
            cap tacc (Tallying.(gamma $$ si))
          ) any sl
        )
      in
      raise (FoundApply(new_res,i,j,sl))
    with
      Tallying.Step1Fail -> (assert (i == 0 &&  j == 0); raise (Tallying.UnSatConstr "apply_raw step1"))
    | Tallying.Step2Fail -> () (* continue *)
  in
  let rec loop i =
    try
      (* Format.printf "Starting expansion %i @\n@." i; *)
      let (ss,tt) =
        if i = 0 then (s,t) else
        ((cap (Positive.substitutefree delta s) (get ai (i-1))),
         (cap (Positive.substitutefree delta t) (get aj (i-1))))
      in
      set ai i ss;
      set aj i tt;
      for j = 0 to i-1 do
        tallying j i;
        tallying i j;
      done;
      tallying i i;
      loop (i+1)
    with FoundApply (res, i, j, sl) -> sl, get ai i, get aj j, res
  in
  loop 0

let apply_full delta s t =
  let _,_,_,res = apply_raw delta s t in
  res

let squareapply delta s t = let s,_,_,res = apply_raw delta s t in (s,res)