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

corrected a bug in var_subst

parent 01674849
Pipeline #1659 failed with stage
in 2 minutes and 14 seconds
......@@ -897,8 +897,7 @@ let guard_decryption state cca_constraints g_data sk fk =
let (l_prem, r_prem) = cs_apply rule state.c_proof.goal in
binary_aux state rule l_prem r_prem sk
(fun state' fk' -> Printf.eprintf "\nleft branch done\n%!";
cs_split state' tail fk') fk in
(fun state' fk' -> cs_split state' tail fk') fk in
cs_split new_state guard_pairs fk
......
......@@ -255,10 +255,11 @@ let rec print_process_decl ppf decl =
(* var_subst s t u : Substitute s by t in u. *)
let rec var_subst : type a. name_string -> msg term -> a term -> a term =
fun s t u -> match u.content with
fun s t u ->
match u.content with
| Name (s',Msg) -> if s = s' then t else u
| Name (s',Bool) -> u
| Fun (s,l) -> t_fun s (List.map (var_subst s t) l)
| Name (s',Bool) -> assert false;
| Fun (sfun,l) -> t_fun sfun (List.map (var_subst s t) l)
| EQ (v,w) -> t_eq (var_subst s t v) (var_subst s t w)
| If (b,v,w) -> t_ite (var_subst s t b)
(var_subst s t v)
......@@ -267,7 +268,8 @@ let rec var_subst : type a. name_string -> msg term -> a term -> a term =
| False -> u
(* process_subst s t p : Substitute Var s by t in the process p. *)
let rec process_subst s t p = match p with
let rec process_subst s t p =
match p with
| Nil -> p
| Apply (s',l) ->
......@@ -283,13 +285,13 @@ let rec process_subst s t p = match p with
Out (c, var_subst s t t', process_subst s t p')
| Parallel (p', p'') ->
Parallel (process_subst s t p',
process_subst s t p'')
Parallel ( process_subst s t p',
process_subst s t p'' )
| IfThenElse (b, p', p'') ->
IfThenElse (var_subst s t b,
process_subst s t p',
process_subst s t p'')
IfThenElse ( var_subst s t b,
process_subst s t p',
process_subst s t p'' )
| Let (s', t', p') ->
if s = s' then p else Let (s', var_subst s t t', process_subst s t p')
......@@ -506,7 +508,6 @@ let ireduce conf side =
let (var, map_fresh') = fresh_name env map_fresh side s in
let env' = env_add_binding env var t in
aux_ireduce
reduced_gp_list
env'
......
......@@ -67,8 +67,7 @@ let make : type a. a term_cnt -> a term = fun c ->
| Not_found ->
incr hcons_cpt ;
HB.add hb c' ;
c'
end
c' end
let t_hash : type a. a term -> int = fun t -> t.hash
......@@ -79,7 +78,18 @@ let t_equal : type a b. a term -> b term -> bool = fun t t' ->
| _ -> false
let t_compare : type a b. a term -> b term -> int = fun t t' ->
Pervasives.compare t.hash t'.hash
match get_sort t,get_sort t' with
| Msg, Msg ->
if t == t' then
0
else
Pervasives.compare t.hash t'.hash
| Bool, Bool ->
if t == t' then
0
else
Pervasives.compare t.hash t'.hash
| _ -> Pervasives.compare t.hash t'.hash
(*********************)
......@@ -113,7 +123,6 @@ let t_true () = make True
let t_false () = make False
(****************)
(* Environement *)
(****************)
......@@ -303,7 +312,6 @@ let rec print_term : type a. env -> Format.formatter -> a term -> unit =
fun env ppf t ->
let open Fmt in
let ident ppf s = pf ppf "%s" s in
let kw style = (styled style ident) in
if term_is_binded env t then
let s = match get_sort t with
......@@ -312,72 +320,80 @@ let rec print_term : type a. env -> Format.formatter -> a term -> unit =
(styled `Bold (styled `Magenta ident)) ppf s
else
match t.content with
| Name (s,Bool) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = BTVar then
(styled `Bold (styled `Magenta ident)) ppf s
else begin
assert (s_type = BTName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
| Name (s,Msg) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = TVar then
(styled `Bold (styled `Magenta ident)) ppf s
else begin
assert (s_type = TName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
print_term_cnt env ppf t
| Fun ("pair",l) ->
begin match l with
| a :: [b] ->
pf ppf "@[<hov 1><%a,@,%a>@]"
(print_term_left_pair_elem env) a
(print_term env) b
and print_term_cnt : type a. env -> Format.formatter -> a term -> unit =
fun env ppf t ->
let open Fmt in
let ident ppf s = pf ppf "%s" s in
let kw style = (styled style ident) in
| _ -> failwith "term printing: pair: wrong number of elements"
end
match t.content with
| Name (s,Bool) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = BTVar then
(styled `Bold (styled `Magenta ident)) ppf s
else begin
assert (s_type = BTName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
| Fun (s,l) ->
pf ppf "@[%a(@[<hov>%a)@]@]"
(kw `Bold) s
(Fmt.list ~sep:(fun ppf () -> pf ppf ",@,") (print_term env)) l
| Name (s,Msg) ->
if is_binded env s then
let s_type = StringMap.find s env.string_types in
if s_type = TVar then
(styled `Bold (styled `Magenta ident)) ppf s
else begin
assert (s_type = TName);
(kw `Magenta) ppf s end
else
(kw `Magenta) ppf s
| True -> (kw `Green) ppf "true"
| Fun ("pair",l) ->
begin match l with
| a :: [b] ->
pf ppf "@[<hov 1><%a,@,%a>@]"
(print_term_left_pair_elem env) a
(print_term env) b
| False -> (kw `Green) ppf "false"
| _ -> failwith "term printing: pair: wrong number of elements"
end
| EQ (u,v) ->
pf ppf "@[<hv 3>%a%a,@,%a%a@]"
(kw `Bold) "EQ("
(print_term env) u
(print_term env) v
(kw `Bold) ")"
| Fun (s,l) ->
pf ppf "@[%a(@[<hov>%a)@]@]"
(kw `Bold) s
(Fmt.list ~sep:(fun ppf () -> pf ppf ",@,") (print_term env)) l
| If (b,u,v) ->
match v.content with
| Fun ("z0",[]) ->
pf ppf "@[<hv>%a %a %a@;<1 2>%a@]"
(kw `Red) "if"
(print_term env) b
(kw `Red) "then"
(print_term env) u
| True -> (kw `Green) ppf "true"
| _ ->
pf ppf "@[<hv>%a %a %a@;<1 2>%a@ %a%a@]"
(kw `Red) "if"
(print_term env) b
(kw `Red) "then"
(print_term env) u
(kw `Red) "else"
(print_term_else_branch env) v
| False -> (kw `Green) ppf "false"
| EQ (u,v) ->
pf ppf "@[<hv 3>%a%a,@,%a%a@]"
(kw `Bold) "EQ("
(print_term env) u
(print_term env) v
(kw `Bold) ")"
| If (b,u,v) ->
match v.content with
| Fun ("z0",[]) ->
pf ppf "@[<hv>%a %a %a@;<1 2>%a@]"
(kw `Red) "if"
(print_term env) b
(kw `Red) "then"
(print_term env) u
| _ ->
pf ppf "@[<hv>%a %a %a@;<1 2>%a@ %a%a@]"
(kw `Red) "if"
(print_term env) b
(kw `Red) "then"
(print_term env) u
(kw `Red) "else"
(print_term_else_branch env) v
and print_term_else_branch : type a. env -> Format.formatter -> a term -> unit =
fun env ppf t ->
......@@ -452,7 +468,7 @@ let print_t_bindings env shell_mode =
if not (StringMap.find s env.hide_bindings) then
pf ppf "%a@[%a@]@."
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
(print_term env) t)
(print_term_cnt env) t)
stdout
......@@ -471,7 +487,7 @@ let print_bt_bindings env shell_mode =
if not (StringMap.find s env.hide_bindings) then
pf ppf "%a@[%a@]"
(styled `Bold (styled `Magenta ident)) (Printf.sprintf "%s:" s)
(print_term env) b)
(print_term_cnt env) b)
stdout
......@@ -695,45 +711,41 @@ let rec term_size : type a. env -> a term -> int = fun env t ->
(* env_add_binding env s t: Add a new binding between the term variable s and
the term t in env. The term t must type-check. *)
let env_add_binding : type a. env -> variable_string -> a term
-> env = fun env s t ->
let env' = try type_check t env with
| e -> Fmt.pf Fmt.stderr "\n%a\n%!" (print_term env) t; raise e in
if StringMap.mem s env'.string_types then
raise (Bad_binding (TVar,(StringMap.find s env'.string_types)));
let env_add_binding : type a. env -> variable_string -> a term -> env =
fun env s t ->
let env' = type_check t env in
let type_map = match get_sort t with
| Msg -> StringMap.add s TVar env'.string_types
| Bool -> StringMap.add s BTVar env'.string_types in
if StringMap.mem s env'.string_types then
raise (Bad_binding (TVar,(StringMap.find s env'.string_types)));
let hide_map = StringMap.add s true env'.hide_bindings in
let type_map = match get_sort t with
| Msg -> StringMap.add s TVar env'.string_types
| Bool -> StringMap.add s BTVar env'.string_types in
let term_map = env'.t_bindings
and bterm_map = env'.bt_bindings in
let hide_map = StringMap.add s true env'.hide_bindings in
let term_map' : msg term StringMap.t = match get_sort t with
| Msg -> StringMap.add s t term_map
| _ -> term_map in
let term_map : msg term StringMap.t = match get_sort t with
| Msg -> StringMap.add s t env'.t_bindings
| _ -> env'.t_bindings in
let r_term_map' = match get_sort t with
| Msg -> TMap.add t s env'.r_t_bindings
| _ -> env'.r_t_bindings in
let r_term_map = match get_sort t with
| Msg -> TMap.add t s env'.r_t_bindings
| _ -> env'.r_t_bindings in
let bterm_map' : boole term StringMap.t = match get_sort t with
| Bool -> StringMap.add s t bterm_map
| _ -> bterm_map in
let bterm_map : boole term StringMap.t = match get_sort t with
| Bool -> StringMap.add s t env'.bt_bindings
| _ -> env'.bt_bindings in
let r_bterm_map' = match get_sort t with
| Bool -> BTMap.add t s env'.r_bt_bindings
| _ -> env'.r_bt_bindings in
let r_bterm_map = match get_sort t with
| Bool -> BTMap.add t s env'.r_bt_bindings
| _ -> env'.r_bt_bindings in
{ t_bindings = term_map';
r_t_bindings = r_term_map';
bt_bindings = bterm_map';
r_bt_bindings = r_bterm_map';
hide_bindings = hide_map;
string_types = type_map }
{ t_bindings = term_map;
r_t_bindings = r_term_map;
bt_bindings = bterm_map;
r_bt_bindings = r_bterm_map;
hide_bindings = hide_map;
string_types = type_map }
(* env_remove_binding env s: Remove the binding associated with s in env. *)
let env_remove_binding env s =
......
......@@ -12,12 +12,11 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
cca2 guard;
cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
......@@ -26,8 +25,8 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
cca2 guard;
......@@ -40,8 +39,8 @@ cond_fresh Left EQ(pi1(pi2(mb_l)),nB_l);
cond_fresh Right EQ(pi1(pi2(mb_r)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
(* Second trace *)
......@@ -55,8 +54,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
cca2 guard;
......@@ -65,12 +64,12 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi2(dec_mb_l_1)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_mb_r_1)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_g5_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_2_0)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
cca2 guard;
......@@ -81,8 +80,8 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
cca2 guard;
......@@ -91,12 +90,12 @@ cond_fresh Left EQ(<nA_l,A()>,nB_l);
cond_fresh Right EQ(<nA_r,A()>,nB_r);
cca2;
cond_fresh Left EQ(pi1(pi2(dec_mb_l_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_mb_r_0)),nB_r);
cond_fresh Left EQ(pi1(pi2(dec_g5_0)),nB_l);
cond_fresh Right EQ(pi1(pi2(dec_g5_2_0)),nB_r);
cca2;
cond_fresh Left EQ(dec_,nB_l);
cond_fresh Right EQ(dec__3_0,nB_r);
cond_fresh Left EQ(dec_g7_0,nB_l);
cond_fresh Right EQ(dec_g7_3_0,nB_r);
cca2;
......@@ -110,8 +109,8 @@ 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