Commit d93cc40f authored by Andrei Paskevich's avatar Andrei Paskevich

Term: remove redundant *_alpha operations

feel free to revert, if you think we might want to make again the
distinction between t_equal and t_equal_alpha in future or just
don't feel like breaking the API.
parent 58ff0109
......@@ -1318,19 +1318,11 @@ let t_subst_single v t1 t = t_subst (Mvs.singleton v t1) t
let t_freevars = add_t_vars
(* alpha-equality *)
let t_equal_alpha = t_equal
module Hterm_alpha = Hterm
(* occurrence check *)
let rec t_occurs r t =
t_equal r t || t_any (t_occurs r) t
let t_occurs_alpha = t_occurs
(* substitutes term [t2] for term [t1] in term [t] *)
let rec t_replace t1 t2 t =
......@@ -1340,8 +1332,6 @@ let t_replace t1 t2 t =
t_ty_check t2 t1.t_ty;
t_replace t1 t2 t
let t_replace_alpha = t_replace
(* constructors with propositional simplification *)
let keep_on_simp_label = create_label "keep_on_simp"
......
......@@ -423,17 +423,7 @@ val t_app_map :
val t_app_fold :
('a -> lsymbol -> ty list -> ty option -> 'a) -> 'a -> term -> 'a
(** Equality modulo alpha *)
val t_equal_alpha : term -> term -> bool
module Hterm_alpha : Exthtbl.S with type key = term
(** Subterm occurrence check and replacement *)
val t_occurs : term -> term -> bool
val t_occurs_alpha : term -> term -> bool
val t_occurs : term -> term -> bool
val t_replace : term -> term -> term -> term
val t_replace_alpha : term -> term -> term -> term
......@@ -15,7 +15,7 @@ open Term
open Decl
let abstraction (keep : lsymbol -> bool) =
let term_table = Hterm_alpha.create 257 in
let term_table = Hterm.create 257 in
let extra_decls = ref [] in
let rec abstract t : term =
......@@ -26,10 +26,10 @@ let abstraction (keep : lsymbol -> bool) =
| Tnot _ | Tbinop _ ->
t_map abstract t
| _ ->
let (ls, tabs) = try Hterm_alpha.find term_table t with Not_found ->
let (ls, tabs) = try Hterm.find term_table t with Not_found ->
let ls = create_lsymbol (id_fresh "abstr") [] t.t_ty in
let tabs = t_app ls [] t.t_ty in
Hterm_alpha.add term_table t (ls, tabs);
Hterm.add term_table t (ls, tabs);
ls, tabs in
extra_decls := ls :: !extra_decls;
tabs in
......
......@@ -33,7 +33,7 @@ let make_rt_rf env =
| Tapp (lselect,[{t_node=Tapp(lstore,[_;a1;b])};a2])
when lselect.ls_name == select &&
lstore.ls_name == store &&
t_equal_alpha a1 a2 -> b
t_equal a1 a2 -> b
| _ -> t
and rf f = TermTF.t_map rt rf f in
rt,rf
......
......@@ -201,7 +201,7 @@ let fmla_cond_subst filter f =
for j = 0 to subl - 1 do
if j <> i then
let (f, s) = subf.(j) in
subf.(j) <- (t_replace_alpha t1 t2 f, s);
subf.(j) <- (t_replace t1 t2 f, s);
done in
let (f, s) = subf.(i) in
match f.t_node with
......
......@@ -162,7 +162,7 @@ let eval_int_rel op _ty ls l =
| _ -> assert false
let term_equality t1 t2 =
if t_equal_alpha t1 t2 then Some true
if t_equal t1 t2 then Some true
else
try
let i1 = big_int_of_term t1 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