aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--parsing/g_vernac.ml42
-rw-r--r--parsing/ppconstr.ml2
-rw-r--r--parsing/q_coqast.ml42
-rw-r--r--plugins/btauto/refl_btauto.ml2
-rw-r--r--pretyping/glob_term.ml2
-rw-r--r--pretyping/glob_term.mli2
-rw-r--r--proofs/redexpr.ml11
-rw-r--r--tactics/tacinterp.ml12
-rw-r--r--tactics/tactics.ml7
10 files changed, 32 insertions, 14 deletions
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index f1b3ffed4..442aab00e 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -334,7 +334,7 @@ GEXTEND Gram
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "lazy"; s = strategy_flag -> Lazy s
| IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute" -> CbvVm
+ | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
| IDENT "unfold"; ul = LIST1 unfold_occ SEP "," -> Unfold ul
| IDENT "fold"; cl = LIST1 constr -> Fold cl
| IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl ] ]
@@ -347,7 +347,7 @@ GEXTEND Gram
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "lazy"; s = strategy_flag -> Lazy s
| IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
- | IDENT "vm_compute" -> CbvVm
+ | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
| IDENT "unfold"; ul = LIST1 unfold_occ -> Unfold ul
| IDENT "fold"; cl = LIST1 constr -> Fold cl
| IDENT "pattern"; pl = LIST1 pattern_occ SEP"," -> Pattern pl
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 029a5c5df..f6b31f547 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -813,7 +813,7 @@ GEXTEND Gram
[ [ IDENT "Eval"; r = Tactic.red_expr; "in"; c = lconstr ->
fun g -> VernacCheckMayEval (Some r, g, c)
| IDENT "Compute"; c = lconstr ->
- fun g -> VernacCheckMayEval (Some Glob_term.CbvVm, g, c)
+ fun g -> VernacCheckMayEval (Some Glob_term.CbvVm None, g, c)
| IDENT "Check"; c = lconstr ->
fun g -> VernacCheckMayEval (None, g, c) ] ]
;
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index fa0755364..16820efdc 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -629,7 +629,7 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| Red true -> error "Shouldn't be accessible from user."
| ExtraRedExpr s -> str s
- | CbvVm -> str "vm_compute"
+ | CbvVm o -> str "vm_compute" ++ pr_opt (pr_with_occurrences pr_pattern) o
let rec pr_may_eval test prc prlc pr2 pr3 = function
| ConstrEval (r,c) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 7df97a075..552c86903 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -174,7 +174,7 @@ let mlexpr_of_red_expr = function
| Glob_term.Pattern l ->
let f = mlexpr_of_list mlexpr_of_occ_constr in
<:expr< Glob_term.Pattern $f l$ >>
- | Glob_term.CbvVm -> <:expr< Glob_term.CbvVm >>
+ | Glob_term.CbvVm o -> <:expr< Glob_term.CbvVm $mlexpr_of_option mlexpr_of_occ_constr o$ >>
| Glob_term.ExtraRedExpr s ->
<:expr< Glob_term.ExtraRedExpr $mlexpr_of_string s$ >>
diff --git a/plugins/btauto/refl_btauto.ml b/plugins/btauto/refl_btauto.ml
index 1d01f3e54..334dcd7e0 100644
--- a/plugins/btauto/refl_btauto.ml
+++ b/plugins/btauto/refl_btauto.ml
@@ -176,7 +176,7 @@ module Btauto = struct
let print_counterexample p env gl =
let var = lapp witness [|p|] in
(* Compute an assignment that dissatisfies the goal *)
- let var = Tacmach.pf_reduction_of_red_expr gl Glob_term.CbvVm var in
+ let var = Tacmach.pf_reduction_of_red_expr gl (Glob_term.CbvVm None) var in
let rec to_list l = match decomp_term l with
| Term.App (c, _)
when c === (Lazy.force CoqList._nil) -> []
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index a4113671f..a736e6eec 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -400,7 +400,7 @@ type ('a,'b,'c) red_expr_gen =
| Fold of 'a list
| Pattern of 'a with_occurrences list
| ExtraRedExpr of string
- | CbvVm
+ | CbvVm of 'c with_occurrences option
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
diff --git a/pretyping/glob_term.mli b/pretyping/glob_term.mli
index 7fb995a88..fcd28eb8f 100644
--- a/pretyping/glob_term.mli
+++ b/pretyping/glob_term.mli
@@ -158,7 +158,7 @@ type ('a,'b,'c) red_expr_gen =
| Fold of 'a list
| Pattern of 'a with_occurrences list
| ExtraRedExpr of string
- | CbvVm
+ | CbvVm of 'c with_occurrences option
type ('a,'b,'c) may_eval =
| ConstrTerm of 'a
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 0430a239e..10e1e66cb 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -191,7 +191,16 @@ let rec reduction_of_red_expr = function
(try reduction_of_red_expr (Stringmap.find s !red_expr_tab)
with Not_found ->
error("unknown user-defined reduction \""^s^"\"")))
- | CbvVm -> (cbv_vm ,VMcast)
+ | CbvVm (Some lp) ->
+ let b = is_reference (snd lp) in
+ let lp = out_with_occurrences lp in
+ let vmfun _ env map c =
+ let tpe = Retyping.get_type_of env map c in
+ Vnorm.cbv_vm env c tpe
+ in
+ let redfun = contextually b lp vmfun in
+ (redfun, VMcast)
+ | CbvVm None -> (cbv_vm, VMcast)
let subst_flags subs flags =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index fecc2bac1..e2a99707f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -569,7 +569,8 @@ let intern_red_expr ist = function
| Lazy f -> Lazy (intern_flag ist f)
| Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
| Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
- | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r ) -> r
+ | CbvVm o -> CbvVm (Option.map (intern_typed_pattern_with_occurrences ist) o)
+ | (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
let intern_in_hyp_as ist lf (id,ipat) =
(intern_hyp_or_metaid ist id, Option.map (intern_intro_pattern lf ist) ipat)
@@ -1365,8 +1366,10 @@ let interp_red_expr ist sigma env = function
| Pattern l ->
Pattern (List.map (interp_constr_with_occurrences ist env sigma) l)
| Simpl o ->
- Simpl(Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
- | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
+ Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
+ | CbvVm o ->
+ CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
+ | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
let pf_interp_red_expr ist gl = interp_red_expr ist (project gl) (pf_env gl)
@@ -2593,7 +2596,8 @@ let subst_redexp subst = function
| Lazy f -> Lazy (subst_flag subst f)
| Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
| Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
- | (Red _ | Hnf | ExtraRedExpr _ | CbvVm as r) -> r
+ | CbvVm o -> CbvVm (Option.map (subst_pattern_with_occurrences subst) o)
+ | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
let subst_raw_may_eval subst = function
| ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_glob_constr subst c)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 988d9f530..96ddc730e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -257,8 +257,13 @@ let bind_red_expr_occurrences occs nbcl redexp =
error_illegal_clause ()
else
Simpl (Some (occs,c))
+ | CbvVm (Some (occl,c)) ->
+ if occl <> all_occurrences_expr then
+ error_illegal_clause ()
+ else
+ CbvVm (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _
- | ExtraRedExpr _ | CbvVm | Fold _ | Simpl None ->
+ | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None ->
error_occurrences_not_unsupported ()
| Unfold [] | Pattern [] ->
assert false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:50:30 +0000