types.ml

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


module TLV = struct

  module Set = struct
    include Set.Make(
      struct
        type t = (Var.var * bool)
        let compare (v1,p1) (v2,p2) =
          let c = Var.compare v1 v2 in
          if c == 0 then
            if p1 == p2 then 0
            else if p1 then 1 else -1
          else c
      end)
    let print sep ppf s =
      let aux1 ppf = function
        |(v,true) -> Format.fprintf ppf "%a" Var.print v
        |(v,false) -> Format.fprintf ppf "~ %a" Var.print v
      in
      let rec aux ppf = function
        |[] -> ()
        |[h] -> aux1 ppf h
        |h::l -> Format.fprintf ppf "%a %s %a" aux1 h sep aux l
      in
      aux ppf (elements s)
  end

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

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

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

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

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

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

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

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

  let has_toplevel x = Set.cardinal x.tlv > 0

  let print ppf x = Set.print ";" ppf x.tlv
  let dump ppf x =
    Format.fprintf ppf "<fv = {%a} ; tlv = {%a}>"
      Var.Set.print x.fv (Set.print ";") x.tlv
  let mem v x = Set.mem v x.tlv

end

module rec Descr :
sig
  (* each kind is represented as a union of itersection of types
   * the type is a union of all kinds
   *
   * we add a new field that contains only variables.
   * Inv :
     * if the bdd of ANY kind is composed only of variables,
       the we move it in vars:
     * From a bdd we move all variables to vars: that belong to
     * to a path in the bdd that contains only variables and end in
     * true
     * A bdd never contains a path that ends in 1 and contains only variables
     *
     * (t1 v a ) ^ ( t2 v b )
     * we need to distribute variables for the intersection
     * (t1 ^ t2) v (t1 ^ b) v (t2 ^ a) v (a ^ b)
     * before we were doing only t1 ^ t2
   *)
  type s = {
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    abstract: 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 : TLV.t
  }
  include Custom.T with type t = s
  val empty: t
  val is_empty : t -> bool
end =
struct
  type s = {
    atoms : BoolAtoms.t;
    ints  : BoolIntervals.t;
    chars : BoolChars.t;
    times : BoolPair.t;
    xml   : BoolPair.t;
    arrow : BoolPair.t;
    record: BoolRec.t;
    abstract: Abstract.t;
    absent: bool;
    toplvars : TLV.t
  }
  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)>\n%a"
      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
      TLV.dump d.toplvars

  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 = TLV.empty
  }

  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 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) &&
      (Abstract.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 = 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

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

(* 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 = TLV.any
}

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 = TLV.pair (descr x).toplvars (descr y).toplvars }
let xml x y = { empty with
                    xml = BoolPair.atom (`Atm (Pair.atom (x,y)));
                    toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }
let arrow x y = { empty with
                    arrow = BoolPair.atom (`Atm (Pair.atom (x,y)));
                    toplvars = TLV.pair (descr x).toplvars (descr y).toplvars }

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

let tlv_from_rec (_, l) =
  let rec aux acc = function
    | (_, n) :: rest -> aux (TLV.pair acc (descr n).toplvars) rest
    | [] -> acc in
  aux TLV.empty (Ident.LabelMap.get l)

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

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

(* Atm = Any ^ a *)
let var a =  {
  times = BoolPair.vars a;
  xml   = BoolPair.vars a;
  arrow = BoolPair.vars a;
  record= BoolRec.vars a;
  ints  = BoolIntervals.vars a;
  atoms = BoolAtoms.vars a;
  chars = BoolChars.vars a;
  abstract = Abstract.empty;
  absent= false;
  toplvars = TLV.singleton (a,true)
}

(* XXX this function could be potentially costly. There should be
 * better way to take trace of top level variables in a type *)
let update_tlv x y t =
  let open TLV in
  let tlv t =
    let aux get bdd : Set.t =
      let l =
        List.fold_left (fun acc (p,n) ->
          let acc1 =
            List.fold_left (fun acc -> function
              |(`Var v) as x -> Set.union acc (Set.singleton (x,true))
              |_ -> acc
            ) Set.empty p
          in
          let acc2 =
            List.fold_left (fun acc -> function
              |(`Var v) as x -> Set.union acc (Set.singleton (x,false))
              |_ -> assert false
            ) acc1 n
          in acc2::acc
        ) [] (get bdd)
      in
      match l with
      |[] -> Set.empty
      |[h] -> h
      |h::l -> List.fold_left Set.inter h l
    in
    List.fold_left Set.union
    (aux BoolChars.get t.chars)
    [
      (aux BoolIntervals.get t.ints);
      (aux BoolAtoms.get t.atoms);
      (aux BoolPair.get t.arrow);
      (aux BoolPair.get t.xml);
      (aux BoolRec.get t.record)
    ]
  in
  let fv t = if Descr.is_empty t then Var.Set.empty else
      Var.Set.union x.toplvars.fv y.toplvars.fv in
  { t with toplvars =
    {
      tlv = tlv t ;
      fv = fv t ;
      isvar = t.toplvars.isvar
  } }
;;

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

let is_var t = TLV.is_single t.toplvars
let no_var t = TLV.no_variables t.toplvars
let has_tlv t = TLV.has_toplevel t.toplvars

let all_vars t = t.toplvars.TLV.fv
let all_tlv t = t.toplvars.TLV.tlv

let cup x y =
  if x == y then x else
    let t = {
      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 = TLV.empty
    } in
    let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}

let cap x y =
  if x == y then x else
    let t = {
      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 = TLV.empty
    } in
    let isvar = (is_var x && equal x t) || (is_var y && equal y t) in
    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}

let diff x y =
  if x == y then empty else
    let t = {
      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 = TLV.empty
    } in
    let isvar = (equal x any && is_var y) || (is_var x && equal y empty) in
    update_tlv x y { t with toplvars = { t.toplvars with TLV.isvar = isvar }}

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