Commit 26a7a9f7 authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

removed Bot

parent 023cb64e
Pipeline #1650 passed with stage
in 2 minutes and 38 seconds
......@@ -175,7 +175,6 @@ let rec alpha_rename :
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
| True,True -> alpha_const
| False,False -> alpha_const
......@@ -258,7 +257,6 @@ let check_name_constraints side cca_constraints s =
let rec dec_pk_fresh :
type a. environment -> side -> cca_constraints -> a term -> unit =
fun env side cca_constraints t -> match eiv_i env t 3 with
| Bot -> ()
| True -> ()
| False -> ()
| Name (_,Bool) -> ()
......@@ -365,7 +363,6 @@ let rec constant_term : type a. environment -> cca_constraints
match eiv_i env d 3 with
| True -> ()
| False -> ()
| Bot -> ()
| Name (s,_) ->
check_name_constraints side cca_constraints s
......@@ -447,8 +444,7 @@ let subterm_encryptions :
| Var _ -> assert false
| Name _ -> acc
| True -> acc
| False -> acc
| Bot -> acc in
| False -> acc in
List.sort_uniq Pervasives.compare (aux [] t)
......@@ -636,7 +632,6 @@ let rec build_context env cca_constraints (t : msg term) (t' : msg term) =
and build_ctxt : type a. a term -> a term -> (a term * a term) =
fun t t' -> match eiv env t, eiv env t' with
| Bot, Bot -> (t,t')
| Name _, Name _ -> (t,t')
| Fun ("enc",[x;r;m_pk]), Fun ("enc",[x';r';m_pk']) ->
......@@ -869,8 +864,6 @@ let rec dec_pairs_from_terms
eiv_i env s 3,
eiv_i env s' 3 with
| Bot, Bot, _, _ -> acc
| Name _, Name _, _, _ -> acc
| Fun ("enc",[_;_;_]), Fun ("enc",[_;_;_]), _, _ ->
......@@ -1016,7 +1009,6 @@ let rec get_keys : type a. name_string list -> environment -> a term
match eiv_i env t 2 with
| False -> acc
| True -> acc
| Bot -> acc
| Name _ -> acc
| Fun ("pk",[Name (r,Msg)]) -> r :: acc
......
......@@ -362,7 +362,6 @@ let auto_ift state =
and term_auto_ift_msg side alg_list acc t =
match eiv env t with
| Bot -> term_auto_ift side alg_list acc
| Name _ -> term_auto_ift side alg_list acc
| Var _ -> assert (false)
......@@ -1527,37 +1526,6 @@ add_new_action
raise (Term_badly_formed error_message)));;
add_new_action
"cs"
(fun ppf () -> Fmt.pf ppf "%a %a %a"
pr_name "cs"
pr_term "b"
pr_term "b'")
(fun ppf () ->
Fmt.pf ppf "deep Case Study on conditionals %a,%a"
pr_term "b" pr_term "b'")
default_exn_handler
(fun y state ->
match parse_b_terms state y with
| [b_u;b_v] ->
let rule = CS_deep (b_u,b_v) in
let (l_prem, r_prem) = cs_deep_apply rule state.c_proof.goal in
binary_aux state rule l_prem r_prem;
| l ->
let error_message =
Printf.sprintf
"Wanted to parse 2 boolean terms and got %d"
(List.length l) in
raise (Term_badly_formed error_message)
);;
(***************************)
(* Binding Related Actions *)
......
......@@ -13,7 +13,7 @@ type rule =
| R : side * 'a term * 'a term * msg term list -> rule
| If_intro of boole term * boole term
| CS of boole term * boole term
| CS_deep of boole term * boole term
| Cond_fresh of side * boole term
exception Bad_rule of string * rule
......@@ -35,7 +35,6 @@ let rule_to_string r = match r with
| FAb -> "FAb"
| If_intro _ -> "If_intro"
| CS _ -> "CS"
| CS_deep _ -> "CS_deep"
| IFT (side,_,_,_) ->
Printf.sprintf "IFT on the %s" (side_to_string side)
......@@ -59,8 +58,7 @@ let print_rule_long : Format.formatter -> rule -> unit =
| FAb -> pf ppf "%s" (rule_to_string r)
| CS (u,v)
| If_intro (u,v)
| CS_deep (u,v) ->
| If_intro (u,v) ->
pf ppf "%s @[<hv 3>%a ->@, %a@]"
(rule_to_string r)
print_term u
......@@ -99,8 +97,6 @@ let new_formula_element ancestor term_pair =
(* Auxilliary functions used by fa_apply *)
let rec fa_get_s env (t : msg term) = match t with
| Bot -> (true, None)
| Name (_,Msg) -> (false, None)
| Var (s,Msg) ->
......@@ -144,12 +140,6 @@ let fa_apply env t t' =
| Var (s,Msg) ->
fa_aux (s_leave,i_leave) (eiv env t)
| Bot ->
let rec f acc i = match i with
| 0 -> acc
| _ -> f (Bot :: acc) (i-1) in
f [] i_leave
| _ -> assert false in
match fa_get_s env t, fa_get_s env t' with
......@@ -222,7 +212,6 @@ let rewrite : type a b. environment -> a term -> a term -> b term
| Name _ -> m
| True -> m
| False -> m
| Bot -> m
| Var _ -> ein env m aux
| Fun (s,l) ->
......@@ -257,7 +246,7 @@ let rewrite : type a b. environment -> a term -> a term -> b term
let ift_apply env u v t encs =
let rec down t = match t with
| Name (_,Msg) | Bot -> rewrite env u v t encs
| Name (_,Msg) -> rewrite env u v t encs
| Var (_,Msg) -> ein env t down
| Fun ("enc",l) ->
......@@ -386,7 +375,7 @@ let rule_apply formula r (t, t') = match r with
| If_intro (b,b') ->
if_intro_apply formula.env t t' (b,b')
| CS _ | CS_deep _ | Duplicate | Cond_fresh _ ->
| CS _ | Duplicate | Cond_fresh _ ->
failwith
(Printf.sprintf "rule_apply: not a unary point-wise rule: %s"
(rule_to_string r))
......@@ -414,7 +403,7 @@ let rule_b_apply formula r (b,b') = match r with
| If_intro (b,b') ->
raise Rule_not_applicable
| CS _ | CS_deep _ | Duplicate | Cond_fresh _ ->
| CS _ | Duplicate | Cond_fresh _ ->
failwith
(Printf.sprintf "rule_apply: not a unary point-wise rule: %s"
(rule_to_string r))
......@@ -470,65 +459,6 @@ let cs_apply r formula =
| _ -> failwith "cs_apply bad rule argument"
(* cs_deep_apply r formula: apply the DeepCaseStudy axiom rule to all positions
of formula, and returns the left and right list of formula elements. *)
let cs_deep_apply r formula =
let rec deep_aux : type a. boole term -> bool -> a term -> a term =
fun b bool u ->
ein formula.env u (fun u -> match u with
| Bot -> u
| Name _ -> u
| Var _ -> u
| True -> u
| False -> u
| Fun (s,l) ->
Fun (s,List.map (deep_aux b bool) l)
| If (b_a,t1,t2) ->
if syntactic_equal formula.env b b_a then
if bool then
If (b_a, deep_aux b bool t1, Bot)
else
If (b_a, Bot, deep_aux b bool t2)
else
If ( deep_aux b bool b_a,
deep_aux b bool t1,
deep_aux b bool t2 )
| EQ (t1,t2) ->
EQ (deep_aux b bool t1, deep_aux b bool t2)) in
match r with
| CS_deep (rule_b, rule_b') ->
List.split (
( { term_pair = Formula.B (rule_b,rule_b');
hidden_status = false;
unitary_result = Unset },
{ term_pair = Formula.B (rule_b,rule_b');
hidden_status = false;
unitary_result = Unset } )
:: List.map
(fun x -> match x.term_pair with
| B (b1,b2) ->
( new_formula_element x (B ( deep_aux rule_b true b1,
deep_aux rule_b' true b2 )),
new_formula_element x (B ( deep_aux rule_b false b1,
deep_aux rule_b' false b2 )) )
| T (u1,u2) ->
( new_formula_element x (T ( deep_aux rule_b true u1,
deep_aux rule_b' true u2 )),
new_formula_element x (T ( deep_aux rule_b false u1,
deep_aux rule_b' false u2 )) ))
formula.formula_element_list)
| _ -> failwith "cs_deep_apply bad rule argument"
(* rewrite_cond_false env b s : Rewrite all occurrences of the conditional
b into False. Moreover, if such occurrences are branching conditional then
......@@ -537,7 +467,6 @@ let rec rewrite_cond_false
: type a. environment -> boole term -> a term -> a term =
fun env b s ->
ein env s (fun t -> match t with
| Bot -> t
| False -> t
| True -> t
| Name _ -> t
......@@ -635,4 +564,4 @@ let cond_fresh_apply r formula = match r with
(first_premise, second_premise, env')
| _ -> failwith "cs_deep_apply bad rule argument"
| _ -> failwith "cond_fresh bad rule argument"
......@@ -12,7 +12,6 @@ type rule =
| R : side * 'a term * 'a term * msg term list -> rule
| If_intro of boole term * boole term
| CS of boole term * boole term
| CS_deep of boole term * boole term
| Cond_fresh of side * boole term
exception Bad_rule of string * rule
......@@ -46,11 +45,6 @@ val unary_apply : formula -> rule -> int -> formula
val cs_apply :
rule -> formula -> formula_element list * formula_element list
(* cs_deep_apply r formula: apply the DeepCaseStudy axiom rule to all positions
of formula, and returns the left and right list of formula elements. *)
val cs_deep_apply :
rule -> formula -> formula_element list * formula_element list
exception Bad_cond_fresh
val cond_fresh_apply :
......
......@@ -9,7 +9,6 @@ type _ sort = | Msg : msg sort
| Bool : boole sort
type _ term =
| Bot : msg term
| True : boole term
| False : boole term
| Name : name_string * 'a sort -> 'a term
......@@ -46,7 +45,6 @@ and cst a = Fun(a,[])
let get_sort : type a. a term -> a sort =
fun t -> match t with
| Bot -> Msg
| Var (_,Msg) -> Msg
| Name (_,Msg) -> Msg
| If _ -> Msg
......@@ -65,7 +63,6 @@ let term_free_variables t =
let rec aux : type a. (string list * string list) ->
a term -> (variable_string list * variable_string list) =
fun (acc,b_acc) t -> match t with
| Bot -> (acc,b_acc)
| Name _ -> (acc,b_acc)
| True -> (acc,b_acc)
| False -> (acc,b_acc)
......@@ -135,8 +132,6 @@ let rec print_term : type a. Format.formatter -> a term -> unit =
(kw `Red) "else"
print_term_else_branch v
| Bot -> (styled `Green (styled `Bold ident)) ppf "Bot"
| True -> (kw `Green) ppf "true"
| False -> (kw `Green) ppf "false"
......@@ -461,7 +456,6 @@ let bind_new_type env s mtype =
(* Type checks t using (ht,ht') *)
let rec type_check : type a. a term -> environment -> environment =
fun t env -> match t with
| Bot -> env
| True -> env
| False -> env
| Name (s,Msg) -> bind_type env s TName
......@@ -503,7 +497,6 @@ exception Unexpandable of string
let rec expand_var :
type a. environment -> a term -> variable_string -> a term =
fun env t s -> match t with
| Bot -> t
| True -> t
| False -> t
| Name _ -> t
......@@ -553,7 +546,6 @@ let rec eiv_i : type a. environment -> a term -> int -> a term =
| _ -> match eiv env t with
| True -> t
| False -> t
| Bot -> t
| Name _ -> t
| Fun (s, l) ->
......@@ -590,7 +582,6 @@ let ein env t f = match t with
(* expand_all env t: Expand the term t in the environment env. *)
let rec expand_all : type a. environment -> a term -> a term =
fun env t -> match t with
| Bot -> t
| Name _ -> t
| True -> t
| False -> t
......@@ -660,7 +651,6 @@ let rec get_head env term = match eiv env term with
Raise No_such_binding is a binding does not exist. *)
let rec set_binded_names : type a. environment -> a term -> a term =
fun env term -> match term with
| Bot -> term
| True -> term
| False -> term
| Name _ -> term
......@@ -707,7 +697,6 @@ let rec term_size : type a. environment -> a term -> int = fun env t ->
match eiv env t with
| True -> 1
| False -> 1
| Bot -> 1
| Name _ -> 1
| Var _ -> assert (false)
| EQ (u, v) -> 1 + (term_size env u) + (term_size env v)
......@@ -732,7 +721,6 @@ type a. environment -> t_bt_pair list -> a term -> a term -> bool =
match eiv env t, eiv env t' with
| Var _, _ -> assert false
| _, Var _ -> assert false
| Bot, Bot -> se env acc
| True, True -> se env acc
| False, False -> se env acc
| Name (s,x), Name (s',x') -> (s = s') && (x = x') && (se env acc)
......@@ -790,7 +778,6 @@ let collect_var_msg : type a. a term -> variable_string -> msg term -> a term =
let rec aux : type a. a term -> a term = fun t ->
match t with
| Bot -> t
| Name _ -> t
| Var _ -> t
| Fun (f_name,l) -> Fun (f_name,List.map aux_msg l)
......@@ -815,7 +802,6 @@ let collect_var_boole : type a. a term -> variable_string -> boole term -> a ter
fun t s b' ->
let rec aux : type a. a term -> a term = fun t -> match t with
| Bot -> t
| Name _ -> t
| Var _ -> t
| True -> t
......@@ -856,7 +842,6 @@ let collect_all env t =
let rec term_dependencies : type a. a term -> alg_sort list
-> alg_sort list = fun t acc -> match t with
| Bot -> acc
| Name _ -> acc
| True -> acc
| False -> acc
......@@ -1011,7 +996,6 @@ let env_remove_binding env s =
No type-checking is done. *)
let rec var_subst : type a. variable_string -> msg term -> a term -> a term =
fun s u t -> match t with
| Bot -> t
| True -> t
| False -> t
......@@ -1036,7 +1020,6 @@ let rec var_subst : type a. variable_string -> msg term -> a term -> a term =
let rec var_bsubst :
type a. variable_string -> boole term -> a term -> a term =
fun s bu t -> match t with
| Bot -> t
| True -> t
| False -> t
......@@ -1084,7 +1067,6 @@ and aux_subterm : type a b. environment -> a term -> b term -> bool =
fun env s t -> match eiv env t with
| True -> false
| False -> false
| Bot -> false
| Name _ -> false
| Var _ -> assert (false)
......@@ -1124,7 +1106,6 @@ let all_subterms : type a b. environment -> a term -> b sort ->
let rec all_sub_aux : type a b. (a,b) all_subterm_partial_type =
fun a sort f g acc ->
match eiv env a with
| Bot -> acc
| True -> acc
| False -> acc
| Var _ -> assert false
......@@ -1181,7 +1162,6 @@ let const_subterm env (s : msg term) (t : msg term) (t_list : msg term list) =
fun t -> match eiv env t with
| True -> false
| False -> false
| Bot -> false
| Name _ -> false
| Var _ -> assert (false)
| EQ (u,v) -> (cst u) || (cst v)
......@@ -1232,7 +1212,6 @@ let compare_cond env b b' =
(* is_if_free t : Returns true iff t does not contain If *)
let rec is_if_free : type a. environment -> a term -> bool =
fun env t -> match eiv env t with
| Bot -> true
| True -> true
| False -> true
| Name _ -> true
......@@ -1248,7 +1227,6 @@ let if_free_conds env t =
let rec aux : type a. boole term list -> a term -> boole term list =
fun acc t -> match eiv env t with
| Bot -> acc
| True -> acc
| False -> acc
| Name _ -> acc
......@@ -1275,7 +1253,6 @@ let conds env t =
let rec aux : type a. boole term list -> a term -> boole term list =
fun acc t -> match eiv env t with
| Bot -> acc
| True -> acc
| False -> acc
| Name _ -> acc
......@@ -1301,7 +1278,6 @@ let simple_normalize : type a. environment -> a term -> a term = fun env t ->
let rec aux : type a. a term -> a term = fun t -> match t with
| Name _ -> t
| Var _ -> assert false
| Bot -> t
| True -> t
| False -> t
......@@ -1378,7 +1354,6 @@ let duplicate_cond_elim : type a. environment -> a term -> a term =
-> a term = fun l_pos l_neg t -> match t with
| Var _ -> assert false
| Name _ -> t
| Bot -> t
| True -> t
| False -> t
......@@ -1409,7 +1384,6 @@ let same_elim : type a. environment -> a term -> a term = fun env t ->
let rec aux : type a. a term -> a term = fun t -> match t with
| True -> t
| False -> t
| Bot -> t
| Name (s,_) -> t
| Var (s,_) -> assert false
| Fun (s,l) ->
......@@ -1446,7 +1420,6 @@ let appear_below : type a. environment -> boole term -> boole term
let rec exists_b : type a. a term -> bool = fun t ->
match eiv env t with
| Var _ -> assert false
| Bot -> false
| Name _ -> false
| True -> false
| False -> false
......@@ -1463,7 +1436,6 @@ let appear_below : type a. environment -> boole term -> boole term
and c_appears : type a. a term -> bool = fun t ->
match eiv env t with
| Var _ -> assert false
| Bot -> false
| Name (_,Msg) -> false
| Name (_,Bool) -> sym_eq env t c
| True -> sym_eq env t c
......@@ -1526,7 +1498,6 @@ let weak_normalize : type a. environment -> a term -> a term = fun env t ->
let rec simplify_conds env pos_cond_list neg_cond_list t =
let rec aux : type a. a term -> a term = fun t -> match t with
| Bot -> t
| Var _ -> assert false
| True -> t
| False -> t
......@@ -1657,7 +1628,6 @@ let r_equal : type a. environment -> a term -> a term -> bool =
let rec print_term_latex : type a. out_channel -> a term -> unit =
fun channel t ->
match t with
| Bot -> fprintf channel "\tbot{}";
| Name (s,Msg) -> fprintf channel "\\nonce{%s}" s
| Name (s,Bool) -> fprintf channel "\\bnonce{%s}" s
| True -> fprintf channel "\\true{}"
......
......@@ -11,7 +11,6 @@ type _ sort = | Msg : msg sort
| Bool : boole sort
type _ term =
| Bot : msg term
| True : boole term
| False : boole term
| Name : name_string * 'a sort -> '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