[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.

1 files changed, 81 insertions, 12 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]