From 1405989f3cfa5aeedfe2f9f3ac2d090c5f0acaff Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 29 May 2019 16:20:17 +0200
Subject: [PATCH] [qed+wp] suppress lc_map and p_iter
---
src/plugins/qed/logic.ml | 4 +++-
src/plugins/qed/term.ml | 9 ++-------
src/plugins/wp/Conditions.ml | 21 ++++++++++++---------
src/plugins/wp/Definitions.ml | 6 +++++-
src/plugins/wp/Lang.ml | 7 -------
src/plugins/wp/Lang.mli | 4 ++--
6 files changed, 24 insertions(+), 27 deletions(-)
diff --git a/src/plugins/qed/logic.ml b/src/plugins/qed/logic.ml
index c7ff0db3acd..6d25e58831d 100644
--- a/src/plugins/qed/logic.ml
+++ b/src/plugins/qed/logic.ml
@@ -380,9 +380,11 @@ sig
(** {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 *)
- val lc_map : (term -> term) -> term -> term
val lc_iter : (term -> unit) -> term -> unit
(** {3 Partial Typing} *)
diff --git a/src/plugins/qed/term.ml b/src/plugins/qed/term.ml
index be689edb26f..75a6867a0a7 100644
--- a/src/plugins/qed/term.ml
+++ b/src/plugins/qed/term.ml
@@ -2329,6 +2329,8 @@ struct
| Rget(r,f) -> e_getfield r f
| Rdef fvs -> e_record fvs
+ let lc_iter f e = repr_iter f e.repr
+
let e_map pool f e =
match e.repr with
| Apply(a,xs) -> e_apply (f a) (List.map f xs)
@@ -2338,13 +2340,6 @@ struct
e_bind q x (f (lc_open x e))
| _ -> rebuild f e
- let lc_map f e =
- match e.repr with
- | Apply(a,xs) -> e_apply (f a) (List.map f xs)
- | _ -> rebuild f e
-
- let lc_iter f e = repr_iter f e.repr
-
let e_iter pool f e =
match e.repr with
| Bind(_,t,e) ->
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index 1426136e80c..a0e859f8d20 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -985,7 +985,7 @@ struct
mutable cst : bool Tmap.t ;
mutable dom : Vars.t ; (* support of defs *)
mutable def : term Tmap.t ; (* defs *)
- mutable mem : term Tmap.t ; (* defs+memo *)
+ mutable cache : F.sigma option ; (* memo *)
}
let rec is_cst s e = match F.repr e with
@@ -1012,6 +1012,7 @@ struct
s.dom <- Vars.union (F.vars a) s.dom ;
s.def <- Tmap.add a e s.def ;
s.def <- Tmap.add p p s.def ;
+ s.cache <- None ;
end
let rec assume s p = match F.repr p with
@@ -1025,13 +1026,16 @@ struct
| Have p | When p | Core p | Init p -> assume s (F.e_prop p)
| Type _ | Branch _ | Either _ | State _ -> ()
- let rec e_apply s e =
- try Tmap.find e s.mem
- with Not_found ->
- let e' = F.QED.lc_map (e_apply s) e in
- s.mem <- Tmap.add e e' s.mem ; e'
+ let subst s =
+ match s.cache with
+ | Some m -> m
+ | None ->
+ let m = Lang.sigma () in
+ F.Subst.add_map m s.def ;
+ s.cache <- Some m ; m
- let p_apply s p = F.p_bool (e_apply s (F.e_prop p))
+ let e_apply s e = F.e_subst (subst s) e
+ let p_apply s p = F.p_subst (subst s) p
let rec c_apply s = function
| State m -> State (Mstate.apply (e_apply s) m)
@@ -1052,13 +1056,12 @@ struct
let simplify (hs,p) =
let s = {
cst = Tmap.empty ;
- mem = Tmap.empty ;
def = Tmap.empty ;
dom = Vars.empty ;
+ cache = None ;
} in
try
List.iter (fun h -> collect s h.condition) hs ;
- s.mem <- s.def ;
let hs = List.map (s_apply s) hs in
let p = p_apply s p in
hs , p
diff --git a/src/plugins/wp/Definitions.ml b/src/plugins/wp/Definitions.ml
index 7769f37de54..45ff8a2953c 100644
--- a/src/plugins/wp/Definitions.ml
+++ b/src/plugins/wp/Definitions.ml
@@ -371,7 +371,11 @@ class virtual visitor main =
if not (Tset.mem t terms) then
begin
self#repr ~bool:false (F.repr t) ;
- F.p_iter self#vpred self#vterm p
+ F.lc_iter
+ (fun e ->
+ if F.is_prop e
+ then self#vpred (F.p_bool e)
+ else self#vterm e) t
end
method private vdefinition = function
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index 21e9a0e9e71..4996cc10890 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -785,13 +785,6 @@ struct
let varsp = vars
let p_expr = repr
let e_expr = repr
- let p_iter fp fe p =
- match QED.repr p with
- | True | False | Kint _ | Kreal _ | Fvar _ | Bvar _ -> ()
- | Eq(a,b) | Neq(a,b) when is_prop a && is_prop b -> fp a ; fp b
- | Eq _ | Neq _ | Leq _ | Lt _ | Times _ | Add _ | Mul _ | Div _ | Mod _
- | Acst _ | Aget _ | Aset _ | Rget _ | Rdef _ | Fun _ | Apply _ -> lc_iter fe p
- | And _ | Or _ | Imply _ | If _ | Not _ | Bind _ -> lc_iter fp p
let pp_tau = Pretty.pp_tau
let context_pp = Context.create "Lang.F.pp"
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 409bbedae1e..537df0b7c76 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -392,13 +392,13 @@ sig
val p_expr : pred -> pred QED.expression
val e_expr : pred -> term QED.expression
- val p_iter : (pred -> unit) -> (term -> unit) -> pred -> unit
+
+ (* val p_iter : (pred -> unit) -> (term -> unit) -> pred -> unit *)
(** {3 Binders} *)
val lc_closed : term -> bool
val lc_iter : (term -> unit) -> term -> unit
- val lc_map : (term -> term) -> term -> term
(** {3 Utilities} *)
--
GitLab