From a25793f9888f410b515230eb265484235e02153e Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 2 Dec 2019 13:17:05 +0100
Subject: [PATCH] [wp] freshen lemma instances
---
src/plugins/wp/Lang.mli | 1 +
src/plugins/wp/TacInstance.ml | 6 +++---
src/plugins/wp/TacInstance.mli | 2 +-
src/plugins/wp/TacLemma.ml | 19 ++++++++++++-------
4 files changed, 17 insertions(+), 11 deletions(-)
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 7f1f0f1a358..517f9857173 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -223,6 +223,7 @@ sig
val pool : ?copy:pool -> unit -> pool
val fresh : pool -> ?basename:string -> tau -> var
+ val alpha : pool -> var -> var
val add_var : pool -> var -> unit
val add_vars : pool -> Vars.t -> unit
diff --git a/src/plugins/wp/TacInstance.ml b/src/plugins/wp/TacInstance.ml
index 1b95285882d..2cba2c899f7 100644
--- a/src/plugins/wp/TacInstance.ml
+++ b/src/plugins/wp/TacInstance.ml
@@ -130,8 +130,8 @@ let bind ~side bindings property : Tactical.process =
let open Conditions in
instance_have ?title:s.descr ~at:s.id bindings property
-let filter x e =
- try F.Tau.equal (F.tau_of_var x) (F.typeof e)
+let filter tau e =
+ try F.Tau.equal tau (F.typeof e)
with Not_found -> true (* allowed to not restrict usage *)
let fieldname ~range k x =
@@ -159,7 +159,7 @@ class instance =
let range = match tau with L.Int -> true | _ -> false in
let tooltip = fieldname ~range env.index x in
env.feedback#update_field
- ~tooltip ~range ~enabled:true ~filter:(filter x) fd ;
+ ~tooltip ~range ~enabled:true ~filter:(filter tau) fd ;
let lemma = F.QED.e_unbind x phi in
let bindings,property = self#wrap env lemma fields in
(x,v) :: bindings , property
diff --git a/src/plugins/wp/TacInstance.mli b/src/plugins/wp/TacInstance.mli
index 46e523c1676..00d5adfe2c1 100644
--- a/src/plugins/wp/TacInstance.mli
+++ b/src/plugins/wp/TacInstance.mli
@@ -29,7 +29,7 @@ open Strategy
val tactical : Tactical.t
val fields : selection field list
val params : parameter list
-val filter : var -> term -> bool
+val filter : tau -> term -> bool
type bindings = (var * selection) list
diff --git a/src/plugins/wp/TacLemma.ml b/src/plugins/wp/TacLemma.ml
index 343dbe4ffb0..3f24df00865 100644
--- a/src/plugins/wp/TacLemma.ml
+++ b/src/plugins/wp/TacLemma.ml
@@ -90,6 +90,12 @@ let search,psearch =
Tactical.search ~id:"lemma" ~title:"Lemma" ~descr:"Lemma to Instantiate"
~browse ~find:Definitions.find_name ()
+
+let fresh pool { l_forall ; l_lemma } =
+ let vars = List.map (F.alpha pool) l_forall in
+ let sigma = Lang.subst l_forall (List.map F.e_var vars) in
+ vars , F.p_subst sigma l_lemma
+
class instance =
object(self)
inherit Tactical.make ~id:"Wp.lemma"
@@ -111,7 +117,7 @@ class instance =
env.feedback#update_field ~enabled:true
~title ~tooltip:env.descr
~range:(match tau with L.Int -> true | _ -> false)
- ~filter:(TacInstance.filter x) fd ;
+ ~filter:(TacInstance.filter tau) fd ;
let bindings,lemma = self#wrap env xs fields in
(x,value)::bindings , lemma
| _ ->
@@ -125,17 +131,16 @@ class instance =
| None ->
self#hide feedback TacInstance.fields ;
Not_configured
- | Some l ->
- let descr = l.Tactical.descr in
- let lemma = l.value.l_lemma in
+ | Some Tactical.{ title ; value = dlem } ->
+ let fields = TacInstance.fields in
+ let vars,lemma = fresh feedback#pool dlem in
+ let descr = Pretty_utils.to_string F.pp_pred lemma in
let bindings,lemma =
- self#wrap { feedback ; descr ; lemma }
- l.value.l_forall TacInstance.fields in
+ self#wrap { feedback ; descr ; lemma } vars fields in
match TacInstance.cardinal 1000 bindings with
| Some n ->
if n > 1 then
feedback#set_descr "Generates %d instances" n ;
- let title = l.title in
let at = Tactical.at selection in
Applicable
(TacInstance.instance_have ~title ?at bindings lemma)
--
GitLab