Commit c0bd5a28 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

type checking and pretty printing is broken in this version

parent 8a9bd931
Pipeline #1657 failed with stage
in 1 minute and 15 seconds
...@@ -90,8 +90,8 @@ let hint_same_shape h1 h2 = match h1, h2 with ...@@ -90,8 +90,8 @@ let hint_same_shape h1 h2 = match h1, h2 with
(* Pretty Printing *) (* Pretty Printing *)
(*******************) (*******************)
let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit = let print_axiom_hint : type a. env -> Format.formatter -> a axiom_hint -> unit =
fun ppf hint -> match hint with fun env ppf hint -> match hint with
| No_cca_hint -> pf ppf "No hint" | No_cca_hint -> pf ppf "No hint"
| Guard_problem (enc_pairs,l_superfl,r_superfl) -> | Guard_problem (enc_pairs,l_superfl,r_superfl) ->
...@@ -99,14 +99,14 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit = ...@@ -99,14 +99,14 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit =
if s_list <> [] then if s_list <> [] then
pf ppf "@;Superfluous on the %s:@[<v 1>%a@]" pf ppf "@;Superfluous on the %s:@[<v 1>%a@]"
(side_to_string side) (side_to_string side)
(list print_term) s_list (list (print_term env)) s_list
else () in else () in
pf ppf "@[<v 0>Missing guards:@;@[<hov>%a@]%a%a@]" pf ppf "@[<v 0>Missing guards:@;@[<hov>%a@]%a%a@]"
(list (fun ppf (a,b) -> (list (fun ppf (a,b) ->
pf ppf "@[<hov>(@[%a@],@,@[%a@])@]" pf ppf "@[<hov>(@[%a@],@,@[%a@])@]"
print_term a (print_term env) a
print_term b)) enc_pairs (print_term env) b)) enc_pairs
(print_superfl Left) l_superfl (print_superfl Left) l_superfl
(print_superfl Right) r_superfl (print_superfl Right) r_superfl
...@@ -114,8 +114,8 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit = ...@@ -114,8 +114,8 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit =
pf ppf "@[<v 1>Encryption randomness appearing twice on the %s:\ pf ppf "@[<v 1>Encryption randomness appearing twice on the %s:\
@;@[%a@]@;@[%a@]@]" @;@[%a@]@;@[%a@]@]"
(side_to_string side) (side_to_string side)
print_term s (print_term env) s
print_term t (print_term env) t
| Bad_randomness (n,side) -> | Bad_randomness (n,side) ->
pf ppf "Encryption randomness %s leaking on the %s" pf ppf "Encryption randomness %s leaking on the %s"
...@@ -129,7 +129,7 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit = ...@@ -129,7 +129,7 @@ let print_axiom_hint : type a. Format.formatter -> a axiom_hint -> unit =
pf ppf "@[<v 1>Decryption appearing where it should not on the %s:\ pf ppf "@[<v 1>Decryption appearing where it should not on the %s:\
@;@[%a@]@]" @;@[%a@]@]"
(side_to_string side) (side_to_string side)
print_term t (print_term env) t
| Bad_secret_key (n,side) -> | Bad_secret_key (n,side) ->
pf ppf "Secret key %s appearing outside a decryption position on the %s" pf ppf "Secret key %s appearing outside a decryption position on the %s"
...@@ -146,8 +146,8 @@ let print_axiom_success : type a. Format.formatter -> a axiom_success -> unit = ...@@ -146,8 +146,8 @@ let print_axiom_success : type a. Format.formatter -> a axiom_success -> unit =
| Decryption -> pf ppf "Dec" | Decryption -> pf ppf "Dec"
let print_res_hint : type a. Format.formatter -> axiom_result -> unit = let print_res_hint : type a. env -> Format.formatter -> axiom_result -> unit =
fun ppf res -> fun env ppf res ->
let open Fmt in let open Fmt in
let ident ppf s = pf ppf "%s" s in let ident ppf s = pf ppf "%s" s in
...@@ -155,4 +155,4 @@ let print_res_hint : type a. Format.formatter -> axiom_result -> unit = ...@@ -155,4 +155,4 @@ let print_res_hint : type a. Format.formatter -> axiom_result -> unit =
| Unset -> assert false | Unset -> assert false
| Success ax_suc -> pf ppf "Success %a" print_axiom_success ax_suc | Success ax_suc -> pf ppf "Success %a" print_axiom_success ax_suc
| Failure _ -> ident ppf "Failure" | Failure _ -> ident ppf "Failure"
| Failure_hint hint -> print_axiom_hint ppf hint | Failure_hint hint -> print_axiom_hint env ppf hint
This diff is collapsed.
...@@ -35,7 +35,7 @@ type cca_constraints = ...@@ -35,7 +35,7 @@ type cca_constraints =
(* Pretty Printing *) (* Pretty Printing *)
(*******************) (*******************)
val print_cca_constraints : Format.formatter -> cca_constraints -> unit val print_cca_constraints : env -> Format.formatter -> cca_constraints -> unit
(*********************************) (*********************************)
...@@ -50,42 +50,42 @@ exception Alpha_conflict of ...@@ -50,42 +50,42 @@ exception Alpha_conflict of
exception Shape_no_match exception Shape_no_match
(* Raises Shape_no_match if the terms are not alpha-equal. *) (* Raises Shape_no_match if the terms are not alpha-equal. *)
val alpha_rename : environment -> alpha_const -> 'a term -> 'a term val alpha_rename : env -> alpha_const -> 'a term -> 'a term
-> alpha_const -> alpha_const
(* subterm_encryptions enc t n: Return the list of encryptions under key sk(n) (* subterm_encryptions enc t n: Return the list of encryptions under key sk(n)
appearing in the term t, in the environment env. *) appearing in the term t, in the environment env. *)
val subterm_encryptions : val subterm_encryptions :
environment -> 'a term -> name_string -> msg term list env -> 'a term -> name_string -> msg term list
exception Case_fail of cca axiom_hint exception Case_fail of cca axiom_hint
(* Return the message and the key used in a decryption oracle call. (* Return the message and the key used in a decryption oracle call.
Return None if the shape of the term is wrong. *) Return None if the shape of the term is wrong. *)
val get_m_dec_oracle : environment -> msg term val get_m_dec_oracle : env -> msg term
-> (msg term * name_string) option -> (msg term * name_string) option
(* enc_oracle_call_case env cca_constraints t t' : Check whether t \sim t' (* enc_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid encryption oracle call. *) is a valid encryption oracle call. *)
val enc_oracle_call_case : environment -> cca_constraints val enc_oracle_call_case : env -> cca_constraints
-> 'a term -> 'a term -> cca_constraints -> 'a term -> 'a term -> cca_constraints
exception Contexts_do_not_exist exception Contexts_do_not_exist
(* equal_up_to_oracle_calls env cca_constraints t t' : Return true iff t and t' (* equal_up_to_oracle_calls env cca_constraints t t' : Return true iff t and t'
are syntactically equal up-to encryption and decryption oracle calls. *) are syntactically equal up-to encryption and decryption oracle calls. *)
val equal_up_to_oracle_calls : environment -> cca_constraints -> msg term val equal_up_to_oracle_calls : env -> cca_constraints -> msg term
-> msg term -> bool -> msg term -> bool
(* equal_up_to_oracle_calls_strict env cca_constraints t t' : Like the function (* equal_up_to_oracle_calls_strict env cca_constraints t t' : Like the function
equal_up_to_oracle_calls, with the extra constraint that the context does not equal_up_to_oracle_calls, with the extra constraint that the context does not
contain secret key material. *) contain secret key material. *)
val equal_up_to_oracle_calls_strict : environment -> cca_constraints -> msg term val equal_up_to_oracle_calls_strict : env -> cca_constraints -> msg term
-> msg term -> bool -> msg term -> bool
(* dec_oracle_call_case env cca_constraints t t' : Check whether t \sim t' (* dec_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid decryption oracle call. *) is a valid decryption oracle call. *)
val dec_oracle_call_case : environment -> cca_constraints val dec_oracle_call_case : env -> cca_constraints
-> 'a term -> 'a term -> cca_constraints -> 'a term -> 'a term -> cca_constraints
...@@ -106,5 +106,5 @@ type extend_cca_result = ...@@ -106,5 +106,5 @@ type extend_cca_result =
calls but should be guarded) when trying to show that t \sim t' is a valid calls but should be guarded) when trying to show that t \sim t' is a valid
dec. oracle call. *) dec. oracle call. *)
val extend_cca_dec_case : val extend_cca_dec_case :
environment -> cca_constraints -> msg term -> msg term -> env -> cca_constraints -> msg term -> msg term ->
extend_cca_result * cca_constraints extend_cca_result * cca_constraints
...@@ -15,7 +15,7 @@ type formula_element = ...@@ -15,7 +15,7 @@ type formula_element =
type formula = type formula =
{ formula_element_list : formula_element list; { formula_element_list : formula_element list;
env : environment } env : env }
(*****************) (*****************)
...@@ -187,12 +187,12 @@ let remove_duplicate formula = ...@@ -187,12 +187,12 @@ let remove_duplicate formula =
List.exists (fun y -> List.exists (fun y ->
match x.term_pair,y.term_pair with match x.term_pair,y.term_pair with
| B (a,a'), B (b,b') -> | B (a,a'), B (b,b') ->
(syntactic_equal formula.env a b) (t_equal a b)
&& (syntactic_equal formula.env a' b') && (t_equal a' b')
| T (a,a'), T (b,b') -> | T (a,a'), T (b,b') ->
(syntactic_equal formula.env a b) (t_equal a b)
&& (syntactic_equal formula.env a' b') && (t_equal a' b')
| _ -> false) | _ -> false)
acc in acc in
...@@ -327,7 +327,7 @@ let print_separator shell_mode = ...@@ -327,7 +327,7 @@ let print_separator shell_mode =
(* Print the left or right formula, depending on the boolean lor_bool. *) (* Print the left or right formula, depending on the boolean lor_bool. *)
let rec print_lor_formula shell_mode lor_bool cpt f = let rec print_lor_formula env shell_mode lor_bool cpt f =
let open Fmt in let open Fmt in
let ident ppf s = pf ppf "%s" s in let ident ppf s = pf ppf "%s" s in
...@@ -349,14 +349,14 @@ let rec print_lor_formula shell_mode lor_bool cpt f = ...@@ -349,14 +349,14 @@ let rec print_lor_formula shell_mode lor_bool cpt f =
if not el.hidden_status then if not el.hidden_status then
pf stdout "%a@[%a@]@." pf stdout "%a@[%a@]@."
number_style (Printf.sprintf "%d:" cpt) number_style (Printf.sprintf "%d:" cpt)
print_term (if lor_bool then b else b'); (print_term env) (if lor_bool then b else b');
print_lor_formula shell_mode lor_bool (cpt + 1) tail; print_lor_formula env shell_mode lor_bool (cpt + 1) tail;
| T (t,t') -> | T (t,t') ->
if not el.hidden_status then if not el.hidden_status then
pf stdout "%a@[%a@]@." pf stdout "%a@[%a@]@."
number_style (Printf.sprintf "%d:" cpt) number_style (Printf.sprintf "%d:" cpt)
print_term (if lor_bool then t else t'); (print_term env) (if lor_bool then t else t');
print_lor_formula shell_mode lor_bool (cpt + 1) tail print_lor_formula env shell_mode lor_bool (cpt + 1) tail
let hashtbl_to_list ht = let hashtbl_to_list ht =
...@@ -378,12 +378,12 @@ let print_formula formula param = ...@@ -378,12 +378,12 @@ let print_formula formula param =
Printf.printf "\n"; Printf.printf "\n";
(* Print the left formula *) (* Print the left formula *)
print_lor_formula shell_mode true 0 formula.formula_element_list; print_lor_formula formula.env shell_mode true 0 formula.formula_element_list;
print_separator shell_mode; print_separator shell_mode;
next_line shell_mode; next_line shell_mode;
(* Print the right formula *) (* Print the right formula *)
print_lor_formula shell_mode false 0 formula.formula_element_list; print_lor_formula formula.env shell_mode false 0 formula.formula_element_list;
(* Print the bindings *) (* Print the bindings *)
let print_bindings = bindings_to_print formula.env in let print_bindings = bindings_to_print formula.env in
......
...@@ -12,7 +12,7 @@ type formula_element = ...@@ -12,7 +12,7 @@ type formula_element =
type formula = type formula =
{ formula_element_list : formula_element list; { formula_element_list : formula_element list;
env : environment } env : env }
exception F_out_of_bound of int exception F_out_of_bound of int
exception F_bad_argument of int exception F_bad_argument of int
...@@ -33,7 +33,7 @@ val update_unitary_result : formula_element -> axiom_result -> formula_element ...@@ -33,7 +33,7 @@ val update_unitary_result : formula_element -> axiom_result -> formula_element
(* new formula ~env:env l l': Create a new formula whose boolean elements are (* new formula ~env:env l l': Create a new formula whose boolean elements are
the element of l and term elements are the elements of l'. A type checking the element of l and term elements are the elements of l'. A type checking
is perfomed before creating the formula *) is perfomed before creating the formula *)
val new_formula : ?env:environment -> (boole term * boole term) list val new_formula : ?env:env -> (boole term * boole term) list
-> (msg term * msg term) list -> formula -> (msg term * msg term) list -> formula
(* c_bind formula new_f: Return a new formula where the formula elements (* c_bind formula new_f: Return a new formula where the formula elements
......
...@@ -61,7 +61,7 @@ let unary_build proof r_and_index_list = ...@@ -61,7 +61,7 @@ let unary_build proof r_and_index_list =
| Bad_rule (s,rule) -> | Bad_rule (s,rule) ->
let err_fun = fun () -> let err_fun = fun () ->
Fmt.pf Fmt.stderr "@[Bad rule:@;%a@;%s@]\n@?%!" Fmt.pf Fmt.stderr "@[Bad rule:@;%a@;%s@]\n@?%!"
print_rule_long rule s in (print_rule_long goal.env) rule s in
( goal, ( goal,
err_fun :: l_fun_error, err_fun :: l_fun_error,
...@@ -247,8 +247,8 @@ let apply_unitary_and_set_feedback : ...@@ -247,8 +247,8 @@ let apply_unitary_and_set_feedback :
(fun el res_el -> update_unitary_result el res_el) (fun el res_el -> update_unitary_result el res_el)
goal.formula_element_list result_list in goal.formula_element_list result_list in
let updated_goal = { formula_element_list = updated_element_list; let updated_goal =
env = goal.env } in { goal with formula_element_list = updated_element_list } in
if print then if print then
begin begin
...@@ -272,10 +272,10 @@ let apply_unitary_and_set_feedback : ...@@ -272,10 +272,10 @@ let apply_unitary_and_set_feedback :
(fun ppf res_el -> pf ppf "%a @[%a@]" (fun ppf res_el -> pf ppf "%a @[%a@]"
(number_style res_el) (number_style res_el)
(cpt:= !cpt + 1; Printf.sprintf "%d:" (!cpt)) (cpt:= !cpt + 1; Printf.sprintf "%d:" (!cpt))
print_res_hint (print_res_hint goal.env)
res_el)) res_el))
result_list result_list
Cca.print_cca_constraints cca_constraints (Cca.print_cca_constraints updated_goal.env) cca_constraints
end; end;
state.c_proof.goal <- updated_goal; state.c_proof.goal <- updated_goal;
...@@ -347,8 +347,8 @@ let apply_ift_heuristic state constraints side t s = ...@@ -347,8 +347,8 @@ let apply_ift_heuristic state constraints side t s =
let (included',strict') = is_included let (included',strict') = is_included
(fun x y -> (fun x y ->
if syntactic_equal env x y then 0 if t_equal x y then 0
else Pervasives.compare x y) else t_compare x y)
s_encryptions t_encryptions in s_encryptions t_encryptions in
(included && included', strict || strict')) (included && included', strict || strict'))
...@@ -933,7 +933,7 @@ let auto_guard state sk fk = ...@@ -933,7 +933,7 @@ let auto_guard state sk fk =
(* Return true if t is a decryption oracle call. *) (* Return true if t is a decryption oracle call. *)
let not_in_g_dec decs t = let not_in_g_dec decs t =
List.exists (syntactic_equal env t) decs in List.exists (t_equal t) decs in
(* We compute all the decryptions appearing on the left and right that are (* We compute all the decryptions appearing on the left and right that are
not subterm of a decryption oracle calls. *) not subterm of a decryption oracle calls. *)
...@@ -953,12 +953,8 @@ let auto_guard state sk fk = ...@@ -953,12 +953,8 @@ let auto_guard state sk fk =
([],[]) goal.formula_element_list in ([],[]) goal.formula_element_list in
(* We remove duplicates *) let l_decs = List.sort_uniq t_compare l_decs
let my_compare t t' = and r_decs = List.sort_uniq t_compare r_decs in
if syntactic_equal env t t' then 0 else Pervasives.compare t t' in
let l_decs = List.sort_uniq my_compare l_decs
and r_decs = List.sort_uniq my_compare r_decs in
(* We compute the pairs of matching decryptions *) (* We compute the pairs of matching decryptions *)
let dec_pairs = let dec_pairs =
...@@ -993,7 +989,7 @@ let auto_guard state sk fk = ...@@ -993,7 +989,7 @@ let auto_guard state sk fk =
(list ~sep:(fun ppf () -> pf ppf "@;") (list ~sep:(fun ppf () -> pf ppf "@;")
(fun ppf (a,b,r) -> pf ppf "@[<hv>%a @,%a@]@;%a@;" (fun ppf (a,b,r) -> pf ppf "@[<hv>%a @,%a@]@;%a@;"
print_term a print_term b print_res_hint r)) (print_term env) a (print_term env) b (print_res_hint env) r))
dec_pairs_with_res) dec_pairs_with_res)
state in state in
...@@ -1020,7 +1016,7 @@ let auto_guard state sk fk = ...@@ -1020,7 +1016,7 @@ let auto_guard state sk fk =
pf stdout "@[<v>Guarded the following decryption pairs:@;%a%!@]" pf stdout "@[<v>Guarded the following decryption pairs:@;%a%!@]"
(list ~sep:(fun ppf () -> pf ppf "@;") (list ~sep:(fun ppf () -> pf ppf "@;")
(pair print_term print_term)) (pair (print_term new_goal.env) (print_term new_goal.env)))
(List.map (fun g_data -> (List.map (fun g_data ->
( g_data.left_guard.dec_term, ( g_data.left_guard.dec_term,
......
...@@ -18,19 +18,6 @@ let parse_problem input_channel = ...@@ -18,19 +18,6 @@ let parse_problem input_channel =
try try
let (decl_list,(p_left,p_right)) = let (decl_list,(p_left,p_right)) =
Term_parser.problem Term_lexer.token lexbuf in Term_parser.problem Term_lexer.token lexbuf in
let _ = debug (fun () ->
Printf.eprintf "Parsed process %d declarations:\n"
(List.length decl_list);
List.iter (fun process ->
print_process_decl Fmt.stderr process;
Fmt.pf Fmt.stderr "@.")
decl_list;
Printf.eprintf "Left process:\n";
print_concrete_process Fmt.stderr p_left;
Fmt.pf Fmt.stderr "@.";
Printf.eprintf "Right process:\n";
print_concrete_process Fmt.stderr p_right;
Fmt.pf Fmt.stderr "@.";) in
(decl_list,(p_left,p_right)) (decl_list,(p_left,p_right))
with with
| Term_lexer.Lexer_Error i -> | Term_lexer.Lexer_Error i ->
...@@ -87,9 +74,25 @@ let main_interactive () = ...@@ -87,9 +74,25 @@ let main_interactive () =
failwith "YOu need to provide a .api file" failwith "YOu need to provide a .api file"
else else
let input_channel = open_in !file_name in let input_channel = open_in !file_name in
let (declarations,(p_l,p_r)) = parse_problem input_channel in let (declarations,(p_l,p_r)) = parse_problem input_channel in
add_declarations declarations; add_declarations declarations;
let env = init_env () in let env = init_env () in
let _ = debug (fun () ->
let open Fmt in
pf stderr "Parsed process %d declarations:\n@.@[<v 0>%a@]\n"
(List.length declarations)
(list (fun ppf process ->
print_process_decl ppf process))
declarations;
pf stderr "Left process:@[%a@]\nRight process:@[%a@]\n@.%!"
(print_concrete_process env) p_l
(print_concrete_process env) p_r) in
List.map (fun (term_pair_list,env') -> List.map (fun (term_pair_list,env') ->
(new_formula ~env:env' [] term_pair_list)) (new_formula ~env:env' [] term_pair_list))
(fold_protocol env p_l p_r) in (fold_protocol env p_l p_r) in
...@@ -135,7 +138,7 @@ let init_cca_constraints key_pairs = ...@@ -135,7 +138,7 @@ let init_cca_constraints key_pairs =
encryptions = []; encryptions = [];
decryptions = [] };; decryptions = [] };;
let test_cca_case cca_fun_name cca_fun cca_constraints let test_cca_case env cca_fun_name cca_fun cca_constraints
left_term right_term axiom_res = left_term right_term axiom_res =
let expect_success = match axiom_res with let expect_success = match axiom_res with
| Success _ -> true | Success _ -> true
...@@ -146,11 +149,12 @@ let test_cca_case cca_fun_name cca_fun cca_constraints ...@@ -146,11 +149,12 @@ let test_cca_case cca_fun_name cca_fun cca_constraints
Printf.eprintf "%s (should be Success)\n%!" s Printf.eprintf "%s (should be Success)\n%!" s
else else
Printf.eprintf "%s (should be Failure)\n%!" s) in Printf.eprintf "%s (should be Failure)\n%!" s) in
debug (fun () -> debug (fun () ->
Printf.eprintf "\nTesting %s call:\n" cca_fun_name; Printf.eprintf "\nTesting %s call:\n" cca_fun_name;
Term.print_term_stderr left_term; Term.print_term_stderr env left_term;
Printf.eprintf "\n ~ \n"; Printf.eprintf "\n ~ \n";
Term.print_term_stderr right_term;); Term.print_term_stderr env right_term;);
match cca_fun env cca_constraints left_term right_term with match cca_fun env cca_constraints left_term right_term with
| exception (Case_fail hint) -> | exception (Case_fail hint) ->
...@@ -165,10 +169,10 @@ let test_cca_case cca_fun_name cca_fun cca_constraints ...@@ -165,10 +169,10 @@ let test_cca_case cca_fun_name cca_fun cca_constraints
| const -> print_result "\nCCA2 Success"; assert (expect_success);; | const -> print_result "\nCCA2 Success"; assert (expect_success);;
let test_dec_oracle_call = let test_dec_oracle_call =
fun x -> test_cca_case "decryption oracle" Cca.dec_oracle_call_case x fun x -> test_cca_case env "decryption oracle" Cca.dec_oracle_call_case x
let test_enc_oracle_call = let test_enc_oracle_call =
fun x -> test_cca_case "encryption oracle" Cca.enc_oracle_call_case x fun x -> test_cca_case env "encryption oracle" Cca.enc_oracle_call_case x
let unit_test_decryption_oracle = fun () -> let unit_test_decryption_oracle = fun () ->
(* 0: Simple decryptions (Success). *) (* 0: Simple decryptions (Success). *)
......
This diff is collapsed.
...@@ -68,10 +68,10 @@ val inject : abstract process -> concrete process ...@@ -68,10 +68,10 @@ val inject : abstract process -> concrete process
(* Process Pretty Printers *) (* Process Pretty Printers *)
(***************************) (***************************)
val print_concrete_process : Format.formatter -> concrete process -> unit val print_concrete_process : env -> Format.formatter -> concrete process -> unit
val print_abstract_process : string -> Format.formatter -> abstract process val print_abstract_process : env -> string -> Format.formatter ->
-> unit abstract process -> unit
val print_process_decl : Format.formatter -> declaration -> unit val print_process_decl : Format.formatter -> declaration -> unit
...@@ -88,5 +88,5 @@ val add_declarations : declaration list -> unit ...@@ -88,5 +88,5 @@ val add_declarations : declaration list -> unit
(********************) (********************)
val fold_protocol : val fold_protocol :
environment -> concrete process -> concrete process -> env -> concrete process -> concrete process ->
((msg term * msg term) list * environment) list ((msg term * msg term) list * env) list
...@@ -47,8 +47,8 @@ let rule_to_string r = match r with ...@@ -47,8 +47,8 @@ let rule_to_string r = match r with
| Cond_fresh (side,_) -> | Cond_fresh (side,_) ->
Printf.sprintf "Cond_fresh %s" (side_to_string side) Printf.sprintf "Cond_fresh %s" (side_to_string side)
let print_rule_long : Format.formatter -> rule -> unit = let print_rule_long : env -> Format.formatter -> rule -> unit =
fun ppf r -> fun env ppf r ->
let open Fmt in let open Fmt in
match r with match r with
| Normalize | Normalize
...@@ -61,27 +61,27 @@ let print_rule_long : Format.formatter -> rule -> unit = ...@@ -61,27 +61,27 @@ let print_rule_long : Format.formatter -> rule -> unit =
| If_intro (u,v) -> | If_intro (u,v) ->
pf ppf "%s @[<hv 3>%a ->@, %a@]" pf ppf "%s @[<hv 3>%a ->@, %a@]"
(rule_to_string r) (rule_to_string r)
print_term u (print_term env) u
print_term v (print_term env) v
| IFT (_,u,v,encs) -> | IFT (_,u,v,encs) ->
pf ppf "%s @[<hv 3>%a ->@, %a@;Encs:@[<v 1>%a@]@]" pf ppf "%s @[<hv 3>%a ->@, %a@;Encs:@[<v 1>%a@]@]"
(rule_to_string r) (rule_to_string r)
print_term u (print_term env) u
print_term v (print_term env) v
(list ~sep:(fun ppf () -> pf ppf "@;") print_term) encs (list ~sep:(fun ppf () -> pf ppf "@;") (print_term env)) encs
| R (_,u,v,encs) -> | R (_,u,v,encs) ->
pf ppf "%s @[<hv 3>%a ->@, %a@;Encs:@[<v 1>%a@]@]" pf ppf "%s @[<hv 3>%a ->@, %a@;Encs:@[<v 1>%a@]@]"
(rule_to_string r) (rule_to_string r)
print_term u (print_term env) u
print_term v (print_term env) v
(list ~sep:(fun ppf () -> pf ppf "@;") print_term) encs (list ~sep:(fun ppf () -> pf ppf "@;") (print_term env)) encs
| Cond_fresh (side,b) -> | Cond_fresh (side,b) ->
pf ppf "%s Cond_fresh %a" pf ppf "%s Cond_fresh %a"
(side_to_string side) (side_to_string side)
print_term b (print_term env) b
(* new_formula_element ancestor term_pair : Create a new formula element for (* new_formula_element ancestor term_pair : Create a new formula element for
term_pair, inheriting some attributes from ancestor. *) term_pair, inheriting some attributes from ancestor. *)
...@@ -171,7 +171,7 @@ let fab_apply env t t' = match t.content,t'.content with ...@@ -171,7 +171,7 @@ let fab_apply env t t' = match t.content,t'.content with
(* rewrite env u v term encs : Rewrite all occurances of u into v in term, (* rewrite env u v term encs : Rewrite all occurances of u into v in term,
except in encs. Remark : if a conditional is equal to EQ(u,v) (or EQ(v,u)) except in encs. Remark : if a conditional is equal to EQ(u,v) (or EQ(v,u))
then the IfThenElse is simplified by keeping only the then branch. *) then the IfThenElse is simplified by keeping only the then branch. *)
let rewrite : type a b. environment -> a term -> a term -> b term let rewrite : type a b. env -> a term -> a term -> b term
-> msg term list -> b term = -> msg term list -> b term =
fun env u v term encs -> fun env u v term encs ->
...@@ -180,13 +180,13 @@ let rewrite : type a b. environment -> a term -> a term -> b term ...@@ -180,13 +180,13 @@ let rewrite : type a b. environment -> a term -> a term -> b term
| Msg, Msg -> | Msg, Msg ->
if List.exists (fun x -> r_equal env x m) encs then if List.exists (fun x -> r_equal env x m) encs then
m m
else if syntactic_equal env m u then else if t_equal m u then
v v
else else
aux_rec m aux_rec m
| Bool, Bool -> | Bool, Bool ->
if syntactic_equal env m u then if t_equal m u then
v v
else else
aux_rec m aux_rec m
...@@ -205,8 +205,8 @@ let rewrite : type a b. environment -> a term -> a term -> b term ...@@ -205,8 +205,8 @@ let rewrite : type a b. environment -> a term -> a term -> b term
begin begin
match get_sort u with match get_sort u with
| Msg -> | Msg ->
if (syntactic_equal env (t_eq u v) m) if (t_equal (t_eq u v) m)
|| (syntactic_equal env (t_eq v u) m) then || (t_equal (t_eq v u) m) then
t_true () t_true ()
else else
t_eq (aux bl) (aux br) t_eq (aux bl) (aux br)
...@@ -235,7 +235,7 @@ let ift_apply env u v t encs = ...@@ -235,7 +235,7 @@ let ift_apply env u v t encs =
| Name (_,Msg) -> rewrite env u v t encs | Name (_,Msg) -> rewrite env u v t encs
| Fun ("enc",l) -> | Fun ("enc",l) ->
if List.exists (fun x -> syntactic_equal env x t) encs then if List.exists (fun x -> t_equal x t) encs then
t t
else else
t_fun "enc" (List.map down l) t_fun "enc" (List.map down l)
...@@ -250,10 +250,10 @@ let ift_apply env u v t encs = ...@@ -250,10 +250,10 @@ let ift_apply env u v t encs =
- if this is not the case we recurse in both branches *and* the - if this is not the case we recurse in both branches *and* the
conditional b (which is then expanded only if the recursive call conditional b (which is then expanded only if the recursive call
produce something else than b) *) produce something else than b) *)
if syntactic_equal env (t_eq u v) b then if t_equal (t_eq u v) b then
t_ite b (rewrite env u v tl encs) (down tr) t_ite b (rewrite env u v tl encs) (down tr)
else if syntactic_equal env (t_eq v u) b then else if t_equal (t_eq v u) b then
t_ite b (rewrite env u v tl encs) (down tr) t_ite b (rewrite env u v tl encs) (down tr)
else else
...@@ -295,7 +295,7 @@ let b_normalize_apply env b b' = ...@@ -295,7 +295,7 @@ let b_normalize_apply env b b' =
bt_combine [pseudo_normalize env b, pseudo_normalize env b'] [] bt_combine [pseudo_normalize env b, pseudo_normalize env b'] []
let r_apply : type a b. environment -> a term -> a term -> side -> b term let r_apply : type a b. env -> a term -> a term -> side -> b term
-> b term -> msg term list -> term_pair list =