Commit ab05ae6d authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

proper english, maybe

parent 6d2c226d
......@@ -172,7 +172,7 @@ let name_alpha_equal : type a.
if they are not alpha-equal, and new_constraints if they are alpha-equal
under new_constraints (which extend alpha_const). *)
let rec alpha_rename :
type a. environement -> alpha_const -> a term -> a term -> alpha_const =
type a. environment -> alpha_const -> a term -> a term -> alpha_const =
fun env alpha_const t t' ->
match (eiv env t), (eiv env t') with
| Bot,Bot -> alpha_const
......@@ -256,7 +256,7 @@ let check_name_constraints side cca_constraints s =
keys except in dec(_,sk(.)) or pk(.), and that occurrences of the encryption
randomness appear with the corresponding message and encryption key. *)
let rec dec_pk_fresh :
type a. environement -> side -> cca_constraints -> a term -> unit =
type a. environment -> side -> cca_constraints -> a term -> unit =
fun env side cca_constraints t -> match eiv_i env t 3 with
| Bot -> ()
| True -> ()
......@@ -325,7 +325,7 @@ let rec dec_pk_fresh :
(* enc_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid encryption oracle call. Raise Case_fail (hint) if this fails. *)
let enc_oracle_call_case : type a. environement -> cca_constraints
let enc_oracle_call_case : type a. environment -> cca_constraints
-> a term -> a term -> cca_constraints =
fun env cca_constraints t t' ->
match eiv_i env t 3, eiv_i env t' 3 with
......@@ -356,10 +356,10 @@ let enc_oracle_call_case : type a. environement -> cca_constraints
(*********************************)
(* constant_term env cca_constraints d side : Return iff the term d is a
constant term in environement env, under constraints cca_constraints. For
constant term in environment env, under constraints cca_constraints. For
this, we need to check that there are no decryption using the cca keys, and
no encryptions. *)
let rec constant_term : type a. environement -> cca_constraints
let rec constant_term : type a. environment -> cca_constraints
-> side -> a term -> unit =
fun env cca_constraints side d ->
match eiv_i env d 3 with
......@@ -410,7 +410,7 @@ let rec constant_term : type a. environement -> cca_constraints
(* symmetrical_part_case env cca_constraints t t': Check whether t \sim t'
is a valid symmetric case under environement env and constraints
is a valid symmetric case under environment env and constraints
cca_constraints. *)
let symmetrical_part_case env cca_constraints t t' =
constant_term env cca_constraints Left t;
......@@ -432,9 +432,9 @@ let symmetrical_part_case env cca_constraints t t' =
(********************************)
(* subterm_encryptions enc t n: Return the list of encryptions under key sk(n)
appearing in the term t, in the environement env. *)
appearing in the term t, in the environment env. *)
let subterm_encryptions :
type a. environement -> a term -> name_string -> msg term list =
type a. environment -> a term -> name_string -> msg term list =
fun env t n->
let rec aux : type a. msg term list -> a term -> msg term list =
......@@ -764,7 +764,7 @@ and shape_check env cca_constraints t t' =
(* dec_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid decryption oracle call. *)
and dec_oracle_call_case
: type a. environement -> cca_constraints
: type a. environment -> cca_constraints
-> a term -> a term -> cca_constraints =
fun env cca_constraints t t' -> match get_sort t, get_sort t' with
| Msg,Msg ->
......@@ -861,7 +861,7 @@ let equal_up_to_oracle_calls_strict env cca_constraints t t' =
Remark: ((c,c'),constraints) should be the result of a call to build_context
on terms s and s'. *)
let rec dec_pairs_from_terms
:type a. environement -> cca_constraints -> a term -> a term -> a term
:type a. environment -> cca_constraints -> a term -> a term -> a term
-> a term -> (msg term * msg term) list -> (msg term * msg term) list
= fun env constraints c c' s s' acc ->
match eiv_i env c 3,
......@@ -922,7 +922,7 @@ let rec dec_pairs_from_terms
failwith "dec_pairs_from_terms: bad call, contexts do not match"
and dec_pairs_from_terms_fun
:type a. environement -> cca_constraints -> a term -> a term -> a term
:type a. environment -> cca_constraints -> a term -> a term -> a term
-> a term -> (msg term * msg term) list -> (msg term * msg term) list =
fun env constraints c c' s s' acc ->
......@@ -1011,7 +1011,7 @@ let extend_cca_dec_case env constraints t t' =
(**************)
(* get_keys acc env t : Return the set of keys appearing in t @ acc. *)
let rec get_keys : type a. name_string list -> environement -> a term
let rec get_keys : type a. name_string list -> environment -> a term
-> name_string list = fun acc env t ->
match eiv_i env t 2 with
| False -> acc
......
......@@ -50,42 +50,42 @@ exception Alpha_conflict of
exception Shape_no_match
(* Raises Shape_no_match if the terms are not alpha-equal. *)
val alpha_rename : environement -> alpha_const -> 'a term -> 'a term
val alpha_rename : environment -> alpha_const -> 'a term -> 'a term
-> alpha_const
(* subterm_encryptions enc t n: Return the list of encryptions under key sk(n)
appearing in the term t, in the environement env. *)
appearing in the term t, in the environment env. *)
val subterm_encryptions :
environement -> 'a term -> name_string -> msg term list
environment -> 'a term -> name_string -> msg term list
exception Case_fail of cca axiom_hint
(* Return the message and the key used in a decryption oracle call.
Return None if the shape of the term is wrong. *)
val get_m_dec_oracle : environement -> msg term
val get_m_dec_oracle : environment -> msg term
-> (msg term * name_string) option
(* enc_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid encryption oracle call. *)
val enc_oracle_call_case : environement -> cca_constraints
val enc_oracle_call_case : environment -> cca_constraints
-> 'a term -> 'a term -> cca_constraints
exception Contexts_do_not_exist
(* 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. *)
val equal_up_to_oracle_calls : environement -> cca_constraints -> msg term
val equal_up_to_oracle_calls : environment -> cca_constraints -> msg term
-> msg term -> bool
(* 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
contain secret key material. *)
val equal_up_to_oracle_calls_strict : environement -> cca_constraints -> msg term
val equal_up_to_oracle_calls_strict : environment -> cca_constraints -> msg term
-> msg term -> bool
(* dec_oracle_call_case env cca_constraints t t' : Check whether t \sim t'
is a valid decryption oracle call. *)
val dec_oracle_call_case : environement -> cca_constraints
val dec_oracle_call_case : environment -> cca_constraints
-> 'a term -> 'a term -> cca_constraints
......@@ -106,5 +106,5 @@ type extend_cca_result =
calls but should be guarded) when trying to show that t \sim t' is a valid
dec. oracle call. *)
val extend_cca_dec_case :
environement -> cca_constraints -> msg term -> msg term ->
environment -> cca_constraints -> msg term -> msg term ->
extend_cca_result * cca_constraints
......@@ -16,7 +16,7 @@ type formula_element =
type formula =
{ formula_element_list : formula_element list;
env : environement }
env : environment }
(*****************)
......
......@@ -13,7 +13,7 @@ type formula_element =
type formula =
{ formula_element_list : formula_element list;
env : environement }
env : environment }
exception F_out_of_bound of int
exception F_bad_argument of int
......@@ -34,7 +34,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
the element of l and term elements are the elements of l'. A type checking
is perfomed before creating the formula *)
val new_formula : ?env:environement -> (boole term * boole term) list
val new_formula : ?env:environment -> (boole term * boole term) list
-> (msg term * msg term) list -> formula
(* c_bind formula new_f: Return a new formula where the formula elements
......
......@@ -109,7 +109,7 @@ let main_interactive () =
(* Some unitary tests *)
(**********************)
(* Create and set-up a dummy state and environement for testing. *)
(* Create and set-up a dummy state and environment for testing. *)
let test_state = dummy_interactive_state ();;
let env = test_state.c_proof.goal.env;;
......
......@@ -395,12 +395,12 @@ type guarded_process = guard * concrete process
type configuration =
{ procs : guarded_process list;
env : environement;
env : environment;
map_fresh : int String_map.t }
(* Apply the internal reduction rules to all process as much as possible.
Notice that when a let binding is encountered, a new binding is added to
the environement. *)
the environment. *)
let ireduce conf side =
let rec aux_ireduce reduced_gp_list env map_fresh acc_gp_list =
......@@ -902,7 +902,7 @@ type f_conf_side =
type f_conf =
{ left_c : f_conf_side;
right_c : f_conf_side;
f_env : environement;
f_env : environment;
f_map_fresh : int String_map.t }
......@@ -928,7 +928,7 @@ let sorted_conf f_conf_side env map_fresh =
map_fresh = map_fresh }
(* apply_action action side f_conf: Apply 'action' to 'f_conf' in the
environement 'env', and return the new f_conf. *)
environment 'env', and return the new f_conf. *)
let apply_action action side f_conf =
let f_conf_side = match side with
| Left -> f_conf.left_c
......@@ -991,7 +991,7 @@ let apply_action action side f_conf =
let norm_outputed_term =
weak_normalize red_new_conf.env outputed_term in
(* We define the new frame variable phi', and bind it in the environement. *)
(* We define the new frame variable phi', and bind it in the environment. *)
let i = List.length frame
and env = red_new_conf.env
and map_fresh = red_new_conf.map_fresh in
......
......@@ -88,5 +88,5 @@ val add_declarations : declaration list -> unit
(********************)
val fold_protocol :
environement -> concrete process -> concrete process ->
((msg term * msg term) list * environement) list
environment -> concrete process -> concrete process ->
((msg term * msg term) list * environment) list
......@@ -195,7 +195,7 @@ let fab_apply env t t' =
(* 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))
then the IfThenElse is simplified by keeping only the then branch. *)
let rewrite : type a b. environement -> a term -> a term -> b term
let rewrite : type a b. environment -> a term -> a term -> b term
-> msg term list -> b term =
fun env u v term encs ->
......@@ -332,7 +332,7 @@ let b_normalize_apply env b b' =
bt_combine [pseudo_normalize env b, pseudo_normalize env b'] []
let r_apply : type a b. environement -> a term -> a term -> side -> b term
let r_apply : type a b. environment -> a term -> a term -> side -> b term
-> b term -> msg term list -> term_pair list =
fun env t t' side u v encs ->
if r_equal env u v then
......@@ -534,7 +534,7 @@ let cs_deep_apply r formula =
b into False. Moreover, if such occurrences are branching conditional then
rewrite the If application into its else branch. *)
let rec rewrite_cond_false
: type a. environement -> boole term -> a term -> a term =
: type a. environment -> boole term -> a term -> a term =
fun env b s ->
ein env s (fun t -> match t with
| Bot -> t
......
......@@ -30,7 +30,7 @@ val print_rule_long : Format.formatter -> rule -> unit
(* 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))
then the IfThenElse is simplified by keeping only the then branch. *)
val rewrite : environement -> 'a term -> 'a term -> 'b term ->
val rewrite : environment -> 'a term -> 'a term -> 'b term ->
msg term list -> 'b term
(*********************)
......
This diff is collapsed.
......@@ -57,7 +57,7 @@ type string_type =
| TName (* Name of sort term *)
| BTName (* Name of sort bool *)
type environement =
type environment =
{ t_bindings : (variable_string, msg term) Hashtbl.t;
bt_bindings : (variable_string, boole term) Hashtbl.t;
hide_bindings : (variable_string, bool) Hashtbl.t;
......@@ -72,56 +72,56 @@ exception Not_type_checking of string
val string_type_to_string : string_type -> string
(* Return an initial environement, with the basic function symbols' sort
(* Return an initial environment, with the basic function symbols' sort
defined. *)
val init_env : unit -> environement
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 : environement -> variable_string -> unit
val hide_binding : environment -> variable_string -> unit
val hide_all_bindings : environement -> unit
val hide_all_bindings : environment -> unit
(* reveal_binding formula s: Reveal the binding associated with s in formula. *)
val reveal_binding : environement -> variable_string -> unit
val reveal_binding : environment -> variable_string -> unit
val reveal_all_bindings : environement -> unit
val reveal_all_bindings : environment -> unit
val copy_env : environement -> environement
val copy_env : environment -> environment
val term_size : environement -> 'a term -> int
val term_size : environment -> 'a term -> int
(*******************)
(* Variable typing *)
(*******************)
(* Variable typing:
- the environement is modified in-place if type-checking succeed.
- the environment is modified in-place if type-checking succeed.
- if the type-checking fails, no modifications are done. *)
(* Return true iff s is binded in the environement. *)
val is_binded : environement -> string -> bool
(* Return true iff s is binded in the environment. *)
val is_binded : environment -> string -> bool
(* fresh_name env pre : Return a string s such that pre is a preffix of s, and
s is fresh in env. *)
val fresh_name : environement -> string -> string
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 : environement -> string -> string_type -> unit
val bind_type : environment -> string -> string_type -> unit
(* 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 : environement -> string -> string_type -> unit
val bind_new_type : environment -> string -> string_type -> unit
(* type_check env t: Type-checks the term t in env. Update the environement env
(* type_check env t: Type-checks the term t in env. Update the environment env
if the type checking is successful. *)
val type_check : environement -> 'a term -> unit
val type_check : environment -> 'a term -> unit
(* type_check_all env l_term b_term: Type-checks all elements in l_term and
b_term in the environement env. *)
val type_check_all : environement -> msg term list -> boole term list -> unit
b_term in the environment env. *)
val type_check_all : environment -> msg term list -> boole term list -> unit
(**********************)
......@@ -131,35 +131,35 @@ val type_check_all : environement -> msg term list -> boole term list -> unit
exception Unexpandable of string
(* expand_var env t s: Expand in t every occurrence of the variable s into its
value in the environement env. *)
val expand_var : environement -> 'a term -> variable_string -> 'a term
value in the environment env. *)
val expand_var : environment -> 'a term -> variable_string -> 'a term
(* expand_all env t: Expand the term t in the environement env. *)
val expand_all : environement -> 'a term -> '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
environement env. Raise an Unexpandable (err_msg) if the variable
environment env. Raise an Unexpandable (err_msg) if the variable
cannot be expanded. *)
val eiv : environement -> 'a term -> 'a term
val eiv : environment -> 'a term -> 'a term
(* Like eiv, but i steps. *)
val eiv_i : environement -> 'a term -> int -> 'a term
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 environement env before applying f. If f is the identity on the
in the environment env before applying f. If f is the identity on the
expanded term then return the unexpanded variable. *)
val ein :
environement -> 'a term -> ('a term -> 'a term) -> 'a term
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.
Warning: Bot is ignored and treaded as a Name *)
val get_head : environement -> msg term -> function_symbol_string option
val get_head : environment -> msg term -> function_symbol_string option
(* Replace a variable by a name if it is binded in the environement. This is
(* Replace a variable by a name if it is binded in the environment. This is
used after parsing a term, to disambiguate between variable and names.
Raise No_such_binding is a binding does not exist. *)
val set_binded_names : environement -> 'a term -> 'a term
val set_binded_names : environment -> 'a term -> 'a term
(***********************)
(* Variable Collection *)
......@@ -168,8 +168,8 @@ val set_binded_names : environement -> 'a term -> 'a term
(* collect_var t s t': Collect in t all subterms t' into a term variable s. *)
val collect_var : 'a term -> variable_string -> 'b term -> 'a term
(* collect_all env t: Collect in t all bindings in the environement env. *)
val collect_all : environement -> 'a term -> 'a term
(* collect_all env t: Collect in t all bindings in the environment env. *)
val collect_all : environment -> 'a term -> 'a term
(*************************)
......@@ -182,30 +182,30 @@ exception Bad_binding of string_type * string_type
(* 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. *)
val env_add_binding : environement -> variable_string -> 'a term -> environement
val env_add_binding : environment -> variable_string -> 'a term -> environment
(************************************************)
(* Syntactic Equality modulo Variable Expantion *)
(************************************************)
(* Syntactic equality modulo the environement. *)
val syntactic_equal : environement -> 'a term -> 'a term -> bool
(* Syntactic equality modulo the environment. *)
val syntactic_equal : environment -> 'a term -> 'a term -> bool
(* R-equality modulo the environement. *)
val r_equal : environement -> 'a term -> 'a term -> bool
(* R-equality modulo the environment. *)
val r_equal : environment -> 'a term -> 'a term -> bool
(*********************)
(* Term Substitution *)
(*********************)
(* var_subst s u t: Replace Var s by u in t: t[u/s].
Be careful, this does not apply the substitution in the environement!
Be careful, this does not apply the substitution in the environment!
No type-checking is done. *)
val var_subst : variable_string -> msg term -> 'a term -> 'a term
(* var_bsubst s bu t: Replace Var s by bu in t: t[bu/s].
Be careful, this does not apply the substitution in the environement!
Be careful, this does not apply the substitution in the environment!
No type-checking is done.*)
val var_bsubst : variable_string -> boole term -> 'a term -> 'a term
......@@ -215,17 +215,17 @@ val var_bsubst : variable_string -> boole term -> 'a term -> 'a term
(********************)
(* subterm env s t : Return true iff s is a subterm of t in env *)
val subterm : environement -> 'a term -> 'b term -> bool
val subterm : environment -> 'a term -> 'b term -> bool
(* all_subterms env a sort f : Return every subterms x of a of sort 'sort' such
that f x holds and g y does not hold for every ancestor y of x (including x).
Can contain duplicates. *)
val all_subterms : environement -> 'a term -> 'b sort -> ('b term -> bool)
val all_subterms : environment -> 'a term -> 'b sort -> ('b term -> bool)
-> ('b term -> bool) -> 'b term list
(* constrained_subterm env s t t_list : Return true iff s is a subterm of t, but
not in a term of t_list. *)
val const_subterm : environement -> msg term -> msg term -> msg term list
val const_subterm : environment -> msg term -> msg term -> msg term list
-> bool
(**********************)
......@@ -233,15 +233,15 @@ val const_subterm : environement -> msg term -> msg term -> msg term list
(**********************)
(* Eliminate all syntactic duplicate on the same branches. *)
val duplicate_cond_elim : environement -> 'a term -> 'a term
val duplicate_cond_elim : environment -> 'a term -> 'a term
(* Reduce all redexes of the form If(b, v, v). Variables are not expanded. *)
val same_elim : environement -> 'a term -> 'a term
val same_elim : environment -> 'a term -> 'a term
(* Remove proj/pair and dec/enc redexes, multiple occurrences of the same
conditional on a branch, and simplify if-same redexes. *)
val weak_normalize : environement -> 'a term -> 'a term
val weak_normalize : environment -> 'a term -> 'a term
(* pseudo_normalize env t : Return a pseudo-normalisation of t (i.e. a R-normal
for a arbitrary total ordering on R-normal if-free conditionals.). *)
val pseudo_normalize : environement -> 'a term -> 'a term
val pseudo_normalize : environment -> 'a term -> 'a term
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