aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/argextend.ml486
-rw-r--r--ltac/extraargs.ml419
-rw-r--r--ltac/extratactics.ml42
-rw-r--r--ltac/g_auto.ml42
-rw-r--r--ltac/g_rewrite.ml46
-rw-r--r--plugins/extraction/g_extraction.ml41
6 files changed, 59 insertions, 57 deletions
diff --git a/grammar/argextend.ml4 b/grammar/argextend.ml4
index adfbd8cfde..dca3e1656f 100644
--- a/grammar/argextend.ml4
+++ b/grammar/argextend.ml4
@@ -73,34 +73,58 @@ let make_extend loc s cl wit = match cl with
let () = Pcoq.grammar_extend $lid:s$ None (None, [(None, None, $rules$)]) in
$lid:s$ >>
-let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
- let rawtyp, rawpr, globtyp, globpr = match typ with
- | `Uniform typ ->
- typ, pr, typ, pr
- | `Specialized (a, b, c, d) -> a, b, c, d
+let warning_redundant prefix s =
+ Printf.eprintf "Redundant [%sTYPED AS] clause in [ARGUMENT EXTEND %s].\n%!" prefix s
+
+let get_type prefix s = function
+| None -> None
+| Some typ ->
+ if is_self s typ then
+ let () = warning_redundant prefix s in None
+ else Some typ
+
+let check_type prefix s = function
+| None -> ()
+| Some _ -> warning_redundant prefix s
+
+let declare_tactic_argument loc s (typ, f, g, h) cl =
+ let rawtyp, rawpr, globtyp, globpr, typ, pr = match typ with
+ | `Uniform (typ, pr) ->
+ let typ = get_type "" s typ in
+ typ, pr, typ, pr, typ, pr
+ | `Specialized (a, rpr, c, gpr, e, tpr) ->
+ (** Check that we actually need the TYPED AS arguments *)
+ let rawtyp = get_type "RAW_" s a in
+ let glbtyp = get_type "GLOB_" s c in
+ let toptyp = get_type "" s e in
+ let () = match g with None -> () | Some _ -> check_type "RAW_" s rawtyp in
+ let () = match f, h with Some _, Some _ -> check_type "GLOB_" s glbtyp | _ -> () in
+ rawtyp, rpr, glbtyp, gpr, toptyp, tpr
in
let glob = match g with
| None ->
- if is_self s rawtyp then
- <:expr< fun ist v -> (ist, v) >>
- else
+ begin match rawtyp with
+ | None -> <:expr< fun ist v -> (ist, v) >>
+ | Some rawtyp ->
<:expr< fun ist v ->
let ans = out_gen $make_globwit loc rawtyp$
(Tacintern.intern_genarg ist
(Genarg.in_gen $make_rawwit loc rawtyp$ v)) in
(ist, ans) >>
+ end
| Some f ->
<:expr< fun ist v -> (ist, $lid:f$ ist v) >>
in
let interp = match f with
| None ->
- if is_self s globtyp then
- <:expr< fun ist v -> Ftactic.return v >>
- else
- <:expr< fun ist x ->
+ begin match globtyp with
+ | None -> <:expr< fun ist v -> Ftactic.return v >>
+ | Some globtyp ->
+ <:expr< fun ist x ->
Ftactic.bind
- (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
+ (Tacinterp.interp_genarg ist (Genarg.in_gen $make_globwit loc globtyp$ x))
(fun v -> Ftactic.return (Tacinterp.Value.cast $make_topwit loc globtyp$ v)) >>
+ end
| Some f ->
(** Compatibility layer, TODO: remove me *)
<:expr<
@@ -112,19 +136,20 @@ let declare_tactic_argument loc s (typ, pr, f, g, h) cl =
>> in
let subst = match h with
| None ->
- if is_self s globtyp then
- <:expr< fun s v -> v >>
- else
+ begin match globtyp with
+ | None -> <:expr< fun s v -> v >>
+ | Some globtyp ->
<:expr< fun s x ->
out_gen $make_globwit loc globtyp$
(Tacsubst.subst_genarg s
(Genarg.in_gen $make_globwit loc globtyp$ x)) >>
+ end
| Some f -> <:expr< $lid:f$>> in
let dyn = match typ with
- | `Uniform typ ->
+ | None -> <:expr< None >>
+ | Some typ ->
if is_self s typ then <:expr< None >>
else <:expr< Some (Genarg.val_tag $make_topwit loc typ$) >>
- | `Specialized _ -> <:expr< None >>
in
let se = mlexpr_of_string s in
let wit = <:expr< $lid:"wit_"^s$ >> in
@@ -180,22 +205,25 @@ EXTEND
"END" ->
declare_vernac_argument loc s pr l ] ]
;
+ argextend_specialized:
+ [ [ rawtyp = OPT [ "RAW_TYPED"; "AS"; rawtyp = argtype -> rawtyp ];
+ "RAW_PRINTED"; "BY"; rawpr = LIDENT;
+ globtyp = OPT [ "GLOB_TYPED"; "AS"; globtyp = argtype -> globtyp ];
+ "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
+ (rawtyp, rawpr, globtyp, globpr) ] ]
+ ;
argextend_header:
- [ [ "TYPED"; "AS"; typ = argtype;
+ [ [ typ = OPT [ "TYPED"; "AS"; typ = argtype -> typ ];
"PRINTED"; "BY"; pr = LIDENT;
f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
- h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ] ->
- (`Uniform typ, pr, f, g, h)
- | "PRINTED"; "BY"; pr = LIDENT;
- f = OPT [ "INTERPRETED"; "BY"; f = LIDENT -> f ];
- g = OPT [ "GLOBALIZED"; "BY"; f = LIDENT -> f ];
h = OPT [ "SUBSTITUTED"; "BY"; f = LIDENT -> f ];
- "RAW_TYPED"; "AS"; rawtyp = argtype;
- "RAW_PRINTED"; "BY"; rawpr = LIDENT;
- "GLOB_TYPED"; "AS"; globtyp = argtype;
- "GLOB_PRINTED"; "BY"; globpr = LIDENT ->
- (`Specialized (rawtyp, rawpr, globtyp, globpr), pr, f, g, h) ] ]
+ special = OPT argextend_specialized ->
+ let repr = match special with
+ | None -> `Uniform (typ, pr)
+ | Some (rtyp, rpr, gtyp, gpr) -> `Specialized (rtyp, rpr, gtyp, gpr, typ, pr)
+ in
+ (repr, f, g, h) ] ]
;
argtype:
[ "2"
diff --git a/ltac/extraargs.ml4 b/ltac/extraargs.ml4
index 4d3507cbc4..fbae17bafc 100644
--- a/ltac/extraargs.ml4
+++ b/ltac/extraargs.ml4
@@ -104,16 +104,14 @@ let glob_occs ist l = l
let subst_occs evm l = l
ARGUMENT EXTEND occurrences
+ TYPED AS int list
PRINTED BY pr_int_list_full
INTERPRETED BY interp_occs
GLOBALIZED BY glob_occs
SUBSTITUTED BY subst_occs
- RAW_TYPED AS occurrences_or_var
RAW_PRINTED BY pr_occurrences
-
- GLOB_TYPED AS occurrences_or_var
GLOB_PRINTED BY pr_occurrences
| [ ne_integer_list(l) ] -> [ ArgArg l ]
@@ -141,10 +139,7 @@ ARGUMENT EXTEND glob
GLOBALIZED BY glob_glob
SUBSTITUTED BY subst_glob
- RAW_TYPED AS constr_expr
RAW_PRINTED BY pr_gen
-
- GLOB_TYPED AS glob_constr_and_expr
GLOB_PRINTED BY pr_gen
[ constr(c) ] -> [ c ]
END
@@ -158,16 +153,14 @@ ARGUMENT EXTEND lconstr
END
ARGUMENT EXTEND lglob
+ TYPED AS glob
PRINTED BY pr_globc
INTERPRETED BY interp_glob
GLOBALIZED BY glob_glob
SUBSTITUTED BY subst_glob
- RAW_TYPED AS constr_expr
RAW_PRINTED BY pr_gen
-
- GLOB_TYPED AS glob_constr_and_expr
GLOB_PRINTED BY pr_gen
[ lconstr(c) ] -> [ c ]
END
@@ -207,9 +200,7 @@ ARGUMENT EXTEND hloc
INTERPRETED BY interp_place
GLOBALIZED BY intern_place
SUBSTITUTED BY subst_place
- RAW_TYPED AS loc_place
RAW_PRINTED BY pr_loc_place
- GLOB_TYPED AS loc_place
GLOB_PRINTED BY pr_loc_place
[ ] ->
[ ConclLocation () ]
@@ -224,12 +215,6 @@ ARGUMENT EXTEND hloc
END
-
-
-
-
-
-
(* Julien: Mise en commun des differentes version de replace with in by *)
let pr_by_arg_tac _prc _prlc prtac opt_c =
diff --git a/ltac/extratactics.ml4 b/ltac/extratactics.ml4
index ba9f82fb96..0b475340e2 100644
--- a/ltac/extratactics.ml4
+++ b/ltac/extratactics.ml4
@@ -980,9 +980,7 @@ let interp_test ist gls = function
ARGUMENT EXTEND test
PRINTED BY pr_itest'
INTERPRETED BY interp_test
- RAW_TYPED AS test
RAW_PRINTED BY pr_test'
- GLOB_TYPED AS test
GLOB_PRINTED BY pr_test'
| [ int_or_var(x) comparison(c) int_or_var(y) ] -> [ Test(c,x,y) ]
END
diff --git a/ltac/g_auto.ml4 b/ltac/g_auto.ml4
index bc98b7d6d4..d4fd8a1df3 100644
--- a/ltac/g_auto.ml4
+++ b/ltac/g_auto.ml4
@@ -174,7 +174,6 @@ END
let pr_hints_path_atom _ _ _ = Hints.pp_hints_path_atom
ARGUMENT EXTEND hints_path_atom
- TYPED AS hints_path_atom
PRINTED BY pr_hints_path_atom
| [ global_list(g) ] -> [ Hints.PathHints (List.map Nametab.global g) ]
| [ "*" ] -> [ Hints.PathAny ]
@@ -183,7 +182,6 @@ END
let pr_hints_path prc prx pry c = Hints.pp_hints_path c
ARGUMENT EXTEND hints_path
- TYPED AS hints_path
PRINTED BY pr_hints_path
| [ "(" hints_path(p) ")" ] -> [ p ]
| [ "!" hints_path(p) ] -> [ Hints.PathStar p ]
diff --git a/ltac/g_rewrite.ml4 b/ltac/g_rewrite.ml4
index c4ef1f297e..395c2cd1b6 100644
--- a/ltac/g_rewrite.ml4
+++ b/ltac/g_rewrite.ml4
@@ -47,10 +47,7 @@ ARGUMENT EXTEND glob_constr_with_bindings
GLOBALIZED BY glob_glob_constr_with_bindings
SUBSTITUTED BY subst_glob_constr_with_bindings
- RAW_TYPED AS constr_expr_with_bindings
RAW_PRINTED BY pr_constr_expr_with_bindings
-
- GLOB_TYPED AS glob_constr_with_bindings
GLOB_PRINTED BY pr_glob_constr_with_bindings
[ constr_with_bindings(bl) ] -> [ bl ]
@@ -76,10 +73,7 @@ ARGUMENT EXTEND rewstrategy
GLOBALIZED BY glob_strategy
SUBSTITUTED BY subst_strategy
- RAW_TYPED AS raw_strategy
RAW_PRINTED BY pr_raw_strategy
-
- GLOB_TYPED AS glob_strategy
GLOB_PRINTED BY pr_glob_strategy
[ glob(c) ] -> [ StratConstr (c, true) ]
diff --git a/plugins/extraction/g_extraction.ml4 b/plugins/extraction/g_extraction.ml4
index 7bd07f6255..ca4e13e125 100644
--- a/plugins/extraction/g_extraction.ml4
+++ b/plugins/extraction/g_extraction.ml4
@@ -35,7 +35,6 @@ let pr_int_or_id _ _ _ = function
| ArgId id -> pr_id id
ARGUMENT EXTEND int_or_id
- TYPED AS int_or_id
PRINTED BY pr_int_or_id
| [ preident(id) ] -> [ ArgId (Id.of_string id) ]
| [ integer(i) ] -> [ ArgInt i ]
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-17 02:55:45 +0000