Commit 062d5039 authored by Kim Nguyễn's avatar Kim Nguyễn

Rework the types modules to seal the internal representation.

parent 9386685d
......@@ -147,26 +147,37 @@ type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ =
absent : bool;
}
module type VarType =
sig
include Bool.V
type descr
val inj : t -> descr
val proj : descr -> t
end
module BoolAtoms = Bool.MakeVar(Atoms)
module BoolIntervals = Bool.MakeVar(Intervals)
module BoolChars = Bool.MakeVar(Chars)
module BoolAbstracts = Bool.MakeVar(Abstracts)
let empty_descr_ = { atoms = Bool.empty;
ints = Bool.empty;
chars = Bool.empty;
times = Bool.empty;
xml = Bool.empty;
arrow = Bool.empty;
record = Bool.empty;
abstract = Bool.empty;
absent = false }
module rec Descr :
sig
include Custom.T with
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t,
BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_
val empty: t
val any : t
val is_empty : t -> bool
end =
struct
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolPair.t,
BoolPair.t, BoolPair.t, BoolRec.t, BoolAbstracts.t) descr_
type t = (BoolAtoms.t, BoolIntervals.t, BoolChars.t, BoolTimes.t,
BoolXml.t, BoolArrow.t, BoolRec.t, BoolAbstracts.t) descr_
let dump ppf d =
Format.fprintf ppf "@[<v 1>types:@\n\
......@@ -174,41 +185,31 @@ struct
@<1> ints: %a@\n\
@<1> chars: %a@\n\
@<1> times: %a@\n\
@<1> xml: %a@\n\
@<1> arrow: %a@\n\
@<1> record: %a@\n\
@<1> xml: %a@\n\
@<1> abstract: %a@\n\
@<1> absent: %b@]@\n"
BoolAtoms.dump d.atoms
BoolIntervals.dump d.ints
BoolChars.dump d.chars
BoolPair.dump d.times
BoolPair.dump d.arrow
BoolTimes.dump d.times
BoolXml.dump d.xml
BoolArrow.dump d.arrow
BoolRec.dump d.record
BoolPair.dump d.xml
BoolAbstracts.dump d.abstract
d.absent
let empty = {
times = BoolPair.empty;
xml = BoolPair.empty;
arrow = BoolPair.empty;
record= BoolRec.empty;
ints = BoolIntervals.empty;
atoms = BoolAtoms.empty;
chars = BoolChars.empty;
abstract = BoolAbstracts.empty;
absent = false;
}
let empty = empty_descr_
let any = {
times = BoolPair.full;
xml = BoolPair.full;
arrow = BoolPair.full;
record = BoolRec.full;
ints = BoolIntervals.full;
atoms = BoolAtoms.full;
chars = BoolChars.full;
times = BoolTimes.full;
xml = BoolXml.full;
arrow = BoolArrow.full;
record = BoolRec.full;
abstract = BoolAbstracts.full;
absent = false;
}
......@@ -217,9 +218,9 @@ struct
BoolChars.check a.chars;
BoolIntervals.check a.ints;
BoolAtoms.check a.atoms;
BoolPair.check a.times;
BoolPair.check a.xml;
BoolPair.check a.arrow;
BoolTimes.check a.times;
BoolXml.check a.xml;
BoolArrow.check a.arrow;
BoolRec.check a.record;
BoolAbstracts.check a.abstract;
()
......@@ -229,9 +230,9 @@ struct
(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) &&
(BoolTimes.equal a.times b.times) &&
(BoolXml.equal a.xml b.xml) &&
(BoolArrow.equal a.arrow b.arrow) &&
(BoolRec.equal a.record b.record) &&
(BoolAbstracts.equal a.abstract b.abstract) &&
(a.absent == b.absent)
......@@ -241,9 +242,9 @@ struct
(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) &&
(BoolTimes.is_empty a.times) &&
(BoolXml.is_empty a.xml) &&
(BoolArrow.is_empty a.arrow) &&
(BoolRec.is_empty a.record) &&
(BoolAbstracts.is_empty a.abstract)
......@@ -252,9 +253,9 @@ struct
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 = BoolTimes.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 = BoolArrow.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
......@@ -265,9 +266,9 @@ struct
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 + BoolTimes.hash a.times in
let accu = 17 * accu + BoolXml.hash a.xml in
let accu = 17 * accu + BoolArrow.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
......@@ -299,10 +300,75 @@ struct
end
and BoolAtoms : VarType with type Atom.t = Atoms.t
and type descr = Descr.t
=
struct
include Bool.MakeVar(Atoms)
type descr = Descr.t
let inj t = { empty_descr_ with atoms = t }
let proj t = t.atoms
end
and BoolIntervals : VarType with type Atom.t = Intervals.t
and type descr = Descr.t
=
struct
include Bool.MakeVar(Intervals)
type descr = Descr.t
let inj t = { empty_descr_ with ints = t }
let proj t = t.ints
end
and BoolChars : VarType with type Atom.t = Chars.t
and type descr = Descr.t
=
struct
include Bool.MakeVar(Chars)
type descr = Descr.t
let inj t = { empty_descr_ with chars = t }
let proj t = t.chars
end
and BoolAbstracts : VarType with type Atom.t = Abstracts.t
and type descr = Descr.t
=
struct
include Bool.MakeVar(Abstracts)
type descr = Descr.t
let inj t = { empty_descr_ with abstract = t }
let proj t = t.abstract
end
and Pair : Bool.S with type elem = (Node.t * Node.t) =
Bool.Make(Custom.Pair(Node)(Node))
and BoolPair : Bool.V with module Atom = Pair = Bool.MakeVar(Pair)
and BoolTimes : VarType with module Atom = Pair
and type descr = Descr.t
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with times = t }
let proj (t : descr) : t = t.times
end
and BoolXml : VarType with module Atom = Pair
and type descr = Descr.t
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with xml = t }
let proj (t : descr) : t = t.xml
end
and BoolArrow : VarType with module Atom = Pair
and type descr = Descr.t
=
struct include Bool.MakeVar(Pair)
type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with arrow = t }
let proj (t : descr) : t = t.arrow
end
(* bool = true means that the record is open that is, that
* the labels that are not in the domain of the map are
......@@ -311,7 +377,14 @@ and BoolPair : Bool.V with module Atom = Pair = Bool.MakeVar(Pair)
and Rec : Bool.S with type elem = bool * Node.t Ident.label_map =
Bool.Make(Custom.Pair(Custom.Bool)(LabelSet.MakeMap(Node)))
and BoolRec : Bool.V with module Atom = Rec = Bool.MakeVar(Rec)
and BoolRec : VarType with module Atom = Rec
and type descr = Descr.t
=
struct include Bool.MakeVar(Rec)
type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with record = t }
let proj (t : descr) : t = t.record
end
module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr)
......@@ -348,9 +421,9 @@ 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 times x y = { empty with times = BoolTimes.atom (`Atm (Pair.atom (x,y))) }
let xml x y = { empty with xml = BoolXml.atom (`Atm (Pair.atom (x,y))) }
let arrow x y = { empty with arrow = BoolArrow.atom (`Atm (Pair.atom (x,y))) }
let record label t =
{ empty with record = BoolRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) }
......@@ -363,13 +436,13 @@ let atom a = { empty with atoms = BoolAtoms.atom (`Atm a) }
(* Atm = Any ^ a *)
let var a =
{
times = BoolPair.var a;
xml = BoolPair.var a;
arrow = BoolPair.var a;
record= BoolRec.var a;
ints = BoolIntervals.var a;
atoms = BoolAtoms.var a;
chars = BoolChars.var a;
times = BoolTimes.var a;
xml = BoolXml.var a;
arrow = BoolArrow.var a;
record= BoolRec.var a;
abstract = BoolAbstracts.var a;
absent = false;
}
......@@ -381,13 +454,13 @@ 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;
times = BoolTimes.cup x.times y.times;
xml = BoolXml.cup x.xml y.xml;
arrow = BoolArrow.cup x.arrow y.arrow;
record= BoolRec.cup x.record y.record;
abstract = BoolAbstracts.cup x.abstract y.abstract;
absent = x.absent || y.absent;
}
......@@ -395,13 +468,13 @@ let cup x y =
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;
ints = BoolIntervals.cap x.ints y.ints;
chars = BoolChars.cap x.chars y.chars;
times = BoolTimes.cap x.times y.times;
xml = BoolXml.cap x.xml y.xml;
arrow = BoolArrow.cap x.arrow y.arrow;
record = BoolRec.cap x.record y.record;
abstract = BoolAbstracts.cap x.abstract y.abstract;
absent= x.absent && y.absent;
}
......@@ -409,13 +482,13 @@ let cap x y =
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;
ints = BoolIntervals.diff x.ints y.ints;
chars = BoolChars.diff x.chars y.chars;
times = BoolTimes.diff x.times y.times;
xml = BoolXml.diff x.xml y.xml;
arrow = BoolArrow.diff x.arrow y.arrow;
record= BoolRec.diff x.record y.record;
abstract = BoolAbstracts.diff x.abstract y.abstract;
absent= x.absent && not y.absent;
}
......@@ -425,9 +498,9 @@ 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) &&
(BoolTimes.trivially_disjoint a.times b.times) &&
(BoolXml.trivially_disjoint a.xml b.xml) &&
(BoolArrow.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))
......@@ -697,11 +770,11 @@ module Witness = struct
| WPair (w1,w2,_) ->
bool_pair
(fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
(BoolPair.leafconj t.times)
(BoolTimes.leafconj t.times)
| WXml (w1,w2,_) ->
bool_pair
(fun (n1,n2) -> node_has n1 w1 && node_has n2 w2)
(BoolPair.leafconj t.xml)
(BoolXml.leafconj t.xml)
| WFun (f,_) ->
bool_pair
(fun (n1,n2) ->
......@@ -711,7 +784,7 @@ module Witness = struct
(match y with None -> false
| Some y -> node_has n2 y))
f)
(BoolPair.leafconj t.arrow)
(BoolArrow.leafconj t.arrow)
| WRecord (f,o,_) ->
bool_rec
(fun (o',f') ->
......@@ -800,9 +873,9 @@ let rec slot d =
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_times (Pair.get (BoolTimes.leafconj d.times));
iter_s s check_xml (Pair.get (BoolXml.leafconj d.xml));
iter_s s check_arrow (Pair.get (BoolArrow.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 -> ());
......@@ -939,14 +1012,14 @@ let times x y =
if subtype any x.Node.descr
&& subtype any y.Node.descr
then
{ empty with times = BoolPair.full }
{ empty with times = BoolTimes.full }
else times x y
let xml x y =
if subtype any x.Node.descr
&& subtype any y.Node.descr
then
{ empty with xml = BoolPair.full }
{ empty with xml = BoolXml.full }
else xml x y
module Cache = struct
......@@ -1077,8 +1150,8 @@ struct
let get ?(kind=`Normal) d =
match kind with
| `Normal -> partition any (BoolPair.leafconj d.times)
| `XML -> partition any_pair (BoolPair.leafconj d.xml)
| `Normal -> partition any (BoolTimes.leafconj d.times)
| `XML -> partition any_pair (BoolXml.leafconj d.xml)
let pi1 = List.fold_left (fun acc (t1,_) -> cup acc t1) empty
let pi2 = List.fold_left (fun acc (_,t2) -> cup acc t2) empty
......@@ -1122,8 +1195,8 @@ struct
let normal ?(kind=`Normal) d =
match kind with
| `Normal -> normal_times (BoolPair.leafconj d.times)
| `XML -> normal_xml (BoolPair.leafconj d.xml)
| `Normal -> normal_times (BoolTimes.leafconj d.times)
| `XML -> normal_xml (BoolXml.leafconj d.xml)
(*
......@@ -1388,7 +1461,7 @@ struct
not (List.exists (check_simple left) right)
let sample t =
let (left,right) = List.find check_line_non_empty (Pair.get (BoolPair.leafconj t.arrow)) in
let (left,right) = List.find check_line_non_empty (Pair.get (BoolArrow.leafconj t.arrow)) in
List.fold_left (fun accu (t,s) -> cap accu (arrow t s))
{ empty with arrow = any.arrow } left
......@@ -1418,7 +1491,7 @@ struct
in
(* considering only arrows here and not poly variables is correct as
* the iface is just an intersection of arrows *)
aux (Pair.get (BoolPair.leafconj s.arrow))
aux (Pair.get (BoolArrow.leafconj s.arrow))
type t = descr * (descr * descr) list list
......@@ -1433,7 +1506,7 @@ struct
else accu
)
(any, [])
(Pair.get (BoolPair.leafconj t.arrow))
(Pair.get (BoolArrow.leafconj t.arrow))
let domain (dom,_) = dom
......@@ -1538,8 +1611,8 @@ module Iter =
if normalize && Pervasives.(kind <> `Arrow) then
let rects =
match kind with
`Times -> Product.normal ~kind:`Normal { Descr.empty with times = BoolPair.atom (`Atm p) }
| `Xml -> Product.normal ~kind:`XML { Descr.empty with xml = BoolPair.atom (`Atm p) }
`Times -> Product.normal ~kind:`Normal { Descr.empty with times = BoolTimes.atom (`Atm p) }
| `Xml -> Product.normal ~kind:`XML { Descr.empty with xml = BoolXml.atom (`Atm p) }
| _ -> assert false
in
List.fold_left (fun acc (d1, d2) -> cup acc (mk (cons d1, cons d2))) empty rects
......@@ -1556,11 +1629,11 @@ module Iter =
~empty ~full:any_char ~cup ~cap ~diff ~atom:(var_or char) t.chars);
(BoolAbstracts.compute
~empty ~full:any_abs ~cup ~cap ~diff ~atom:(var_or abs) t.abstract);
(BoolPair.compute
(BoolTimes.compute
~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Times)) t.times);
(BoolPair.compute
(BoolXml.compute
~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Xml)) t.xml);
(BoolPair.compute
(BoolArrow.compute
~empty ~full:any_arrow ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Arrow)) t.arrow);
(BoolRec.compute
~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);]
......@@ -1609,11 +1682,11 @@ module Iter =
abstract = aux (fun i -> { empty with abstract = i })
(module BoolAbstracts) t.abstract;
times = aux (fun i -> { empty with times = i })
(module BoolPair) t.times;
(module BoolTimes) t.times;
xml = aux (fun i -> { empty with xml = i })
(module BoolPair) t.xml;
(module BoolXml) t.xml;
arrow = aux (fun i -> { empty with arrow = i })
(module BoolPair) t.arrow;
(module BoolArrow) t.arrow;
record = aux (fun i -> { empty with record = i })
(module BoolRec) t.record;
}
......@@ -1657,7 +1730,7 @@ module Iter =
let cplx_bdd (type atom) (type atom2)
any
do_atom
(module BV : Bool.V with type Atom.t = atom and type Atom.elem = atom2)
(module BV : VarType with type Atom.t = atom and type Atom.elem = atom2)
acc
bdd
=
......@@ -1669,9 +1742,9 @@ module Iter =
let acc = simple_bdd any_atoms (var_or atoms) (module BoolAtoms) acc t.atoms in
let acc = simple_bdd any_chars (var_or chars) (module BoolChars) acc t.chars in
let acc = simple_bdd any_abstract (var_or abstract) (module BoolAbstracts) acc t.abstract in
let acc = cplx_bdd any_times times (module BoolPair) acc t.times in
let acc = cplx_bdd any_xml xml (module BoolPair) acc t.xml in
let acc = cplx_bdd any_arrow arrow (module BoolPair) acc t.arrow in
let acc = cplx_bdd any_times times (module BoolTimes) acc t.times in
let acc = cplx_bdd any_xml xml (module BoolXml) acc t.xml in
let acc = cplx_bdd any_arrow arrow (module BoolArrow) acc t.arrow in
let acc = cplx_bdd any_record record (module BoolRec) acc t.record in
match acc with
[ e ] -> e
......@@ -2006,7 +2079,7 @@ module Print = struct
let named_xml = ref DescrPairMap.empty
let register_global (cu,name,al) d =
let d = uniq d in
if equal { d with xml = BoolPair.empty } empty then begin
if equal { d with xml = BoolXml.empty } empty then begin
match Product.get ~kind:`XML d with
| [(t1,t2)] ->
if DescrPairMap.mem (t1,t2) !named_xml then ()
......@@ -2019,7 +2092,7 @@ module Print = struct
let unregister_global d =
let d = uniq d in
if equal { d with xml = BoolPair.empty } empty then begin
if equal { d with xml = BoolXml.empty } empty then begin
match Product.get ~kind:`XML d with
| [(t1,t2)] ->
named_xml := DescrPairMap.remove (t1,t2) !named_xml
......@@ -2046,11 +2119,23 @@ module Print = struct
b == BoolRec.empty ||
(is_empty { empty with record = BoolRec.diff BoolRec.full b})
let trivial_pair b = b == BoolPair.empty || b == BoolPair.full
let trivial (type atom) (module T : VarType with type Atom.t = atom
and type descr = Descr.t) t =
let t1 = T.inj (T.proj t) in
is_empty t1 ||
is_empty (diff (T.inj T.full) t1)
let worth_abbrev d =
not (
trivial (module BoolTimes) d
&& trivial (module BoolXml) d
&& trivial (module BoolArrow) d
&& trivial (module BoolRec) d
)
(* let worth_abbrev d =
not (trivial_pair d.times && trivial_pair d.xml &&
trivial_pair d.arrow && trivial_rec d.record)
*)
let worth_complement d =
let dd = diff any d in
......@@ -2156,9 +2241,9 @@ module Print = struct
fill_line (module BoolIntervals) h (fun t -> t.ints) (fun t u -> {t with ints = u }) d;
fill_line (module BoolChars) h (fun t -> t.chars) (fun t u -> {t with chars = u }) d;
fill_line (module BoolAtoms) h (fun t -> t.atoms) (fun t u -> {t with atoms = u }) d;
fill_line (module BoolPair) h (fun t -> t.times) (fun t u -> {t with times = u }) d;
fill_line (module BoolPair) h (fun t -> t.xml) (fun t u -> {t with xml = u }) d;
fill_line (module BoolPair) h (fun t -> t.arrow) (fun t u -> {t with arrow = u }) d;
fill_line (module BoolTimes) h (fun t -> t.times) (fun t u -> {t with times = u }) d;
fill_line (module BoolXml) h (fun t -> t.xml) (fun t u -> {t with xml = u }) d;
fill_line (module BoolArrow) h (fun t -> t.arrow) (fun t u -> {t with arrow = u }) d;
fill_line (module BoolRec) h (fun t -> t.record) (fun t u -> {t with record = u }) d;
fill_line (module BoolAbstracts) h (fun t -> t.abstract) (fun t u -> {t with abstract = u }) d;
let h =
......@@ -2178,9 +2263,9 @@ module Print = struct
let t = update_field (module BoolIntervals) (fun t -> t.ints) (fun t u -> {t with ints = u }) no_var t in
let t = update_field (module BoolChars) (fun t -> t.chars) (fun t u -> {t with chars = u }) no_var t in
let t = update_field (module BoolAtoms) (fun t -> t.atoms) (fun t u -> {t with atoms = u }) no_var t in
let t = update_field (module BoolPair) (fun t -> t.times) (fun t u -> {t with times = u }) no_var t in
let t = update_field (module BoolPair) (fun t -> t.xml) (fun t u -> {t with xml = u }) no_var t in
let t = update_field (module BoolPair) (fun t -> t.arrow) (fun t u -> {t with arrow = u }) no_var t in
let t = update_field (module BoolTimes) (fun t -> t.times) (fun t u -> {t with times = u }) no_var t in
let t = update_field (module BoolXml) (fun t -> t.xml) (fun t u -> {t with xml = u }) no_var t in
let t = update_field (module BoolArrow) (fun t -> t.arrow) (fun t u -> {t with arrow = u }) no_var t in
let t = update_field (module BoolRec) (fun t -> t.record) (fun t u -> {t with record = u }) no_var t in
let t = update_field (module BoolAbstracts) (fun t -> t.abstract) (fun t u -> {t with abstract = u }) no_var t in t
in
......@@ -2369,7 +2454,7 @@ module Print = struct
List.fold_left (fun acc (t1,t2) ->
(Pair (prepare t1, prepare t2)) :: acc
)
u_acc (Product.partition any (BoolPair.leafconj tt.times))
u_acc (Product.partition any (BoolTimes.leafconj tt.times))
in
(* xml pairs *)
......@@ -2387,7 +2472,7 @@ module Print = struct
List.rev_map (fun (ta,tb) ->
(Xml (tag, prepare ta, prepare tb))
) (Product.get t2);
) (Product.partition any_pair (BoolPair.leafconj tt.xml))
) (Product.partition any_pair (BoolXml.leafconj tt.xml))
)
) @ u_acc
in
......@@ -2403,7 +2488,7 @@ module Print = struct
(prepare (descr t), prepare (descr s))) n
in
(Arrows (p,n))
) (Pair.get (BoolPair.leafconj tt.arrow))) @ u_acc
) (Pair.get (BoolArrow.leafconj tt.arrow))) @ u_acc
in
(* records *)
......@@ -2993,13 +3078,13 @@ let rec rec_normalize d =
memo_normalize := DescrMap.add d n !memo_normalize;
let times =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal d)
(fun accu (d1,d2) -> BoolTimes.cup accu (BoolTimes.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolTimes.empty (Product.normal d)
in
let xml =
List.fold_left
(fun accu (d1,d2) -> BoolPair.cup accu (BoolPair.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolPair.empty (Product.normal ~kind:`XML d)
(fun accu (d1,d2) -> BoolXml.cup accu (BoolXml.atom (`Atm (Pair.atom (rec_normalize d1, rec_normalize d2)))))
BoolXml.empty (Product.normal ~kind:`XML d)
in
let record = d.record
in
......@@ -3707,13 +3792,13 @@ module Tallying = struct
let single_ints = single_aux interval
let single_times = single_aux (fun p -> { empty with times = BoolPair.atom (`Atm p) })
let single_times = single_aux (fun p -> { empty with times = BoolTimes.atom (`Atm p) })
let single_xml = single_aux (fun p -> { empty with xml = BoolPair.atom (`Atm p) })
let single_xml = single_aux (fun p -> { empty with xml = BoolXml.atom (`Atm p) })
let single_record = single_aux (fun p -> { empty with record = BoolRec.atom (`Atm p) })
let single_arrow = single_aux (fun p -> { empty with arrow = BoolPair.atom (`Atm p) })
let single_arrow = single_aux (fun p -> { empty with arrow = BoolArrow.atom (`Atm p) })
(* check if there exists a toplevel variable : fun (pos,neg) *)
let toplevel delta single norm_rec mem p n =
......@@ -3817,11 +3902,11 @@ module Tallying = struct
DEBUG normrec (Format.eprintf "@[ - After Chars constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_ints normints acc (BoolIntervals.get t.ints) in
DEBUG normrec (Format.eprintf "@[ - After Ints constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_times normpair acc (BoolPair.get t.times) in
let acc = aux single_times normpair acc (BoolTimes.get t.times) in
DEBUG normrec (Format.eprintf "@[ - After Times constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_xml normpair acc (BoolPair.get t.xml) in
let acc = aux single_xml normpair acc (BoolXml.get t.xml) in
DEBUG normrec (Format.eprintf "@[ - After Xml constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_arrow normarrow acc (BoolPair.get t.arrow) in
let acc = aux single_arrow normarrow acc (BoolArrow.get t.arrow) in
DEBUG normrec (Format.eprintf "@[ - After Arrow constraints: %a @]@\n" CS.pp_s acc);
let acc = aux single_abstract normabstract acc (BoolAbstracts.get t.abstract) in
DEBUG normrec (Format.eprintf "@[ - After Abstract constraints: %a @]@\n" CS.pp_s acc);
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment