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

started using hashcons. Code does not compile

parent e5d0d7a2
......@@ -388,7 +388,7 @@ let auto_ift state =
| AB t :: alg_list' -> term_auto_ift_boole side alg_list' acc t
and term_auto_ift_msg side alg_list acc t =
match eiv env t with
match t.content with
| Name _ -> term_auto_ift side alg_list acc
| Var _ -> assert (false)
......@@ -404,7 +404,7 @@ let auto_ift state =
| _ -> assert false
and term_auto_ift_boole side alg_list acc t =
match eiv env t with
match t.content with
| True -> term_auto_ift side alg_list acc
| False -> term_auto_ift side alg_list acc
| Name _ -> term_auto_ift side alg_list acc
......@@ -515,11 +515,9 @@ let rec auto_function_application state (sk : (state,'a) sk) fk =
List.fold_left2 (fun (i,rule_list,state) formula_element res_el ->
match formula_element.term_pair with
| B (left_term,right_term) ->
let exp_left = eiv env left_term
and exp_right = eiv env right_term in
begin
match exp_left, exp_right with
match left_term.content, right_term.content with
(* We try to match (u,v) with (u',v') or with (v',u'). If such a math
exists, then we apply Fab (inversing u and v if necessary).
Otherwise we do nothing. *)
......@@ -580,7 +578,7 @@ let rec auto_function_application state (sk : (state,'a) sk) fk =
env constraints left_term right_term)
&& (not res_el_success) in
match use_fab,eiv env left_term, eiv env right_term with
match use_fab, left_term.content, right_term.content with
| true, If _, If _ ->
(i+1,(FAb,i) :: rule_list,state)
| _ -> (i+1, rule_list,state))
......@@ -730,7 +728,7 @@ let create_guard_data_side goal encs t =
let guarded_t = build_dec_oracle encs t m in
(* We add a new term binding for the guarded decryption *)
let g_t_name_suffix = match t with
let g_t_name_suffix = match t.content with
| Var (s,Msg) -> s
| Fun("dec",[Fun (s,_);_]) -> s
| _ -> "" in
......@@ -748,7 +746,7 @@ let create_guard_data_side goal encs t =
let new_goal = add_binding goal g_t_name guarded_t in
let get_enc_content env alpha = match eiv env alpha with
let get_enc_content env alpha = match alpha.content with
| Fun ("enc",[m;r;pk]) -> m
| _ -> assert false in
......@@ -761,7 +759,7 @@ let create_guard_data_side goal encs t =
let g_u = rewrite c_goal.env t x u []
|> weak_normalize c_goal.env in
match g_u with
match g_u.content with
| Var _ -> c_goal
| _ ->
let new_c_goal = add_binding c_goal var_fresh g_u in
......@@ -925,7 +923,7 @@ let auto_guard state sk fk =
let (_,CCA_constraints constr,_) = apply_axiom goal CCA in
(* Return true if t is a decryption. *)
let is_dec t = match eiv env t with
let is_dec t = match t.content with
| Fun("dec",[_;Fun("sk",[_])]) -> true
| _ -> false in
......
This diff is collapsed.
......@@ -10,14 +10,18 @@ type variable_string = string
type _ sort = | Msg : msg sort
| Bool : boole sort
type _ term = private
| True : boole term
| False : boole term
| Name : name_string * 'a sort -> 'a term
| Var : variable_string * 'a sort -> 'a term
| Fun : function_symbol_string * msg term list -> msg term
| If : boole term * msg term * msg term -> msg term
| EQ : msg term * msg term -> boole term
type 'a term = private { hash : int;
content : 'a term_cnt }
and _ term_cnt = private
| True : boole term_cnt
| False : boole term_cnt
| Name : name_string * 'a sort -> 'a term_cnt
| Var : variable_string * 'a sort -> 'a term_cnt
| Fun : function_symbol_string * msg term list -> msg term_cnt
| If : boole term * msg term * msg term -> msg term_cnt
| EQ : msg term * msg term -> boole term_cnt
(*****************)
(* Miscellaneous *)
......@@ -170,19 +174,19 @@ val expand_var : environment -> 'a term -> variable_string -> 'a term
(* expand_all env t: Expand the term t in the environment env. *)
val expand_all : environment -> 'a term -> 'a term
(* eiv env t: Expand t if it is a variable, using the
environment env. Raise an Unexpandable (err_msg) if the variable
cannot be expanded. *)
val eiv : environment -> 'a term -> 'a term
(* (\* eiv env t: Expand t if it is a variable, using the *)
(* environment env. Raise an Unexpandable (err_msg) if the variable *)
(* cannot be expanded. *\) *)
(* val eiv : environment -> 'a term -> 'a term *)
(* Like eiv, but i steps. *)
val eiv_i : environment -> 'a term -> int -> 'a term
(* (\* Like eiv, but i steps. *\) *)
(* val eiv_i : environment -> 'a term -> int -> 'a term *)
(* ein env t f: Apply f to t. If t is a variable tries to expand it
in the environment env before applying f. If f is the identity on the
expanded term then return the unexpanded variable. *)
val ein :
environment -> 'a term -> ('a term -> 'a term) -> 'a term
(* (\* ein env t f: Apply f to t. If t is a variable tries to expand it *)
(* in the environment env before applying f. If f is the identity on the *)
(* expanded term then return the unexpanded variable. *\) *)
(* val ein : *)
(* environment -> 'a term -> ('a term -> 'a term) -> 'a term *)
(* get_head env term: return Some f, where f is the head function symbol of
term modulo if-homomorphism. Return None if it does not exists.
......
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