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> --- kernel/conv_oracle.ml | 6 ++++++ kernel/conv_oracle.mli | 2 +- 2 files changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel') diff --git a/kernel/conv_oracle.ml b/kernel/conv_oracle.ml index 9b87c194c5..3ee1d2fb1f 100644 --- a/kernel/conv_oracle.ml +++ b/kernel/conv_oracle.ml @@ -19,6 +19,12 @@ open Names * The default value is [Level 100]. *) type level = Expand | Level of int | Opaque +let pr_level = function + | Expand -> Pp.str "expand" + | Level 0 -> Pp.str "transparent" + | Level n -> Pp.int n + | Opaque -> Pp.str "opaque" + let default = Level 0 let is_default = function | Level 0 -> true diff --git a/kernel/conv_oracle.mli b/kernel/conv_oracle.mli index b25488d94a..930edf6c49 100644 --- a/kernel/conv_oracle.mli +++ b/kernel/conv_oracle.mli @@ -27,6 +27,7 @@ val oracle_order : ('a -> Constant.t) -> oracle -> bool -> * The default value (transparent constants) is [Level 0]. *) type level = Expand | Level of int | Opaque +val pr_level : level -> Pp.t val transparent : level (** Check whether a level is transparent *) @@ -42,4 +43,3 @@ val set_strategy : oracle -> Constant.t tableKey -> level -> oracle val fold_strategy : (Constant.t tableKey -> level -> 'a -> 'a) -> oracle -> 'a -> 'a val get_transp_state : oracle -> TransparentState.t - -- cgit v1.2.3