Commit 3f7498a2 authored by Kim Nguyễn's avatar Kim Nguyễn
Browse files

Remove some unneeded lookups to speed up tallying.

parent 89159c52
......@@ -267,9 +267,18 @@ end
(** Generation of constraint [norm(t,M)] function of the paper.
*)
module GlobalMemo = Hashtbl.Make (Custom.Pair (Types) (Var.Set))
module GlobalMemo = Hashtbl.Make (Var.Set)
module LocalMemo = Hashtbl.Make (Types)
(* The global cache is indexed by a set of monomorphic variables.
The only situation where it is re-used is when the same type with the
exact same variables (internally, not variables with the same name) is
used several times.
This situation often occurs in practice when applying the same polymorphic
function in the body of another one (e.g. List.map f aplied to several times
to lists with similar types).
*)
let global_memo = GlobalMemo.create 17
let cons_to_type (type atom) (module K : Kind with type Dnf.atom = atom)
......@@ -322,55 +331,52 @@ let fold_union acc delta mem to_type norm_atom dnf =
(** norm function that generates constraints. *)
let rec norm delta mem t =
try GlobalMemo.find global_memo (t, delta)
with Not_found -> (
try
let finished, cst = LocalMemo.find mem t in
if finished then cst else ConstrSet.sat
with Not_found ->
if is_empty t then ConstrSet.sat
else
let vars = Subst.vars t in
if Var.Set.subset vars delta then ConstrSet.unsat
else if Subst.is_var t then
let v, p = Subst.extract t in
if Var.Set.mem delta v then ConstrSet.unsat
else ConstrSet.single_var v (if p then (empty, empty) else (any, any))
else begin
LocalMemo.add mem t (false, ConstrSet.sat);
let res =
Iter.fold
(fun acc pack t ->
if ConstrSet.is_unsat acc then acc
else
match pack with
| Iter.Int m | Char m | Atom m | Abstract m ->
let module K = (val m) in
let to_type at = K.(mk (Dnf.mono at)) in
let dnf = K.(Dnf.get_partial (get_vars t)) in
fold_union acc delta mem to_type (norm_basic to_type) dnf
| Times m | Xml m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type norm_prod dnf
| Function m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type norm_arrow dnf
| Record m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type (norm_record to_type) dnf
| Absent -> acc)
ConstrSet.sat t
in
LocalMemo.replace mem t (true, res);
res
end)
try
let finished, cst = LocalMemo.find mem t in
if finished then cst else ConstrSet.sat
with Not_found ->
if is_empty t then ConstrSet.sat
else
let vars = Subst.vars t in
if Var.Set.subset vars delta then ConstrSet.unsat
else if Subst.is_var t then
let v, p = Subst.extract t in
if Var.Set.mem delta v then ConstrSet.unsat
else ConstrSet.single_var v (if p then (empty, empty) else (any, any))
else begin
LocalMemo.add mem t (false, ConstrSet.sat);
let res =
Iter.fold
(fun acc pack t ->
if ConstrSet.is_unsat acc then acc
else
match pack with
| Iter.Int m | Char m | Atom m | Abstract m ->
let module K = (val m) in
let to_type at = K.(mk (Dnf.mono at)) in
let dnf = K.(Dnf.get_partial (get_vars t)) in
fold_union acc delta mem to_type (norm_basic to_type) dnf
| Times m | Xml m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type norm_prod dnf
| Function m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type norm_arrow dnf
| Record m ->
let module K = (val m) in
let to_type = cons_to_type (module K) in
let dnf = K.(Dnf.get_full (get_vars t)) in
fold_union acc delta mem to_type (norm_record to_type) dnf
| Absent -> acc)
ConstrSet.sat t
in
LocalMemo.replace mem t (true, res);
res
end
and norm_prod delta mem (lpos, lneg) =
let rec neg_part t1 t2 = function
......@@ -441,10 +447,15 @@ and norm_record to_type delta mem line =
ConstrSet.sat (Record.get trec)
with Exit -> ConstrSet.unsat
let norm delta t =
try GlobalMemo.find global_memo (t, delta)
with Not_found ->
let get_local delta =
try GlobalMemo.find global_memo delta with
Not_found ->
let mem = LocalMemo.create 17 in
GlobalMemo.add global_memo delta mem;
mem
let norm delta t =
let mem = get_local delta in
norm delta mem t
(* Merging of constraints. *)
......@@ -570,7 +581,7 @@ exception FoundSquareSub of Types.t Var.Map.map list
exception UnsatConstr of string
let squaresubtype delta s t =
GlobalMemo.clear global_memo;
(*GlobalMemo.clear global_memo;*)
let ai = ref [||] in
let tallying i =
try
......@@ -605,7 +616,7 @@ let is_squaresubtype delta s t =
exception FoundApply of t * int * int * Types.t Var.Map.map list
let apply_raw delta s t =
GlobalMemo.clear global_memo;
(*GlobalMemo.clear global_memo;*)
let vgamma = Var.mk "Gamma" in
let gamma = var vgamma in
let cgamma = cons gamma in
......@@ -633,7 +644,7 @@ let apply_raw delta s t =
in
let rec loop i =
try
(* Format.eprintf "Starting expansion %i @\n@." i; *)
(* Format.eprintf "Starting expansion %i @\n@." i; *)
let ss, tt =
if i = 0 then (s, t)
else
......@@ -660,15 +671,12 @@ let apply_full delta s t =
let squareapply delta s t =
try
let s, _, _, res = apply_raw delta s t in
Some (s, res)
let s, _, _, res = apply_raw delta s t in
Some (s, res)
with UnsatConstr _ -> None
let apply_raw delta s t =
try
Some (apply_raw delta s t)
with UnsatConstr _ -> None
let apply_raw delta s t =
try Some (apply_raw delta s t) with UnsatConstr _ -> None
let tallying delta types =
try tallying delta types with Step1Fail | Step2Fail -> []
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