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

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

  include SortedList.FiniteCofinite(T)
  let trivially_disjoint = disjoint
  let compute ~empty ~full ~cup ~cap ~diff ~atom b = assert false
  let get _ = assert false
  let iter _ = assert false

  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 ]

type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ =
  {
    atoms    : 'atoms;
    ints     : 'ints;
    chars    : 'chars;
    times    : 'times;
    xml      : 'xml;
    arrow    : 'arrow;
    record   : 'record;
    abstract : 'abstract;
    absent   : bool;
  }



module BoolAtoms = Bool.MakeVar(Atoms)
module BoolIntervals = Bool.MakeVar(Intervals)
module BoolChars = Bool.MakeVar(Chars)
module BoolAbstracts = Bool.MakeVar(Abstracts)

module rec Descr :
sig
  include Custom.T with
	    type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
		      BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_
  val empty: t
  val any : t
  val is_empty : t -> bool
end =
struct

  type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
	    BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_

  let dump ppf d =
    Format.fprintf ppf "@[<v 1>types:@\n\
@<1>    atoms: %a@\n\
@<1>     ints: %a@\n\
@<1>    chars: %a@\n\
@<1>    times: %a@\n\
@<1>    arrow: %a@\n\
@<1>   record: %a@\n\
@<1>      xml: %a@\n\
@<1> abstract: %a@\n\
@<1>   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;
  }

  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 : Bool.V with module Atom = Pair = Bool.MakeVar(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 : Bool.V with module Atom = Rec = Bool.MakeVar(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 dummy_print = (fun _ _ -> assert false)
let forward_print = ref dummy_print

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.var a;
  xml   = BoolPair.var a;
  arrow = BoolPair.var a;
  record= BoolRec.var a;
  ints  = BoolIntervals.var a;
  atoms = BoolAtoms.var a;
  chars = BoolChars.var a;
  abstract = BoolAbstracts.var 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) }

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)


(* perform some semantic simplifications around type constructors *)
let atom a =
  let atm =
  if Atoms.(is_empty (diff full a)) then
    BoolAtoms.full
  else BoolAtoms.atom (`Atm a)
  in
  { empty with atoms = atm }

let times x y =
  if subtype any x.Node.descr
    && subtype any y.Node.descr
  then
    { empty with times = BoolPair.full }
  else times x y

let xml x y =
  if subtype any x.Node.descr
    && subtype any y.Node.descr
  then
    { empty with xml = BoolPair.full }
  else xml x y

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 Iter =
  struct
    let any_node2 = any_node, any_node

    let compute ?(normalize=false) ~empty ~full ~cup ~cap ~diff ~var ~atom ~int ~char ~times ~xml ~arrow ~record ~abs ~opt t
      =
      let var_or f =
        function `Atm a -> f a
               | `Var v -> var v
      in
      let any_atom = atom Atoms.full in
      let any_int = int Intervals.full in
      let any_char = char Chars.full in
      let any_abs = abs Abstracts.full in
      let any_times = times any_node2 in
      let any_xml = xml any_node2 in
      let any_record = record (true,LabelMap.empty) in
      let any_arrow = diff full
          (List.fold_left cup any_atom
             [ any_int; any_char; any_abs; any_times; any_xml; any_record ])
      in
      let record_bdd p =
        Rec.compute ~empty ~full:any_record ~cup ~cap ~diff ~atom:record p
      in
      let prod_bdd kind p =
        let any,mk =
          match kind with
          `Times -> any_times, times
          | `Xml -> any_xml, xml
          | `Arrow -> any_arrow, arrow
        in
        if normalize && Pervasives.(kind <> `Arrow) then
          let rects =
            match kind with
              `Times -> Product.normal ~kind:`Normal { Descr.empty with times = BoolPair.atom (`Atm p) }
            | `Xml -> Product.normal ~kind:`XML { Descr.empty with xml = BoolPair.atom (`Atm p) }
            | _ -> assert false
          in
          List.fold_left (fun acc (d1, d2) -> cup acc (mk (cons d1, cons d2))) empty rects
        else
          Pair.compute ~empty ~full:any ~cup ~cap ~diff ~atom:mk p
      in
      List.fold_left (fun acc e -> cup acc e)
        (opt t.absent)
        [ (BoolAtoms.compute
             ~empty ~full:any_atom ~cup ~cap ~diff ~atom:(var_or atom) t.atoms);
          (BoolIntervals.compute
             ~empty ~full:any_int ~cup ~cap ~diff ~atom:(var_or int) t.ints);
          (BoolChars.compute
             ~empty ~full:any_char ~cup ~cap ~diff ~atom:(var_or char) t.chars);
          (BoolAbstracts.compute
             ~empty ~full:any_abs ~cup ~cap ~diff ~atom:(var_or abs) t.abstract);
          (BoolPair.compute
             ~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Times)) t.times);
          (BoolPair.compute
             ~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Xml)) t.xml);
          (BoolPair.compute
             ~empty ~full:any_arrow ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Arrow)) t.arrow);
          (BoolRec.compute
             ~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);]


    let simplify =
      let memo = DescrHash.create 17 in
      let aux (type atom)
          inj
          (module BV : Bool.V with type Atom.t = atom ) b
          =
        let clean b =
          if is_empty (inj b) then BV.empty else b
        in
        let rec loop b =
        match BV.extract b with
          `Split(`Var v, p, i , n) ->
            let p = loop p in
            let i = loop i in
            let n = loop n in
            let tp = inj p and tn = inj n in
            if disjoint tp tn then b
            else
              let v' = clean (BV.var v) in
              let p' = clean BV.(cap v' (diff p n)) in
              let n' = clean BV.(diff (diff n p) v') in
              let i' = clean (BV.cap n p) in
              let i'' = clean (BV.cup i i') in
              BV.(cup i'' (cup p' n'))

        | _ -> b
        in
        loop b
      in
      fun t ->
        try DescrHash.find memo t with
          Not_found ->
            let res =
              { t with
                atoms = aux (fun i -> { empty with atoms = i })
                  (module BoolAtoms) t.atoms;
                chars = aux (fun i -> { empty with chars = i })
                  (module BoolChars) t.chars;
                ints = aux (fun i -> { empty with ints = i })
                  (module BoolIntervals) t.ints;
                abstract = aux (fun i -> { empty with abstract = i })
                  (module BoolAbstracts) t.abstract;
                times = aux (fun i -> { empty with times = i })
                  (module BoolPair) t.times;
                xml = aux (fun i -> { empty with xml = i })
                  (module BoolPair) t.xml;
                arrow = aux (fun i -> { empty with arrow = i })
                  (module BoolPair) t.arrow;
                record = aux (fun i -> { empty with record = i })
                  (module BoolRec) t.record;
              }
            in
            DescrHash.add memo t res;
            DescrHash.add memo res res;
            res

    let compute_bdd ~typ ~cup ~cap ~neg ~var ~atoms ~ints ~chars ~times ~xml ~arrow ~record ~abstract ~absent t =
      let t = simplify t in
      let any_node2 = any_node, any_node in
      let any_atoms = atoms Atoms.full in
      let any_ints = ints Intervals.full in
      let any_chars = chars Chars.full in
      let any_abstract = abstract Abstracts.full in
      let any_times = times any_node2 in
      let any_xml = xml any_node2 in
      let any_record = record (true,LabelMap.empty) in
      let any_arrow = typ Arrow.any
        (*neg (cup ([ any_atoms;
                    any_ints; any_chars; any_abstract;
                    any_times; any_xml; any_record ])) *)
      in
      let var_or do_atom =
        function `Var v -> var v
        | `Atm atm -> do_atom atm
      in
      let simple_bdd (type bdd) (type atom)
          any
          do_atom
          (module B : Bool.S with type t = bdd and type elem = atom) acc bv =
        List.fold_left (fun acc (ipos, ineg) ->
          match List.map do_atom ipos, List.map do_atom ineg
          with
          | []  , [] -> any :: acc
          | [ e ] , [] -> e :: acc
          | [], l -> cap (any :: List.map neg l) :: acc
          | l1, l2 -> cap (l1 @ List.map neg l2) :: acc
        ) acc (B.get bv)
      in
      let cplx_bdd (type atom) (type atom2)
          any
          do_atom
          (module BV : Bool.V with type Atom.t = atom and type Atom.elem = atom2)
          acc
          bdd
          =
         simple_bdd (cap[]) (var_or (fun t -> cup (simple_bdd (any) do_atom (module BV.Atom) [] t)))
           (module BV) acc bdd
      in
      let acc = absent t.absent in
      let acc = simple_bdd any_ints (var_or ints) (module BoolIntervals) acc t.ints in
      let acc = simple_bdd any_atoms (var_or atoms) (module BoolAtoms) acc t.atoms in
      let acc = simple_bdd any_chars (var_or chars) (module BoolChars) acc t.chars in
      let acc = simple_bdd any_abstract (var_or abstract) (module BoolAbstracts) acc t.abstract in
      let acc = cplx_bdd any_times times (module BoolPair) acc t.times in
      let acc = cplx_bdd any_xml xml (module BoolPair) acc t.xml in
      let acc = cplx_bdd any_arrow arrow (module BoolPair) acc t.arrow in
      let acc = cplx_bdd any_record record (module BoolRec) acc t.record in
      match acc with
        [ e ] -> e
      | _ -> cup acc


  end

module Variable =
  struct
    type t = Var.t

    let var_cache = DescrHash.create 17
    let collect_vars t =
      let memo = DescrHash.create 17 in
      let union s1 s2 =
        match s1, s2 with
        Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
        | None, Some s | Some s, None -> Some s
        | _ -> None
      in
      let inter s1 s2 =
        match s1, s2 with
        Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
        | _ -> None
      in
      let union3 (x1,y1,z1) (x2,y2,z2) =
        union x1 x2, union y1 y2, union z1 z2
      in
      let inter3 (x1,y1,z1) (x2,y2,z2) =
        inter x1 x2, inter y1 y2, inter z1 z2
      in
      let empty = Some Var.Set.empty in
      let empty3 = empty,empty,empty in
      let no3 = None, None, None in
      let cst_empty3 _ = empty3 in
      let rec loop t =
        try
          DescrHash.find memo t
        with
        Not_found ->
          DescrHash.add memo t empty3;
          let res =
            Iter.compute ~normalize:true
              ~empty:no3
              ~full:empty3
              ~cup:union3
              ~cap:inter3
              ~diff:(fun (x1,y1,z1) (x2, y2, z2) ->
                  inter x1 x2, inter y1 z2, inter z1 y2)
              ~var:(fun v -> let e = Some (Var.Set.singleton v) in
                     e,e,empty)
              ~int:cst_empty3
              ~char:cst_empty3
              ~atom:cst_empty3
              ~abs:cst_empty3
              ~xml:prod
              ~times:prod
              ~arrow:arrow
              ~record:record
              ~opt:cst_empty3 t
          in
          DescrHash.replace memo t res;
          res
      and prod (t1, t2) =
        let _,y1,z1 = loop (descr t1)
        and _,y2,z2 = loop (descr t2) in
        empty, union y1 y2, union z1 z2
      and arrow (t1, t2) =
        let _,y1,z1 = loop (descr t1)
        and _,y2,z2 = loop (descr t2) in
        empty,  union z1 y2, union y1 z2
      and record (b, lm) =
        let _, y, z = List.fold_left (fun acc (_,t) ->
            union3 acc (loop (descr t))) empty3 (LabelMap.get lm)
        in
        empty, y, z
      in
      loop t

    let collect_vars2 t =
      let memo = DescrHash.create 17 in
      let empty3 = Var.Set.(empty,empty,empty) in
      let merge l =
        List.fold_left (fun (a1, a2, a3) (s1, s2, s3) ->
          Var.Set.(cup a1 s1, cup a2 s2, cup a3 s3))
          empty3 l
      in
      let cst_empty3 _ = empty3 in
      let rec loop t =
        try
          DescrHash.find memo t
        with
        Not_found ->
          DescrHash.add memo t empty3;
          let res =
            Iter.compute_bdd
              ~typ:cst_empty3
              ~cup:merge
              ~cap:merge
              ~neg:(fun (a, b, c) -> (a , c , b))
              ~var:(fun v -> let e = Var.Set.singleton v in
                     e,e,Var.Set.empty)
              ~ints:cst_empty3
              ~chars:cst_empty3
              ~atoms:cst_empty3
              ~abstract:cst_empty3
              ~xml:prod
              ~times:prod
              ~arrow:arrow
              ~record:record
              ~absent:(fun _ -> []) t
          in
          DescrHash.replace memo t res;
          res
      and prod (t1, t2) =
        let _,y1,z1 = loop (descr t1)
        and _,y2,z2 = loop (descr t2) in
        Var.Set.(empty, cup y1 y2, cup z1 z2)
      and arrow (t1, t2) =
        let _,y1,z1 = loop (descr t1)
        and _,y2,z2 = loop (descr t2) in
        Var.Set.(empty, cup z1 y2, cup y1 z2)
      and record (b, lm) =
        let _, y, z = merge (List.map (fun  (_,t) -> (loop (descr t))) (LabelMap.get lm))
        in
        Var.Set.empty, y, z
      in
      loop t


    let no_var t =
      let memo = DescrHash.create 17 in
      let rec loop t =
        try
          DescrHash.find memo t
        with
        Not_found ->
          DescrHash.add memo t ();
          Iter.compute_bdd
            ~typ:ignore
            ~cup:ignore
            ~cap:ignore
            ~neg:ignore
            ~var:(fun _ -> raise Not_found)
            ~ints:ignore
            ~chars:ignore
            ~atoms:ignore
            ~abstract:ignore
            ~xml:prod
            ~times:prod
            ~arrow:prod
            ~record:record
            ~absent:(fun _ -> []) t

      and prod (t1, t2) = loop (descr t1);
        loop (descr t2)
      and record (b, lm) =
        List.iter
          (fun  (_,t) -> (loop (descr t))) (LabelMap.get lm)
      in
      try
        loop t; true
      with Not_found -> false



    let collect_vars t =
      let _extract = function Some e -> e | None -> Var.Set.empty in
      try
        DescrHash.find var_cache t
      with Not_found ->
        let tlv, pos, neg = collect_vars2 t in
(*        let tlv, pos, neg = extract tlv, extract pos, extract neg in *)
        let res = tlv, pos, neg, Var.Set.cup pos neg in
        DescrHash.add var_cache t res;
        res

    let all_vars t =
      let _, _, _, all = collect_vars t in
      all

    let is_ground =
      let h = DescrHash.create 17 in
      fun t ->
        try
          DescrHash.find h t
        with
          Not_found -> let b = no_var t in
                      DescrHash.add h t b; b

(*    let is_ground t = Var.Set.is_empty (all_vars t) *)
    let no_var = is_ground

    let is_closed delta t =
      Var.Set.subset (all_vars t) delta

    let all_tlv t =
      let tlv, _, _, _ = collect_vars t in tlv

    let has_tlv t = not (Var.Set.is_empty (all_tlv t))

    let check_var =
      let cache = DescrHash.create 17 in
      let aux t =
        let tlv, pos, neg, _ = collect_vars t in
        match Var.Set.get tlv with
          [] | _::_::_ -> `NotVar
        | [ v ] ->
          let is_pos = Var.Set.mem pos v
          and is_neg = Var.Set.mem neg v in
          assert (is_pos || is_neg);
          if is_pos && is_neg then
            (* this variable is positive and negative. It must
               therefore be in a type of the form 'a&Int | Char\a *)
            `NotVar
          else if is_pos && equiv t (var v) then `Pos v
          else if is_neg && equiv t (diff any (var v)) then `Neg v
          else `NotVar
      in
      fun t ->
        try DescrHash.find cache t with Not_found ->
          let r = aux t in DescrHash.add cache t r; r

    let is_var t = (check_var t) != `NotVar

    let extract t =
      match check_var t with
      `Pos v -> v,true
      | `Neg v -> v,false
      | _ -> raise (Invalid_argument "Variable.extract")

    let extract_variable = extract

  end

let is_var = Variable.is_var
let no_var = Variable.no_var
let all_tlv = Variable.all_tlv
let has_tlv = Variable.has_tlv
let all_vars = Variable.all_vars
let extract_variable = Variable.extract_variable
let is_closed = Variable.is_closed



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 * (Var.var * t) list

  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
    | Display of string
    | 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,al) d =
    let d = uniq d in
    if equal { d with xml = BoolPair.empty } empty then begin
       match Product.get ~kind:`XML d with
	 | [(t1,t2)] ->
	     if DescrPairMap.mem (t1,t2) !named_xml then ()
	     else
	       named_xml := DescrPairMap.add (t1,t2) (cu,name,al) !named_xml
	 | _ -> ()
    end;
    if DescrMap.mem d !named then ()
    else named := DescrMap.add d (cu,name,al) !named

  let unregister_global d =
    let d = uniq d in
    if equal { d with xml = BoolPair.empty } empty then begin
      match Product.get ~kind:`XML d with
	 | [(t1,t2)] ->
	     named_xml := DescrPairMap.remove (t1,t2) !named_xml
	 | _ -> ()
    end;
    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 dd = diff any d in
    let aux x = if is_empty x then 1 else 0 in
    let n =
      aux { empty with atoms = dd.atoms }  +
      aux { empty with chars = dd.chars } +
      aux { empty with ints = dd.ints } +
      aux { empty with times =  dd.times } +
      aux { empty with xml = dd.xml } +
      aux { empty with arrow = dd.arrow } +
      aux { empty with record = dd.record } +
      aux { empty with abstract = dd.abstract }
    in
    n >= 5

  let proper_seq t =
    let memo = DescrHash.create 17 in
    let rec loop t =
      DescrHash.mem memo t ||
      begin
        DescrHash.add memo t ();
        not (has_tlv t) &&
        List.for_all (fun (_, t2) ->
            loop t2)
          (Product.get ~kind:`Normal t)
      end
    in
    loop t
  let bool_type =
    { empty with atoms = BoolAtoms.atom
        (`Atm(Atoms.cup
                (Atoms.atom (Atoms.V.mk_ascii "false"))
                (Atoms.atom (Atoms.V.mk_ascii "true"))))
    }


  (** [prepare d] massages a type and convert it to the syntactic form.
      Rough algorithm:
      - check whether [d] has been memoized (recursive types)
      - check whether [d] has a toplevel name
      - check whether [d] may be absent (as part of a record field)
      - check whether [d] needs to be expanded (i.e. isn't a trivially
      empty or full pair or record
      - for each kind (Atoms, Integers, Chars, Products, …) composing the type:
        - Check whether the type is worth complementing (that is write
          (Any \ Int) rather than (Arrow | Char | Atoms | ...)
        - Separate and factorize toplevel variables (so that
           'a&'b&Int | 'b&Int is written as 'b&Int.
        - Print out the toplevel variables present in all kinds
        - Print for each kind the top-level variables and the variable-less part.
          - special case for products and atoms:
            - products that are sequence types are written as regular expressions
            - if an atomic type is finite and contains the atoms `false and `true
              then write it has Bool.
  *)
  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
          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 x -> (Var.Set.add x acc_v, acc_a)
        ) (Var.Set.empty, init) l
      in
      let fill_line (type atom) (module BV : Bool.V with type Atom.t = atom)
		    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
      let d = Iter.simplify d 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 atom) (module BV : Bool.V with type Atom.t = atom)
		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 (cap 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 begin
        (slot.def <- [Neg (alloc [])];slot)
      end 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.(cap accp vp, cap 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
        (* list of (factv & remv & t) *)
        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 diff_nd n1 n2 =
          match n1, n2 with
          | { def = []; _ }, { def = []; _ } -> []
          | _ , { def = []; _ } -> n1.def
          | { def = []; _ }, _ -> [ Neg n2 ]
          | _ -> [ Diff(n1, n2) ]
        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
            (* [rem] prints the variable-less part of the type.
               [pos] is true iff [rem] is positive
            *)
            let print_topvars pos rem =
              let rem = List.rev rem in
              let alloc_l = function [] -> []
                | l -> [ alloc l ]
              in
              let lpos =
                List.fold_left (fun acc e ->
                  (alloc [e]) :: acc )
                (alloc_l (if pos then rem else [])) (print_vars pvars)
              in
              let lneg = List.rev_append (print_vars nvars)
                (if pos then [] else rem)
              in
              let lmid = alloc_l (List.rev (print_pnvars lvars)) in
              diff_nd
                (alloc [ inter_nd (lpos @ lmid) ])
                (alloc lneg)
            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 = Atoms.is_finite (BoolAtoms.leafconj tt.atoms) in
            let u_acc, tt =
              let tt_times = { empty with times = tt.times } in
              if subtype tt_times seqs_descr && proper_seq tt_times then
                let seq = cap tt seqs_descr in
                let seq_times = { empty with times = seq.times } in
                if is_empty seq || (is_empty seq_times && not finite_atoms) then
                  [], tt
                else
                  let tt =
                    let d = diff tt seqs_descr in
                    if finite_atoms then d
                    else cup d (cap tt nil_type)
                  in
                  [ (Regexp (decompile seq)) ], tt
              else
                [], tt
            in

            (* base types *)
            let u_acc =
              (List.map (fun x -> Atomic x) (Chars.print (BoolChars.leafconj tt.chars)))
              @ u_acc
            in
            let u_acc =
              (List.map (fun x -> (Atomic x)) (Intervals.print (BoolIntervals.leafconj tt.ints)))
              @ u_acc
            in
            let u_acc, tt = if finite_atoms && subtype bool_type tt then
                (Display "Bool") :: u_acc,
              diff tt bool_type
              else
                u_acc, tt
            in
            let pr_atoms l =
              List.fold_left (fun acc (ns, atm) ->
                (match atm with
                  `Finite l ->
                    List.map (fun a ->
                      Atomic (fun ppf -> Atoms.V.print_quote ppf a)) l
                | `Cofinite  l ->
                  [ Diff (alloc [ Atomic (fun ppf ->
                    Format.fprintf ppf "`%a"
                      Ns.InternalPrinter.print_any_ns ns) ]
                    ,
                          alloc (List.map (fun a ->
                            Atomic (fun ppf -> Atoms.V.print_quote ppf a)) l))
                  ]) @ acc
              ) [] l
            in
            let u_acc =
              match Atoms.extract (BoolAtoms.leafconj tt.atoms) with
                `Finite l -> (pr_atoms l) @ u_acc
              | `Cofinite [] -> (Display "Atom") :: u_acc
              | `Cofinite l ->  (Diff (alloc[Display "Atom"],
                                      alloc (pr_atoms l))) :: u_acc
            in
            (* pairs *)
            let u_acc =
              List.fold_left (fun acc (t1,t2) ->
                (Pair (prepare t1, prepare t2)) :: acc
              )
                u_acc (Product.partition any (BoolPair.leafconj tt.times))
            in

            (* xml pairs *)
            let u_acc =
              (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 (BoolPair.leafconj tt.xml))
               )
              ) @ u_acc
            in

            (* arrows *)
            let u_acc =
              (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 (BoolPair.leafconj tt.arrow))) @ u_acc
            in

            (* records *)
            let u_acc =
              (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 (BoolRec.leafconj tt.record)) })
              ) @ u_acc
            in
            let u_acc =
              (List.map (fun x -> (Atomic x))
                 (Abstracts.print (BoolAbstracts.leafconj tt.abstract))
              ) @ u_acc
            in
            assert (not tt.absent); (* is taken care of at the top *)
            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 _ | Display _-> ()
    | 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

(* 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 (List.rev l);
      cpar ppf ~level:pri_op pri

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


  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
    | Display s -> Format.fprintf ppf "%s" s
    | 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)

  and print_gname ppf = function
    |(cu,n,[]) -> Format.fprintf ppf "@[%s%a@]" cu Ns.QName.print n
    |(cu,n,al) ->
      let local_pp ppf t =
        let old_to_print = !to_print in
        let old_count_name = !count_name in
        let old_memo = DescrHash.copy memo in
        to_print := [];
        count_name := 0;
        DescrHash.clear memo;
        pp_type ppf t;
        to_print := old_to_print;
        count_name := old_count_name;
        DescrHash.iter (fun k v -> DescrHash.add memo k v) old_memo
      in
        Format.fprintf ppf "@[%s%a " cu Ns.QName.print n;
        Utils.pp_list ~delim:("(",")") local_pp ppf
          (List.map snd al);

        Format.fprintf ppf "@]"

  and 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

  and 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 wrap_formatter ppf =
    let out_fun,flush_fun = Format.pp_get_formatter_output_functions ppf () in
    let buffer = Buffer.create 16 in
    let prev_char = "\000" in
    let new_out_fun str start len =
      for i = start to start + len - 1 do
        let c = str.[i] in
        if c == '*' && prev_char.[0] == '(' then
          Buffer.add_char buffer ' '
        else if c == ')' && prev_char.[0] == '*' then
          Buffer.add_char buffer ' ';
        prev_char.[0] <- c;
        Buffer.add_char buffer c;
      done;
      let new_str = Buffer.contents buffer in
      Buffer.clear buffer;
      out_fun new_str 0 (String.length new_str)
    in
    let new_flush_fun () =
      let new_str = Buffer.contents buffer in
      let len = String.length new_str in
      if len > 0 then begin
        Buffer.clear buffer;
        out_fun new_str 0 len;
      end;
      flush_fun ();
    in
    Format.pp_set_formatter_output_functions ppf new_out_fun new_flush_fun;
    fun () ->
      Format.pp_print_flush ppf ();
      Format.pp_set_formatter_output_functions ppf out_fun flush_fun


  let pp_type ppf t =
    let reset = wrap_formatter ppf in
    pp_type ppf t;
    reset ()

  let pp_noname ppf t =
    let reset = wrap_formatter ppf in
    pp_noname ppf t;
    reset ()


  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

  let gmemo = Hashtbl.create 17

  let dump ppf t =
    let module NodeSet = Set.Make(Node) in
    Format.fprintf ppf "@[%a@]@\n" Descr.dump t;
    let nodes = ref NodeSet.empty in
    let ignore2 _ _ = () in
    let pair (n1, n2) =
      nodes := NodeSet.add n1 (NodeSet.add n2 !nodes)
    in
    Iter.compute ~empty:() ~full:() ~cup:ignore2 ~cap:ignore2 ~diff:ignore2
      ~var:ignore ~atom:ignore ~int:ignore ~char:ignore ~abs:ignore ~opt:ignore
      ~times:pair ~xml:pair ~arrow:pair ~record:(fun (_,lm) ->
        LabelMap.iter (fun n -> nodes := NodeSet.add n !nodes) lm) t;
    match NodeSet.elements !nodes with
      [] -> ()
    | l -> Format.fprintf ppf "@[<v 3> where:@\n";
      List.iter (fun n -> Hashtbl.replace gmemo n.Node.id n.Node.descr;
        Format.fprintf ppf "X%i = @[%a@]@\n" n.Node.id pp_noname n.Node.descr)
        l;
      Format.fprintf ppf "@]@\n"


  let dump_by_id ppf i =
    try dump ppf (Hashtbl.find gmemo i) with Not_found ->
      Format.fprintf ppf "Unbound node id: %i@\n" i

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

  (* 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_gname 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)
      | _ -> 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;
            mutable descr : Descr.t option;
          }

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

  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 solve_gen ?(stop_descr=(fun _ -> None)) ?(stop_node=(fun _ -> None)) v =
    let rec make_descr seen v =
      if List.memq v seen then empty else
        let seen = v :: seen in
        match stop_descr v with
        Some t -> t
        | None ->
          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 ->
        match stop_node v with
        | Some t -> v.node <- Some t; t
        | None -> let n = make () in
          v.node <- Some n;
          let d = make_descr [] v in
          define n d;
          n
    in
    internalize (make_node v)

  let solve v = solve_gen v

(* We shadow the corresponding definitions in the outer module *)
  let forward () = { def = `Cup []; node = None; descr = 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 empty = ty empty
  let any = ty any

  let binop e f may_flat mk vl =
    let has_f = ref false in
    let vl = List.map (fun v ->
        match may_flat v with
        | Some vl -> vl
        | None ->
          if v == e then [] else if v == f then (has_f := true; [])
          else [ v ]
      ) vl
    in
    if !has_f then f else
      match List.concat vl with
        [ v ] -> v
      | vl -> mk vl

  let cup = binop empty any
      (function { def = `Cup (_::_ as vl) ; _ } -> Some vl | _ -> None)
      (fun l -> cons (`Cup l))
  let cap = binop any empty
      (function { def = `Cap (_::_ as vl) ; _ } -> Some vl | _ -> None)
      (fun l -> cons (`Cap l))

  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 diff v1 v2 = cap [v1 ; (neg v2)]

  let get_opt = function Some t -> t | None -> T.any

  let decompose ?(stop=(fun _ -> None)) t =
    let memo = DescrHash.create 17 in
    let rec loop t =
      let res =
      try
        DescrHash.find memo t
      with
      Not_found ->
        let node_t = forward () in
        let () = DescrHash.add memo t node_t in
        let rhs =
          match stop t with
          | Some s -> s
          | None -> loop_struct t
        in
        node_t.def <- (rhs).def;
        node_t.descr <- Some t;
        node_t
      in
      res.descr <- Some t; res
    and loop_struct t =
      Iter.compute ~empty:empty ~full:any
        ~cup:(fun v1 v2 -> cup [v1;v2])
        ~cap:(fun v1 v2 -> cap [v1;v2])
        ~diff:diff
        ~var ~int:interval ~char ~atom ~abs:abstract
        ~xml:(fun (t1, t2) -> xml (loop (descr t1)) (loop (descr t2)))
        ~times:(fun (t1, t2) -> times (loop (descr t1)) (loop (descr t2)))
        ~arrow:(fun (t1, t2) -> arrow (loop (descr t1)) (loop (descr t2)))
        ~record:(fun (b, lm) -> record b (List.map (fun (l,t) ->
            let t = descr t in
            t.absent, l, loop t) (LabelMap.get lm)))
        ~opt:(function true -> ty Record.absent | _ -> empty) t
    in
    loop t

  let decompose2 ?(stop=(fun _ -> None)) t =
    let memo = DescrHash.create 17 in
    let rec loop t =
      let res =
        try
          DescrHash.find memo t
        with
          Not_found ->
            let node_t = forward () in
            let () = DescrHash.add memo t node_t in
            let rhs =
              match stop t with
              | Some s -> s
              | None -> loop_struct t
            in
            node_t.def <- (rhs).def;
            node_t.descr <- Some t;
            node_t
      in
      res.descr <- Some t; res
    and loop_struct t =
      Iter.compute_bdd
        ~typ:ty
        ~cup
        ~cap
        ~neg
        ~var
        ~ints:interval
        ~chars:char
        ~atoms:atom
        ~abstract:abstract
        ~xml:(fun (t1, t2) -> xml (loop (descr t1)) (loop (descr t2)))
        ~times:(fun (t1, t2) -> times (loop (descr t1)) (loop (descr t2)))
        ~arrow:(fun (t1, t2) -> arrow (loop (descr t1)) (loop (descr t2)))
        ~record:(fun (b, lm) -> record b (List.map (fun (l,t) ->
          let t = descr t in
          t.absent, l, loop t) (LabelMap.get lm)))
        ~absent:(function true -> [ty Record.absent] | _ -> []) t
    in
    loop t

end

module Substitution =
struct
  module Map = Var.Set.Map
  type t = Descr.t Map.map

  let identity = Map.empty

  module MemoSubst = Hashtbl.Make(
      struct
        type t = Descr.t * Descr.t Map.map
        let equal ((t1, m1) as x1) ((t2, m2) as x2) =
          x1 == x2
          || ((equiv t1 t2) && (Map.equal equiv m1 m2))
        let hash (t, m) =
          Descr.hash t + 17 * Map.hash Descr.hash m
      end
    )

  let print ppf m =
    Utils.pp_list (fun ppf (v, t) -> Format.fprintf ppf "%a:%a"
                      Var.pp v Print.pp_type t) ppf (Map.get m)

  let add v t m =
    if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
    else Map.add v t m

  let of_list l =
    List.fold_left (fun acc (v, t) -> add v t acc) identity l

  let decompose t =
    let open Positive in
    let res = decompose2
      ~stop:(fun x -> if Variable.no_var x then Some (ty x) else
                if Variable.is_var t then
                  let v, p = extract_variable t in
                  Some (if p then Positive.var v else neg (var v))
                else None)
      t
    in
    res

  let subst_cache = MemoSubst.create 17
  let get_opt = function Some e -> e | None -> raise Not_found
  let app_subst t subst =
    if Map.is_empty subst then t else
    let todo = ref [] in
    try
      MemoSubst.find subst_cache (t, subst)
    with
    Not_found ->

      let res =
        if List.for_all (fun (v, t) -> equiv t (var v)) (Map.get subst) then t
        else
        let v = decompose t in
        descr (
          Positive.solve_gen ~stop_descr:(fun v ->
              try
                Some (MemoSubst.find subst_cache
                        (get_opt v.Positive.descr, subst))
              with
                Not_found ->
                let () =
                  match v.Positive.descr,v.Positive.node with
                    Some t, Some n -> todo := (t, n) :: !todo
                  | _ -> ()
                in
                match v.Positive.def with
                  `Variable d -> (try Some  (Map.assoc d subst)
                                  with Not_found -> None)
                | _ -> None
            ) v)
      in
      let lsubst = Map.get subst in
      List.iter (fun (t, n) ->
          let nt = descr n in
          if not (DescrMap.mem nt !Print.named) then begin
            try
              let (cu, name, args) = DescrMap.find t !Print.named in
              if equiv t nt then
                Print.register_global (cu, name, args) nt
              else
                let dom_args = Var.Set.from_list (List.map fst args) in
                let dom,not_dom = List.fold_left
                    (fun (acct, accf) (v,t) ->
                       if Var.Set.mem dom_args v then v :: acct, accf
                       else acct, t::accf) ([],[]) lsubst
                in
                if (Var.Set.equal (Var.Set.from_list dom) dom_args)
                && (List.for_all no_var not_dom)
                then
                  let nargs = List.map (fun (v, _) -> v,Map.assoc v subst) args in
                  Print.register_global (cu, name, nargs) nt
            with Not_found -> ()
          end;
          let key = (t, subst) in
          if not (MemoSubst.mem subst_cache key) then
            MemoSubst.add subst_cache key nt) !todo;
      let res = if equiv t res then t else res in
      MemoSubst.add subst_cache (t,subst) res;res


  let full t l =
    if no_var t then t else
      app_subst t (of_list l)

  let single t s = full t [s]

  let freshen delta t =
    if no_var t then t else
    let vars = Var.Set.diff (all_vars t) delta in
    let subst = Map.init (fun v -> var (Var.fresh v)) vars in
    app_subst t subst

  let kind delta k t =
    if no_var t then t else
      let vars = Var.Set.diff (all_vars t) delta in
      let subst = Map.init (fun v -> var (Var.set_kind k v)) vars in
      app_subst t subst

  let solve_rectype t alpha =
    let x = make () in
    let n = Positive.solve_gen ~stop_node:(fun v -> match  v.Positive.def with
        |  `Variable d when Var.equal d alpha -> Some x
        | _ -> None) (decompose t)
    in
    define x (descr n);
    descr x

  let clean_type delta t =
    if no_var t then t else
      let _tlv,pos, neg, all = Variable.collect_vars t in
      DEBUG clean_type (Format.eprintf " - for type %a pos: %a, neg: %a, all: %a, tlv: %a@\n"
                          Print.pp_type t
                          Var.Set.pp pos Var.Set.pp neg Var.Set.pp all Var.Set.pp _tlv);
      let vars = Var.Set.diff all delta in
      if Var.Set.is_empty vars then t else
        let idx = ref 0 in
        let rec freshvar () =
          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 delta x then
            (* if the name is taken by a variable in delta, restart *)
            (incr idx; freshvar ())
          else x
        in
        let subst = Map.init
                      (fun v ->
                let is_pos = Var.Set.mem pos v in
                let is_neg = Var.Set.mem neg v in
                if is_pos && is_neg then var (freshvar ())
                else if is_pos then empty else any
              ) vars
        in
        app_subst t subst

  let clean_type delta t =
    let res = clean_type delta t in
    DEBUG clean_type (Format.eprintf "@[ Calling clean_type(%a,@, %a) = %a@]@\n%!"
                        Var.Set.pp delta Print.pp_type t Print.pp_type res);
    res


  let hide_vars t =
    if no_var t then t else
      let _,pos, neg, all = Variable.collect_vars t in
        let subst = Map.init
            (fun v ->
               let is_pos = Var.Set.mem pos v in
               let is_neg = Var.Set.mem neg v in
               if is_pos == is_neg then var v
                else if is_pos then any else empty
            ) all
      in
      app_subst t subst

end


module Tallying = struct

  type constr =
    |Pos of (Var.var * Descr.t) (** alpha <= t | alpha \in P *)
    |Neg of (Descr.t * 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 =
      let c = Descr.compare t1 t2 in
      if c = 0 then 0 else
      if equiv t1 t2 then 0
      else c

    (* 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.t * Descr.t) 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 delta v then map
        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
      let for_all = VarMap.for_all
    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.t 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 []
      let filter = List.filter
    end

    type s = S.t
    type m = M.t
    type es = ES.t
    type sigma = Descr.t E.t
    module SUB = SortedList.FiniteCofinite(struct
      type t = Descr.t 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 c =
      let constr =
        match c with
        |Pos (v,s) -> M.singleton v (empty,s)
        |Neg (s,v) -> M.singleton v (s,any)
      in
      S.singleton constr

    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 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 variable : fun (pos,neg) *)
  let toplevel delta single norm_rec mem p n =
    let _compare delta v1 v2 =
      let monov1 = Var.Set.mem delta v1 in
      let monov2 = Var.Set.mem delta v2 in
      if monov1 == monov2 then
        Var.compare v1 v2
      else
        if monov1 then 1 else -1
    in
    match (p,n) with
    |([], (`Var x)::neg) ->
        let t = single (false,x,[],neg) in
        CS.singleton (Neg (t, x))

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

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

    |([`Atm a], (`Var x)::neg) ->
        let t = single (false,x,p,neg) in
        CS.singleton (Neg (t,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 *)


  module NormMemoHash = Hashtbl.Make(Custom.Pair(Descr)(Var.Set))

  let memo_norm = NormMemoHash.create 17
  let () = Format.pp_set_margin Format.err_formatter 100


  let rec norm (t,delta,mem) =
    DEBUG normrec (
      Format.eprintf
        " @[Entering norm rec(%a):@\n" Print.pp_type t);
    let res =
      try
        (* If we find it in the global hashtable, we are finished *)
        let res = NormMemoHash.find memo_norm (t, delta) in
        DEBUG normrec (Format.eprintf
                         "@[ - Result found in global table @]@\n");
        res
      with
        Not_found ->
          try
            let finished, cst = NormMemoHash.find mem (t, delta) in
            DEBUG normrec (Format.eprintf
                             "@[ - Result found in local table, finished = %b @]@\n" finished);
            if finished then cst else CS.sat
          with
            Not_found ->
              begin
                let res =
                  (* base cases *)
                  if is_empty t then begin
                    DEBUG normrec (Format.eprintf "@[ - Empty type case @]@\n");
                    CS.sat
                  end else if no_var t then begin
                    DEBUG normrec (Format.eprintf "@[ - No var case @]@\n");
                    CS.unsat
                  end else if is_var t then begin
                    let (v,p) = extract_variable t in
                    if Var.Set.mem delta v then begin
                      DEBUG normrec (Format.eprintf "@[ - Monomorphic var case @]@\n");
                      CS.unsat (* if it is monomorphic, unsat *)
                    end else begin
                      DEBUG normrec (Format.eprintf "@[ - Polymorphic var case @]@\n");
                      (* otherwise, create a single constraint according to its polarity *)
                      let s = if p then (Pos (v,empty)) else (Neg (any,v)) in
                      CS.singleton s
                    end
                  end else begin (* type is not empty and is not a variable *)
                    DEBUG normrec (Format.eprintf "@[ - Inductive case:@\n");
                    let mem = NormMemoHash.add mem (t,delta) (false, CS.sat); mem in
                    let t = Iter.simplify t 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
                    DEBUG normrec (Format.eprintf "@[ - After Atoms constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_chars normchars acc (BoolChars.get t.chars) in
                    DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
                    DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_times normpair acc (BoolPair.get t.times) in
                    DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
                    DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
                    DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
                    let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
                    DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
                      (* XXX normrec is not tested at all !!! *)
                    let acc = aux single_record normrec acc (BoolRec.get t.record) in
                    DEBUG normrec (Format.eprintf "@[ - After Record constraints: %a @]@\n" CS.pp_s acc);
                    let acc = (* Simplify the constraints on that type *)
                      CS.S.filter
                        (fun m -> CS.M.for_all (fun v (s, t) ->
                          if Var.Set.mem delta v then
                              (* constraint on a monomorphic variables must be trivial *)
                            let x = var v in subtype s x && subtype x t
                          else true (*
                                      subtype s t || (non_empty (cap s t)) *)
                         ) m)
                        acc
                    in
                    DEBUG normrec (Format.eprintf "@[ - After Filtering constraints: %a @]@\n" CS.pp_s acc);
                    DEBUG normrec (Format.eprintf "@]@\n");
                    acc
                  end
                in
                NormMemoHash.replace mem (t, delta) (true,res); res
              end
    in
    DEBUG normrec (Format.eprintf
                     "Leaving norm rec(%a) = %a@]@\n%!"
                     Print.pp_type t
                     CS.pp_s res
    );
    res

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



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

  (* merge needs delta because it calls norm recursively *)
  let rec merge m delta cache =
    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 Cache.lookup x cache != None then acc
          else
            let cache, _ = Cache.find ignore x cache in
            let n = norm delta x in
            if CS.S.is_empty n then
              raise (UnSatConstr "merge2");
            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 cache))
                c1 CS.S.empty
            in
            CS.union c2 acc
      ) 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 Cache.emp

  (* Add constraints of the form { alpha = ( s v fresh ) ^ t } *)

  let solve delta s =

    let aux alpha (s,t) acc =
      (* we cannot solve twice the same variable *)
      assert(not(CS.E.mem alpha acc));
      let v = Var.mk (Printf.sprintf "#fr_%s" (Var.id alpha)) in
      let b = var v 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
            if Var.Set.mem delta beta then aux alpha (s, t) acc
            else
              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 *)
        (* solve_rectype remove also all previously introduced fresh variables *)
        let x = Substitution.solve_rectype 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 (Substitution.single s (alpha,x)) acc
          ) e1 CS.E.empty
        in
        (* Format.printf "es = %a\n" CS.print_e es; *)
        let sigma = aux ((CS.E.add alpha x sol)) es in
        let talpha = CS.E.fold (fun v sub acc -> Substitution.single acc (v,sub)) sigma x in
        CS.E.add alpha talpha sigma
      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 delta (merge delta c)) acc
        with UnSatConstr _ -> acc
      ) n CS.ES.empty
    in
    if CS.ES.is_empty m then raise Step2Fail else
    let el =
      CS.ES.fold (fun e acc -> CS.ES.add (unify e) acc ) m CS.ES.empty
    in
    (CS.ES.elements el)

  (* apply sigma to t *)
  let (>>) t si = CS.E.fold (fun v sub acc -> Substitution.single 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.cup (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.cap !vst !vsi))
    in
    let filterdiff t si sj =
      let vsj = get sj in
      not(Var.Set.is_empty (Var.Set.cap !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.cup (all_vars v) acc
      ) e acc
    ) Var.Set.empty ll

  let is_identity = List.for_all (CS.E.is_empty)
  let identity = [CS.E.empty]

  let filter f sl =
    if is_identity sl then sl else
    List.fold_left (fun acc si ->
      let e = CS.E.filter (fun v _ -> f v) si in
      if CS.E.is_empty e then acc else e::acc
    ) [] sl


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 (Substitution.freshen 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 =
      DEBUG apply_raw (Format.eprintf " @[Entering apply_raw (delta:@[%a@], @[%a@], @[%a@])@\n%!"
                         Var.Set.pp delta
                         Print.pp_type s
                         Print.pp_type t
      );

  Tallying.NormMemoHash.clear Tallying.memo_norm;
  let s = Substitution.kind delta Var.function_kind s in
  let t = Substitution.kind delta Var.argument_kind t in
  let vgamma = Var.mk "Gamma" in
  let gamma = var vgamma 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 =
        Substitution.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 (Substitution.freshen delta s) (get ai (i-1))),
         (cap (Substitution.freshen 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) ->
      DEBUG apply_raw (Format.eprintf " Leaving apply_raw (delta:@[%a@], @[%a@], @[%a@]) = @[%a@], @[%a@] @]@\n%!"
                         Var.Set.pp delta
                         Print.pp_type s
                         Print.pp_type t
                         Print.pp_type res
                         Tallying.CS.pp_sl 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)