Commit 5641fa93 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Further simplify the type algebra code, using the newly introduced combinators...

Further simplify the type algebra code, using the newly introduced combinators (map/fold/iter) over types.
parent 1db0d21a
open Ident open Ident
open Encodings open Encodings
let (@@) f a = f a
let count = ref 0 let count = ref 0
let () = let () =
...@@ -147,12 +145,13 @@ type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ = ...@@ -147,12 +145,13 @@ type ('atoms, 'ints, 'chars, 'times, 'xml, 'arrow, 'record, 'abstract) descr_ =
absent : bool; absent : bool;
} }
module type VarType = module type VarTypeSig =
sig sig
include Bool.V include Bool.V
type descr type descr
val inj : t -> descr val inj : t -> descr
val proj : descr -> t val proj : descr -> t
val update : descr -> t -> descr
end end
let empty_descr_ = { atoms = Bool.empty; let empty_descr_ = { atoms = Bool.empty;
...@@ -298,7 +297,7 @@ struct ...@@ -298,7 +297,7 @@ 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 VarAtoms : VarType with type Atom.t = Atoms.t and VarAtoms : VarTypeSig with type Atom.t = Atoms.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -306,9 +305,10 @@ and VarAtoms : VarType with type Atom.t = Atoms.t ...@@ -306,9 +305,10 @@ and VarAtoms : VarType with type Atom.t = Atoms.t
type descr = Descr.t type descr = Descr.t
let inj t = { empty_descr_ with atoms = t } let inj t = { empty_descr_ with atoms = t }
let proj t = t.atoms let proj t = t.atoms
let update t d = { t with atoms = d }
end end
and VarIntervals : VarType with type Atom.t = Intervals.t and VarIntervals : VarTypeSig with type Atom.t = Intervals.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -316,9 +316,10 @@ and VarIntervals : VarType with type Atom.t = Intervals.t ...@@ -316,9 +316,10 @@ and VarIntervals : VarType with type Atom.t = Intervals.t
type descr = Descr.t type descr = Descr.t
let inj t = { empty_descr_ with ints = t } let inj t = { empty_descr_ with ints = t }
let proj t = t.ints let proj t = t.ints
let update t d = { t with ints = d }
end end
and VarChars : VarType with type Atom.t = Chars.t and VarChars : VarTypeSig with type Atom.t = Chars.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -326,9 +327,10 @@ and VarChars : VarType with type Atom.t = Chars.t ...@@ -326,9 +327,10 @@ and VarChars : VarType with type Atom.t = Chars.t
type descr = Descr.t type descr = Descr.t
let inj t = { empty_descr_ with chars = t } let inj t = { empty_descr_ with chars = t }
let proj t = t.chars let proj t = t.chars
let update t d = { t with chars = d }
end end
and VarAbstracts : VarType with type Atom.t = Abstracts.t and VarAbstracts : VarTypeSig with type Atom.t = Abstracts.t
and type descr = Descr.t and type descr = Descr.t
= =
struct struct
...@@ -336,36 +338,40 @@ and VarAbstracts : VarType with type Atom.t = Abstracts.t ...@@ -336,36 +338,40 @@ and VarAbstracts : VarType with type Atom.t = Abstracts.t
type descr = Descr.t type descr = Descr.t
let inj t = { empty_descr_ with abstract = t } let inj t = { empty_descr_ with abstract = t }
let proj t = t.abstract let proj t = t.abstract
let update t d = { t with abstract = d }
end end
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 VarTimes : VarType with module Atom = Pair and VarTimes : VarTypeSig with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
type descr = Descr.t type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with times = t } let inj (t : t) : descr = { empty_descr_ with times = t }
let proj (t : descr) : t = t.times let proj (t : descr) : t = t.times
let update (t : descr) (d : t) : descr = { t with times = d }
end end
and VarXml : VarType with module Atom = Pair and VarXml : VarTypeSig with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
type descr = Descr.t type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with xml = t } let inj (t : t) : descr = { empty_descr_ with xml = t }
let proj (t : descr) : t = t.xml let proj (t : descr) : t = t.xml
let update (t : descr) (d : t) : descr = { t with xml = d }
end end
and VarArrow : VarType with module Atom = Pair and VarArrow : VarTypeSig with module Atom = Pair
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Pair) struct include Bool.MakeVar(Pair)
type descr = Descr.t type descr = Descr.t
let inj (t : t) : descr = { empty_descr_ with arrow = t } let inj (t : t) : descr = { empty_descr_ with arrow = t }
let proj (t : descr) : t = t.arrow let proj (t : descr) : t = t.arrow
let update (t : descr) (d : t) : descr = { t with arrow = d }
end end
(* bool = true means that the record is open that is, that (* bool = true means that the record is open that is, that
...@@ -375,15 +381,20 @@ end ...@@ -375,15 +381,20 @@ 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 VarRec : VarType with module Atom = Rec and VarRec : VarTypeSig with module Atom = Rec
and type descr = Descr.t and type descr = Descr.t
= =
struct include Bool.MakeVar(Rec) struct include Bool.MakeVar(Rec)
type descr = Descr.t type descr = Descr.t
let full_atom = Rec.atom (true, LabelMap.empty)
let inj (t : t) : descr = { empty_descr_ with record = t } let inj (t : t) : descr = { empty_descr_ with record = t }
let proj (t : descr) : t = t.record let proj (t : descr) : t = t.record
let update (t : descr) (d : t) : descr = { t with record = d }
end end
module type VarType = VarTypeSig with type descr = Descr.t
module DescrHash = Hashtbl.Make(Descr) module DescrHash = Hashtbl.Make(Descr)
module DescrMap = Map.Make(Descr) module DescrMap = Map.Make(Descr)
module DescrSet = Set.Make(Descr) module DescrSet = Set.Make(Descr)
...@@ -419,17 +430,17 @@ let non_constructed_or_absent = ...@@ -419,17 +430,17 @@ 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 = VarTimes.atom (`Atm (Pair.atom (x,y))) } let times x y = VarTimes.inj (VarTimes.atom (`Atm (Pair.atom (x,y))))
let xml x y = { empty with xml = VarXml.atom (`Atm (Pair.atom (x,y))) } let xml x y = VarXml.inj (VarXml.atom (`Atm (Pair.atom (x,y))))
let arrow x y = { empty with arrow = VarArrow.atom (`Atm (Pair.atom (x,y))) } let arrow x y = VarArrow.inj (VarArrow.atom (`Atm (Pair.atom (x,y))))
let record label t = let record label t =
{ empty with record = VarRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))) } VarRec.inj (VarRec.atom (`Atm (Rec.atom (true,LabelMap.singleton label t))))
let record_fields x = let record_fields x =
{ empty with record = VarRec.atom (`Atm (Rec.atom x)) } VarRec.inj (VarRec.atom (`Atm (Rec.atom x)))
let atom a = { empty with atoms = VarAtoms.atom (`Atm a) } let atom a = VarAtoms.inj (VarAtoms.atom (`Atm a))
(* Atm = Any ^ a *) (* Atm = Any ^ a *)
let var a = let var a =
...@@ -445,14 +456,14 @@ let var a = ...@@ -445,14 +456,14 @@ let var a =
absent = false; absent = false;
} }
let char c = { empty with chars = VarChars.atom (`Atm c) } let char c = VarChars.inj (VarChars.atom (`Atm c))
let interval i = { empty with ints = VarIntervals.atom (`Atm i) } let interval i = VarIntervals.inj (VarIntervals.atom (`Atm i))
let abstract a = { empty with abstract = VarAbstracts.atom (`Atm a) } let abstract a = VarAbstracts.inj (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 = VarIntervals.cup x.ints y.ints; ints = VarIntervals.cup x.ints y.ints;
atoms = VarAtoms.cup x.atoms y.atoms; atoms = VarAtoms.cup x.atoms y.atoms;
chars = VarChars.cup x.chars y.chars; chars = VarChars.cup x.chars y.chars;
times = VarTimes.cup x.times y.times; times = VarTimes.cup x.times y.times;
...@@ -996,30 +1007,6 @@ let subtype d1 d2 = is_empty (diff d1 d2) ...@@ -996,30 +1007,6 @@ let subtype d1 d2 = is_empty (diff d1 d2)
let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1) let equiv d1 d2 = (subtype d1 d2) && (subtype d2 d1)
(* perform some semantic simplifications around type constructors *)
let atom a =
let atm =
if Atoms.(is_empty (diff full a)) then
VarAtoms.full
else VarAtoms.atom (`Atm a)
in
{ empty with atoms = atm }
let times x y =
if subtype any x.Node.descr
&& subtype any y.Node.descr
then
{ empty with times = VarTimes.full }
else times x y
let xml x y =
if subtype any x.Node.descr
&& subtype any y.Node.descr
then
{ empty with xml = VarXml.full }
else xml x y
module Cache = struct module Cache = struct
type 'a cache = type 'a cache =
...@@ -1577,123 +1564,71 @@ end ...@@ -1577,123 +1564,71 @@ end
module Iter = module Iter =
struct struct
let any_node2 = any_node, any_node
let compute ?(normalize=false) ~empty ~full ~cup ~cap ~diff ~var ~atom ~int ~char ~times ~xml ~arrow ~record ~abs ~opt t let all_fields : (module VarType) array = [|
(module VarAtoms); (module VarIntervals);
(module VarChars); (module VarTimes);
(module VarXml); (module VarArrow);
(module VarRec); (module VarAbstracts)
|]
let fold ?(abs=(fun _ x -> x))
(f : (module VarType) -> Descr.t -> 'a -> 'a) (t : Descr.t)
(acc : 'a) : 'a
= =
let var_or f = let acc = abs t.absent acc in
function `Atm a -> f a Array.fold_left (fun acc m -> f m t acc) acc all_fields
| `Var v -> var v
in let map ?(abs=(fun x -> x))
let any_atom = atom Atoms.full in (f : (module VarType) -> Descr.t -> Descr.t)
let any_int = int Intervals.full in (t : Descr.t) : Descr.t =
let any_char = char Chars.full in fold ~abs:(fun a t -> { t with absent = abs a })
let any_abs = abs Abstracts.full in (fun (module V : VarType) t acc ->
let any_times = times any_node2 in V.update acc (V.proj (f (module V) t)))
let any_xml = xml any_node2 in t empty
let any_record = record (true,LabelMap.empty) in
let any_arrow = diff full let iter ?(abs=(fun _ -> ()))
(List.fold_left cup any_atom (f : (module VarType) -> Descr.t -> unit) t
[ any_int; any_char; any_abs; any_times; any_xml; any_record ]) =
in fold ~abs:(fun a () -> abs a) (fun m t () -> f m t) t ()
let record_bdd p =
Rec.compute ~empty ~full:any_record ~cup ~cap ~diff ~atom:record p let clean_field (module V : VarType) t =
in let t_bdd = V.proj t in
let prod_bdd kind p = if is_empty (V.inj t_bdd) then V.update t V.empty else
let any,mk = if is_empty V.(inj (diff full t_bdd)) then V.update t V.full
match kind with else t
`Times -> any_times, times
| `Xml -> any_xml, xml
| `Arrow -> any_arrow, arrow
in
if normalize && Pervasives.(kind <> `Arrow) then
let rects =
match kind with
`Times -> Product.normal ~kind:`Normal { Descr.empty with times = VarTimes.atom (`Atm p) }
| `Xml -> Product.normal ~kind:`XML { Descr.empty with xml = VarXml.atom (`Atm p) }
| _ -> assert false
in
List.fold_left (fun acc (d1, d2) -> cup acc (mk (cons d1, cons d2))) empty rects
else
Pair.compute ~empty ~full:any ~cup ~cap ~diff ~atom:mk p
in
List.fold_left (fun acc e -> cup acc e)
(opt t.absent)
[ (VarAtoms.compute
~empty ~full:any_atom ~cup ~cap ~diff ~atom:(var_or atom) t.atoms);
(VarIntervals.compute
~empty ~full:any_int ~cup ~cap ~diff ~atom:(var_or int) t.ints);
(VarChars.compute
~empty ~full:any_char ~cup ~cap ~diff ~atom:(var_or char) t.chars);
(VarAbstracts.compute
~empty ~full:any_abs ~cup ~cap ~diff ~atom:(var_or abs) t.abstract);
(VarTimes.compute
~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Times)) t.times);
(VarXml.compute
~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Xml)) t.xml);
(VarArrow.compute
~empty ~full:any_arrow ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Arrow)) t.arrow);
(VarRec.compute
~empty ~full:any_record ~cup ~cap ~diff ~atom:(var_or record_bdd) t.record);]
let clean_type t = map clean_field t
let simplify = let simplify =
let memo = DescrHash.create 17 in let memo = DescrHash.create 17 in
let aux (type atom) let aux (module V : VarType) t =
inj let clean b = V.proj (clean_field (module V) (V.inj b)) in
(module BV : Bool.V with type Atom.t = atom ) b
=
let clean b =
if is_empty (inj b) then BV.empty else b
in
let rec loop b = let rec loop b =
match BV.extract b with match V.extract b with
`Split(`Var v, p, i , n) -> `Split(`Var v, p, i , n) ->
let p = loop p in let p = loop p and i = loop i and n = loop n in
let i = loop i in let tp = V.inj p and tn = V.inj n in
let n = loop n in
let tp = inj p and tn = inj n in
if disjoint tp tn then b if disjoint tp tn then b
else else
let v' = clean (BV.var v) in let v' = V.var v in
let p' = clean BV.(cap v' (diff p n)) in let p' = clean V.(cap v' (diff p n)) in
let n' = clean BV.(diff (diff n p) v') in let n' = clean V.(diff (diff n p) v') in
let i' = clean (BV.cap n p) in let i' = clean (V.cap n p) in
let i'' = clean (BV.cup i i') in let i'' = clean (V.cup i i') in
BV.(cup i'' (cup p' n')) clean V.(cup i'' (cup p' n'))
| _ -> b
| _ -> b
in in
loop b V.inj (loop (V.proj t))
in in
fun t -> fun t ->
try DescrHash.find memo t with try DescrHash.find memo t with
Not_found -> Not_found ->
let res = let res = clean_type (map aux t) in
{ t with DescrHash.add memo t res;
atoms = aux (fun i -> { empty with atoms = i }) DescrHash.add memo res res;
(module VarAtoms) t.atoms; res
chars = aux (fun i -> { empty with chars = i })
(module VarChars) t.chars;
ints = aux (fun i -> { empty with ints = i })
(module VarIntervals) t.ints;
abstract = aux (fun i -> { empty with abstract = i })
(module VarAbstracts) t.abstract;
times = aux (fun i -> { empty with times = i })
(module VarTimes) t.times;
xml = aux (fun i -> { empty with xml = i })
(module VarXml) t.xml;
arrow = aux (fun i -> { empty with arrow = i })
(module VarArrow) t.arrow;
record = aux (fun i -> { empty with record = i })
(module VarRec) t.record;
}
in
DescrHash.add memo t res;
DescrHash.add memo res res;
res
let compute_bdd ~typ ~cup ~cap ~neg ~var ~atoms ~ints ~chars ~times ~xml ~arrow ~record ~abstract ~absent t = let compute ~cup ~cap ~neg ~var ~atoms ~ints ~chars ~times ~xml ~arrow ~record ~abstract ~absent t =
let t = simplify t in let t = simplify t in
let any_node2 = any_node, any_node in let any_node2 = any_node, any_node in
let any_atoms = atoms Atoms.full in let any_atoms = atoms Atoms.full in
...@@ -1703,37 +1638,39 @@ module Iter = ...@@ -1703,37 +1638,39 @@ module Iter =
let any_times = times any_node2 in let any_times = times any_node2 in
let any_xml = xml any_node2 in let any_xml = xml any_node2 in
let any_record = record (true,LabelMap.empty) in let any_record = record (true,LabelMap.empty) in
let any_arrow = typ Arrow.any let any_arrow = arrow (empty_node,any_node) in
(*neg (cup ([ any_atoms;
any_ints; any_chars; any_abstract;
any_times; any_xml; any_record ])) *)
in
let var_or do_atom = let var_or do_atom =
function `Var v -> var v function `Var v -> var v
| `Atm atm -> do_atom atm | `Atm atm -> do_atom atm
in in
let simple_bdd (type bdd) (type atom) let simple_bdd (type bdd) (type atom)
any any
do_atom do_atom
(module B : Bool.S with type t = bdd and type elem = atom) acc bv = (module B : Bool.S with type t = bdd and type elem = atom)
acc
bv
=
List.fold_left (fun acc (ipos, ineg) -> List.fold_left (fun acc (ipos, ineg) ->
match List.map do_atom ipos, List.map do_atom ineg match List.map do_atom ipos, List.map do_atom ineg
with with
| [] , [] -> any :: acc | [] , [] -> any :: acc
| [ e ] , [] -> e :: acc | [ e ] , [] -> e :: acc
| [], l -> cap (any :: List.map neg l) :: acc | [], l -> cap (any :: List.map neg l) :: acc
| l1, l2 -> cap (l1 @ List.map neg l2) :: acc | l1, l2 -> cap (l1 @ List.map neg l2) :: acc
) acc (B.get bv) ) acc (B.get bv)
in in
let cplx_bdd (type atom) (type atom2) let cplx_bdd (type atom) (type atom2)
any any
do_atom do_atom
(module BV : VarType with type Atom.t = atom and type Atom.elem = atom2) (module V : VarType with type Atom.t = atom
acc and type Atom.elem = atom2)
bdd acc
= bdd
simple_bdd (cap[]) (var_or (fun t -> cup (simple_bdd (any) do_atom (module BV.Atom) [] t))) =
(module BV) acc bdd simple_bdd (cap[])
(var_or (fun t -> cup (simple_bdd (any) do_atom
(module V.Atom) [] t)))
(module V) acc bdd
in in
let acc = absent t.absent in let acc = absent t.absent in
let acc = simple_bdd any_ints (var_or ints) (module VarIntervals) acc t.ints in let acc = simple_bdd any_ints (var_or ints) (module VarIntervals) acc t.ints in
...@@ -1747,8 +1684,6 @@ module Iter = ...@@ -1747,8 +1684,6 @@ module Iter =
match acc with match acc with
[ e ] -> e [ e ] -> e
| _ -> cup acc | _ -> cup acc
end end
module Variable = module Variable =
...@@ -1756,74 +1691,8 @@ module Variable = ...@@ -1756,74 +1691,8 @@ module Variable =
type t = Var.t type t = Var.t
let var_cache = DescrHash.create 17 let var_cache = DescrHash.create 17
let collect_vars t =
let memo = DescrHash.create 17 in
let union s1 s2 =
match s1, s2 with
Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
| None, Some s | Some s, None -> Some s
| _ -> None
in
let inter s1 s2 =
match s1, s2 with
Some s1, Some s2 -> Some (Var.Set.cup s1 s2)
| _ -> None
in
let union3 (x1,y1,z1) (x2,y2,z2) =
union x1 x2, union y1 y2, union z1 z2
in
let inter3 (x1,y1,z1) (x2,y2,z2) =
inter x1 x2, inter y1 y2, inter z1 z2
in