Merge branch 'fix/wp/alpha-convert-lemma' into 'stable/calcium'

[wp] freshen lemma instances

See merge request frama-c/frama-c!2467

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
 

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

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
 

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)