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

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

  include SortedList.FiniteCofinite(T)
  let full = any

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

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

end

type pair_kind = [ `Normal | `XML ]

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

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

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

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

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

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

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

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

  let compare a b =
    if a == b then 0
    else let c = BoolAtoms.compare a.atoms b.atoms in if c <> 0 then c
    else let c = BoolChars.compare a.chars b.chars in if c <> 0 then c
    else let c = BoolIntervals.compare a.ints b.ints in if c <> 0 then c
    else let c = BoolPair.compare a.times b.times in if c <> 0 then c
    else let c = BoolPair.compare a.xml b.xml in if c <> 0 then c
    else let c = BoolPair.compare a.arrow b.arrow in if c <> 0 then c
    else let c = BoolRec.compare a.record b.record in if c <> 0 then c
    else let c = BoolAbstracts.compare a.abstract b.abstract in if c <> 0 then c
    else if a.absent && not b.absent then -1
    else if b.absent && not a.absent then 1
    else 0

  let hash a =
    let accu = BoolChars.hash a.chars in
    let accu = 17 * accu + BoolIntervals.hash a.ints in
    let accu = 17 * accu + BoolAtoms.hash a.atoms in
    let accu = 17 * accu + BoolPair.hash a.times in
    let accu = 17 * accu + BoolPair.hash a.xml in
    let accu = 17 * accu + BoolPair.hash a.arrow in
    let accu = 17 * accu + BoolRec.hash a.record in
    let accu = 17 * accu + BoolAbstracts.hash a.abstract in
    let accu = if a.absent then accu+5 else accu in
    accu

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

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

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

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

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

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

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

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

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 (