From 2edbbfee7fdcfb2a4804524091930c5dab7b9db4 Mon Sep 17 00:00:00 2001
From: Jason Gross
Date: Sun, 19 Apr 2020 17:37:27 -0400
Subject: Add a `with_strategy` tactic

Useful for guarding calls to `unfold` or `cbv` to ensure that, e.g.,
`Opaque foo` doesn't break some automation which tries to unfold `foo`.

We have some timeouts in the strategy success file.  We should not run
into issues, because we are not really testing how long these take.  We
could just as well use `Timeout 60` or longer, we just want to make sure
the file dies more quickly rather than taking over 10^100 steps.

Note that this tactic does not play well with `abstract`; I have a
potentially controversial change that fixes this issue.

One of the lines in the doc comes from
https://github.com/coq/coq/pull/12129#issuecomment-619771556

Co-Authored-By: Pierre-Marie Pédrot <pierre-marie.pedrot@irif.fr>
Co-Authored-By: Théo Zimmermann <theo.zimmermann@inria.fr>
Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com>
---
 tactics/tactics.ml  | 23 +++++++++++++++++++++++
 tactics/tactics.mli |  6 ++++++
 2 files changed, 29 insertions(+)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index e4809332c5..b17f02f224 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -5045,6 +5045,29 @@ let unify ?(state=TransparentState.full) x y =
     Proofview.tclZERO (PretypeError (env, sigma, CannotUnify (x, y, None)))
   end
 
+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
+  Proofview.tclENV >>= fun env ->
+  let orig_kl = List.map (fun (_lvl, k) ->
+      (Conv_oracle.get_strategy (Environ.oracle 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 <*>
+  k <*>
+  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..fb4367f3aa 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 ->
+  unit Proofview.tactic -> unit Proofview.tactic
+
 (** {6 Simple form of basic tactics. } *)
 
 module Simple : sig
-- 
cgit v1.2.3