aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/top_printers.ml4
-rw-r--r--grammar/argextend.mlp12
-rw-r--r--grammar/q_util.mli2
-rw-r--r--grammar/q_util.mlp2
-rw-r--r--grammar/tacextend.mlp17
-rw-r--r--grammar/vernacextend.mlp16
-rw-r--r--parsing/egramml.ml4
-rw-r--r--parsing/egramml.mli2
-rw-r--r--plugins/ltac/g_ltac.ml48
-rw-r--r--plugins/ltac/pptactic.ml7
-rw-r--r--plugins/ltac/pptactic.mli2
-rw-r--r--plugins/ltac/tacentries.ml14
-rw-r--r--plugins/ltac/tacentries.mli2
13 files changed, 54 insertions, 38 deletions
diff --git a/dev/top_printers.ml b/dev/top_printers.ml
index f8498c402..ce6d5dff0 100644
--- a/dev/top_printers.ml
+++ b/dev/top_printers.ml
@@ -510,7 +510,7 @@ let _ =
extend_vernac_command_grammar ("PrintConstr", 0) None
[GramTerminal "PrintConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+ (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
let _ =
try
@@ -526,7 +526,7 @@ let _ =
extend_vernac_command_grammar ("PrintPureConstr", 0) None
[GramTerminal "PrintPureConstr";
GramNonTerminal
- (Loc.ghost,rawwit wit_constr,Extend.Aentry Pcoq.Constr.constr)]
+ (Loc.ghost,Some (rawwit wit_constr),Extend.Aentry Pcoq.Constr.constr)]
(* Setting printer of unbound global reference *)
open Names
diff --git a/grammar/argextend.mlp b/grammar/argextend.mlp
index d00ee4e5d..5cfcc6fd2 100644
--- a/grammar/argextend.mlp
+++ b/grammar/argextend.mlp
@@ -40,7 +40,8 @@ let make_topwit loc arg = <:expr< Genarg.topwit $make_wit loc arg$ >>
let make_act loc act pil =
let rec make = function
| [] -> <:expr< (fun loc -> $act$) >>
- | ExtNonTerminal (_, p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
+ | ExtNonTerminal (_, None) :: tl -> <:expr< (fun $lid:"_"$ -> $make tl$) >>
+ | ExtNonTerminal (_, Some p) :: tl -> <:expr< (fun $lid:p$ -> $make tl$) >>
| ExtTerminal _ :: tl ->
<:expr< (fun _ -> $make tl$) >> in
make (List.rev pil)
@@ -63,7 +64,7 @@ let is_ident x = function
| _ -> false
let make_extend loc s cl wit = match cl with
-| [[ExtNonTerminal (Uentry e, id)], act] when is_ident id act ->
+| [[ExtNonTerminal (Uentry e, Some id)], act] when is_ident id act ->
(** Special handling of identity arguments by not redeclaring an entry *)
<:str_item<
value $lid:s$ =
@@ -246,10 +247,13 @@ EXTEND
genarg:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING -> ExtTerminal s
] ]
;
diff --git a/grammar/q_util.mli b/grammar/q_util.mli
index 5b3eb3202..0b3def058 100644
--- a/grammar/q_util.mli
+++ b/grammar/q_util.mli
@@ -23,7 +23,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
val mlexpr_of_list : ('a -> MLast.expr) -> 'a list -> MLast.expr
diff --git a/grammar/q_util.mlp b/grammar/q_util.mlp
index 8b930cf36..87262e1c8 100644
--- a/grammar/q_util.mlp
+++ b/grammar/q_util.mlp
@@ -25,7 +25,7 @@ type user_symbol =
type extend_token =
| ExtTerminal of string
-| ExtNonTerminal of user_symbol * string
+| ExtNonTerminal of user_symbol * string option
let mlexpr_of_list f l =
List.fold_right
diff --git a/grammar/tacextend.mlp b/grammar/tacextend.mlp
index b14fba975..3057ee58c 100644
--- a/grammar/tacextend.mlp
+++ b/grammar/tacextend.mlp
@@ -31,19 +31,19 @@ let mlexpr_of_ident id =
let rec make_patt = function
| [] -> <:patt< [] >>
- | ExtNonTerminal (_, p) :: l ->
+ | ExtNonTerminal (_, Some p) :: l ->
<:patt< [ $lid:p$ :: $make_patt l$ ] >>
| _::l -> make_patt l
let rec make_let raw e = function
| [] -> <:expr< fun $lid:"ist"$ -> $e$ >>
- | ExtNonTerminal (g, p) :: l ->
+ | ExtNonTerminal (g, Some p) :: l ->
let t = type_of_user_symbol g in
let loc = MLast.loc_of_expr e in
let e = make_let raw e l in
let v =
if raw then <:expr< Genarg.out_gen $make_rawwit loc t$ $lid:p$ >>
- else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
+ else <:expr< Tacinterp.Value.cast $make_topwit loc t$ $lid:p$ >> in
<:expr< let $lid:p$ = $v$ in $e$ >>
| _::l -> make_let raw e l
@@ -75,7 +75,7 @@ let rec mlexpr_of_symbol = function
let make_prod_item = function
| ExtTerminal s -> <:expr< Tacentries.TacTerm $str:s$ >>
| ExtNonTerminal (g, id) ->
- <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_ident id$ >>
+ <:expr< Tacentries.TacNonTerm $default_loc$ $mlexpr_of_symbol g$ $mlexpr_of_option mlexpr_of_ident id$ >>
let mlexpr_of_clause cl =
mlexpr_of_list (fun (a,_,_) -> mlexpr_of_list make_prod_item a) cl
@@ -87,7 +87,7 @@ let is_constr_gram = function
| _ -> false
let make_var = function
- | ExtNonTerminal (_, p) -> Some p
+ | ExtNonTerminal (_, p) -> p
| _ -> assert false
let declare_tactic loc tacname ~level classification clause = match clause with
@@ -158,10 +158,13 @@ EXTEND
tacargs:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING ->
let () = if s = "" then failwith "Empty terminal." in
ExtTerminal s
diff --git a/grammar/vernacextend.mlp b/grammar/vernacextend.mlp
index 436a7f0d9..7c99b52e8 100644
--- a/grammar/vernacextend.mlp
+++ b/grammar/vernacextend.mlp
@@ -27,7 +27,7 @@ type rule = {
let rec make_let e = function
| [] -> e
- | ExtNonTerminal (g, p) :: l ->
+ | ExtNonTerminal (g, Some p) :: l ->
let t = type_of_user_symbol g in
let loc = MLast.loc_of_expr e in
let e = make_let e l in
@@ -42,7 +42,7 @@ let make_clause { r_patt = pt; r_branch = e; } =
(* To avoid warnings *)
let mk_ignore c pt =
let fold accu = function
- | ExtNonTerminal (_, p) -> p :: accu
+ | ExtNonTerminal (_, Some p) -> p :: accu
| _ -> accu
in
let names = List.fold_left fold [] pt in
@@ -101,10 +101,11 @@ let make_fun_classifiers loc s c l =
let make_prod_item = function
| ExtTerminal s -> <:expr< Egramml.GramTerminal $str:s$ >>
- | ExtNonTerminal (g, id) ->
+ | ExtNonTerminal (g, ido) ->
let nt = type_of_user_symbol g in
let base s = <:expr< Pcoq.genarg_grammar ($mk_extraarg loc s$) >> in
- <:expr< Egramml.GramNonTerminal $default_loc$ $make_rawwit loc nt$
+ let typ = match ido with None -> None | Some _ -> Some nt in
+ <:expr< Egramml.GramNonTerminal $default_loc$ $mlexpr_of_option (make_rawwit loc) typ$
$mlexpr_of_prod_entry_key base g$ >>
let mlexpr_of_clause cl =
@@ -178,10 +179,13 @@ EXTEND
args:
[ [ e = LIDENT; "("; s = LIDENT; ")" ->
let e = parse_user_entry e "" in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
| e = LIDENT; "("; s = LIDENT; ","; sep = STRING; ")" ->
let e = parse_user_entry e sep in
- ExtNonTerminal (e, s)
+ ExtNonTerminal (e, Some s)
+ | e = LIDENT ->
+ let e = parse_user_entry e "" in
+ ExtNonTerminal (e, None)
| s = STRING ->
ExtTerminal s
] ]
diff --git a/parsing/egramml.ml b/parsing/egramml.ml
index 97a3e89a5..984957589 100644
--- a/parsing/egramml.ml
+++ b/parsing/egramml.ml
@@ -17,7 +17,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
| GramNonTerminal :
- Loc.t * 'a raw_abstract_argument_type * ('s, 'a) symbol -> 's grammar_prod_item
+ Loc.t * 'a raw_abstract_argument_type option * ('s, 'a) symbol -> 's grammar_prod_item
type 'a ty_arg = ('a -> raw_generic_argument)
@@ -38,7 +38,7 @@ let rec ty_rule_of_gram = function
AnyTyRule r
| GramNonTerminal (_, t, tok) :: rem ->
let AnyTyRule rem = ty_rule_of_gram rem in
- let inj = Some (fun obj -> Genarg.in_gen t obj) in
+ let inj = Option.map (fun t obj -> Genarg.in_gen t obj) t in
let r = TyNext (rem, tok, inj) in
AnyTyRule r
diff --git a/parsing/egramml.mli b/parsing/egramml.mli
index 1ad947200..29baaf052 100644
--- a/parsing/egramml.mli
+++ b/parsing/egramml.mli
@@ -15,7 +15,7 @@ open Vernacexpr
type 's grammar_prod_item =
| GramTerminal of string
- | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type *
+ | GramNonTerminal : Loc.t * 'a Genarg.raw_abstract_argument_type option *
('s, 'a) Extend.symbol -> 's grammar_prod_item
val extend_vernac_command_grammar :
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index ca5d198c2..d717ed0a5 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -460,7 +460,9 @@ END
let pr_ltac_production_item = function
| Tacentries.TacTerm s -> quote (str s)
-| Tacentries.TacNonTerm (_, (arg, sep), id) ->
+| Tacentries.TacNonTerm (_, (arg, None), None) -> str arg
+| Tacentries.TacNonTerm (_, (arg, Some _), None) -> assert false
+| Tacentries.TacNonTerm (_, (arg, sep), Some id) ->
let sep = match sep with
| None -> mt ()
| Some sep -> str "," ++ spc () ++ quote (str sep)
@@ -470,7 +472,9 @@ let pr_ltac_production_item = function
VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
| [ string(s) ] -> [ Tacentries.TacTerm s ]
| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
- [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), p) ]
+ [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, sep), Some p) ]
+| [ ident(nt) ] ->
+ [ Tacentries.TacNonTerm (loc, (Names.Id.to_string nt, None), None) ]
END
VERNAC COMMAND EXTEND VernacTacticNotation
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index b73b66e56..a61957559 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -51,7 +51,7 @@ let pr_global x = Nametab.pr_global_env Id.Set.empty x
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type grammar_terminals = Genarg.ArgT.any Extend.user_symbol grammar_tactic_prod_item_expr list
@@ -264,8 +264,9 @@ type 'a extra_genarg_printer =
let rec pack prods args = match prods, args with
| [], [] -> []
| TacTerm s :: prods, args -> TacTerm s :: pack prods args
- | TacNonTerm (loc, symb, id) :: prods, arg :: args ->
- TacNonTerm (loc, (symb, arg), id) :: pack prods args
+ | TacNonTerm (_, _, None) :: prods, args -> pack prods args
+ | TacNonTerm (loc, symb, (Some _ as ido)) :: prods, arg :: args ->
+ TacNonTerm (loc, (symb, arg), ido) :: pack prods args
| _ -> raise Not_found
in
let prods = pack pp.pptac_prods l in
diff --git a/plugins/ltac/pptactic.mli b/plugins/ltac/pptactic.mli
index 729338fb9..433f342c4 100644
--- a/plugins/ltac/pptactic.mli
+++ b/plugins/ltac/pptactic.mli
@@ -21,7 +21,7 @@ open Ppextend
type 'a grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type 'a raw_extra_genarg_printer =
(constr_expr -> std_ppcmds) ->
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index 32750383b..91262f6fd 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -21,7 +21,7 @@ open Nameops
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type raw_argument = string * string option
type argument = Genarg.ArgT.any Extend.user_symbol
@@ -174,9 +174,9 @@ let add_tactic_entry (kn, ml, tg) state =
in
let map = function
| TacTerm s -> GramTerminal s
- | TacNonTerm (loc, s, _) ->
+ | TacNonTerm (loc, s, ido) ->
let EntryName (typ, e) = prod_item_of_symbol tg.tacgram_level s in
- GramNonTerminal (loc, typ, e)
+ GramNonTerminal (loc, Option.map (fun _ -> typ) ido, e)
in
let prods = List.map map tg.tacgram_prods in
let rules = make_rule mkact prods in
@@ -202,7 +202,7 @@ let register_tactic_notation_entry name entry =
let interp_prod_item = function
| TacTerm s -> TacTerm s
- | TacNonTerm (loc, (nt, sep), id) ->
+ | TacNonTerm (loc, (nt, sep), ido) ->
let symbol = parse_user_entry nt sep in
let interp s = function
| None ->
@@ -220,7 +220,7 @@ let interp_prod_item = function
end
in
let symbol = interp_entry_name interp symbol in
- TacNonTerm (loc, symbol, id)
+ TacNonTerm (loc, symbol, ido)
let make_fresh_key =
let id = Summary.ref ~name:"TACTIC-NOTATION-COUNTER" 0 in
@@ -296,7 +296,7 @@ let inTacticGrammar : tactic_grammar_obj -> obj =
let cons_production_parameter = function
| TacTerm _ -> None
-| TacNonTerm (_, _, id) -> Some id
+| TacNonTerm (_, _, ido) -> ido
let add_glob_tactic_notation local ~level prods forml ids tac =
let parule = {
@@ -362,7 +362,7 @@ let add_ml_tactic_notation name ~level prods =
let open Tacexpr in
let get_id = function
| TacTerm s -> None
- | TacNonTerm (_, _, id) -> Some id
+ | TacNonTerm (_, _, ido) -> ido
in
let ids = List.map_filter get_id prods in
let entry = { mltac_name = name; mltac_index = len - i - 1 } in
diff --git a/plugins/ltac/tacentries.mli b/plugins/ltac/tacentries.mli
index 069504473..dac62dad3 100644
--- a/plugins/ltac/tacentries.mli
+++ b/plugins/ltac/tacentries.mli
@@ -20,7 +20,7 @@ val register_ltac : locality_flag -> Tacexpr.tacdef_body list -> unit
type 'a grammar_tactic_prod_item_expr = 'a Pptactic.grammar_tactic_prod_item_expr =
| TacTerm of string
-| TacNonTerm of Loc.t * 'a * Names.Id.t
+| TacNonTerm of Loc.t * 'a * Names.Id.t option
type raw_argument = string * string option
(** An argument type as provided in Tactic notations, i.e. a string like
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-17 01:59:43 +0000