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 ++++++++++++++++++++++++++++++++++++++++++-------
 vernac/attributes.mli   | 26 +++++++++++---
 vernac/g_vernac.mlg     |  3 +-
 vernac/ppvernac.ml      | 12 +------
 vernac/vernacentries.ml | 10 ++++--
 5 files changed, 113 insertions(+), 31 deletions(-)

(limited to 'vernac')

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
-- 
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 +++++++++++++++++++++++++++++++++++++++------------
 vernac/attributes.mli |  7 +++---
 vernac/g_vernac.mlg   |  2 +-
 3 files changed, 50 insertions(+), 19 deletions(-)

(limited to 'vernac')

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)
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 60195fe790..03a14a03ff 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -88,7 +88,7 @@ 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. *)
 
-(** Define boolean attribute [name], of the form [name={on,off}]. The
+(** Define boolean attribute [name], of the form [name={yes,no}]. The
    attribute may only be set once for a command. *)
 val bool_attribute : name:string -> bool option attribute
 
@@ -99,9 +99,8 @@ val deprecated_bool_attribute
   -> 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. *)
+   be set once for a command; this attribute both accepts the old [on]
+   [off] syntax and new attribute syntax [on=yes] [on=no] *)
 
 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 d9b664e243..116cfc6413 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -137,7 +137,7 @@ GRAMMAR EXTEND Gram
       | IDENT "Cumulative" ->
         { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
       | IDENT "NonCumulative" ->
-        { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+        { ("universes", VernacFlagList ["cumulative", VernacFlagLeaf (FlagIdent "no")]) }
       | IDENT "Private" ->
         { ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
       | IDENT "Program" ->
-- 
cgit v1.2.3


From 6aeee2e4e37d4b8ffb8c50c109903ad336c8bdfa Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias
Date: Sun, 15 Nov 2020 15:57:37 +0100
Subject: [attributes] Update error message referring to deprecated syntax.

---
 vernac/vernacentries.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'vernac')

diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2edd9d4d11..0f63dfe5ce 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -674,7 +674,7 @@ let is_polymorphic_inductive_cumulativity =
 let polymorphic_cumulative =
   let error_poly_context () =
     user_err
-      Pp.(str "The cumulative and noncumulative attributes can only be used in a polymorphic context.");
+      Pp.(str "The cumulative attribute can only be used in a polymorphic context.");
   in
   let open Attributes in
   let open Notations in
-- 
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')

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