Merge PR #12129: Add a `with_strategy` tactic

Ack-by: Zimmi48
Ack-by: ejgallego
Ack-by: herbelin
Ack-by: ppedrot

2 files changed, 80 insertions, 0 deletions

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4809332c5..c2654486e1 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5045,6 +5045,80 @@ let unify ?(state=TransparentState.full) x y =
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
+(** [tclWRAPFINALLY before tac finally] runs [before] before each
+    entry-point of [tac] and passes the result of [before] to
+    [finally], which is then run at each exit-point of [tac],
+    regardless of whether it succeeds or fails.  Said another way, if
+    [tac] succeeds, then it behaves as [before >>= fun v -> tac >>= fun
+    ret -> finally v <*> tclUNIT ret]; otherwise, if [tac] fails with
+    [e], it behaves as [before >>= fun v -> finally v <*> tclZERO
+    e].  Note that if [tac] succeeds [n] times before finally failing,
+    [before] and [finally] are both run [n+1] times (once around each
+    succuess, and once more around the final failure). *)
+(* We should probably export this somewhere, but it's not clear
+   where. As per
+   https://github.com/coq/coq/pull/12197#discussion_r418480525 and
+   https://gitter.im/coq/coq?at=5ead5c35347bd616304e83ef, we don't
+   export it from Proofview, because it seems somehow not primitive
+   enough.  We don't export it from this file because it is more of a
+   tactical than a tactic.  But we also don't export it from Tacticals
+   because all of the non-New tacticals there operate on `tactic`, not
+   `Proofview.tactic`, and all of the `New` tacticals that deal with
+   multi-success things are focussing, i.e., apply their arguments on
+   each goal separately (and it even says so in the comment on `New`),
+   whereas it's important that `tclWRAPFINALLY` doesn't introduce
+   extra focussing. *)
+let rec tclWRAPFINALLY before tac finally =
+  let open Proofview in
+  let open Proofview.Notations in
+  before >>= fun v -> tclCASE tac >>= function
+  | Fail (e, info) -> finally v >>= fun () -> tclZERO ~info e
+  | Next (ret, tac') -> tclOR
+                          (finally v >>= fun () -> tclUNIT ret)
+                          (fun e -> tclWRAPFINALLY before (tac' e) finally)
+
+let with_set_strategy lvl_ql k =
+  let glob_key r =
+    match r with
+    | GlobRef.ConstRef sp -> ConstKey sp
+    | GlobRef.VarRef id -> VarKey id
+    | _ -> user_err Pp.(str
+                          "cannot set an inductive type or a constructor as transparent") in
+  let kl = List.concat (List.map (fun (lvl, ql) -> List.map (fun q -> (lvl, glob_key q)) ql) lvl_ql) in
+  tclWRAPFINALLY
+    (Proofview.tclENV >>= fun env ->
+     let orig_kl = List.map (fun (_lvl, k) ->
+         (Conv_oracle.get_strategy (Environ.oracle env) k, k))
+         kl in
+     (* Because the global env might be desynchronized from the
+        proof-local env, we need to update the global env to have this
+        tactic play nicely with abstract.
+        TODO: When abstract no longer depends on Global, delete this
+        let orig_kl_global = ... in *)
+     let orig_kl_global = List.map (fun (_lvl, k) ->
+         (Conv_oracle.get_strategy (Environ.oracle (Global.env ())) k, k))
+         kl in
+     let env = List.fold_left (fun env (lvl, k) ->
+         Environ.set_oracle env
+           (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env kl in
+     Proofview.Unsafe.tclSETENV env <*>
+     (* TODO: When abstract no longer depends on Global, remove this
+        [Proofview.tclLIFT] block *)
+     Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+         List.iter (fun (lvl, k) -> Global.set_strategy k lvl) kl)) <*>
+     Proofview.tclUNIT (orig_kl, orig_kl_global))
+    k
+    (fun (orig_kl, orig_kl_global) ->
+       (* TODO: When abstract no longer depends on Global, remove this
+          [Proofview.tclLIFT] block *)
+       Proofview.tclLIFT (Proofview.NonLogical.make (fun () ->
+           List.iter (fun (lvl, k) -> Global.set_strategy k lvl) orig_kl_global)) <*>
+       Proofview.tclENV >>= fun env ->
+       let env = List.fold_left (fun env (lvl, k) ->
+           Environ.set_oracle env
+             (Conv_oracle.set_strategy (Environ.oracle env) k lvl)) env orig_kl in
+       Proofview.Unsafe.tclSETENV env)
+
 module Simple = struct
   (** Simplified version of some of the above tactics *)
 
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index c84ba17f23..b6eb48a3d9 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -435,6 +435,12 @@ val declare_intro_decomp_eq :
    (types * constr * constr) ->
    constr * types -> unit Proofview.tactic) -> unit
 
+(** Tactic analogous to the [Strategy] vernacular, but only applied
+   locally to the tactic argument *)
+val with_set_strategy :
+  (Conv_oracle.level * Names.GlobRef.t list) list ->
+  'a Proofview.tactic -> 'a Proofview.tactic
+
 (** {6 Simple form of basic tactics. } *)
 
 module Simple : sig