From fb8697df992a7256dd2980521bf00d544b94176c Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 29 May 2019 15:49:17 +0200
Subject: [PATCH] [qed] suppress f_map and f_iter
---
src/plugins/qed/logic.ml | 3 ---
src/plugins/qed/term.ml | 11 -----------
src/plugins/wp/Cint.ml | 6 +++---
3 files changed, 3 insertions(+), 17 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 94ce3aa7a62..c7ff0db3acd 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -382,9 +382,6 @@ sig
val e_map : pool -> (term -> term) -> term -> term
val e_iter : pool -> (term -> unit) -> term -> unit
- val f_map : (int -> term -> term) -> int -> term -> term
- val f_iter : (int -> term -> unit) -> int -> term -> unit
-
val lc_map : (term -> term) -> term -> term
val lc_iter : (term -> unit) -> term -> unit
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index c3df0e1d46e..be689edb26f 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2338,12 +2338,6 @@ struct
e_bind q x (f (lc_open x e))
| _ -> rebuild f e
- let f_map f n e =
- match e.repr with
- | Bind(q,t,e) -> c_bind q t (f (succ n) e)
- | Apply(a,xs) -> e_apply (f n a) (List.map (f n) xs)
- | _ -> rebuild (f n) e
-
let lc_map f e =
match e.repr with
| Apply(a,xs) -> e_apply (f a) (List.map f xs)
@@ -2359,11 +2353,6 @@ struct
lc_iter f (lc_open x e)
| _ -> lc_iter f e
- let f_iter f n e =
- match e.repr with
- | Bind(_,_,e) -> f (succ n) e
- | _ -> lc_iter (f n) e
-
(* -------------------------------------------------------------------------- *)
(* --- Sub-terms --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 02fb5bd9326..d567a02694d 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -868,7 +868,7 @@ let is_cint_simplifier = object (self)
t v domain
method assume p =
- let rec aux i t =
+ let rec aux t =
match Lang.F.repr t with
| _ when not (is_prop t) -> ()
| Fun(g,[a]) ->
@@ -877,10 +877,10 @@ let is_cint_simplifier = object (self)
self#narrow_dom a ubound
with Not_found -> ()
end
- | And _ -> Lang.F.QED.f_iter aux i t
+ | And _ -> Lang.F.QED.lc_iter aux t
| _ -> ()
in
- aux 0 (Lang.F.e_prop p)
+ aux (Lang.F.e_prop p)
method target _ = ()
method fixpoint = ()
--
GitLab