Commit f31c8bf6 authored by Kim Nguyễn's avatar Kim Nguyễn

Make it so that the substitution function preserves as much sharing as...

Make it so that the substitution function preserves as much sharing as possible from the original type.
parent 792df7c1
......@@ -1501,34 +1501,28 @@ module Iter =
function `Atm a -> f a
| `Var v -> var v
in
let prod_bdd kind p =
let rects = Product.get ~kind
(if kind == `Normal then
{Descr.empty with times = BoolPair.atom (`Atm p) }
else {Descr.empty with xml = BoolPair.atom (`Atm p) })
in
List.fold_left
(fun acc (t1, t2) ->
let t1 = cons t1 and t2 = cons t2 in
cup acc (if kind == `Normal
then times (t1, t2) else xml (t1, t2))) empty rects
in
let record_bdd p =
Rec.compute ~empty ~full:(record (true,LabelMap.empty)) ~cup ~cap ~diff ~atom:record p
in
let any_atom = atom Atoms.full in
let any_int = int Intervals.full in
let any_char = char Chars.full in
let any_abs = abs Abstracts.full in
let any_times = prod_bdd `Normal Pair.full in
let any_xml = prod_bdd `XML Pair.full in
let any_record = record_bdd Rec.full in
let any_times = times any_node2 in
let any_xml = xml any_node2 in
let any_record = record (true,LabelMap.empty) in
let any_arrow = diff full
(List.fold_left cup any_atom
[ any_int; any_char; any_abs; any_times; any_xml; any_record ])
in
let arrow_bdd p =
Pair.compute ~empty ~full:any_arrow ~cup ~cap ~diff ~atom:arrow p
let record_bdd p =
Rec.compute ~empty ~full:any_record ~cup ~cap ~diff ~atom:record p
in
let prod_bdd kind p =
let any,mk =
match kind with
`Times -> any_times, times
| `Xml -> any_xml, xml
| `Arrow -> any_arrow, arrow
in
Pair.compute ~empty ~full:any ~cup ~cap ~diff ~atom:mk p
in
List.fold_left (fun acc e -> cup acc e)
(opt t.absent)
......@@ -1541,11 +1535,11 @@ module Iter =
(BoolAbstracts.compute
~empty ~full:any_abs ~cup ~cap ~diff ~atom:(var_or abs) t.abstract);
(BoolPair.compute
~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Normal)) t.times);
~empty ~full:any_times ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Times)) t.times);
(BoolPair.compute
~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `XML)) t.xml);
~empty ~full:any_xml ~cup ~cap ~diff ~atom:(var_or (prod_bdd `Xml)) t.xml);
(BoolPair.compute
~empty ~full:any_arrow ~cup ~cap ~diff ~atom:(var_or arrow_bdd) t.arrow);
~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);]
......@@ -2716,7 +2710,8 @@ module Positive = struct
|`Xml of v * v
|`Record of bool * (bool * Ns.Label.t * v) list
]
and v = { mutable def : rhs; mutable node : node option;
and v = { mutable def : rhs;
mutable node : node option;
mutable descr : Descr.t option;
}
......@@ -2847,7 +2842,9 @@ module Positive = struct
| Some s -> s
| None -> loop_struct t
in
node_t.def <- (rhs).def; node_t
node_t.def <- (rhs).def;
node_t.descr <- Some t;
node_t
in
res.descr <- Some t; res
and loop_struct t =
......@@ -2874,6 +2871,18 @@ struct
let identity = Map.empty
module MemoSubst = Hashtbl.Make(
struct
type t = Descr.t * Descr.t Map.map
let equal ((t1, m1) as x1) ((t2, m2) as x2) =
x1 == x2
|| ((equiv t1 t2) && (Map.equal equiv m1 m2))
let hash (t, m) =
Descr.hash t + 17 * Map.hash Descr.hash m
end
)
let add v t m =
if is_var t && Var.(equal v (Set.choose (all_vars t))) then m
else Map.add v t m
......@@ -2881,19 +2890,6 @@ struct
let of_list l =
List.fold_left (fun acc (v, t) -> add v t acc) identity l
module Memo = Hashtbl.Make
(struct
type subst = t
type t = Descr.t * subst
let equal ((t1, l1) as k1) ((t2, l2) as k2) =
k1 == k2
|| ((t1 == t2 || Descr.equal t1 t2)
&& (l1 == l2 || Map.equal Descr.equal l1 l2))
let hash (t, l) =
(Descr.hash t + 31 * Map.hash Descr.hash l) land 0x3fff_ffff
end)
let global_memo = Memo.create 17
let decompose t =
let open Positive in
let res = decompose
......@@ -2906,15 +2902,53 @@ struct
in
res
let app_subst v subst =
let subst_cache = MemoSubst.create 17
let get_opt = function Some e -> e | None -> raise Not_found
let app_subst t subst =
if Map.is_empty subst then t else
let todo = ref [] in
try
MemoSubst.find subst_cache (t, subst)
with
Not_found ->
let res =
let v = decompose t in
descr (
Positive.solve_gen ~stop_descr:(fun v ->
try
Some (MemoSubst.find subst_cache
(get_opt v.Positive.descr, subst))
with
Not_found ->
let () =
match v.Positive.descr,v.Positive.node with
Some t, Some n -> todo := (t, n) :: !todo
| _ -> ()
in
match v.Positive.def with
`Variable d -> (try Some (Map.assoc d subst) with Not_found -> None)
| _ -> None) v
`Variable d -> (try Some (Map.assoc d subst)
with Not_found -> None)
| _ -> None
) v)
in
let lsubst = Map.get subst in
List.iter (fun (t, n) ->
let nt = descr n in
if not (DescrMap.mem nt !Print.named) then begin
try
let (cu, name, args) = DescrMap.find t !Print.named in
Print.register_global (cu, name, lsubst) nt;
with Not_found -> ()
end;
let key = (t, subst) in
if not (MemoSubst.mem subst_cache key) then
MemoSubst.add subst_cache key nt) !todo;
MemoSubst.add subst_cache (t,subst) res; res
let full t l =
if no_var t then t else
descr (app_subst (decompose t) (of_list l))
app_subst t (of_list l)
let single t s = full t [s]
......@@ -2922,13 +2956,13 @@ struct
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.fresh v)) vars in
descr (app_subst (decompose t) subst)
app_subst t subst
let kind delta k t =
if no_var t then t else
let vars = Var.Set.diff (all_vars t) delta in
let subst = Map.init (fun v -> var (Var.set_kind k v)) vars in
descr (app_subst (decompose t) subst)
app_subst t subst
let solve_rectype t alpha =
let x = make () in
......@@ -2967,7 +3001,7 @@ struct
else if is_pos then empty else any
) vars
in
descr (app_subst (decompose t) subst)
app_subst t subst
end
......
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