From 1248aed77ee36778cd440c14c4550dc97f78520b Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Wed, 20 Nov 2019 16:27:09 +0100 Subject: make VernacArguments closer to user syntax ie keep the fake arguments "/" and "&" instead of getting their index at parsing time. --- vernac/comArguments.ml | 19 ++++++++++++++++++- vernac/comArguments.mli | 2 -- vernac/g_vernac.mlg | 31 +++++++------------------------ vernac/ppvernac.ml | 22 ++++++++-------------- vernac/prettyp.ml | 26 ++++++++++++++++++++++++-- vernac/vernacentries.ml | 4 ++-- vernac/vernacexpr.ml | 8 +++++--- 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 -- cgit v1.2.3