Commit 872141c0 authored by Raphael Rieu-Helft's avatar Raphael Rieu-Helft
Browse files

Memoize results of get_decl

parent 6ef0273e
......@@ -150,10 +150,10 @@
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="8"/></proof>
</goal>
<goal name="VC sprod.2" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
</goal>
<goal name="VC sprod.3" expl="exceptional postcondition" proved="true">
<proof prover="0" timelimit="5" memlimit="2000"><result status="valid" time="0.00" steps="4"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......@@ -1131,7 +1131,7 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.10" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.11" expl="precondition" proved="true">
......@@ -1141,24 +1141,24 @@
<proof prover="2"><result status="valid" time="0.06"/></proof>
</goal>
<goal name="VC linear_decision.13" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="21"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="21"/></proof>
<proof prover="2"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC linear_decision.14" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="39"/></proof>
</goal>
<goal name="VC linear_decision.15" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.16" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.17" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.18" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.19" expl="assertion" proved="true">
......@@ -1180,10 +1180,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC linear_decision.25" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="49"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
</goal>
<goal name="VC linear_decision.26" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="31"/></proof>
</goal>
<goal name="VC linear_decision.27" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -1195,10 +1195,10 @@
<proof prover="0"><result status="valid" time="0.02" steps="26"/></proof>
</goal>
<goal name="VC linear_decision.30" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="49"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="49"/></proof>
</goal>
<goal name="VC linear_decision.31" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="31"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="31"/></proof>
</goal>
<goal name="VC linear_decision.32" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
......@@ -1232,34 +1232,34 @@
<proof prover="0"><result status="valid" time="0.02" steps="44"/></proof>
</goal>
<goal name="VC linear_decision.42" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
</goal>
<goal name="VC linear_decision.43" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC linear_decision.44" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.45" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC linear_decision.46" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.47" expl="variant decrease" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="23"/></proof>
<proof prover="0"><result status="valid" time="0.01" steps="23"/></proof>
</goal>
<goal name="VC linear_decision.48" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="42"/></proof>
</goal>
<goal name="VC linear_decision.49" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="28"/></proof>
<proof prover="0"><result status="valid" time="0.03" steps="28"/></proof>
</goal>
<goal name="VC linear_decision.50" expl="precondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="25"/></proof>
</goal>
<goal name="VC linear_decision.51" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.52" expl="exceptional postcondition" proved="true">
......@@ -1305,17 +1305,17 @@
<proof prover="0"><result status="valid" time="0.02" steps="35"/></proof>
</goal>
<goal name="VC linear_decision.66" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.67" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.00"/></proof>
</goal>
<goal name="VC linear_decision.68" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.00"/></proof>
<proof prover="0"><result status="valid" time="0.02" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.69" expl="exceptional postcondition" proved="true">
<proof prover="0"><result status="valid" time="0.01" steps="5"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.70" expl="precondition" proved="true">
......@@ -1359,16 +1359,16 @@
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.82" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC linear_decision.83" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.84" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.01"/></proof>
<proof prover="2"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC linear_decision.85" expl="exceptional postcondition" proved="true">
<proof prover="2"><result status="valid" time="0.02"/></proof>
<proof prover="2"><result status="valid" time="0.01"/></proof>
</goal>
</transf>
</goal>
......
......@@ -197,13 +197,13 @@
<proof prover="2" timelimit="5" memlimit="2000"><result status="valid" time="1.02" steps="137"/></proof>
</goal>
<goal name="VC toom22_mul.40" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC toom22_mul.41" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC toom22_mul.42" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.43" expl="precondition" proved="true">
<proof prover="1"><result status="valid" time="0.58"/></proof>
......@@ -262,13 +262,13 @@
<proof prover="3"><result status="timeout" time="1.00"/></proof>
</goal>
<goal name="VC toom22_mul.51" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.03"/></proof>
</goal>
<goal name="VC toom22_mul.52" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.53" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.03"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC toom22_mul.54" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.60" steps="151"/></proof>
......@@ -436,7 +436,7 @@
<proof prover="1"><result status="valid" time="0.08"/></proof>
</goal>
<goal name="VC toom22_mul.101" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.04"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.102" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
......@@ -445,7 +445,7 @@
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.104" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.04"/></proof>
</goal>
<goal name="VC toom22_mul.105" expl="precondition" proved="true">
<proof prover="2"><result status="valid" time="0.80" steps="176"/></proof>
......@@ -499,16 +499,16 @@
<proof prover="2"><result status="valid" time="1.13" steps="141"/></proof>
</goal>
<goal name="VC toom22_mul.113" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC toom22_mul.114" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.115" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.01"/></proof>
<proof prover="3"><result status="valid" time="0.02"/></proof>
</goal>
<goal name="VC toom22_mul.116" expl="postcondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
<proof prover="3"><result status="valid" time="0.01"/></proof>
</goal>
<goal name="VC toom22_mul.117" expl="precondition" proved="true">
<proof prover="3"><result status="valid" time="0.02"/></proof>
......
......@@ -698,6 +698,8 @@ let get_decl env mm rs =
aux l
| _ -> Mid.find id tm.mod_known
let get_decl env mm = Wrs.memoize 17 (fun rs -> get_decl env mm rs)
let builtin_progs = Hrs.create 17
let eval_true _ _ = Vbool true
......@@ -932,6 +934,7 @@ type info = {
vars: value Mid.t;
recs: rsymbol Mrs.t;
funs: decl Mrs.t;
get_decl: rsymbol -> Mltree.decl;
cs: string list; (* callstack for debugging *)
}
......@@ -1004,7 +1007,7 @@ let rec interp_expr info (e:Mltree.expr) : value =
f rs (List.map (interp_expr info) le))
else begin
let decl = try Mrs.find rs info.funs
with Not_found -> get_decl info.env info.mm rs in
with Not_found -> info.get_decl rs in
Debug.dprintf debug_interp "decl found@.";
match decl with
| Dlet (Lsym (rs, _ty, vl, e)) ->
......@@ -1256,7 +1259,8 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
(*let mm = Mstr.singleton ms pmod in*)
Debug.dprintf debug_refl "module map built@.";
get_builtin_progs env;
let decl = get_decl env mm rs in
let get_decl = get_decl env mm in
let decl = get_decl rs in
Debug.dprintf debug_refl "initial decl found@.";
let args = List.map (fun pv -> pv.pv_vs) rs.rs_cty.cty_args in
let rec reify_post = function
......@@ -1294,6 +1298,7 @@ let reflection_by_function do_trans s env = Trans.store (fun task ->
funs = Mrs.empty;
recs = Mrs.empty;
vars = vars;
get_decl = get_decl;
cs = [];
} in
Debug.dprintf debug_refl "eval_fun@.";
......
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