diff options
| -rw-r--r-- | vernac/attributes.ml | 93 | ||||
| -rw-r--r-- | vernac/attributes.mli | 26 | ||||
| -rw-r--r-- | vernac/g_vernac.mlg | 3 | ||||
| -rw-r--r-- | vernac/ppvernac.ml | 12 | ||||
| -rw-r--r-- | vernac/vernacentries.ml | 10 |
5 files changed, 113 insertions, 31 deletions
diff --git a/vernac/attributes.ml b/vernac/attributes.ml index efba6d332a..fd4fe3d47d 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -11,13 +11,29 @@ open CErrors (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +let pr_vernac_flag_leaf = function + | FlagIdent b -> Pp.str b + | FlagString s -> Pp.(quote (str s)) + +let rec pr_vernac_flag_value = let open Pp in function + | VernacFlagEmpty -> mt () + | VernacFlagLeaf l -> str "=" ++ pr_vernac_flag_leaf l + | VernacFlagList s -> surround (prlist_with_sep pr_comma pr_vernac_flag s) +and pr_vernac_flag (s, arguments) = + let open Pp in + str s ++ (pr_vernac_flag_value arguments) + let warn_unsupported_attributes = CWarnings.create ~name:"unsupported-attributes" ~category:"parsing" ~default:CWarnings.AsError (fun atts -> @@ -105,9 +121,54 @@ let single_key_parser ~name ~key v prev args = assert_once ~name prev; v -let bool_attribute ~name ~on ~off : bool option attribute = - attribute_of_list [(on, single_key_parser ~name ~key:on true); - (off, single_key_parser ~name ~key:off false)] +(** [key_value_attribute ~key ~default ~values] parses a attribute [key=value] + with possible [key] [value] in [values], [default] is for compatibility for users + doing [qualif(key)] which is parsed as [qualif(key=default)] *) +let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option attribute = + let parser = function + | Some v -> + CErrors.user_err Pp.(str "key '" ++ str key ++ str "' has been already set.") + | None -> + begin function + | VernacFlagLeaf (FlagIdent b) -> + begin match CList.assoc_f String.equal b values with + | exception Not_found -> + CErrors.user_err + Pp.(str "Invalid value '" ++ str b ++ str "' for key " ++ str key ++ fnl () ++ + str "use one of " ++ (pr_sequence str (List.map fst values))) + | value -> value + end + | VernacFlagEmpty -> + default + | err -> + CErrors.user_err Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try " ++ str key ++ str "=value instead.") + end + in + attribute_of_list [key, parser] + +let bool_attribute ~name : bool option attribute = + let values = ["yes", true; "no", false] in + key_value_attribute ~key:name ~default:true ~values + +let legacy_bool_attribute ~name ~on ~off : bool option attribute = + attribute_of_list + [(on, single_key_parser ~name ~key:on true); + (off, single_key_parser ~name ~key:off false)] + +(* important note: we use on as the default for the new bool_attribute ! *) +let deprecated_bool_attribute ~name ~on ~off : bool option attribute = + bool_attribute ~name:on ++ legacy_bool_attribute ~name ~on ~off |> map (function + | None, None -> + None + | None, Some v -> + (* Will insert deprecation warning *) + Some v + | Some v, None -> Some v + | Some v1, Some v2 -> + CErrors.user_err + Pp.(str "attribute " ++ str name ++ + str ": cannot specify legacy and modern syntax at the same time.") + ) (* Variant of the [bool] attribute with only two values (bool has three). *) let get_bool_value ~key ~default = @@ -161,7 +222,10 @@ let () = let open Goptions in let program = enable_attribute ~key:"program" ~default:(fun () -> !program_mode) -let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global" +let locality = + deprecated_bool_attribute + ~name:"Locality" + ~on:"local" ~off:"global" let option_locality = let name = "Locality" in @@ -188,12 +252,17 @@ let is_universe_polymorphism = fun () -> !b let polymorphic_base = - bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" >>= function + deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" >>= function | Some b -> return b | None -> return (is_universe_polymorphism()) let template = - qualify_attribute ukey (bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate") + qualify_attribute ukey + (deprecated_bool_attribute + ~name:"Template" + ~on:"template" ~off:"notemplate") let polymorphic = qualify_attribute ukey polymorphic_base @@ -201,12 +270,12 @@ let polymorphic = let deprecation_parser : Deprecation.t key_parser = fun orig args -> assert_once ~name:"deprecation" orig; match args with - | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ] - | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ; "note", VernacFlagLeaf (FlagString note) ] + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ; "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since ~note () - | VernacFlagList [ "since", VernacFlagLeaf since ] -> + | VernacFlagList [ "since", VernacFlagLeaf (FlagString since) ] -> Deprecation.make ~since () - | VernacFlagList [ "note", VernacFlagLeaf note ] -> + | VernacFlagList [ "note", VernacFlagLeaf (FlagString note) ] -> Deprecation.make ~note () | _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute") @@ -228,7 +297,7 @@ let canonical_instance = let uses_parser : string key_parser = fun orig args -> assert_once ~name:"using" orig; match args with - | VernacFlagLeaf str -> str + | VernacFlagLeaf (FlagString str) -> str | _ -> CErrors.user_err (Pp.str "Ill formed \"using\" attribute") let using = attribute_of_list ["using",uses_parser] diff --git a/vernac/attributes.mli b/vernac/attributes.mli index 1969665082..60195fe790 100644 --- a/vernac/attributes.mli +++ b/vernac/attributes.mli @@ -9,13 +9,19 @@ (************************************************************************) (** The type of parsing attribute data *) +type vernac_flag_type = + | FlagIdent of string + | FlagString of string + type vernac_flags = vernac_flag list and vernac_flag = string * vernac_flag_value and vernac_flag_value = | VernacFlagEmpty - | VernacFlagLeaf of string + | VernacFlagLeaf of vernac_flag_type | VernacFlagList of vernac_flags +val pr_vernac_flag : vernac_flag -> Pp.t + type +'a attribute (** The type of attributes. When parsing attributes if an ['a attribute] is present then an ['a] value will be produced. @@ -82,10 +88,20 @@ val attribute_of_list : (string * 'a key_parser) list -> 'a option attribute (** Make an attribute from a list of key parsers together with their associated key. *) -val bool_attribute : name:string -> on:string -> off:string -> bool option attribute -(** Define boolean attribute [name] with value [true] when [on] is - provided and [false] when [off] is provided. The attribute may only - be set once for a command. *) +(** Define boolean attribute [name], of the form [name={on,off}]. The + attribute may only be set once for a command. *) +val bool_attribute : name:string -> bool option attribute + +val deprecated_bool_attribute + : name:string + -> on:string + -> off:string + -> bool option attribute +(** Define boolean attribute [name] with will be set when [on] is + provided and unset when [off] is provided. The attribute may only + be set once for a command; this attribute both accepts the old + [name(on)] [name(off)] and new attribute syntax, with [on] taken as + the key. *) val qualify_attribute : string -> 'a attribute -> 'a attribute (** [qualified_attribute qual att] treats [#[qual(atts)]] like [att] diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg index 1aff76114b..d9b664e243 100644 --- a/vernac/g_vernac.mlg +++ b/vernac/g_vernac.mlg @@ -119,7 +119,8 @@ GRAMMAR EXTEND Gram ] ; attr_value: - [ [ "=" ; v = string -> { VernacFlagLeaf v } + [ [ "=" ; v = string -> { VernacFlagLeaf (FlagString v) } + | "=" ; v = IDENT -> { VernacFlagLeaf (FlagIdent v) } | "(" ; a = attribute_list ; ")" -> { VernacFlagList a } | -> { VernacFlagEmpty } ] ] diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml index 442269ebda..4cee4f7a47 100644 --- a/vernac/ppvernac.ml +++ b/vernac/ppvernac.ml @@ -1331,20 +1331,10 @@ let pr_control_flag (p : control_flag) = let pr_vernac_control flags = Pp.prlist pr_control_flag flags -let rec pr_vernac_flag (k, v) = - let k = keyword k in - let open Attributes in - match v with - | VernacFlagEmpty -> k - | VernacFlagLeaf v -> k ++ str " = " ++ qs v - | VernacFlagList m -> k ++ str "( " ++ pr_vernac_flags m ++ str " )" -and pr_vernac_flags m = - prlist_with_sep (fun () -> str ", ") pr_vernac_flag m - let pr_vernac_attributes = function | [] -> mt () - | flags -> str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut () + | flags -> str "#[" ++ prlist_with_sep pr_comma Attributes.pr_vernac_flag flags ++ str "]" ++ cut () let pr_vernac ({v = {control; attrs; expr}} as v) = tag_vernac v diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml index 4e52af7959..2edd9d4d11 100644 --- a/vernac/vernacentries.ml +++ b/vernac/vernacentries.ml @@ -678,9 +678,15 @@ let polymorphic_cumulative = in let open Attributes in let open Notations in + (* EJGA: this seems redudant with code in attributes.ml *) qualify_attribute "universes" - (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic" - ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative") + (deprecated_bool_attribute + ~name:"Polymorphism" + ~on:"polymorphic" ~off:"monomorphic" + ++ + deprecated_bool_attribute + ~name:"Cumulativity" + ~on:"cumulative" ~off:"noncumulative") >>= function | Some poly, Some cum -> (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive |