aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--vernac/comArguments.ml19
-rw-r--r--vernac/comArguments.mli2
-rw-r--r--vernac/g_vernac.mlg31
-rw-r--r--vernac/ppvernac.ml22
-rw-r--r--vernac/prettyp.ml26
-rw-r--r--vernac/vernacentries.ml4
-rw-r--r--vernac/vernacexpr.ml8
7 files changed, 64 insertions, 48 deletions
diff --git a/vernac/comArguments.ml b/vernac/comArguments.ml
index 737e0427ec..15077298aa 100644
--- a/vernac/comArguments.ml
+++ b/vernac/comArguments.ml
@@ -60,7 +60,7 @@ let warn_arguments_assert =
(* [nargs_for_red] is the number of arguments required to trigger reduction,
[args] is the main list of arguments statuses,
[more_implicits] is a list of extra lists of implicit statuses *)
-let vernac_arguments ~section_local reference args more_implicits nargs_for_red nargs_before_bidi flags =
+let vernac_arguments ~section_local reference args more_implicits flags =
let env = Global.env () in
let sigma = Evd.from_env env in
let assert_flag = List.mem `Assert flags in
@@ -83,6 +83,23 @@ let vernac_arguments ~section_local reference args more_implicits nargs_for_red
if clear_implicits_flag && default_implicits_flag then
err_incompat "clear implicits" "default implicits";
+ let args, nargs_for_red, nargs_before_bidi, _i =
+ List.fold_left (fun (args,red,bidi,i) arg ->
+ match arg with
+ | RealArg arg -> (arg::args,red,bidi,i+1)
+ | VolatileArg ->
+ if Option.has_some red
+ then CErrors.user_err Pp.(str "The \"/\" modifier may only occur once.");
+ (args,Some i,bidi,i)
+ | BidiArg ->
+ if Option.has_some bidi
+ then CErrors.user_err Pp.(str "The \"&\" modifier may only occur once.");
+ (args,red,Some i,i))
+ ([],None,None,0)
+ args
+ in
+ let args = List.rev args in
+
let sr = smart_global reference in
let inf_names =
let ty, _ = Typeops.type_of_global_in_context env sr in
diff --git a/vernac/comArguments.mli b/vernac/comArguments.mli
index f78e01a11f..71effddf67 100644
--- a/vernac/comArguments.mli
+++ b/vernac/comArguments.mli
@@ -13,7 +13,5 @@ val vernac_arguments
-> Libnames.qualid Constrexpr.or_by_notation
-> Vernacexpr.vernac_argument_status list
-> (Names.Name.t * Impargs.implicit_kind) list list
- -> int option
- -> int option
-> Vernacexpr.arguments_modifier list
-> unit
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index a78f4645c2..36b6cd8e9d 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -786,25 +786,8 @@ GRAMMAR EXTEND Gram
];
mods = OPT [ ":"; l = LIST1 arguments_modifier SEP "," -> { l } ] ->
{ let mods = match mods with None -> [] | Some l -> List.flatten l in
- let slash_position = ref None in
- let ampersand_position = ref None in
- let rec parse_args i = function
- | [] -> []
- | `Id x :: args -> x :: parse_args (i+1) args
- | `Slash :: args ->
- if Option.is_empty !slash_position then
- (slash_position := Some i; parse_args i args)
- else
- user_err Pp.(str "The \"/\" modifier can occur only once")
- | `Ampersand :: args ->
- if Option.is_empty !ampersand_position then
- (ampersand_position := Some i; parse_args i args)
- else
- user_err Pp.(str "The \"&\" modifier can occur only once")
- in
- let args = parse_args 0 (List.flatten args) in
let more_implicits = Option.default [] more_implicits in
- VernacArguments (qid, args, more_implicits, !slash_position, !ampersand_position, mods) }
+ VernacArguments (qid, List.flatten args, more_implicits, mods) }
| IDENT "Implicit"; "Type"; bl = reserv_list ->
{ VernacReserve bl }
@@ -848,17 +831,17 @@ GRAMMAR EXTEND Gram
argument_spec_block: [
[ item = argument_spec ->
{ let name, recarg_like, notation_scope = item in
- [`Id { name=name; recarg_like=recarg_like;
+ [RealArg { name=name; recarg_like=recarg_like;
notation_scope=notation_scope;
implicit_status = NotImplicit}] }
- | "/" -> { [`Slash] }
- | "&" -> { [`Ampersand] }
+ | "/" -> { [VolatileArg] }
+ | "&" -> { [BidiArg] }
| "("; items = LIST1 argument_spec; ")"; sc = OPT scope_delimiter ->
{ let f x = match sc, x with
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = NotImplicit}) items }
| "["; items = LIST1 argument_spec; "]"; sc = OPT scope_delimiter ->
@@ -866,7 +849,7 @@ GRAMMAR EXTEND Gram
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = Implicit}) items }
| "{"; items = LIST1 argument_spec; "}"; sc = OPT scope_delimiter ->
@@ -874,7 +857,7 @@ GRAMMAR EXTEND Gram
| None, x -> x | x, None -> Option.map (fun y -> CAst.make ~loc y) x
| Some _, Some _ -> user_err Pp.(str "scope declared twice") in
List.map (fun (name,recarg_like,notation_scope) ->
- `Id { name=name; recarg_like=recarg_like;
+ RealArg { name=name; recarg_like=recarg_like;
notation_scope=f notation_scope;
implicit_status = MaximallyImplicit}) items }
]
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 3dbf7afb78..ebdadc0865 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1068,7 +1068,7 @@ let string_of_definition_object_kind = let open Decls in function
| Some Flags.Current -> [SetOnlyParsing]
| Some v -> [SetCompatVersion v]))
)
- | VernacArguments (q, args, more_implicits, nargs, nargs_before_bidi, mods) ->
+ | VernacArguments (q, args, more_implicits, mods) ->
return (
hov 2 (
keyword "Arguments" ++ spc() ++
@@ -1079,28 +1079,22 @@ let string_of_definition_object_kind = let open Decls in function
| Impargs.Implicit -> str "[" ++ x ++ str "]"
| Impargs.MaximallyImplicit -> str "{" ++ x ++ str "}"
| Impargs.NotImplicit -> x in
- let rec print_arguments n nbidi l =
- match n, nbidi, l with
- | Some 0, _, l -> spc () ++ str"/" ++ print_arguments None nbidi l
- | _, Some 0, l -> spc () ++ str"&" ++ print_arguments n None l
- | None, None, [] -> mt()
- | _, _, [] ->
- let dummy = {name=Anonymous; recarg_like=false;
- notation_scope=None; implicit_status=Impargs.NotImplicit}
- in
- print_arguments n nbidi [dummy]
- | n, nbidi, { name = id; recarg_like = k;
+ let rec print_arguments = function
+ | [] -> mt()
+ | VolatileArg :: l -> spc () ++ str"/" ++ print_arguments l
+ | BidiArg :: l -> spc () ++ str"&" ++ print_arguments l
+ | RealArg { name = id; recarg_like = k;
notation_scope = s;
implicit_status = imp } :: tl ->
spc() ++ pr_br imp (pr_if k (str"!") ++ Name.print id ++ pr_s s) ++
- print_arguments (Option.map pred n) (Option.map pred nbidi) tl
+ print_arguments tl
in
let rec print_implicits = function
| [] -> mt ()
| (name, impl) :: rest ->
spc() ++ pr_br impl (Name.print name) ++ print_implicits rest
in
- print_arguments nargs nargs_before_bidi args ++
+ print_arguments args ++
if not (List.is_empty more_implicits) then
prlist (fun l -> str"," ++ print_implicits l) more_implicits
else (mt ()) ++
diff --git a/vernac/prettyp.ml b/vernac/prettyp.ml
index 5ebc89892c..ea49cae9db 100644
--- a/vernac/prettyp.ml
+++ b/vernac/prettyp.ml
@@ -259,6 +259,13 @@ let implicit_kind_of_status = function
| None -> Anonymous, NotImplicit
| Some (id,_,(maximal,_)) -> Name id, if maximal then MaximallyImplicit else Implicit
+let dummy = {
+ Vernacexpr.implicit_status = NotImplicit;
+ name = Anonymous;
+ recarg_like = false;
+ notation_scope = None;
+}
+
let is_dummy {Vernacexpr.implicit_status; name; recarg_like; notation_scope} =
name = Anonymous && not recarg_like && notation_scope = None && implicit_status = NotImplicit
@@ -287,6 +294,20 @@ let rec main_implicits i renames recargs scopes impls =
then [] (* we may have a trail of dummies due to eg "clear scopes" *)
else status :: rest
+let rec insert_fake_args volatile bidi impls =
+ let open Vernacexpr in
+ match volatile, bidi with
+ | Some 0, _ -> VolatileArg :: insert_fake_args None bidi impls
+ | _, Some 0 -> BidiArg :: insert_fake_args volatile None impls
+ | None, None -> List.map (fun a -> RealArg a) impls
+ | _, _ ->
+ let hd, tl = match impls with
+ | impl :: impls -> impl, impls
+ | [] -> dummy, []
+ in
+ let f = Option.map pred in
+ RealArg hd :: insert_fake_args (f volatile) (f bidi) tl
+
let print_arguments ref =
let qid = Nametab.shortest_qualid_of_global Id.Set.empty ref in
let flags, recargs, nargs_for_red =
@@ -312,12 +333,13 @@ let print_arguments ref =
let impls = main_implicits 0 renames recargs scopes impls in
let moreimpls = List.map (fun (_,i) -> List.map implicit_kind_of_status i) moreimpls in
let bidi = Pretyping.get_bidirectionality_hint ref in
- if impls = [] && moreimpls = [] && nargs_for_red = None && bidi = None && flags = [] then []
+ let impls = insert_fake_args nargs_for_red bidi impls in
+ if impls = [] && moreimpls = [] && flags = [] then []
else
let open Constrexpr in
let open Vernacexpr in
[Ppvernac.pr_vernac_expr
- (VernacArguments (CAst.make (AN qid), impls, moreimpls, nargs_for_red, bidi, flags))]
+ (VernacArguments (CAst.make (AN qid), impls, moreimpls, flags))]
let print_name_infos ref =
let type_info_for_implicit =
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 128c30908b..4569da5bd5 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2167,10 +2167,10 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
vernac_hints ~atts dbnames hints)
| VernacSyntacticDefinition (id,c,b) ->
VtDefault(fun () -> vernac_syntactic_definition ~atts id c b)
- | VernacArguments (qid, args, more_implicits, nargs, bidi, flags) ->
+ | VernacArguments (qid, args, more_implicits, flags) ->
VtDefault(fun () ->
with_section_locality ~atts
- (ComArguments.vernac_arguments qid args more_implicits nargs bidi flags))
+ (ComArguments.vernac_arguments qid args more_implicits flags))
| VernacReserve bl ->
VtDefault(fun () ->
unsupported_attributes atts;
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 564c55670d..ce96d9265c 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -250,13 +250,17 @@ type vernac_cumulative = VernacCumulative | VernacNonCumulative
(** {6 The type of vernacular expressions} *)
-type vernac_argument_status = {
+type vernac_one_argument_status = {
name : Name.t;
recarg_like : bool;
notation_scope : string CAst.t option;
implicit_status : Impargs.implicit_kind;
}
+type vernac_argument_status =
+ | VolatileArg | BidiArg
+ | RealArg of vernac_one_argument_status
+
type arguments_modifier =
[ `Assert
| `ClearBidiHint
@@ -383,8 +387,6 @@ type nonrec vernac_expr =
qualid or_by_notation *
vernac_argument_status list (* Main arguments status list *) *
(Name.t * Impargs.implicit_kind) list list (* Extra implicit status lists *) *
- int option (* Number of args to trigger reduction *) *
- int option (* Number of args before bidirectional typing *) *
arguments_modifier list
| VernacReserve of simple_binder list
| VernacGeneralizable of (lident list) option
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:11:47 +0000