Commit 5aad657b authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

cont. funct. env.

parent 9bbd6b47
Pipeline #1644 passed with stage
in 2 minutes and 6 seconds
......@@ -1921,22 +1921,26 @@ let create_guard_data_side goal encs t =
new_c_goal in
let f_fold c_goal (var,u) =
if subterm c_goal.env t u then
let subst_list =
g_data_side.guarded_dec
:: (List.map (get_enc_content c_goal.env) encs) in
List.fold_left (add_binding_aux var u) c_goal subst_list
else
c_goal in
(* For every current binding, we add (if necessary) new bindings *)
let new_goal' =
Hashtbl.fold (fun var u c_goal ->
if subterm c_goal.env t u then
let subst_list =
g_data_side.guarded_dec
:: (List.map (get_enc_content c_goal.env) encs) in
List.fold_left (add_binding_aux var u) c_goal subst_list
List.fold_left f_fold new_goal (get_bindings new_goal.env Msg) in
else
c_goal)
goal.env.t_bindings new_goal in
let new_goal'' =
List.fold_left f_fold new_goal' (get_bindings new_goal'.env Bool) in
( g_data_side, new_goal' )
( g_data_side, new_goal'' )
let create_guard_data goal enc_pairs t t' =
......
......@@ -112,18 +112,21 @@ let main_interactive () =
(* Create and set-up a dummy state and environment for testing. *)
let test_state = dummy_interactive_state ();;
let env = test_state.c_proof.goal.env;;
Hashtbl.add env.string_types "kA" TName;
Hashtbl.add env.string_types "kA_0" TName;
Hashtbl.add env.string_types "kB" TName;
Hashtbl.add env.string_types "kB_0" TName;
Hashtbl.add env.string_types "r0" TName;
Hashtbl.add env.string_types "r0_0" TName;
Hashtbl.add env.string_types "nA" TName;
Hashtbl.add env.string_types "nA_0" TName;;
Hashtbl.add env.string_types "nB" TName;
Hashtbl.add env.string_types "nB_0" TName;;
let env =
let env = test_state.c_proof.goal.env in
List.fold_left (fun env (s,tt) -> bind_type env s tt)
env
( ("kA", TName)
:: ("kA_0", TName)
:: ("kB", TName)
:: ("kB_0", TName)
:: ("r0", TName)
:: ("r0_0", TName)
:: ("nA", TName)
:: ("nA_0", TName)
:: ("nB", TName)
:: [("nB_0", TName)] )
let init_cca_constraints key_pairs =
{ alpha = { msg_constraints = key_pairs;
......
......@@ -297,6 +297,12 @@ let copy_env env =
hide_bindings = Hashtbl.copy env.hide_bindings;
string_types = Hashtbl.copy env.string_types }
let get_bindings : type a. environment -> a sort
-> (variable_string * a term) list =
fun env sort -> match sort with
| Msg -> Hashtbl.fold (fun var u acc -> (var,u) :: acc) env.t_bindings []
| Bool -> Hashtbl.fold (fun var u acc -> (var,u) :: acc) env.bt_bindings []
let debug_print_string_types ht =
debug (fun () ->
Printf.eprintf "Type-checking error, outputting the current type table:\n";
......
......@@ -78,6 +78,9 @@ val string_type_to_string : string_type -> string
defined. *)
val init_env : unit -> environment
val get_bindings : environment -> 'a sort -> (variable_string * 'a term) list
exception No_such_binding of variable_string
(* hide_binding formula s: Hide the binding associated with s in formula. *)
......
......@@ -12,7 +12,7 @@ cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
cca2 guard;
......@@ -26,7 +26,7 @@ cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
cca2 guard;
......@@ -40,7 +40,7 @@ cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
(* Second trace *)
......@@ -55,7 +55,7 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
cca2 guard;
......@@ -69,7 +69,7 @@ cond_fresh Right EQ(pi1(pi2(dec_mb_r_1)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
cca2 guard;
......@@ -81,7 +81,7 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
cca2 guard;
......@@ -95,7 +95,7 @@ cond_fresh Right EQ(pi1(pi2(dec_mb_r_0)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__3_0,nB_r);
cca2;
......@@ -110,7 +110,7 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__2_0,nB_r);
cca2 guard;
......@@ -122,6 +122,6 @@ cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2 guard;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__0,nB_r);
cond_fresh Right EQ(dec__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