From e0380f347d2ebf61b81760a365eea8c84ad3ada4 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 15 Oct 2020 17:39:39 +0200 Subject: [attributes] Allow boolean, single-value attributes. Following discussion in https://github.com/coq/coq/pull/12586 , we extend the syntax `val=string` to support also arbitrary values. In particular we support boolean ones, or arbitrary key-pair lists. This complements the current form `val="string"`, and makes more sense in general. Current syntax for the boolean version is `attr=yes` or `attr=no`, but we could be more liberal if desired. The general new guideline is that `foo(vals)` is reserved for the case where `vals` is a list, whereas `foo=val` is for attributes that allow a unique assignment. This commit only introduces the support, next commits will migrate some attributes to this new syntax and deprecate the old versions. --- vernac/attributes.ml | 93 +++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 81 insertions(+), 12 deletions(-) (limited to 'vernac/attributes.ml') 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] -- cgit v1.2.3 From c609c05cf4a5a2a36ca46a0ea890c954d0ae2a5b Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 12 Nov 2020 20:21:36 +0100 Subject: [attributes] Deprecate `attr(true)` syntax in favor of booelan attributes. We introduce a warning so boolean attributes are expected to be of the form `attr={yes,no}` or just `attr` (for `yes`). We update the documentation, test-suite, and changelog. --- vernac/attributes.ml | 60 ++++++++++++++++++++++++++++++++++++++++------------ 1 file changed, 46 insertions(+), 14 deletions(-) (limited to 'vernac/attributes.ml') diff --git a/vernac/attributes.ml b/vernac/attributes.ml index fd4fe3d47d..04b1f128d3 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -156,12 +156,20 @@ let legacy_bool_attribute ~name ~on ~off : bool option attribute = (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_warning = + CWarnings.create + ~name:"deprecated-attribute-syntax" + ~category:"parsing" + ~default:CWarnings.Enabled + (fun name -> + Pp.(str "Syntax for switching off boolean attributes has been updated, use " ++ str name ++ str "=no instead.")) + 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 *) + deprecated_bool_attribute_warning name; Some v | Some v, None -> Some v | Some v1, Some v2 -> @@ -174,8 +182,16 @@ let deprecated_bool_attribute ~name ~on ~off : bool option attribute = let get_bool_value ~key ~default = function | VernacFlagEmpty -> default - | VernacFlagList [ "true", VernacFlagEmpty ] -> true - | VernacFlagList [ "false", VernacFlagEmpty ] -> false + | VernacFlagList [ "true", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + true + | VernacFlagList [ "false", VernacFlagEmpty ] -> + deprecated_bool_attribute_warning key; + false + | VernacFlagLeaf (FlagIdent "yes") -> + true + | VernacFlagLeaf (FlagIdent "no") -> + false | _ -> user_err Pp.(str "Attribute " ++ str key ++ str " only accepts boolean values.") let enable_attribute ~key ~default : bool attribute = @@ -222,21 +238,37 @@ let () = let open Goptions in let program = enable_attribute ~key:"program" ~default:(fun () -> !program_mode) -let locality = - deprecated_bool_attribute - ~name:"Locality" - ~on:"local" ~off:"global" - -let option_locality = +(* This is a bit complex as the grammar in g_vernac.mlg doesn't + distingish between the boolean and ternary case.*) +let option_locality_parser = let name = "Locality" in attribute_of_list [ - ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal); - ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal); - ("export", single_key_parser ~name ~key:"export" Goptions.OptExport); - ] >>= function + ("local", single_key_parser ~name ~key:"local" Goptions.OptLocal) + ; ("global", single_key_parser ~name ~key:"global" Goptions.OptGlobal) + ; ("export", single_key_parser ~name ~key:"export" Goptions.OptExport) + ] + +let option_locality = + option_locality_parser >>= function | None -> return Goptions.OptDefault | Some l -> return l +(* locality is supposed to be true when local, false when global *) +let locality = + let locality_to_bool = + function + | Goptions.OptLocal -> + true + | Goptions.OptGlobal -> + false + | Goptions.OptExport -> + CErrors.user_err Pp.(str "export attribute not supported here") + | Goptions.OptDefault -> + CErrors.user_err Pp.(str "default attribute not supported here") + in + option_locality_parser >>= function l -> + return (Option.map locality_to_bool l) + let ukey = "universes" let universe_polymorphism_option_name = ["Universe"; "Polymorphism"] @@ -287,7 +319,7 @@ let only_polymorphism atts = parse polymorphic atts let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty] -let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty] +let vernac_monomorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagLeaf (FlagIdent "no")] let canonical_field = enable_attribute ~key:"canonical" ~default:(fun () -> true) -- cgit v1.2.3 From efa6673158f5eaa3fc11c0b3d1e3285c4acc129a Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Mon, 16 Nov 2020 16:18:06 +0100 Subject: [attributes] Add output test suite for errors, improve error printing. --- vernac/attributes.ml | 9 +++++++-- 1 file changed, 7 insertions(+), 2 deletions(-) (limited to 'vernac/attributes.ml') diff --git a/vernac/attributes.ml b/vernac/attributes.ml index 04b1f128d3..fdaeedef8c 100644 --- a/vernac/attributes.ml +++ b/vernac/attributes.ml @@ -121,6 +121,9 @@ let single_key_parser ~name ~key v prev args = assert_once ~name prev; v +let pr_possible_values ~values = + Pp.(str "{" ++ prlist_with_sep pr_comma str (List.map fst values) ++ str "}") + (** [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)] *) @@ -135,13 +138,15 @@ let key_value_attribute ~key ~default ~(values : (string * 'a) list) : 'a option | 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))) + str "use one of " ++ pr_possible_values ~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.") + CErrors.user_err + Pp.(str "Invalid syntax " ++ pr_vernac_flag (key, err) ++ str ", try " + ++ str key ++ str "=" ++ pr_possible_values ~values ++ str " instead.") end in attribute_of_list [key, parser] -- cgit v1.2.3