Commit 1db0d21a authored by Kim Nguyễn's avatar Kim Nguyễn

Rename the Bool* modules into Var* (which makes way more sense).

parent 062d5039
...@@ -349,8 +349,8 @@ binary_op_cst "dump_to_file_utf8" ...@@ -349,8 +349,8 @@ binary_op_cst "dump_to_file_utf8"
(* Integer operators *) (* Integer operators *)
let intop f x y = let intop f x y =
let s = Types.BoolIntervals.leafconj x in let s = Types.VarIntervals.leafconj x in
let t = Types.BoolIntervals.leafconj y in let t = Types.VarIntervals.leafconj y in
(f s t) (f s t)
;; ;;
......
...@@ -870,8 +870,8 @@ module Compile = struct ...@@ -870,8 +870,8 @@ module Compile = struct
let split_kind basic prod xml record = { let split_kind basic prod xml record = {
basic = basic; basic = basic;
atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.BoolAtoms.leafconj (Types.Atom.get t), r) basic); atoms = Atoms.mk_map (List.map (fun (t,r) -> Types.VarAtoms.leafconj (Types.Atom.get t), r) basic);
chars = Chars.mk_map (List.map (fun (t,r) -> Types.BoolChars.leafconj (Types.Char.get t), r) basic); chars = Chars.mk_map (List.map (fun (t,r) -> Types.VarChars.leafconj (Types.Char.get t), r) basic);
prod = prod; prod = prod;
xml = xml; xml = xml;
record = record record = record
......
...@@ -55,9 +55,9 @@ let rec single memo t = ...@@ -55,9 +55,9 @@ let rec single memo t =
let memo = D.add t memo in let memo = D.add t memo in
let pair (t1,t2) = Types.Pair (single memo t1, single memo t2) in let pair (t1,t2) = Types.Pair (single memo t1, single memo t2) in
let xml (t1,t2) = Types.Xml (single memo t1, single memo t2) in let xml (t1,t2) = Types.Xml (single memo t1, single memo t2) in
let int t = Types.Integer (Intervals.single (Types.BoolIntervals.leafconj (Types.Int.get t))) in let int t = Types.Integer (Intervals.single (Types.VarIntervals.leafconj (Types.Int.get t))) in
let atom t = Types.Atom (Atoms.single (Types.BoolAtoms.leafconj (Types.Atom.get t))) in let atom t = Types.Atom (Atoms.single (Types.VarAtoms.leafconj (Types.Atom.get t))) in
let char t = Types.Char (Chars.single (Types.BoolChars.leafconj (Types.Char.get t))) in let char t = Types.Char (Chars.single (Types.VarChars.leafconj (Types.Char.get t))) in
let fields = function let fields = function
| (true,_) -> assert false | (true,_) -> assert false
| (false,t) -> single memo t in | (false,t) -> single memo t in
......
...@@ -168,16 +168,16 @@ let empty_descr_ = { atoms = Bool.empty; ...@@ -168,16 +168,16 @@ let empty_descr_ = { atoms = Bool.empty;
module rec Descr : module rec Descr :
sig sig
include Custom.T with include Custom.T with
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t, type t = (VarAtoms.t, VarIntervals.t, VarChars.t, VarTimes.t,
BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_ VarXml.t, VarArrow.t, VarRec.t, VarAbstracts.t) descr_
val empty: t val empty: t
val any : t val any : t
val is_empty : t -> bool val is_empty : t -> bool
end = end =
struct struct
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t, type t = (VarAtoms.t, VarIntervals.t, VarChars.t, VarTimes.t,
BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_ VarXml.t, VarArrow.t, VarRec.t, VarAbstracts.t) descr_
let dump ppf d = let dump ppf d =
Format.fprintf ppf "@[<v 1>types:@\n\ Format.fprintf ppf "@[<v 1>types:@\n\
...@@ -190,87 +190,87 @@ struct ...@@ -190,87 +190,87 @@ struct
@<1> record: %a@\n\ @<1> record: %a@\n\
@<1> abstract: %a@\n\ @<1> abstract: %a@\n\
@<1> absent: %b@]@\n" @<1> absent: %b@]@\n"
BoolAtoms.dump d.atoms VarAtoms.dump d.atoms
BoolIntervals.dump d.ints VarIntervals.dump d.ints
BoolChars.dump d.chars VarChars.dump d.chars
BoolTimes.dump d.times VarTimes.dump d.times
BoolXml.dump d.xml VarXml.dump d.xml
BoolArrow.dump d.arrow VarArrow.dump d.arrow
BoolRec.dump d.record VarRec.dump d.record
BoolAbstracts.dump d.abstract VarAbstracts.dump d.abstract
d.absent d.absent
let empty = empty_descr_ let empty = empty_descr_
let any = { let any = {
ints = BoolIntervals.full; ints = VarIntervals.full;
atoms = BoolAtoms.full; atoms = VarAtoms.full;
chars = BoolChars.full; chars = VarChars.full;
times = BoolTimes.full; times = VarTimes.full;
xml = BoolXml.full; xml = VarXml.full;
arrow = BoolArrow.full; arrow = VarArrow.full;
record = BoolRec.full; record = VarRec.full;
abstract = BoolAbstracts.full; abstract = VarAbstracts.full;
absent = false; absent = false;
} }
let check a = let check a =
BoolChars.check a.chars; VarChars.check a.chars;
BoolIntervals.check a.ints; VarIntervals.check a.ints;
BoolAtoms.check a.atoms; VarAtoms.check a.atoms;
BoolTimes.check a.times; VarTimes.check a.times;
BoolXml.check a.xml; VarXml.check a.xml;
BoolArrow.check a.arrow; VarArrow.check a.arrow;
BoolRec.check a.record; VarRec.check a.record;
BoolAbstracts.check a.abstract; VarAbstracts.check a.abstract;
() ()
let equal a b = let equal a b =
(a == b) || ( (a == b) || (
(BoolAtoms.equal a.atoms b.atoms) && (VarAtoms.equal a.atoms b.atoms) &&
(BoolChars.equal a.chars b.chars) && (VarChars.equal a.chars b.chars) &&
(BoolIntervals.equal a.ints b.ints) && (VarIntervals.equal a.ints b.ints) &&
(BoolTimes.equal a.times b.times) && (VarTimes.equal a.times b.times) &&
(BoolXml.equal a.xml b.xml) && (VarXml.equal a.xml b.xml) &&
(BoolArrow.equal a.arrow b.arrow) && (VarArrow.equal a.arrow b.arrow) &&
(BoolRec.equal a.record b.record) && (VarRec.equal a.record b.record) &&
(BoolAbstracts.equal a.abstract b.abstract) && (VarAbstracts.equal a.abstract b.abstract) &&
(a.absent == b.absent) (a.absent == b.absent)
) )
let is_empty a = let is_empty a =
(BoolAtoms.is_empty a.atoms) && (VarAtoms.is_empty a.atoms) &&
(BoolChars.is_empty a.chars) && (VarChars.is_empty a.chars) &&
(BoolIntervals.is_empty a.ints) && (VarIntervals.is_empty a.ints) &&
(BoolTimes.is_empty a.times) && (VarTimes.is_empty a.times) &&
(BoolXml.is_empty a.xml) && (VarXml.is_empty a.xml) &&
(BoolArrow.is_empty a.arrow) && (VarArrow.is_empty a.arrow) &&
(BoolRec.is_empty a.record) && (VarRec.is_empty a.record) &&
(BoolAbstracts.is_empty a.abstract) (VarAbstracts.is_empty a.abstract)
let compare a b = let compare a b =
if a == b then 0 if a == b then 0
else let c = BoolAtoms.compare a.atoms b.atoms in if c <> 0 then c else let c = VarAtoms.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 = VarChars.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 = VarIntervals.compare a.ints b.ints in if c <> 0 then c
else let c = BoolTimes.compare a.times b.times in if c <> 0 then c else let c = VarTimes.compare a.times b.times in if c <> 0 then c
else let c = BoolXml.compare a.xml b.xml in if c <> 0 then c else let c = VarXml.compare a.xml b.xml in if c <> 0 then c
else let c = BoolArrow.compare a.arrow b.arrow in if c <> 0 then c else let c = VarArrow.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 = VarRec.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 let c = VarAbstracts.compare a.abstract b.abstract in if c <> 0 then c
else if a.absent && not b.absent then -1 else if a.absent && not b.absent then -1
else if b.absent && not a.absent then 1 else if b.absent && not a.absent then 1
else 0 else 0
let hash a = let hash a =
let accu = BoolChars.hash a.chars in let accu = VarChars.hash a.chars in
let accu = 17 * accu + BoolIntervals.hash a.ints in let accu = 17 * accu + VarIntervals.hash a.ints in
let accu = 17 * accu + BoolAtoms.hash a.atoms in let accu = 17 * accu + VarAtoms.hash a.atoms in
let accu = 17 * accu + BoolTimes.hash a.times in let accu = 17 * accu + VarTimes.hash a.times in
let accu = 17 * accu + BoolXml.hash a.xml in let accu = 17 * accu + VarXml.hash a.xml in
let accu = 17 * accu + BoolArrow.hash a.arrow in let accu = 17 * accu + VarArrow.hash a.arrow in
let accu = 17 * accu + BoolRec.hash a.record in let accu = 17 * accu + VarRec.hash a.record in
let accu = 17 * accu + BoolAbstracts.hash a.abstract in let accu = 17 * accu + VarAbstracts.hash a.abstract in
let accu = if a.absent then accu+5 else accu in let accu = if a.absent then accu+5 else accu in
accu accu
...@@ -297,10 +297,8 @@ struct ...@@ -297,10 +297,8 @@ struct
let mk id d = { id = id; cu = Compunit.current (); descr = d } let mk id d = { id = id; cu = Compunit.current (); descr = d }
end end
and BoolAtoms : VarType with type Atom.t = Atoms.t and VarAtoms : VarType with type Atom.t = Atoms.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -310,7 +308,7 @@ and BoolAtoms : VarType with type Atom.t = Atoms.t ...@@ -310,7 +308,7 @@ and BoolAtoms : VarType with type Atom.t = Atoms.t
let proj t = t.atoms let proj t = t.atoms
end end
and BoolIntervals : VarType with type Atom.t = Intervals.t and VarIntervals : VarType with type Atom.t = Intervals.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -320,7 +318,7 @@ and BoolIntervals : VarType with type Atom.t = Intervals.t ...@@ -320,7 +318,7 @@ and BoolIntervals : VarType with type Atom.t = Intervals.t
let proj t = t.ints let proj t = t.ints
end end
and BoolChars : VarType with type Atom.t = Chars.t and VarChars : VarType with type Atom.t = Chars.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -330,7 +328,7 @@ and BoolChars : VarType with type Atom.t = Chars.t ...@@ -330,7 +328,7 @@ and BoolChars : VarType with type Atom.t = Chars.t
let proj t = t.chars let proj t = t.chars
end end
and BoolAbstracts : VarType with type Atom.t = Abstracts.t and VarAbstracts : VarType with type Atom.t = Abstracts.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -343,7 +341,7 @@ and BoolAbstracts : VarType with type Atom.t = Abstracts.t ...@@ -343,7 +341,7 @@ and BoolAbstracts : VarType with type Atom.t = Abstracts.t
and Pair : Bool.S with type elem = (Node.t * Node.t) = and Pair : Bool.S with type elem = (Node.t * Node.t) =
Bool.Make(Custom.Pair(Node)(Node)) Bool.Make(Custom.Pair(Node)(Node))
and BoolTimes : VarType with module Atom = Pair and VarTimes : VarType with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
...@@ -352,7 +350,7 @@ and BoolTimes : VarType with module Atom = Pair ...@@ -352,7 +350,7 @@ and BoolTimes : VarType with module Atom = Pair
let proj (t : descr) : t = t.times let proj (t : descr) : t = t.times
end end
and BoolXml : VarType with module Atom = Pair and VarXml : VarType with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
...@@ -361,7 +359,7 @@ and BoolXml : VarType with module Atom = Pair ...@@ -361,7 +359,7 @@ and BoolXml : VarType with module Atom = Pair
let proj (t : descr) : t = t.xml let proj (t : descr) : t = t.xml
end end
and BoolArrow : VarType with module Atom = Pair and VarArrow : VarType with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
...@@ -377,7 +375,7 @@ end ...@@ -377,7 +375,7 @@ end
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map = and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node))) Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
and BoolRec : VarType with module Atom = Rec and VarRec : VarType with module Atom = Rec
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Rec) struct include Bool.MakeVar(Rec)
...@@ -421,88 +419,88 @@ let non_constructed_or_absent = ...@@ -421,88 +419,88 @@ let non_constructed_or_absent =
{ non_constructed with absent = true } { non_constructed with absent = true }
(* Descr.t type constructors *) (* Descr.t type constructors *)
let times x y = { empty with times = BoolTimes.atom (`Atm (Pair.atom (x,y))) } let times x y = { empty with times = VarTimes.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolXml.atom (`Atm (Pair.atom (x,y))) } let xml x y = { empty with xml = VarXml.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolArrow.atom (`Atm (Pair.atom (x,y))) } let arrow x y = { empty with arrow = VarArrow.atom (`Atm (Pair.atom (x,y))) }
let record label t = let record label t =
{ empty with record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) } { empty with record = VarRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
let record_fields x = let record_fields x =
{ empty with record = BoolRec.atom (`Atm (Rec.atom x)) } { empty with record = VarRec.atom (`Atm (Rec.atom x)) }
let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) } let atom a = { empty with atoms = VarAtoms.atom (`Atm a) }
(* Atm = Any ^ a *) (* Atm = Any ^ a *)
let var a = let var a =
{ {
ints = BoolIntervals.var a; ints = VarIntervals.var a;
atoms = BoolAtoms.var a; atoms = VarAtoms.var a;
chars = BoolChars.var a; chars = VarChars.var a;
times = BoolTimes.var a; times = VarTimes.var a;
xml = BoolXml.var a; xml = VarXml.var a;
arrow = BoolArrow.var a; arrow = VarArrow.var a;
record= BoolRec.var a; record= VarRec.var a;
abstract = BoolAbstracts.var a; abstract = VarAbstracts.var a;
absent = false; absent = false;
} }
let char c = { empty with chars = BoolChars.atom (`Atm c) } let char c = { empty with chars = VarChars.atom (`Atm c) }
let interval i = { empty with ints = BoolIntervals.atom (`Atm i) } let interval i = { empty with ints = VarIntervals.atom (`Atm i) }
let abstract a = { empty with abstract = BoolAbstracts.atom (`Atm a) } let abstract a = { empty with abstract = VarAbstracts.atom (`Atm a) }
let cup x y = let cup x y =
if x == y then x else if x == y then x else
{ {
ints = BoolIntervals.cup x.ints y.ints; ints = VarIntervals.cup x.ints y.ints;
atoms = BoolAtoms.cup x.atoms y.atoms; atoms = VarAtoms.cup x.atoms y.atoms;
chars = BoolChars.cup x.chars y.chars; chars = VarChars.cup x.chars y.chars;
times = BoolTimes.cup x.times y.times; times = VarTimes.cup x.times y.times;
xml = BoolXml.cup x.xml y.xml; xml = VarXml.cup x.xml y.xml;
arrow = BoolArrow.cup x.arrow y.arrow; arrow = VarArrow.cup x.arrow y.arrow;
record= BoolRec.cup x.record y.record; record= VarRec.cup x.record y.record;
abstract = BoolAbstracts.cup x.abstract y.abstract; abstract = VarAbstracts.cup x.abstract y.abstract;
absent = x.absent || y.absent; absent = x.absent || y.absent;
} }
let cap x y = let cap x y =
if x == y then x else if x == y then x else
{ {
atoms = BoolAtoms.cap x.atoms y.atoms; atoms = VarAtoms.cap x.atoms y.atoms;
ints = BoolIntervals.cap x.ints y.ints; ints = VarIntervals.cap x.ints y.ints;
chars = BoolChars.cap x.chars y.chars; chars = VarChars.cap x.chars y.chars;
times = BoolTimes.cap x.times y.times; times = VarTimes.cap x.times y.times;
xml = BoolXml.cap x.xml y.xml; xml = VarXml.cap x.xml y.xml;
arrow = BoolArrow.cap x.arrow y.arrow; arrow = VarArrow.cap x.arrow y.arrow;
record = BoolRec.cap x.record y.record; record = VarRec.cap x.record y.record;
abstract = BoolAbstracts.cap x.abstract y.abstract; abstract = VarAbstracts.cap x.abstract y.abstract;
absent= x.absent && y.absent; absent= x.absent && y.absent;
} }
let diff x y = let diff x y =
if x == y then empty else if x == y then empty else
{ {
atoms = BoolAtoms.diff x.atoms y.atoms; atoms = VarAtoms.diff x.atoms y.atoms;
ints = BoolIntervals.diff x.ints y.ints; ints = VarIntervals.diff x.ints y.ints;
chars = BoolChars.diff x.chars y.chars; chars = VarChars.diff x.chars y.chars;
times = BoolTimes.diff x.times y.times; times = VarTimes.diff x.times y.times;
xml = BoolXml.diff x.xml y.xml; xml = VarXml.diff x.xml y.xml;
arrow = BoolArrow.diff x.arrow y.arrow; arrow = VarArrow.diff x.arrow y.arrow;
record= BoolRec.diff x.record y.record; record= VarRec.diff x.record y.record;
abstract = BoolAbstracts.diff x.abstract y.abstract; abstract = VarAbstracts.diff x.abstract y.abstract;
absent= x.absent && not y.absent; absent= x.absent && not y.absent;
} }
(* TODO: optimize disjoint check for boolean combinations *) (* TODO: optimize disjoint check for boolean combinations *)
let trivially_disjoint a b = let trivially_disjoint a b =
(BoolChars.trivially_disjoint a.chars b.chars) && (VarChars.trivially_disjoint a.chars b.chars) &&
(BoolIntervals.trivially_disjoint a.ints b.ints) && (VarIntervals.trivially_disjoint a.ints b.ints) &&
(BoolAtoms.trivially_disjoint a.atoms b.atoms) && (VarAtoms.trivially_disjoint a.atoms b.atoms) &&
(BoolTimes.trivially_disjoint a.times b.times) && (VarTimes.trivially_disjoint a.times b.times) &&
(BoolXml.trivially_disjoint a.xml b.xml) && (VarXml.trivially_disjoint a.xml b.xml) &&
(BoolArrow.trivially_disjoint a.arrow b.arrow) && (VarArrow.trivially_disjoint a.arrow b.arrow) &&
(BoolRec.trivially_disjoint a.record b.record) && (VarRec.trivially_disjoint a.record b.record) &&
(BoolAbstracts.trivially_disjoint a.abstract b.abstract) && (VarAbstracts.trivially_disjoint a.abstract b.abstract) &&
(not (a.absent && b.absent)) (not (a.absent && b.absent))
let rec constant = function let rec constant = function
...@@ -764,17 +762,17 @@ module Witness = struct ...@@ -764,17 +762,17 @@ module Witness = struct
(* type_has checks if a witness is contained in the union of (* type_has checks if a witness is contained in the union of
* the leafs of a bdd, ignoring all variables. *) * the leafs of a bdd, ignoring all variables. *)
and type_has t = function and type_has t = function
| WInt i -> Intervals.contains i (BoolIntervals.leafconj t.ints) | WInt i -> Intervals.contains i (VarIntervals.leafconj t.ints)
| WChar c -> Chars.contains c (BoolChars.leafconj t.chars) | WChar c -> Chars.contains c (VarChars.leafconj t.chars)
| WAtom a -> Atoms.contains_sample a (BoolAtoms.leafconj t.atoms) | WAtom a -> Atoms.contains_sample a (VarAtoms.leafconj t.atoms)
| WPair (w1,w2,_) -> | WPair (w1,w2,_) ->
bool_pair bool_pair
(fun (n1,n2) -> node_has n1 w1 && node_has n2 w2) (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
(BoolTimes.leafconj t.times) (VarTimes.leafconj t.times)
| WXml (w1,w2,_) -> | WXml (w1,w2,_) ->
bool_pair bool_pair
(fun (n1,n2) -> node_has n1 w1 && node_has n2 w2) (fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
(BoolXml.leafconj t.xml) (VarXml.leafconj t.xml)
| WFun (f,_) -> | WFun (f,_) ->
bool_pair bool_pair
(fun (n1,n2) -> (fun (n1,n2) ->
...@@ -784,7 +782,7 @@ module Witness = struct ...@@ -784,7 +782,7 @@ module Witness = struct
(match y with None -> false (match y with None -> false
| Some y -> node_has n2 y)) | Some y -> node_has n2 y))
f) f)
(BoolArrow.leafconj t.arrow) (VarArrow.leafconj t.arrow)
| WRecord (f,o,_) -> | WRecord (f,o,_) ->
bool_rec bool_rec
(fun (o',f') -> (fun (o',f') ->
...@@ -803,9 +801,9 @@ module Witness = struct ...@@ -803,9 +801,9 @@ module Witness = struct
because of an invariant. Otherwise, we must because of an invariant. Otherwise, we must
check that all are WAbsent here. *) check that all are WAbsent here. *)
with Exit -> false)) with Exit -> false))
(BoolRec.leafconj t.record) (VarRec.leafconj t.record)
| WAbsent -> t.absent | WAbsent -> t.absent
| WAbstract a -> Abstracts.contains_sample a (BoolAbstracts.leafconj t.abstract) | WAbstract a -> Abstracts.contains_sample a (VarAbstracts.leafconj t.abstract)
end end
type slot = { mutable status : status; type slot = { mutable status : status;
...@@ -859,24 +857,24 @@ let rec slot d = ...@@ -859,24 +857,24 @@ let rec slot d =
Stats.Counter.incr count_subtype; Stats.Counter.incr count_subtype;
(* XXX here I call leafconj a zilliontime. REWRITE !!! *) (* XXX here I call leafconj a zilliontime. REWRITE !!! *)
if d.absent then slot_nempty Witness.WAbsent if d.absent then slot_nempty Witness.WAbsent
else if not (Intervals.is_empty (BoolIntervals.leafconj d.ints)) else if not (Intervals.is_empty (VarIntervals.leafconj d.ints))
then slot_nempty (Witness.WInt (Intervals.sample (BoolIntervals.leafconj d.ints))) then slot_nempty (Witness.WInt (Intervals.sample (VarIntervals.leafconj d.ints)))
else if not (Atoms.is_empty (BoolAtoms.leafconj d.atoms)) else if not (Atoms.is_empty (VarAtoms.leafconj d.atoms))
then slot_nempty (Witness.WAtom (Atoms.sample (BoolAtoms.leafconj d.atoms))) then slot_nempty (Witness.WAtom (Atoms.sample (VarAtoms.leafconj d.atoms)))
else if not (Chars.is_empty (BoolChars.leafconj d.chars)) else if not (Chars.is_empty (VarChars.leafconj d.chars))
then slot_nempty (Witness.WChar (Chars.sample (BoolChars.leafconj d.chars))) then slot_nempty (Witness.WChar (Chars.sample (VarChars.leafconj d.chars)))
else if not (Abstracts.is_empty (BoolAbstracts.leafconj d.abstract)) else if not (Abstracts.is_empty (VarAbstracts.leafconj d.abstract))
then slot_nempty (Witness.WAbstract (Abstracts.sample (BoolAbstracts.leafconj d.abstract))) then slot_nempty (Witness.WAbstract (Abstracts.sample (VarAbstracts.leafconj d.abstract)))
else try else try
DescrHash.find memo d DescrHash.find memo d
with Not_found -> with Not_found ->
let s = { status = Maybe; active = false; notify = Nothing } in let s = { status = Maybe; active = false; notify = Nothing } in
DescrHash.add memo d s; DescrHash.add memo d s;
(try (try
iter_s s check_times (Pair.get (BoolTimes.leafconj d.times)); iter_s s check_times (Pair.get (VarTimes.leafconj d.times));
iter_s s check_xml (Pair.get (BoolXml.leafconj d.xml)); iter_s s check_xml (Pair.get (VarXml.leafconj d.xml));
iter_s s check_arrow (Pair.get (BoolArrow.leafconj d.arrow)); iter_s s check_arrow (Pair.get (VarArrow.leafconj d.arrow));
iter_s s check_record (get_record (BoolRec.leafconj d.record)); iter_s s check_record (get_record (VarRec.leafconj d.record));
if s.active then marks := s :: !marks else s.status <- Empty; if s.active then marks := s :: !marks else s.status <- Empty;
with NotEmpty -> ()); with NotEmpty -> ());
s s
...@@ -1003,8 +1001,8 @@ let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1) ...@@ -1003,8 +1001,8 @@ let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
let atom a = let atom a =
let atm = let atm =
if Atoms.(is_empty (diff full a)) then if Atoms.(is_empty (diff full a)) then
BoolAtoms.full VarAtoms.full
else BoolAtoms.atom (`Atm a) else VarAtoms.atom (`Atm a)
in in
{ empty with atoms = atm } { empty with atoms = atm }
...@@ -1012,14 +1010,14 @@ let times x y = ...@@ -1012,14 +1010,14 @@ let times x y =
if subtype any x.Node.descr if subtype any x.Node.descr
&& subtype any y.Node.descr && subtype any y.Node.descr
then then
{ empty with times = BoolTimes.full } { empty with times = VarTimes.full }
else times x y else times x y
let xml x y = let xml x y =
if subtype any x.Node.descr if subtype any x.Node.descr
&& subtype any y.Node.descr && subtype any y.Node.descr
then then
{ empty with xml = BoolXml.full } { empty with xml = VarXml.full }
else xml x y else xml x y
module Cache = struct module Cache = struct
...@@ -1150,8 +1148,8 @@ struct ...@@ -1150,8 +1148,8 @@ struct
let get ?(kind=`Normal) d = let get ?(kind=`Normal) d =
match kind with match kind with
| `Normal -> partition any (BoolTimes.leafconj d.times) | `Normal -> partition any (VarTimes.leafconj d.times)
| `XML -> partition any_pair (BoolXml.leafconj d.xml) | `XML -> partition any_pair (VarXml.leafconj d.xml)
let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty 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 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
...@@ -1195,8 +1193,8 @@ struct ...@@ -1195,8 +1193,8 @@ struct
let normal ?(kind=`Normal) d = let normal ?(kind=`Normal) d =
match kind with match kind with
| `Normal -> normal_times (BoolTimes.leafconj d.times) | `Normal -> normal_times (VarTimes.leafconj d.times)
| `XML -> normal_xml (BoolXml.leafconj d.xml) | `XML -> normal_xml (VarXml.leafconj d.xml)
(* (*
...@@ -1276,7 +1274,7 @@ struct ...@@ -1276,7 +1274,7 @@ struct
end end
module TR = Normal.Make(T)(R) module TR = Normal.Make(T)(R)
let any_record = { empty with record = BoolRec.full } let any_record = { empty with record = VarRec.full }
let atom o l = let atom o l =
if o && LabelMap.is_empty l then any_record else if o && LabelMap.is_empty l then any_record else
...@@ -1312,7 +1310,7 @@ struct ...@@ -1312,7 +1310,7 @@ struct
| [] -> (p,accu) :: b in