diff --git a/types/types.ml b/types/types.ml index 13cef839135fc995b4a8434e3efefc9109eea1c9..16c5c39394bb04cf027a3942eff1eb7630705338 100644 --- a/types/types.ml +++ b/types/types.ml @@ -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 = - Positive.solve_gen ~stop_descr:(fun v -> - match v.Positive.def with - `Variable d -> (try Some (Map.assoc d subst) with Not_found -> None) - | _ -> None) v + 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) + 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