Commit 9bbd6b47 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

continued to prepare the way for functional environments

parent ab05ae6d
Pipeline #1643 passed with stage
in 1 minute and 48 seconds
......@@ -79,10 +79,10 @@ let new_formula ?env:(env=init_env ()) l l' =
unitary_result = Unset })
l') in
type_check_formula_element_list env form;
let env' = type_check_formula_element_list env form in
{ formula_element_list = form;
env = env}
env = env' }
(* Cut list l in l1,x,l2 such that |l1| = i - 1 and l = l1 @ [x] @ l2 *)
let cut l i =
......@@ -109,10 +109,10 @@ let bind formula my_fun =
let f' = my_fun formula.formula_element_list in
type_check_formula_element_list env' f';
let env'' = type_check_formula_element_list env' f' in
{ formula_element_list = f';
env = env' }
env = env'' }
(* c_bind formula new_f: Return a new formula where the formula elements
have been replaced by new_f. *)
......
......@@ -1162,7 +1162,10 @@ add_new_action
match parse_b_terms state b_string, string_to_side side_string with
| [b], Some side ->
let rule = Cond_fresh (side,b) in
let (l_prem, r_prem) = cond_fresh_apply rule state.c_proof.goal in
let (l_prem, r_prem, env') =
cond_fresh_apply rule state.c_proof.goal in
state.c_proof.goal <- { state.c_proof.goal with env = env' };
binary_aux state rule l_prem r_prem;
......@@ -1281,11 +1284,15 @@ add_new_action
| Scanf.Scan_failure _ ->
sscanf y "bind %s@!" (fun z ->
if z = "*" then
hide_all_bindings state.c_proof.goal.env
let env' = hide_all_bindings state.c_proof.goal.env in
state.c_proof.goal <- { state.c_proof.goal with env = env' };
else
let l_s = parse_string_list z in
List.iter (hide_binding state.c_proof.goal.env) l_s
let env' = List.fold_left
hide_binding state.c_proof.goal.env l_s in
state.c_proof.goal <- { state.c_proof.goal with env = env' };
));;
add_new_action
......@@ -1316,11 +1323,15 @@ add_new_action
| Scanf.Scan_failure _ ->
sscanf y "bind %s@!" (fun z ->
if z = "*" then
reveal_all_bindings state.c_proof.goal.env
let env' = reveal_all_bindings state.c_proof.goal.env in
state.c_proof.goal <- { state.c_proof.goal with env = env' };
else
let l_string = parse_string_list z in
List.iter (reveal_binding state.c_proof.goal.env) l_string
let l_s = parse_string_list z in
let env' = List.fold_left
reveal_binding state.c_proof.goal.env l_s in
state.c_proof.goal <- { state.c_proof.goal with env = env' };
));;
......@@ -1908,8 +1919,6 @@ let create_guard_data_side goal encs t =
| _ ->
let new_c_goal = add_binding c_goal var_fresh g_u in
hide_binding new_c_goal.env var_fresh;
new_c_goal in
(* For every current binding, we add (if necessary) new bindings *)
......
......@@ -426,8 +426,6 @@ let ireduce conf side =
let env' = env_add_binding env var t in
(* hide_binding env var in *)
(Var (var,Msg)) :: acc_args, env', map_fresh')
([],env,map_fresh) l l_arg_names in
......@@ -444,8 +442,7 @@ let ireduce conf side =
| g, New (s, p') ->
let (name, map_fresh') = fresh_name env map_fresh side s in
let env' = copy_env env in
bind_new_type env' name TName;
let env' = bind_new_type env name TName in
aux_ireduce
reduced_gp_list
......@@ -487,8 +484,6 @@ let ireduce conf side =
let env' = env_add_binding env var t in
(* hide_binding env var in *)
aux_ireduce
reduced_gp_list
env'
......@@ -877,17 +872,16 @@ let get_adv_term conf frame phi side s =
let adv_term = Fun (adv_term_fun_name, [phi]) in
(* Declare function type (it may be already declared) *)
bind_type env adv_term_fun_name (TFun 1);
let env' = bind_type env adv_term_fun_name (TFun 1) in
(* We bind Var s to the message computed by the attacker. *)
let (var,map_fresh') = fresh_name env map_fresh side s in
let (var,map_fresh') = fresh_name env' map_fresh side s in
let env' = env_add_binding env var adv_term in
(* hide_binding env var in *)
let env'' = env_add_binding env' var adv_term in
let adv_term_var = Var (var,Msg) in
let new_conf = { conf with env = env';
let new_conf = { conf with env = env'';
map_fresh = map_fresh' } in
(adv_term_var, new_conf)
......@@ -1003,8 +997,6 @@ let apply_action action side f_conf =
let env' = env_add_binding env var_phi' term_phi' in
(* hide_binding env var_phi' in *)
let phi' = Var (var_phi',Msg) in
let f_conf_side' = { f_procs = red_new_conf.procs;
......
......@@ -564,22 +564,6 @@ let rec rewrite_cond_false
exception Bad_cond_fresh
(* Used to generate fresh name for the cond_fresh rule. *)
let rec fresh_name env s i =
let fresh_s =
s ^ "_fresh" ^ (if i = 0 then "" else string_of_int i) in
(* If fresh_s was already used then reiterate the process. *)
if Hashtbl.mem env.string_types fresh_s then
fresh_name env s (i+1)
else
begin
bind_new_type env fresh_s TName;
fresh_s
end
let cond_fresh_apply r formula = match r with
| Cond_fresh (side,b) ->
......@@ -631,20 +615,24 @@ let cond_fresh_apply r formula = match r with
cond_fresh_term formula_element u1 u2)
formula.formula_element_list in
let second_premise = match eiv_i formula.env b 2 with
let (second_premise, env') = match eiv_i formula.env b 2 with
| EQ (Name (n, Msg), u) | EQ (u, Name (n, Msg)) ->
let n_fresh = fresh_name formula.env n 0 in
{ term_pair = T (Name (n, Msg), Name (n_fresh, Msg));
hidden_status = false;
unitary_result = Unset }
let n_fresh = fresh_name formula.env (n ^ "_fresh") in
let env' = bind_new_type formula.env n_fresh TName in
( { term_pair = T (Name (n, Msg), Name (n_fresh, Msg));
hidden_status = false;
unitary_result = Unset }
:: [ { term_pair = T (u, u);
hidden_status = false;
unitary_result = Unset } ]
:: [ { term_pair = T (u, u);
hidden_status = false;
unitary_result = Unset } ],
env' )
| _ -> raise Bad_cond_fresh in
(first_premise, second_premise)
(first_premise, second_premise, env')
| _ -> failwith "cs_deep_apply bad rule argument"
......@@ -54,4 +54,4 @@ val cs_deep_apply :
exception Bad_cond_fresh
val cond_fresh_apply :
rule -> formula -> formula_element list * formula_element list
rule -> formula -> formula_element list * formula_element list * environment
......@@ -310,18 +310,22 @@ exception No_such_binding of variable_string
(* hide_binding env s: Hide the binding associated with s in env. *)
let hide_binding env s =
if Hashtbl.mem env.t_bindings s then
let new_env = copy_env env in
if Hashtbl.mem new_env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = TVar);
Hashtbl.replace env.hide_bindings s true
assert (Hashtbl.find new_env.string_types s = TVar);
Hashtbl.replace new_env.hide_bindings s true;
new_env
end
else if Hashtbl.mem env.bt_bindings s then
else if Hashtbl.mem new_env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = BTVar);
Hashtbl.replace env.hide_bindings s true
assert (Hashtbl.find new_env.string_types s = BTVar);
Hashtbl.replace new_env.hide_bindings s true;
new_env
end
else
......@@ -329,33 +333,42 @@ let hide_binding env s =
let hide_all_bindings env =
let new_env = copy_env env in
Hashtbl.filter_map_inplace
(fun s _ -> Some true)
env.hide_bindings;;
new_env.hide_bindings;
new_env;;
(* reveal_binding env s: Reveal the binding associated with s in env. *)
let reveal_binding env s =
if Hashtbl.mem env.t_bindings s then
let new_env = copy_env env in
if Hashtbl.mem new_env.t_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = TVar);
Hashtbl.replace env.hide_bindings s false
assert (Hashtbl.find new_env.string_types s = TVar);
Hashtbl.replace new_env.hide_bindings s false;
new_env
end
else if Hashtbl.mem env.bt_bindings s then
else if Hashtbl.mem new_env.bt_bindings s then
begin
(* Sanity Check *)
assert (Hashtbl.find env.string_types s = BTVar);
Hashtbl.replace env.hide_bindings s false
assert (Hashtbl.find new_env.string_types s = BTVar);
Hashtbl.replace new_env.hide_bindings s false;
new_env
end
else
raise (No_such_binding s)
let reveal_all_bindings env =
let new_env = copy_env env in
Hashtbl.filter_map_inplace
(fun s _ -> Some false)
env.hide_bindings;;
env.hide_bindings;
new_env;;
(*******************)
(* Variable typing *)
......@@ -417,25 +430,29 @@ let bind_type_aux (ht,ht') s mtype =
else
Hashtbl.add ht' s mtype
(* bind_type env s mtype: Add a new binding between s and mtype if it
does not already exists. *)
(* bind_type env s mtype: Add a new binding between s and mtype if it does
not already exists. *)
let bind_type env s mtype =
if Hashtbl.mem env.string_types s then
begin
if not (Hashtbl.find env.string_types s = mtype) then
let error_message = Printf.sprintf
if not (Hashtbl.find env.string_types s = mtype) then
let error_message = Printf.sprintf
"3. Wanted to bind %s to type %s, but it was already bound to %s\n\
Dumping the type table.\n"
s
(string_type_to_string mtype)
(string_type_to_string (Hashtbl.find env.string_types s)) in
debug_print_string_types env.string_types;
raise (Not_type_checking error_message);
end
let _ = debug_print_string_types env.string_types in
raise (Not_type_checking error_message);
else
env
else
Hashtbl.add env.string_types s mtype
let new_env = copy_env env in
let _ = Hashtbl.add new_env.string_types s mtype in
new_env
(* bind_new_type env s mtype: Add a new binding between s and mtype. If s is
already binded in env, raise a Not_type_checking exception. *)
......@@ -449,11 +466,16 @@ let bind_new_type env s mtype =
(string_type_to_string mtype)
(string_type_to_string (Hashtbl.find env.string_types s)) in
debug_print_string_types env.string_types;
let _ = debug_print_string_types env.string_types in
raise (Not_type_checking error_message)
else
Hashtbl.add env.string_types s mtype
let new_env = copy_env env in
let _ = Hashtbl.add new_env.string_types s mtype in
new_env
type ht_pair =
......@@ -484,26 +506,32 @@ let rec type_check_aux : type a. ht_pair -> a term -> unit = fun ht_pair t ->
type_check_aux ht_pair u;
type_check_aux ht_pair v;;
(* type_check env t: Type-checks the term t in env. Update the environment env
if the type checking is successful. *)
(* type_check env t: Type-checks the term t in env. *)
let type_check env t =
let ht' = Hashtbl.create ~random:false 10 in
type_check_aux (env.string_types,ht') t;
Hashtbl.iter (Hashtbl.add env.string_types) ht';;
let new_env = copy_env env in
let _ = Hashtbl.iter (Hashtbl.add new_env.string_types) ht' in
new_env
(* type_check_all env l_term b_term: Type-checks all elements in l_term and
b_term in the environment env. *)
let type_check_all : environment -> msg term list -> boole term list -> unit =
fun env l_term l_bterm ->
let type_check_all : environment -> msg term list -> boole term list
-> environment = fun env l_term l_bterm ->
let ht' = Hashtbl.create ~random:false 10 in
List.iter (type_check_aux (env.string_types,ht')) l_term;
List.iter (type_check_aux (env.string_types,ht')) l_bterm;
Hashtbl.iter (Hashtbl.add env.string_types) ht';;
let new_env = copy_env env in
let _ = Hashtbl.iter (Hashtbl.add new_env.string_types) ht' in
new_env
(**********************)
......@@ -944,40 +972,38 @@ exception Bad_binding of string_type * string_type
let env_add_binding : type a. environment -> variable_string -> a term
-> environment =
fun env s t ->
type_check env t;
let env' = type_check env t in
let collected_t = collect_all env t in
let collected_t = collect_all env' t in
if Hashtbl.mem env.string_types s then
raise (Bad_binding (TVar,(Hashtbl.find env.string_types s)))
if Hashtbl.mem env'.string_types s then
raise (Bad_binding (TVar,(Hashtbl.find env'.string_types s)))
else
begin
let env' = copy_env env in
let env'' = copy_env env' in
let _ = match get_sort collected_t with
| Msg -> Hashtbl.add env'.string_types s TVar
| Bool -> Hashtbl.add env'.string_types s BTVar in
| Msg -> Hashtbl.add env''.string_types s TVar
| Bool -> Hashtbl.add env''.string_types s BTVar in
Hashtbl.filter_map_inplace
(fun _ u -> Some (collect_var u s collected_t))
env'.t_bindings;
env''.t_bindings;
Hashtbl.filter_map_inplace
(fun _ bu -> Some (collect_var bu s collected_t))
env'.bt_bindings;
env''.bt_bindings;
let _ = match get_sort collected_t with
| Msg -> Hashtbl.add env'.t_bindings s collected_t
| Bool -> Hashtbl.add env'.bt_bindings s collected_t in
Hashtbl.add env'.hide_bindings s true;
| Msg -> Hashtbl.add env''.t_bindings s collected_t
| Bool -> Hashtbl.add env''.bt_bindings s collected_t in
Hashtbl.add env''.hide_bindings s true;
env'
env''
end
(*********************)
(* Term Substitution *)
(*********************)
......
......@@ -2,7 +2,9 @@ type msg
type boole
type name_string = string
type function_symbol_string = string
type variable_string = string
type _ sort = | Msg : msg sort
......@@ -79,14 +81,14 @@ val init_env : unit -> environment
exception No_such_binding of variable_string
(* hide_binding formula s: Hide the binding associated with s in formula. *)
val hide_binding : environment -> variable_string -> unit
val hide_binding : environment -> variable_string -> environment
val hide_all_bindings : environment -> unit
val hide_all_bindings : environment -> environment
(* reveal_binding formula s: Reveal the binding associated with s in formula. *)
val reveal_binding : environment -> variable_string -> unit
val reveal_binding : environment -> variable_string -> environment
val reveal_all_bindings : environment -> unit
val reveal_all_bindings : environment -> environment
val copy_env : environment -> environment
......@@ -109,19 +111,20 @@ val fresh_name : environment -> string -> string
(* bind_type env s mtype: Add a new binding between s and mtype if it
does not already exists. *)
val bind_type : environment -> string -> string_type -> unit
val bind_type : environment -> string -> string_type -> environment
(* bind_new_type env s mtype: Add a new binding between s and mtype. If s is
already binded in env, raise a Not_type_checking exception. *)
val bind_new_type : environment -> string -> string_type -> unit
val bind_new_type : environment -> string -> string_type -> environment
(* type_check env t: Type-checks the term t in env. Update the environment env
if the type checking is successful. *)
val type_check : environment -> 'a term -> unit
val type_check : environment -> 'a term -> environment
(* type_check_all env l_term b_term: Type-checks all elements in l_term and
b_term in the environment env. *)
val type_check_all : environment -> msg term list -> boole term list -> unit
val type_check_all : environment -> msg term list -> boole term list
-> environment
(**********************)
......
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