From badb5b9c7fb1dd7b2dce70b3b56cbd482e604131 Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 25 Jun 2019 14:21:16 +0200
Subject: [PATCH] [qed] introduces f_map, f_iter and removes e_map, e_iter
---
src/plugins/qed/logic.ml | 19 ++++++++++++-------
src/plugins/qed/term.ml | 26 +++++++++++++++-----------
src/plugins/wp/Cint.ml | 2 +-
3 files changed, 28 insertions(+), 19 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index 6620c41a9b3..0c1fd5a80c2 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -387,13 +387,18 @@ sig
val lc_term : term -> lc_term
val lc_repr : lc_term -> term
- (** {3 Recursion Scheme} *)
-
- val e_map : pool -> (term -> term) -> term -> term
- (** Open and close binders *)
-
- val e_iter : pool -> (term -> unit) -> term -> unit
- (** Open binders *)
+ (** {3 Iteration Scheme} *)
+
+ val f_map : ?pool:pool -> (term -> term) -> term -> term
+ (** Pass and open binders, maps its direct sub-terms
+ and then close then opened binders
+ Raises Invalid_argument in case of a bind-term without pool.
+ The optional pool must contain all free variables of the term. *)
+
+ val f_iter : ?pool:pool -> (term -> unit) -> term -> unit
+ (** Iterates over its direct sub-terms (pass and open binders)
+ Raises Invalid_argument in case of a bind-term without pool.
+ The optional pool must contain all free variables of the term. *)
val lc_iter : (term -> unit) -> term -> unit
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index 58b7ee820bf..a3e8ac03b50 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2354,22 +2354,26 @@ struct
let lc_iter f e = repr_iter f e.repr
- let e_map pool f e =
+ let f_map ?pool f e =
match e.repr with
| Apply(a,xs) -> e_apply (f a) (List.map f xs)
- | Bind(q,t,e) ->
- add_term pool e ;
- let x = fresh pool t in
- e_bind q x (f (lc_open x e))
+ | Bind _ ->
+ let pool = match pool with
+ | None -> raise (Invalid_argument "Qed.ogic.Term.f_map")
+ | Some pool -> pool in
+ let ctx,a = e_open pool e in
+ e_close ctx (rebuild f a)
| _ -> rebuild f e
- let e_iter pool f e =
+ let f_iter ?pool f e =
match e.repr with
- | Bind(_,t,e) ->
- add_term pool e ;
- let x = fresh pool t in
- lc_iter f (lc_open x e)
- | _ -> lc_iter f e
+ | Bind _ ->
+ let pool = match pool with
+ | None -> raise (Invalid_argument "Qed.ogic.Term.f_iter")
+ | Some pool -> pool in
+ let _,a = e_open pool e in
+ f a
+ | _ -> repr_iter f e.repr
(* -------------------------------------------------------------------------- *)
(* --- Sub-terms --- *)
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index d567a02694d..d3c3677929e 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -950,7 +950,7 @@ let is_cint_simplifier = object (self)
with Not_found -> t
end
| Imply (l1,l2) -> e_imply (List.map (walk ~is_goal:false) l1) (walk ~is_goal l2)
- | _ -> Lang.F.QED.e_map pool (walk ~is_goal) t in
+ | _ -> Lang.F.QED.f_map ~pool (walk ~is_goal) t in
Lang.F.p_bool (walk ~is_goal (Lang.F.e_prop p))
method simplify_exp (e : term) = e
--
GitLab