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 Co-Authored-By: Théo Zimmermann Co-Authored-By: Michael Soegtrop <7895506+MSoegtropIMC@users.noreply.github.com> --- parsing/g_prim.mlg | 8 +++++++- parsing/pcoq.ml | 2 ++ parsing/pcoq.mli | 1 + 3 files changed, 10 insertions(+), 1 deletion(-) (limited to 'parsing') diff --git a/parsing/g_prim.mlg b/parsing/g_prim.mlg index 9c50109bb3..7cabd850ad 100644 --- a/parsing/g_prim.mlg +++ b/parsing/g_prim.mlg @@ -53,7 +53,7 @@ GRAMMAR EXTEND Gram bignat bigint natural integer identref name ident var preident fullyqualid qualid reference dirpath ne_lstring ne_string string lstring pattern_ident pattern_identref by_notation - smart_global bar_cbrace; + smart_global bar_cbrace strategy_level; preident: [ [ s = IDENT -> { s } ] ] ; @@ -140,4 +140,10 @@ GRAMMAR EXTEND Gram bar_cbrace: [ [ test_pipe_closedcurly; "|"; "}" -> { () } ] ] ; + strategy_level: + [ [ IDENT "expand" -> { Conv_oracle.Expand } + | IDENT "opaque" -> { Conv_oracle.Opaque } + | n=integer -> { Conv_oracle.Level n } + | IDENT "transparent" -> { Conv_oracle.transparent } ] ] + ; END diff --git a/parsing/pcoq.ml b/parsing/pcoq.ml index 5b0562fb0d..2cc16f85d5 100644 --- a/parsing/pcoq.ml +++ b/parsing/pcoq.ml @@ -276,6 +276,7 @@ module Prim = let reference = make_gen_entry uprim "reference" let by_notation = Entry.create "by_notation" let smart_global = Entry.create "smart_global" + let strategy_level = gec_gen "strategy_level" (* parsed like ident but interpreted as a term *) let var = gec_gen "var" @@ -505,6 +506,7 @@ let () = Grammar.register0 wit_ident (Prim.ident); Grammar.register0 wit_var (Prim.var); Grammar.register0 wit_ref (Prim.reference); + Grammar.register0 wit_smart_global (Prim.smart_global); Grammar.register0 wit_sort_family (Constr.sort_family); Grammar.register0 wit_constr (Constr.constr); () diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli index 90088be307..bd64d21518 100644 --- a/parsing/pcoq.mli +++ b/parsing/pcoq.mli @@ -170,6 +170,7 @@ module Prim : val ne_lstring : lstring Entry.t val var : lident Entry.t val bar_cbrace : unit Entry.t + val strategy_level : Conv_oracle.level Entry.t end module Constr : -- cgit v1.2.3