Commit e5d0d7a2 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

using external constructors for terms

parent 58e124fc
Pipeline #1653 passed with stage
in 3 minutes and 10 seconds
......@@ -37,7 +37,7 @@ let extend_axiom : type a. formula -> a axiom_type ->
| Failure_hint _ ->
let dummy_bad_dec_hint =
Failure_hint (Bad_decryption (Name ("",Msg),Left)) in
Failure_hint (Bad_decryption (t_name "" Msg,Left)) in
if (hint_same_shape res_el dummy_bad_dec_hint)
&& (is_msg_term_pair el.term_pair) then
......
......@@ -58,8 +58,8 @@ let print_alpha_constraints ppf alpha =
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
print_term (Name (l,Msg))
print_term (Name (r,Msg))))
print_term (t_name l Msg)
print_term (t_name r Msg)))
alpha.msg_constraints
(styled `Bold ident) "Bool constraints : "
......@@ -68,8 +68,8 @@ let print_alpha_constraints ppf alpha =
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
print_term (Name (l,Msg))
print_term (Name (r,Msg))))
print_term (t_name l Msg)
print_term (t_name r Msg)))
alpha.bool_constraints;;
let print_cca_constraints_aux long ppf constraints =
......@@ -97,8 +97,8 @@ let print_cca_constraints_aux long ppf constraints =
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a)"
print_term (Name (l,Msg))
print_term (Name (r,Msg))))
print_term (t_name l Msg)
print_term (t_name r Msg)))
constraints.key_pairs
(styled `Bold ident) "Bool Encryption rands :"
......@@ -107,8 +107,8 @@ let print_cca_constraints_aux long ppf constraints =
~sep:(fun ppf () -> pf ppf "@ ")
(fun ppf (l,r) ->
pf ppf "(%a, %a) "
print_term (Name (l,Msg))
print_term (Name (r,Msg))))
print_term (t_name l Msg)
print_term (t_name r Msg)))
constraints.encryption_rands
print_alpha_constraints constraints.alpha
......@@ -280,7 +280,7 @@ let rec dec_pk_fresh :
raise (Case_fail (Bad_randomness (s,side)));
end
else
dec_pk_fresh env side cca_constraints (Fun ("sk",[Name(s,Msg)]));
dec_pk_fresh env side cca_constraints (t_fun "sk" [t_name s Msg]);
dec_pk_fresh env side cca_constraints u;
......@@ -302,10 +302,10 @@ let rec dec_pk_fresh :
side )));
end
else
dec_pk_fresh env side cca_constraints (Name (r,Msg));
dec_pk_fresh env side cca_constraints (t_name r Msg);
dec_pk_fresh env side cca_constraints m;
dec_pk_fresh env side cca_constraints (Fun ("pk",[Name (pk,Msg)]));
dec_pk_fresh env side cca_constraints (t_fun "pk" [t_name pk Msg]);
| Fun (s,l) -> List.iter (dec_pk_fresh env side cca_constraints) l
......@@ -626,7 +626,7 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
else
let (new_l,new_l') =
List.split (List.map2 build_ctxt l l') in
(Fun (s,new_l), Fun (s',new_l'))
(t_fun s new_l, t_fun s' new_l')
| _ -> assert false
......@@ -637,8 +637,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
| Fun ("enc",[x;r;m_pk]), Fun ("enc",[x';r';m_pk']) ->
(* We check whether this is already an encryption oracle calls. *)
if is_an_enc_call env (!current_cca_constraints) t t' then
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]) )
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [] )
(* If not, we check whether we can add it. *)
else
......@@ -649,8 +649,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
current_cca_constraints := new_constraints;
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]) )
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [] )
with
| Case_fail (No_cca_hint) | Case_fail (No_alpha_renaming _) ->
......@@ -660,8 +660,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
| Fun ("dec",[x;sk]), Fun ("dec",[x';sk']) ->
(* We check whether this is already a decryption oracle calls. *)
if is_a_dec_call env (!current_cca_constraints) t t' then
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]))
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [])
(* If not, we check whether we can add it. *)
else
......@@ -672,8 +672,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
current_cca_constraints := new_constraints;
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]) )
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [] )
with
| Case_fail _ -> build_ctxt_fun_case t t'
......@@ -681,8 +681,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
| If (b,u,v), If (b',u',v') ->
if is_a_dec_call env (!current_cca_constraints) t t' then
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]) )
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [] )
(* If not, we check whether we can add it. *)
else
......@@ -693,8 +693,8 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
current_cca_constraints := new_constraints;
( Fun (ctxt_placeholder_string,[]),
Fun (ctxt_placeholder_string,[]) )
( t_fun ctxt_placeholder_string [],
t_fun ctxt_placeholder_string [] )
with
| Case_fail _ ->
......@@ -702,7 +702,7 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
and (new_v, new_v') = build_ctxt v v'
and (new_b, new_b') = build_ctxt b b' in
(If (new_b,new_u,new_v), If (new_b',new_u',new_v'))
(t_ite new_b new_u new_v, t_ite new_b' new_u' new_v')
end
| Fun (s,l), Fun (s',l') ->
......@@ -712,7 +712,7 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
let (new_u, new_u') = build_ctxt u u'
and (new_v, new_v') = build_ctxt v v' in
(EQ (new_u,new_v), EQ (new_u',new_v'))
(t_eq new_u new_v, t_eq new_u' new_v')
| True, True -> (t,t')
| False, False -> (t,t')
......
......@@ -283,11 +283,11 @@ let clean_bindings formula =
let appears : type a. a sort -> variable_string -> bool = fun sort var ->
List.exists (fun el -> match el.term_pair with
| B (b,b') -> (subterm formula.env (Var (var,sort)) b)
|| (subterm formula.env (Var (var,sort)) b')
| B (b,b') -> (subterm formula.env (t_var var sort) b)
|| (subterm formula.env (t_var var sort) b')
| T (u,u') -> (subterm formula.env (Var (var,sort)) u)
|| (subterm formula.env (Var (var,sort)) u'))
| T (u,u') -> (subterm formula.env (t_var var sort) u)
|| (subterm formula.env (t_var var sort) u'))
formula.formula_element_list in
let f_fold : type a. variable_string list -> (variable_string * a term) ->
......
......@@ -538,7 +538,7 @@ let rec auto_function_application state (sk : (state,'a) sk) fk =
[FA,i]
else if reversed then
(* Careful about the order here. *)
(R (Left,EQ(u,v),EQ(v,u),[]),i) :: [FA,i]
(R (Left,t_eq u v,t_eq v u,[]),i) :: [FA,i]
else
[] in
......@@ -673,7 +673,7 @@ let extend_unitary : type a. a axiom_type -> state -> state =
is the decrypted term. *)
let rec build_dec_oracle encs t m = match encs with
| [] -> t
| e :: encs' -> If (EQ(m,e), Fun ("z0",[]), build_dec_oracle encs' t m)
| e :: encs' -> t_ite (t_eq m e) (t_cst "z0") (build_dec_oracle encs' t m)
(* build_guarded_dec encs t m : Build a r_equal guarded version of t, where
each guard appear twice. The 'then' case of the second appearance is a
......@@ -685,7 +685,7 @@ let build_guarded_dec encs t m =
let rec build list = match list with
| [] -> oracle_call
| e :: list' -> If (EQ(m,e), t, build list') in
| e :: list' -> t_ite (t_eq m e) t (build list') in
build encs
......@@ -716,7 +716,7 @@ let guard_term env g_data_side t =
let rec add_guards list = match list with
| [] -> rewrite env dec g_dec t []
| e :: list' -> If (EQ(m,e), t, add_guards list') in
| e :: list' -> t_ite (t_eq m e) t (add_guards list') in
add_guards encs
......@@ -744,7 +744,7 @@ let create_guard_data_side goal encs t =
{ dec_term = t;
dec_term_content = m;
guard_enc_list = encs;
guarded_dec = Var (g_t_name,Msg) } in
guarded_dec = t_var g_t_name Msg } in
let new_goal = add_binding goal g_t_name guarded_t in
......@@ -890,7 +890,7 @@ let guard_decryption state cca_constraints g_data sk fk =
and r_encs = g_data.right_guard.guard_enc_list in
let guard_pairs =
List.map2 (fun e1 e2 -> (EQ(l_m,e1), EQ(r_m,e2))) l_encs r_encs in
List.map2 (fun e1 e2 -> (t_eq l_m e1, t_eq r_m e2)) l_encs r_encs in
let rec cs_split state guards fk = match guards with
| [] -> sk state fk
......
......@@ -6,7 +6,6 @@ open Axiom
open Rule
open Debug
open Interactive
open Nsl
open Cca
open Axiom_result
open Side
......@@ -85,7 +84,7 @@ let main_interactive () =
in
let formula_list =
if !file_name = "" then
[Nsl.nsl]
failwith "YOu need to provide a .api file"
else
let input_channel = open_in !file_name in
let (declarations,(p_l,p_r)) = parse_problem input_channel in
......
open Term
open Formula
open Interactive
let pi1 x = Fun ("pi1",[x])
and pi2 x = Fun ("pi2",[x])
and pair x y = Fun ("pair",[x;y])
let pk x = Fun ("pk",[x])
and sk x = Fun ("sk",[x])
and dec x y = Fun ("dec",[x;y])
and enc m r pk = Fun ("enc",[m;r;pk])
let na = Name ("na",Msg)
and nb = Name ("nb",Msg)
let nka = Name ("nka",Msg)
and nkb = Name ("nkb",Msg)
let cpt = ref 0
let r () = cpt := !cpt + 1; Name ("r" ^ (string_of_int (!cpt - 1)),Msg)
let pka = pk nka
and pkb = pk nkb
and ska = sk nka
and skb = sk nkb
and zero = Fun ("z0",[])
and a = Fun ("A",[])
and b = Fun ("B",[])
and g_to phi = Fun ("to" ^ string_of_int (List.length phi),phi)
and h phi sk = dec (Fun ("g" ^ string_of_int (List.length phi),phi)) sk
and ite b u v = If (b,u,v)
let phi0 = pka :: pkb :: a :: b :: [enc (pair na a) (r ()) pkb]
let t1 s =
ite (EQ (g_to(phi0),a))
(
ite (EQ (pi1 (h phi0 ska),a))
(
ite (EQ (pi2 (pi2 ((h phi0 ska))),b))
(enc
(pi1 (pi2 (h phi0 ska)))
(r ())
pkb
)
(zero)
)
(zero)
)
(
ite (EQ (pi2 (h phi0 skb),a))
(enc
(pair (pi1 (h phi0 skb)) (pair s b))
(r ())
pka
)
(zero)
)
let l_phi1 = phi0 @ [t1 nb]
let r_phi1 = phi0 @ [t1 zero]
let t2 phi1 s =
ite (EQ (g_to(phi0),a))
(
ite (EQ (pi2 (h phi1 skb),a))
(enc
(pair (pi1 (h phi1 skb)) (pair s b))
(r ())
pka
)
(zero)
)
(
ite (EQ (pi1 (h phi1 ska),a))
(
ite (EQ (pi2 (pi2 ((h phi1 ska))),b))
(enc
(pi1 (pi2 (h phi1 ska)))
(r ())
pkb
)
(zero)
)
(zero)
)
let l_phi2 = l_phi1 @ [t2 l_phi1 nb]
let r_phi2 = r_phi1 @ [t2 r_phi1 zero]
let nsl_bindings =
[("pka", pka);
("pkb",pkb);
("ska",ska);
("skb",skb);
("h0a",h phi0 ska);
("hl1a",h l_phi1 ska);
("hr1a",h r_phi1 ska);
("h0b",h phi0 skb);
("hl1b",h l_phi1 skb);
("hr1b",h r_phi1 skb)]
let nsl = List.fold_left
(fun formula (s,t) -> Formula.add_binding formula s t)
(Formula.new_formula [] (List.combine l_phi2 r_phi2))
nsl_bindings
......@@ -365,7 +365,7 @@ let rec print_guard ppf g =
let ident = fun ppf s -> pf ppf "%s" s in
match g with
| NilGuard -> print_term ppf True
| NilGuard -> print_term ppf (t_true ())
| Guard b -> pf ppf "@[%a@]" print_term b
| NGuard b ->
......@@ -424,7 +424,7 @@ let ireduce conf side =
let env' = env_add_binding env var t in
(Var (var,Msg)) :: acc_args, env', map_fresh')
(t_var var Msg) :: acc_args, env', map_fresh')
([],env,map_fresh) l l_arg_names in
(List.rev l_args,env',map_fresh')
......@@ -446,7 +446,7 @@ let ireduce conf side =
reduced_gp_list
env'
map_fresh'
((g, process_subst s (Name (name,Msg)) p') :: acc_gp_list')
((g, process_subst s (t_name name Msg) p') :: acc_gp_list')
| g, Parallel (p', p'') ->
aux_ireduce
......@@ -486,7 +486,7 @@ let ireduce conf side =
reduced_gp_list
env'
map_fresh'
((g, process_subst s (Var (var,Msg)) p') :: acc_gp_list') in
((g, process_subst s (t_var var Msg) p') :: acc_gp_list') in
let (gp_list',env',map_fresh') =
aux_ireduce [] conf.env conf.map_fresh conf.procs in
......@@ -830,14 +830,14 @@ let rec term_from_itree env itree = match itree with
and term_from_guard env g t1 t2 = match g with
| NilGuard -> t1
| Guard b -> If (b, t1, t2)
| NGuard b -> If (b, t2, t1)
| Guard b -> t_ite b t1 t2
| NGuard b -> t_ite b t2 t1
| Conj (b, g2) ->
If (b, term_from_guard env g2 t1 t2, t2)
t_ite b (term_from_guard env g2 t1 t2) t2
| NConj (b, g2) ->
If (b, t2, term_from_guard env g2 t1 t2)
t_ite b t2 (term_from_guard env g2 t1 t2)
(* Sort a list of actions using the lexicographical order on (x,c) where
x \in \{AIn,AOut\} and c is the (inputting or outputting) channel name
......@@ -867,7 +867,7 @@ let get_adv_term conf frame phi side s =
let adv_term_fun_name = "g" ^ (string_of_int i) in
(* We reverse the frame, as it is stored in reversed order *)
let adv_term = Fun (adv_term_fun_name, [phi]) in
let adv_term = t_fun adv_term_fun_name [phi] in
(* Declare function type (it may be already declared) *)
let env' = bind_type env adv_term_fun_name (TFun 1) in
......@@ -877,7 +877,7 @@ let get_adv_term conf frame phi side s =
let env'' = env_add_binding env' var adv_term in
let adv_term_var = Var (var,Msg) in
let adv_term_var = t_var var Msg in
let new_conf = { conf with env = env'';
map_fresh = map_fresh' } in
......@@ -950,7 +950,7 @@ let apply_action action side f_conf =
{ partial_conf' with procs = (g,p') :: partial_conf'.procs } in
let partial_itree' = Node ( g,
Leave (Fun ("input",[])),
Leave (t_fun "input" []),
partial_itree ) in
(partial_conf'', partial_itree')
......@@ -972,7 +972,7 @@ let apply_action action side f_conf =
| _ -> assert false)
({ sorted_conf with procs = [] } , Leave (Fun ("silence",[])))
({ sorted_conf with procs = [] } , Leave (t_fun "silence" []))
sorted_conf.procs in
let red_new_conf = ireduce new_conf side in
......@@ -991,11 +991,11 @@ let apply_action action side f_conf =
let (var_phi', map_fresh') =
fresh_name env map_fresh side ("phi" ^ string_of_int i) in
let term_phi' = Fun ("pair", [phi; norm_outputed_term]) in
let term_phi' = t_fun "pair" [phi; norm_outputed_term] in
let env' = env_add_binding env var_phi' term_phi' in
let phi' = Var (var_phi',Msg) in
let phi' = t_var var_phi' Msg in
let f_conf_side' = { f_procs = red_new_conf.procs;
frame = norm_outputed_term :: frame;
......@@ -1108,12 +1108,12 @@ let fold_protocol env left_process right_process =
let left_f_conf_s =
{ f_procs = l_red_conf.procs;
frame = [];
phi = Fun ("g_e",[]) } in
phi = t_fun "g_e" [] } in
let right_f_conf_s =
{ f_procs = r_red_conf.procs;
frame = [];
phi = Fun ("g_e",[]) } in
phi = t_fun "g_e" [] } in
aux { left_c = left_f_conf_s;
right_c = right_f_conf_s;
......
......@@ -128,7 +128,7 @@ let fa_apply env t t' =
| If (b,u,v) ->
List.map2
(fun x y -> If (b,x,y))
(fun x y -> t_ite b x y)
(fa_aux (s_leave,i_leave) u)
(fa_aux (s_leave,i_leave) v)
......@@ -215,26 +215,26 @@ let rewrite : type a b. environment -> a term -> a term -> b term
| Var _ -> ein env m aux
| Fun (s,l) ->
Fun (s, List.map aux l)
t_fun s (List.map aux l)
| EQ (bl,br) ->
begin
match get_sort u with
| Msg ->
if (syntactic_equal env (EQ (u,v)) m)
|| (syntactic_equal env (EQ (v,u)) m) then
True
if (syntactic_equal env (t_eq u v) m)
|| (syntactic_equal env (t_eq v u) m) then
t_true ()
else
EQ (aux bl, aux br)
t_eq (aux bl) (aux br)
| Bool -> EQ (aux bl, aux br)
| Bool -> t_eq (aux bl) (aux br)
end
| If (b,tl,tr) ->
match aux b with
| True -> aux tl
| False -> aux tr
| _ as r_b -> If (r_b, aux tl, aux tr) in
| _ as r_b -> t_ite r_b (aux tl) (aux tr) in
aux term
......@@ -253,9 +253,9 @@ let ift_apply env u v t encs =
if List.exists (fun x -> syntactic_equal env x t) encs then
t
else
Fun ("enc", List.map down l)
t_fun "enc" (List.map down l)
| Fun (s,l) -> Fun (s, List.map down l)
| Fun (s,l) -> t_fun s (List.map down l)
| If (b,tl,tr) ->
(* This case is tricky to handle.
......@@ -265,11 +265,11 @@ let ift_apply env u v t encs =
- if this is not the case we recurse in both branches *and* the
conditional b (which is then expanded only if the recursive call
produce something else than b) *)
if syntactic_equal env (EQ(u,v)) b then
If (b,rewrite env u v tl encs,down tr)
if syntactic_equal env (t_eq u v) b then
t_ite b (rewrite env u v tl encs) (down tr)
else if syntactic_equal env (EQ(v,u)) b then
If (b,rewrite env u v tl encs,down tr)
else if syntactic_equal env (t_eq v u) b then
t_ite b (rewrite env u v tl encs) (down tr)
else
begin try
......@@ -277,16 +277,16 @@ let ift_apply env u v t encs =
match exp_b with
| EQ (bl,br) ->
let b_res = EQ (down bl, down br) in
let b_res = t_eq (down bl) (down br) in
if syntactic_equal env b_res exp_b then
If (b, down tl, down tr)
t_ite b (down tl) (down tr)
else
If (b_res, down tl, down tr)
t_ite b_res (down tl) (down tr)
| _ -> If (b, down tl, down tr)
| _ -> t_ite b (down tl) (down tr)
with
| Unexpandable _ -> If (b, down tl, down tr)
| Unexpandable _ -> t_ite b (down tl) (down tr)
end
| _ -> assert false in
......@@ -306,8 +306,8 @@ let b_ift_rule_apply env side u v b b' encs =
let next_cond = ein env apply_on (fun b ->
match b with
| EQ(tl,tr) -> EQ ( ift_apply env u v tl encs,
ift_apply env u v tr encs )
| EQ(tl,tr) ->
t_eq (ift_apply env u v tl encs) (ift_apply env u v tr encs )
| _ -> b) in
match side with
......@@ -347,10 +347,10 @@ let if_intro_apply env t t' (b,b') =
let intro_apply t b =
try match eiv env b with
| EQ (u,v) -> If (b,rewrite env u v t [],t)
| _ -> If (b, t, t)
| EQ (u,v) -> t_ite b (rewrite env u v t []) t
| _ -> t_ite b t t
with
| Unexpandable _ -> If (b, t, t) in
| Unexpandable _ -> t_ite b t t in
bt_combine [] [intro_apply t b, intro_apply t' b']
......@@ -474,21 +474,21 @@ let rec rewrite_cond_false
| EQ (u,v) ->
if syntactic_equal env b t then
False
t_false ()
else
EQ ( rewrite_cond_false env b u,
rewrite_cond_false env b v )
t_eq (rewrite_cond_false env b u)
(rewrite_cond_false env b v)
| Fun (f_s,l) -> Fun (f_s,List.map (rewrite_cond_false env b) l)
| Fun (f_s,l) -> t_fun f_s (List.map (rewrite_cond_false env b) l)
| If (b',u,v) ->
if syntactic_equal env b b' then
rewrite_cond_false env b v
else
If ( rewrite_cond_false env b b',
rewrite_cond_false env b u,
rewrite_cond_false env b v ))
t_ite (rewrite_cond_false env b b')
(rewrite_cond_false env b u)
(rewrite_cond_false env b v))
exception Bad_cond_fresh
......@@ -551,7 +551,7 @@ let cond_fresh_apply r formula = match r with
let env' = bind_new_type formula.env n_fresh TName in
( { term_pair = T (Name (n, Msg), Name (n_fresh, Msg));
( { term_pair = T (t_name n Msg, t_name n_fresh Msg);
hidden_status = false;
unitary_result = Unset }
......
......@@ -8,7 +8,7 @@ type variable_string = string
type _ sort = | Msg : msg sort
| Bool : boole sort
type _ term =
type _ term =
| True : boole term
| False : boole term
| Name : name_string * 'a sort -> 'a term
......@@ -22,27 +22,6 @@ type _ term =
(* Miscellaneous *)
(*****************)
let enc u r pk = Fun("enc",[u;Name (r,Msg);Fun ("pk",[Name (pk,Msg)])])
and ite b u v = If (b,u,v)
and dec u sk = Fun("dec",[u;Fun ("sk",[Name (sk,Msg)])])
and pair a b = Fun("pair",[a;b])
and sk s = Fun("sk",[Name (s,Msg)])
and pk s = Fun("pk",[Name (s,Msg)])
and eq a b = EQ(a,b)
and name r = Name (r,Msg)
and var r = Var (r,Msg)
and cst a = Fun(a,[])
let get_sort : type a. a term -> a sort =
fun t -> match t with
| Var (_,Msg) -> Msg
......@@ -76,6 +55,39 @@ let term_free_variables t =
aux ([],[]) t
(*********************)
(* Smart Constructor *)
(*********************)
let t_fun s l = Fun (s,l)
let t_enc u r pk = t_fun "enc" [u;Name (r,Msg);Fun ("pk",[Name (pk,Msg)])]
and t_ite b u v = If (b,u,v)
and t_dec u sk = t_fun "dec" [u;Fun ("sk",[Name (sk,Msg)])]
and t_pair a b = t_fun "pair" [a;b]
and t_sk s = t_fun "sk" [Name (s,Msg)]
and t_pk s = t_fun "pk" [Name (s,Msg)]
and t_eq a b = EQ(a,b)
and t_name : type a. name_string -> a sort -> a term =
fun r sort -> Name (r,sort)
and t_var : type a. variable_string -> a sort -> a term =
fun r sort -> Var (r,sort)
and t_cst a = t_fun a []
and t_true () = True
and t_false () = False
(************************)
(* Term Pretty Printing *)
(************************)
......@@ -1575,10 +1587,7 @@ let pseudo_normalize : type a. environment -> a term -> a term = fun env t ->
let r_equal : type a. environment -> a term -> a term -> bool =
fun env t t' ->
let test = (* match get_sort t' with *)
(* | Msg -> syntactic_equal env t' *)
(* TODO *)
(* | _ -> false *) false in