Commit a876fa3e authored by Adrien KOUTSOS's avatar Adrien KOUTSOS

some cleanup preparing for euf-cma axiom

parent 66ccc0e4
This diff is collapsed.
......@@ -13,7 +13,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
| Cond_fresh of side * boole term
exception Bad_rule of string * rule
......@@ -83,6 +82,7 @@ let print_rule_long : env -> Format.formatter -> rule -> unit =
(side_to_string side)
(print_term env) b
(* new_formula_element ancestor term_pair : Create a new formula element for
term_pair, inheriting some attributes from ancestor. *)
let new_formula_element ancestor term_pair =
......@@ -354,6 +354,7 @@ let rule_apply formula r (t, t') = match r with
| Restr -> failwith "rule_apply: no possible Restr here"
(* Apply the rule r to boolean terms (b,b'),
and return a list with the new terms *)
let rule_b_apply formula r (b,b') = match r with
......@@ -382,6 +383,7 @@ let rule_b_apply formula r (b,b') = match r with
| Restr -> failwith "rule_apply: no possible Restr here"
(*********************)
(* Rule Applications *)
(*********************)
......
......@@ -14,6 +14,7 @@ type rule =
| CS of boole term * boole term
| Cond_fresh of side * boole term
exception Bad_rule of string * rule
exception Rule_not_applicable
......
......@@ -997,7 +997,7 @@ let if_free_conds t =
aux [] t
(* conds env t : Return the list of conditionals appearing in t. *)
let conds env t =
let conds t =
let rec aux : type a. boole term list -> a term -> boole term list =
fun acc t -> match t.content with
......@@ -1224,10 +1224,10 @@ let weak_normalize : type a. a term -> a term = fun t ->
|> same_elim )
(t_equal) t
(* simplify_conds env pos_cond_list neg_cond_list t : Replace all occurrences
(* simplify_conds pos_cond_list neg_cond_list t : Replace all occurrences
of pos_cond_list by True (and reduce), and of neg_cond_list by False (and
reduce). The term t must be weakly normalized. *)
let rec simplify_conds env pos_cond_list neg_cond_list t =
let rec simplify_conds pos_cond_list neg_cond_list t =
let rec aux : type a. a term -> a term = fun t -> match t.content with
| True -> t
......@@ -1280,7 +1280,7 @@ let _pseudo_normalize : type a. env -> a term -> a term = fun env t ->
and build_ctxt cond_list pos_conds neg_conds t =
match cond_list with
| [] ->
let simp_t = simplify_conds env pos_conds neg_conds t in
let simp_t = simplify_conds pos_conds neg_conds t in
ps_aux pos_conds neg_conds simp_t
| b :: tail ->
t_ite b
......@@ -1337,8 +1337,8 @@ let _r_equal : type a. env -> (a term * a term) -> bool = fun env (t,t') ->
let nt = pseudo_normalize env t
and nt' = pseudo_normalize env t' in
let cond_nt = List.sort_uniq (compare_cond) (conds env nt)
and cond_nt' = List.sort_uniq (compare_cond) (conds env nt') in
let cond_nt = List.sort_uniq (compare_cond) (conds nt)
and cond_nt' = List.sort_uniq (compare_cond) (conds nt') in
(* Debug.debug (fun () -> if test then *)
(* begin *)
......@@ -1357,8 +1357,8 @@ let _r_equal : type a. env -> (a term * a term) -> bool = fun env (t,t') ->
let rec eq_aux s s' = match s.content with
| If (b,u,v) ->
(eq_aux u (simplify_conds env [b] [] s'))
&& (eq_aux v (simplify_conds env [] [b] s'))
(eq_aux u (simplify_conds [b] [] s'))
&& (eq_aux v (simplify_conds [] [b] s'))
| _ ->
t_equal s s' in
......
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