Commit 1f5ed38f authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

memoisation for term normalization:

nsl example is done in 12s instead of 18 for me
parent 5cfe894b
......@@ -463,7 +463,6 @@ let auto_ift state =
binding tables. *)
let weakly_normalize_proof ?collect:(c=false) state =
let goal = state.c_proof.goal in
let env = goal.env in
let (_, rewrite_simplification_rule_list) =
List.fold_left (fun (i,rule_list) formula_element ->
......@@ -471,8 +470,8 @@ let weakly_normalize_proof ?collect:(c=false) state =
| B _ -> (i+1,rule_list)
| T (left_term,right_term) ->
let w_l_t = weak_normalize env left_term
and w_r_t = weak_normalize env right_term in
let w_l_t = weak_normalize left_term
and w_r_t = weak_normalize right_term in
let new_rule_list =
(R (Left,left_term, w_l_t, []),i)
......@@ -756,7 +755,7 @@ let create_guard_data_side goal encs t =
let var_fresh = fresh_name c_goal.env var in
let g_u = rewrite c_goal.env t x u []
|> weak_normalize c_goal.env in
|> weak_normalize in
match g_u.content with
(* | Var _ -> c_goal *)
......
......@@ -1012,7 +1012,7 @@ let apply_action action side f_conf =
(* We weakly normalize the outputed term. *)
let norm_outputed_term =
weak_normalize red_new_conf.env outputed_term in
weak_normalize outputed_term in
(* We define the new frame variable phi', and bind it in the environment. *)
let i = List.length frame
......
This diff is collapsed.
......@@ -221,14 +221,14 @@ val const_subterm : env -> msg term -> msg term -> msg term list
(**********************)
(* Eliminate all syntactic duplicate on the same branches. *)
val duplicate_cond_elim : env -> 'a term -> 'a term
val duplicate_cond_elim : 'a term -> 'a term
(* Reduce all redexes of the form If(b, v, v). Variables are not expanded. *)
val same_elim : env -> 'a term -> 'a term
val same_elim : 'a term -> 'a term
(* Remove proj/pair and dec/enc redexes, multiple occurrences of the same
conditional on a branch, and simplify if-same redexes. *)
val weak_normalize : env -> 'a term -> 'a term
val weak_normalize : 'a term -> 'a term
(* pseudo_normalize env t : Return a pseudo-normalisation of t (i.e. a R-normal
for a arbitrary total ordering on R-normal if-free conditionals.). *)
......
......@@ -98,7 +98,6 @@ cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
(* Third trace *)
cca2 guard;
......@@ -121,7 +120,7 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__2_0,nB_r);
cond_fresh Left EQ(dec_g5_0,nB_l);
cond_fresh Right EQ(dec_g5_2_0,nB_r);
cca2 guard;
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