aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--parsing/g_basevernac.ml42
-rw-r--r--parsing/g_ltac.ml49
-rw-r--r--parsing/g_tactic.ml417
-rw-r--r--parsing/g_vernac.ml44
-rw-r--r--parsing/pcoq.ml42
-rw-r--r--parsing/pcoq.mli2
-rw-r--r--parsing/ppconstr.ml4
-rw-r--r--parsing/q_coqast.ml44
-rw-r--r--pretyping/rawterm.ml2
-rw-r--r--pretyping/rawterm.mli2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/tacred.mli2
-rw-r--r--tactics/tacinterp.ml4
13 files changed, 35 insertions, 23 deletions
diff --git a/parsing/g_basevernac.ml4 b/parsing/g_basevernac.ml4
index 6fdabef5a..4089f7004 100644
--- a/parsing/g_basevernac.ml4
+++ b/parsing/g_basevernac.ml4
@@ -90,7 +90,7 @@ GEXTEND Gram
VernacSearch (SearchRewrite c, l)
(* TODO: rapprocher Eval et Check *)
- | IDENT "Eval"; g = OPT natural; r = Tactic.red_tactic; "in";
+ | IDENT "Eval"; g = OPT natural; r = Tactic.red_expr; "in";
c = constr -> VernacCheckMayEval (Some r, g, c)
| IDENT "Check"; g = OPT natural; c = constr ->
VernacCheckMayEval (None, g, c)
diff --git a/parsing/g_ltac.ml4 b/parsing/g_ltac.ml4
index 0a8e2c5f8..fe6561b97 100644
--- a/parsing/g_ltac.ml4
+++ b/parsing/g_ltac.ml4
@@ -18,6 +18,7 @@ open Coqast
open Rawterm
open Tacexpr
open Ast
+open Tactic
ifdef Quotify then
open Qast
@@ -25,8 +26,6 @@ open Qast
ifdef Quotify then
open Q
-open Tactic
-
type let_clause_kind =
| LETTOPCLAUSE of Names.identifier * Genarg.constr_ast
| LETCLAUSE of
@@ -194,7 +193,7 @@ GEXTEND Gram
tactic_letarg:
(* Cannot be merged with tactic_arg1, since then "In"/"And" are
parsed as lqualid! *)
- [ [ IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
+ [ [ IDENT "Eval"; rtc = red_expr; "in"; c = Constr.constr ->
ConstrMayEval (ConstrEval (rtc,c))
| IDENT "Inst"; id = Prim.rawident; "["; c = Constr.constr; "]" ->
ConstrMayEval (ConstrContext (id,c))
@@ -204,7 +203,7 @@ GEXTEND Gram
| ta = tactic_arg0 -> ta ] ]
;
tactic_arg1:
- [ [ IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = Constr.constr ->
+ [ [ IDENT "Eval"; rtc = red_expr; "in"; c = Constr.constr ->
ConstrMayEval (ConstrEval (rtc,c))
| IDENT "Inst"; id = Prim.rawident; "["; c = Constr.constr; "]" ->
ConstrMayEval (ConstrContext (id,c))
@@ -247,7 +246,7 @@ GEXTEND Gram
[ [ tac = tactic_expr -> tac ] ]
;
Vernac_.command:
- [ [ deftok; "Definition"; name = Prim.rawident; ":="; body=Tactic.tactic ->
+ [ [ deftok; "Definition"; name = Prim.rawident; ":="; body = tactic ->
Vernacexpr.VernacDeclareTacticDefinition (loc, [name, body])
| deftok; "Definition"; name = Prim.rawident; largs=LIST1 input_fun;
":="; body=tactic_expr ->
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 77bbc03ee..285511890 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -76,7 +76,7 @@ ifdef Quotify then open Q
GEXTEND Gram
GLOBAL: simple_tactic constrarg constr_with_bindings quantified_hypothesis
- red_tactic int_or_var castedopenconstr;
+ red_expr int_or_var castedopenconstr;
int_or_var:
[ [ n = integer -> Genarg.ArgArg n
@@ -124,7 +124,7 @@ GEXTEND Gram
constrarg:
[ [ IDENT "Inst"; id = rawident; "["; c = constr; "]" ->
ConstrContext (id, c)
- | IDENT "Eval"; rtc = Tactic.red_tactic; "in"; c = constr ->
+ | IDENT "Eval"; rtc = Tactic.red_expr; "in"; c = constr ->
ConstrEval (rtc,c)
| IDENT "Check"; c = constr -> ConstrTypeOf c
| c = constr -> ConstrTerm c ] ]
@@ -205,6 +205,19 @@ GEXTEND Gram
| IDENT "Fold"; cl = LIST1 constr -> Fold cl
| IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl ] ]
;
+ (* This is [red_tactic] including possible extensions *)
+ red_expr:
+ [ [ IDENT "Red" -> Red false
+ | IDENT "Hnf" -> Hnf
+ | IDENT "Simpl" -> Simpl
+ | IDENT "Cbv"; s = LIST1 red_flag -> Cbv (make_red_flag s)
+ | IDENT "Lazy"; s = LIST1 red_flag -> Lazy (make_red_flag s)
+ | IDENT "Compute" -> Cbv (make_red_flag [FBeta;FIota;FDeltaBut [];FZeta])
+ | IDENT "Unfold"; ul = LIST1 unfold_occ -> Unfold ul
+ | IDENT "Fold"; cl = LIST1 constr -> Fold cl
+ | IDENT "Pattern"; pl = LIST1 pattern_occ -> Pattern pl
+ | s = IDENT; c = constr -> ExtraRedExpr (s,c) ] ]
+ ;
hypident:
[ [ id = id_or_meta -> InHyp id
| "("; "Type"; "of"; id = id_or_meta; ")" -> InHypType id ] ]
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 9397e7658..caa3b7916 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -97,7 +97,7 @@ let test_plurial_form = function
(* Gallina declarations *)
GEXTEND Gram
- GLOBAL: gallina gallina_ext (* reduce *) thm_token;
+ GLOBAL: gallina gallina_ext thm_token;
thm_token:
[ [ "Theorem" -> Theorem
@@ -133,7 +133,7 @@ GEXTEND Gram
[ [ ll = LIST1 params SEP ";" -> List.flatten ll ] ]
;
reduce:
- [ [ IDENT "Eval"; r = Tactic.red_tactic; "in" -> Some r
+ [ [ IDENT "Eval"; r = Tactic.red_expr; "in" -> Some r
| -> None ] ]
;
binders_list:
diff --git a/parsing/pcoq.ml4 b/parsing/pcoq.ml4
index 10f6d67b7..d26613b10 100644
--- a/parsing/pcoq.ml4
+++ b/parsing/pcoq.ml4
@@ -410,7 +410,7 @@ module Tactic =
let quantified_hypothesis =
make_gen_entry utactic rawwit_quant_hyp "quantified_hypothesis"
let int_or_var = make_gen_entry utactic rawwit_int_or_var "int_or_var"
- let red_tactic = make_gen_entry utactic rawwit_red_expr "red_tactic"
+ let red_expr = make_gen_entry utactic rawwit_red_expr "red_expr"
let simple_tactic = make_entry utactic inTacticAtomAstType "simple_tactic"
let tactic_arg = Gram.Entry.create "tactic:tactic_arg"
let tactic = make_gen_entry utactic rawwit_tactic "tactic"
diff --git a/parsing/pcoq.mli b/parsing/pcoq.mli
index b3c3db414..61e2f9771 100644
--- a/parsing/pcoq.mli
+++ b/parsing/pcoq.mli
@@ -158,7 +158,7 @@ module Tactic :
val constrarg : constr_ast may_eval Gram.Entry.e
val quantified_hypothesis : quantified_hypothesis Gram.Entry.e
val int_or_var : int or_var Gram.Entry.e
- val red_tactic : raw_red_expr Gram.Entry.e
+ val red_expr : raw_red_expr Gram.Entry.e
val simple_tactic : raw_atomic_tactic_expr Gram.Entry.e
val tactic_arg : raw_tactic_arg Gram.Entry.e
val tactic : raw_tactic_expr Gram.Entry.e
diff --git a/parsing/ppconstr.ml b/parsing/ppconstr.ml
index d73c69ee6..ad120fe19 100644
--- a/parsing/ppconstr.ml
+++ b/parsing/ppconstr.ml
@@ -132,8 +132,8 @@ let pr_red_expr (pr_constr,pr_ref) = function
hov 1 (str "Pattern" ++
prlist(fun (nl,c) -> prlist (pr_arg int) nl ++ (pr_arg pr_constr) c) l)
| (Red true | Cbv _ | Lazy _) -> error "Shouldn't be accessible from user"
- | ExtraRedExpr (s,l) ->
- hov 1 (str s ++ prlist (pr_arg pr_constr) l)
+ | ExtraRedExpr (s,c) ->
+ hov 1 (str s ++ pr_arg pr_constr c)
let rec pr_may_eval pr = function
| ConstrEval (r,c) ->
diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4
index 14bd4498b..debe3ba93 100644
--- a/parsing/q_coqast.ml4
+++ b/parsing/q_coqast.ml4
@@ -203,8 +203,8 @@ let mlexpr_of_red_expr = function
let f1 = mlexpr_of_list mlexpr_of_int in
let f = mlexpr_of_list (mlexpr_of_pair f1 mlexpr_of_constr) in
<:expr< Rawterm.Pattern $f l$ >>
- | Rawterm.ExtraRedExpr (s,l) ->
- let l = mlexpr_of_list mlexpr_of_constr l in
+ | Rawterm.ExtraRedExpr (s,c) ->
+ let l = mlexpr_of_constr c in
<:expr< Rawterm.ExtraRedExpr $mlexpr_of_string s$ $l$ >>
let rec mlexpr_of_argtype loc = function
diff --git a/pretyping/rawterm.ml b/pretyping/rawterm.ml
index c7e2b0eb3..9f39a1db9 100644
--- a/pretyping/rawterm.ml
+++ b/pretyping/rawterm.ml
@@ -143,7 +143,7 @@ type ('a,'b) red_expr_gen =
| Unfold of (int list * 'b) list
| Fold of 'a list
| Pattern of (int list * 'a) list
- | ExtraRedExpr of string * 'a list
+ | ExtraRedExpr of string * 'a
type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
diff --git a/pretyping/rawterm.mli b/pretyping/rawterm.mli
index 3a6d68115..d6543323e 100644
--- a/pretyping/rawterm.mli
+++ b/pretyping/rawterm.mli
@@ -110,7 +110,7 @@ type ('a,'b) red_expr_gen =
| Unfold of (int list * 'b) list
| Fold of 'a list
| Pattern of (int list * 'a) list
- | ExtraRedExpr of string * 'a list
+ | ExtraRedExpr of string * 'a
type 'a or_metanum = AN of loc * 'a | MetaNum of loc * int
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9bdf5822f..1242b8414 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -789,7 +789,7 @@ let make_flag f =
let red_expr_tab = ref Stringmap.empty
-type generic_reduction_function = constr list -> reduction_function
+type generic_reduction_function = constr -> reduction_function
let declare_red_expr s f =
try
@@ -807,7 +807,7 @@ let reduction_of_redexp = function
| Unfold ubinds -> unfoldn ubinds
| Fold cl -> fold_commands cl
| Pattern lp -> pattern_occs lp
- | ExtraRedExpr (s,cl) -> Stringmap.find s !red_expr_tab cl
+ | ExtraRedExpr (s,c) -> Stringmap.find s !red_expr_tab c
(* Used in several tactics. *)
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index c03c67c09..0224a9768 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -76,7 +76,7 @@ type red_expr = (constr, evaluable_global_reference) red_expr_gen
val reduction_of_redexp : red_expr -> reduction_function
-type generic_reduction_function = constr list -> reduction_function
+type generic_reduction_function = constr -> reduction_function
val declare_red_expr : string -> generic_reduction_function -> unit
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2d8f7c904..9895f955d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -390,7 +390,7 @@ let glob_redexp ist = function
| Lazy f -> Lazy (glob_flag ist f)
| Pattern l -> Pattern (List.map (glob_pattern ist) l)
| (Red _ | Simpl | Hnf as r) -> r
- | ExtraRedExpr (s,l) -> ExtraRedExpr (s, List.map (glob_constr ist) l)
+ | ExtraRedExpr (s,c) -> ExtraRedExpr (s, glob_constr ist c)
(* Interprets an hypothesis name *)
let glob_hyp_location ist = function
@@ -1009,7 +1009,7 @@ let redexp_interp ist = function
| Lazy f -> Lazy (flag_interp ist f)
| Pattern l -> Pattern (List.map (pattern_interp ist) l)
| (Red _ | Simpl | Hnf as r) -> r
- | ExtraRedExpr (s,l) -> ExtraRedExpr (s,List.map (constr_interp ist) l)
+ | ExtraRedExpr (s,c) -> ExtraRedExpr (s,constr_interp ist c)
let interp_may_eval f ist = function
| ConstrEval (r,c) ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 02:49:54 +0000