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>

8 files changed, 84 insertions, 0 deletions

diff --git a/plugins/ltac/extraargs.mlg b/plugins/ltac/extraargs.mlg
index c4731e5c34..eb53fd45d0 100644
--- a/plugins/ltac/extraargs.mlg
+++ b/plugins/ltac/extraargs.mlg
@@ -31,6 +31,8 @@ let create_generic_quotation name e wit =
 let () = create_generic_quotation "integer" Pcoq.Prim.integer Stdarg.wit_int
 let () = create_generic_quotation "string" Pcoq.Prim.string Stdarg.wit_string
 
+let () = create_generic_quotation "smart_global" Pcoq.Prim.smart_global Stdarg.wit_smart_global
+
 let () = create_generic_quotation "ident" Pcoq.Prim.ident Stdarg.wit_ident
 let () = create_generic_quotation "reference" Pcoq.Prim.reference Stdarg.wit_ref
 let () = create_generic_quotation "uconstr" Pcoq.Constr.lconstr Stdarg.wit_uconstr
@@ -342,3 +344,55 @@ let pr_lpar_id_colon _ _ _ _ = mt ()
 ARGUMENT EXTEND test_lpar_id_colon TYPED AS unit PRINTED BY { pr_lpar_id_colon }
 | [ local_test_lpar_id_colon(x) ] -> { () }
 END
+
+{
+
+(* Work around a limitation of the macro system *)
+let strategy_level0 = Pcoq.Prim.strategy_level
+
+let pr_strategy _ _ _ v = Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level PRINTED BY { pr_strategy }
+| [ strategy_level0(n) ] -> { n }
+END
+
+{
+
+let intern_strategy ist v = match v with
+| ArgVar id -> ArgVar (Tacintern.intern_hyp ist id)
+| ArgArg v -> ArgArg v
+
+let subst_strategy _ v = v
+
+let interp_strategy ist gl = function
+| ArgArg n -> gl.Evd.sigma, n
+| ArgVar { CAst.v = id; CAst.loc } ->
+  let v =
+    try Id.Map.find id ist.lfun
+    with Not_found ->
+      CErrors.user_err ?loc
+        (str "Unbound variable " ++ Id.print id ++ str".")
+  in
+  let v =
+    try Tacinterp.Value.cast (Genarg.topwit wit_strategy_level) v
+    with CErrors.UserError _ -> Taccoerce.error_ltac_variable ?loc id None v "a strategy_level"
+  in
+  gl.Evd.sigma, v
+
+let pr_loc_strategy _ _ _ v = Pputils.pr_or_var Conv_oracle.pr_level v
+
+}
+
+ARGUMENT EXTEND strategy_level_or_var
+    TYPED AS strategy_level
+    PRINTED BY { pr_strategy }
+    INTERPRETED BY { interp_strategy }
+    GLOBALIZED BY { intern_strategy }
+    SUBSTITUTED BY { subst_strategy }
+    RAW_PRINTED BY { pr_loc_strategy }
+    GLOB_PRINTED BY { pr_loc_strategy }
+| [ strategy_level(n) ] -> { ArgArg n }
+| [ identref(id) ] -> { ArgVar id }
+END
diff --git a/plugins/ltac/extraargs.mli b/plugins/ltac/extraargs.mli
index fbdb7c0032..e52bf55f71 100644
--- a/plugins/ltac/extraargs.mli
+++ b/plugins/ltac/extraargs.mli
@@ -78,3 +78,7 @@ val wit_in_clause :
   (lident Locus.clause_expr,
    lident Locus.clause_expr,
    Id.t   Locus.clause_expr) Genarg.genarg_type
+
+val wit_strategy_level : Conv_oracle.level Genarg.uniform_genarg_type
+
+val wit_strategy_level_or_var : (Conv_oracle.level Locus.or_var, Conv_oracle.level Locus.or_var, Conv_oracle.level) Genarg.genarg_type
diff --git a/plugins/ltac/extratactics.mlg b/plugins/ltac/extratactics.mlg
index 0bad3cbe5b..ffb597d4cb 100644
--- a/plugins/ltac/extratactics.mlg
+++ b/plugins/ltac/extratactics.mlg
@@ -1119,3 +1119,11 @@ let tclOPTIMIZE_HEAP =
 TACTIC EXTEND optimize_heap
 | [ "optimize_heap" ] -> { tclOPTIMIZE_HEAP }
 END
+
+(** Tactic analogous to [Strategy] vernacular *)
+
+TACTIC EXTEND with_strategy
+| [ "with_strategy" strategy_level_or_var(v) "[" ne_smart_global_list(q) "]" tactic3(tac) ] -> {
+  with_set_strategy [(v, q)] (Tacinterp.tactic_of_value ist tac)
+}
+END
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index 09f1fc371a..d74e981c6d 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -1325,6 +1325,8 @@ let () =
   register_basic_print0 wit_int_or_var (pr_or_var int) (pr_or_var int) int;
   register_basic_print0 wit_ref
     pr_qualid (pr_or_var (pr_located pr_global)) pr_global;
+  register_basic_print0 wit_smart_global
+    (pr_or_by_notation pr_qualid) (pr_or_var (pr_located pr_global)) pr_global;
   register_basic_print0 wit_ident pr_id pr_id pr_id;
   register_basic_print0 wit_var pr_lident pr_lident pr_id;
   register_print0 wit_intropattern pr_raw_intro_pattern pr_glob_intro_pattern pr_intro_pattern_env [@warning "-3"];
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 04d85ed390..91d26519b8 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -293,6 +293,13 @@ let coerce_to_evaluable_ref env sigma v =
     | VarRef var -> EvalVarRef var
     | ConstRef c -> EvalConstRef c
     | IndRef _ | ConstructRef _ -> fail ()
+  else if has_type v (topwit wit_smart_global) then
+    let open GlobRef in
+    let r = out_gen (topwit wit_smart_global) v in
+    match r with
+    | VarRef var -> EvalVarRef var
+    | ConstRef c -> EvalConstRef c
+    | IndRef _ | ConstructRef _ -> fail ()
   else
     match Value.to_constr v with
     | Some c when isConst sigma c -> EvalConstRef (fst (destConst sigma c))
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml
index 597c3fdaac..929fd5e132 100644
--- a/plugins/ltac/tacintern.ml
+++ b/plugins/ltac/tacintern.ml
@@ -305,6 +305,12 @@ let intern_evaluable_reference_or_by_notation ist = function
       (Notation.interp_notation_as_global_reference ?loc
         GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc)
 
+let intern_smart_global ist = function
+  | {v=AN r} -> intern_global_reference ist r
+  | {v=ByNotation (ntn,sc);loc} ->
+      ArgArg (loc, (Notation.interp_notation_as_global_reference ?loc
+        GlobRef.(function ConstRef _ | VarRef _ -> true | _ -> false) ntn sc))
+
 (* Globalize a reduction expression *)
 let intern_evaluable ist r =
   let f ist r =
@@ -813,6 +819,7 @@ let intern_ltac ist tac =
 
 let () =
   Genintern.register_intern0 wit_int_or_var (lift intern_int_or_var);
+  Genintern.register_intern0 wit_smart_global (lift intern_smart_global);
   Genintern.register_intern0 wit_ref (lift intern_global_reference);
   Genintern.register_intern0 wit_pre_ident (fun ist c -> (ist,c));
   Genintern.register_intern0 wit_ident intern_ident';
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 6debc7d9b9..d1f031b418 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -2022,6 +2022,7 @@ let interp_pre_ident ist env sigma s =
 
 let () =
   register_interp0 wit_int_or_var (fun ist n -> Ftactic.return (interp_int_or_var ist n));
+  register_interp0 wit_smart_global (lift interp_reference);
   register_interp0 wit_ref (lift interp_reference);
   register_interp0 wit_pre_ident (lift interp_pre_ident);
   register_interp0 wit_ident (lift interp_ident);
diff --git a/plugins/ltac/tacsubst.ml b/plugins/ltac/tacsubst.ml
index 600c30b403..ed298b7e66 100644
--- a/plugins/ltac/tacsubst.ml
+++ b/plugins/ltac/tacsubst.ml
@@ -280,6 +280,7 @@ and subst_genarg subst (GenArg (Glbwit wit, x)) =
 let () =
   Genintern.register_subst0 wit_int_or_var (fun _ v -> v);
   Genintern.register_subst0 wit_ref subst_global_reference;
+  Genintern.register_subst0 wit_smart_global subst_global_reference;
   Genintern.register_subst0 wit_pre_ident (fun _ v -> v);
   Genintern.register_subst0 wit_ident (fun _ v -> v);
   Genintern.register_subst0 wit_var (fun _ v -> v);