types.ml

open Ident
open Encodings

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 Abstract =
struct
  module T = Custom.String
  type abs = T.t

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

  include SortedList.FiniteCofinite(T)

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

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

type pair_kind = [ `Normal | `XML ]

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

type tlvs =  { s : Var.Set.t ; b : bool }

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

  let print_lst ppf =
    List.iter (fun f -> f ppf; Format.fprintf ppf " |")

  let dump ppf d =
    Format.fprintf ppf "<types atoms(%a) ints(%a) chars(%a) times(%a) arrow(%a) record(%a) xml(%a) abstract(%a) absent(%b)>"
      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
      Abstract.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 = Abstract.empty;
    absent= false;
    toplvars = { s = Var.Set.empty ; b = true }
  }

  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;
    Abstract.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) &&
      (Abstract.equal a.abstract b.abstract) &&
      (a.absent == b.absent)
    )

  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 = Abstract.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 + Abstract.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu

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

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

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

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

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

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

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

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

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

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

(* two representation possible. either all fields (except vars) are full, OR
 * the field vars is full.
 *)
let any =  {
  times = BoolPair.full; 
  xml   = BoolPair.full; 
  arrow = BoolPair.full; 
  record= BoolRec.full; 
  ints  = BoolIntervals.full;
  atoms = BoolAtoms.full;
  chars = BoolChars.full;
  abstract = Abstract.any;
  absent= false;
  toplvars = { s = Var.Set.empty ; b = true }
}

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))); toplvars = {empty.toplvars with b = false } }
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) }
let var a =  {
  (* Atm = Any ^ a *)
  times = BoolPair.vars a;
  xml   = BoolPair.vars a; 
  arrow = BoolPair.vars a; 
  record= BoolRec.vars a; 
  ints  = BoolIntervals.vars a;
  atoms = BoolAtoms.vars a;
  chars = BoolChars.vars a;
  abstract = Abstract.empty;
  absent= false;
  toplvars = { s = Var.Set.singleton a; b = true }
}

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 = a }

let get_abstract t = t.abstract

(* union is component wise + a pass to extract variables
 * Var = ( t1.Var v t2.Var ) v ( extracted variables )
 *)
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 = Abstract.cup x.abstract y.abstract;
    absent= x.absent || y.absent;
    toplvars = { s = Var.Set.union x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
  }

(* intersection 
 *)
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 = Abstract.cap x.abstract y.abstract;
    absent= x.absent && y.absent;
    toplvars = { s = Var.Set.inter x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
  }

(* 
 *
 * t1 // t2 = ( t1.Atm ^ - t2.Atm ^ t2.Var ) v
 *            ( t1.Var ^ t2.Var )
 *
 * Atm t1.Atm // ( t2.Atm v t2.Var )
 * Var ( t1.Var // t2.Var ) v ( extracted variables )
 *)    
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 = Abstract.diff x.abstract y.abstract;
    absent= x.absent && not y.absent;
    toplvars = { s = Var.Set.diff x.toplvars.s y.toplvars.s; b = x.toplvars.b && y.toplvars.b }
  }
    
(* 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) &&
  (Abstract.disjoint a.abstract b.abstract) &&
  (not (a.absent && b.absent))

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

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)

(* substitute variables occurring in t accoding to the function subvar *)
let rec substfree_aux subvar (t,mem) =
  let module C ( X : BoolVar.S ) = 
    struct
      let atom_aux ?noderec subvar_aux = 
        let open X in function
          (* this subvar is acutally specialized on subatoms, subints, etc ... *)
          |`Var z -> subvar_aux vars (`Var z)
          |`Atm bdd when X.T.is_empty bdd || X.T.is_full bdd -> atom (`Atm bdd)
          |`Atm bdd ->
              begin match noderec with
              |None -> atom (`Atm bdd)
              |Some f -> f bdd (* f = subpairs ... *)
              end
          |_ -> assert false

      let subst ?noderec subvar_aux bdd = 
        let open X in
        let atom z = atom_aux ?noderec subvar_aux z in
        compute ~empty ~full:`True ~cup ~cap ~diff ~atom bdd
    end
  in
  let subpairs bdd =
    List.fold_left (fun acc (left,rigth) ->
      let deep_subst f l = 
        List.fold_left (fun acc (t1,t2) -> 
          let d1 = cons (substfree_aux subvar ((descr t1),mem)) in 
          let d2 = cons (substfree_aux subvar ((descr t2),mem)) in
          BoolPair.cap acc (f(BoolPair.atom(`Atm (Pair.atom (d1,d2)))))
        ) BoolPair.full l
      in
      let neg_atm x = BoolPair.diff BoolPair.full x in
      let pos_atm x = x in
      let acc1 = BoolPair.cap (deep_subst pos_atm left) (deep_subst neg_atm rigth) in
      BoolPair.cup acc acc1
    ) BoolPair.empty (Pair.get bdd)
  in
  let subatoms vars v = match subvar v with |`Constr s -> s.atoms |`Var z -> vars (`Var z) in
  let subints vars v = match subvar v with |`Constr s -> s.ints |`Var z -> vars (`Var z) in
  let subchars vars v = match subvar v with |`Constr s -> s.chars |`Var z -> vars (`Var z) in
  let subarrow vars v = match subvar v with |`Constr s -> s.arrow |`Var z -> vars (`Var z) in
  let subxml vars v = match subvar v with |`Constr s -> s.xml |`Var z -> vars (`Var z) in
  let subtimes vars v = match subvar v with |`Constr s -> s.times |`Var z -> vars (`Var z) in
  let subrecord vars v = match subvar v with |`Constr s -> s.record |`Var z -> vars (`Var z) in
  let tlv s =
    Var.Set.fold (fun v acc ->
      match subvar v with 
      |`Var z -> Var.Set.add (`Var z) acc
      |_ -> acc
    ) s Var.Set.empty
  in
  try DescrHash.find mem t
  with Not_found ->
    let tsub = 
      {
        atoms = (let module M = C(BoolAtoms) in M.subst) subatoms t.atoms;
        ints  = (let module M = C(BoolIntervals) in M.subst) subints t.ints;
        chars = (let module M = C(BoolChars) in M.subst) subchars t.chars;
        times = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subtimes t.times;
        xml   = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subxml t.xml;
        (* XXX record still not done . need to define ~f:subrecord *)
        record= (let module M = C(BoolRec) in M.subst) subrecord t.record;
        arrow = (let module M = C(BoolPair) in M.subst) ~noderec:subpairs subarrow t.arrow;
        abstract = t.abstract;
        absent= t.absent;
        toplvars = { t.toplvars with s = tlv (t.toplvars.s) }
      }
    in
    DescrHash.add mem t tsub;
    tsub

(* substitute in t all occurrences of v by the type s *)
let subst t (v,s) =
  let subvar (`Var v,s) (`Var z) =
    if Var.equal (`Var v) (`Var z) then `Constr s else (`Var z)
  in
  substfree_aux (subvar (v,s)) (t,DescrHash.create 17)

(* substitute in t all variables with a free variables *)
(* using a Hashtbl here hides lots of in place modifications *)
(* the hashtbl can be used to remember all substitutions *)
let substfree t =
  let subvar tbl z =
    try Hashtbl.find tbl z
    with Not_found -> begin
      let v = Var.fresh () in
      Hashtbl.add tbl z v;
      v
    end
  in
  substfree_aux (subvar (Hashtbl.create 17)) (t,DescrHash.create 17)

(* substitute all variables with s *)
let substvariance t =
  let subvar (`Var t) = 
    Format.printf "%a\n" Var.dump (`Var t);
    match Var.variance (`Var t) with
    |`Covariant -> `Constr any 
    |`ContraVariant -> `Constr empty
    |_ -> `Var t
  in
  substfree_aux subvar (t,DescrHash.create 17)

(* 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 Abstract.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 * Abstract.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) -> Abstract.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 print_witness 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)" print_witness w1 print_witness w2
    | WXml (w1,w2,_) -> 
	Format.fprintf ppf "XML(%a,%a)" print_witness w1 print_witness w2
    | WRecord (ws,o,_) ->
	Format.fprintf ppf "{";
	LabelMap.iteri
	  (fun l w -> Format.fprintf ppf " %a=%a" 
	     Label.print_attr l print_witness 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->" print_witness x;
		     match y with
		       | None -> Format.fprintf ppf "#"
		       | Some y -> print_witness 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 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@." 
	print_witness 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 -> Abstract.contains_sample a 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