Merge PR #7920: Generic syntax for attributes

12 files changed, 211 insertions, 58 deletions

diff --git a/CHANGES b/CHANGES
index 689c1eff6..6dce7b0db 100644
--- a/CHANGES
+++ b/CHANGES
@@ -68,6 +68,8 @@ Vernacular Commands
 - New Set Hint Variables/Constants Opaque/Transparent commands for setting
   globally the opacity flag of variables and constants in hint databases,
   overwritting the opacity set of the hint database.
+- Added generic syntax for “attributes”, as in:
+  `#[local] Lemma foo : bar.`
 
 Coq binaries and process model
 
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index e13625286..ac6a20198 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -103,7 +103,7 @@ Special tokens
     ! % & && ( () ) * + ++ , - -> . .( ..
     / /\ : :: :< := :> ; < <- <-> <: <= <> =
     => =_D > >-> >= ? ?= @ [ \/ ] ^ { | |-
-    || } ~
+    || } ~ #[
 
   Lexical ambiguities are resolved according to the “longest match”
   rule: when a sequence of non alphanumerical characters can be
@@ -495,6 +495,7 @@ The Vernacular
 ==============
 
 .. productionlist:: coq
+   decorated-sentence : [`decoration`] `sentence`
    sentence           : `assumption`
                       : | `definition`
                       : | `inductive`
@@ -523,6 +524,11 @@ The Vernacular
    proof              : Proof . … Qed .
                       : | Proof . … Defined .
                       : | Proof . … Admitted .
+   decoration : #[ `attributes` ]
+   attributes : [`attribute`, … , `attribute`]
+   attribute :  `ident`
+   :| `ident` = `string`
+   :| `ident` ( `attributes` )
 
 .. todo:: This use of … in this grammar is inconsistent
           What about removing the proof part of this grammar from this chapter
@@ -534,6 +540,9 @@ commands of Gallina. A sentence of the vernacular language, like in
 many natural languages, begins with a capital letter and ends with a
 dot.
 
+Sentences may be *decorated* with so-called *attributes*,
+which are described in the corresponding section (:ref:`gallina-attributes`).
+
 The different kinds of command are described hereafter. They all suppose
 that the terms occurring in the sentences are well-typed.
 
@@ -1388,3 +1397,53 @@ using the keyword :cmd:`Qed`.
 .. [2]
    Except if the inductive type is empty in which case there is no
    equation that can be used to infer the return type.
+
+.. _gallina-attributes:
+
+Attributes
+-----------
+
+Any vernacular command can be decorated with a list of attributes, enclosed
+between ``#[`` (hash and opening square bracket) and ``]`` (closing square bracket)
+and separated by commas ``,``.
+
+Each attribute has a name (an identifier) and may have a value.
+A value is either a :token:`string` (in which case it is specified with an equal ``=`` sign),
+or a list of attributes, enclosed within brackets.
+
+Currently,
+the following attributes names are recognized:
+
+``monomorphic``, ``polymorphic``
+    Take no value, analogous to the ``Monomorphic`` and ``Polymorphic`` flags
+    (see :ref:`polymorphicuniverses`).
+
+``program``
+    Takes no value, analogous to the ``Program`` flag
+    (see :ref:`programs`).
+
+``global``, ``local``
+    Take no value, analogous to the ``Global`` and ``Local`` flags
+    (see :ref:`controlling-locality-of-commands`).
+
+``deprecated``
+    Takes as value the optional attributes ``since`` and ``note``;
+    both have a string value.
+
+Here are a few examples:
+
+.. coqtop:: all reset
+
+        From Coq Require Program.
+        #[program] Definition one : nat := S _.
+        Next Obligation.
+          exact O.
+        Defined.
+
+        #[deprecated(since="8.9.0", note="use idtac instead")]
+        Ltac foo := idtac.
+
+        Goal True.
+        Proof.
+          now foo.
+        Abort.
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index e01dcbcb6..6be80d29a 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -199,11 +199,8 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly = List.fold_left (fun poly f ->
-          match f with
-          | VernacPolymorphic b -> b
-          | (VernacProgram | VernacLocal _) -> poly
-        ) poly f in
+      let _, atts = Vernacentries.attributes_of_flags f Vernacinterp.(mk_atts ~polymorphic:poly ()) in
+      let poly = atts.Vernacinterp.polymorphic in
       static_classifier ~poly e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
diff --git a/test-suite/success/attribute-syntax.v b/test-suite/success/attribute-syntax.v
new file mode 100644
index 000000000..83fb3d0c8
--- /dev/null
+++ b/test-suite/success/attribute-syntax.v
@@ -0,0 +1,23 @@
+From Coq Require Program.
+
+Section Scope.
+
+#[local] Coercion nat_of_bool (b: bool) : nat :=
+  if b then 0 else 1.
+
+Check (refl_equal : true = 0 :> nat).
+
+End Scope.
+
+Fail Check 0 = true :> nat.
+
+#[polymorphic]
+Definition ι T (x: T) := x.
+
+Check ι _ ι.
+
+#[program]
+Fixpoint f (n: nat) {wf lt n} : nat := _.
+
+#[deprecated(since="8.9.0")]
+Ltac foo := foo.
diff --git a/vernac/class.ml b/vernac/class.ml
index 133726702..e425e6474 100644
--- a/vernac/class.ml
+++ b/vernac/class.ml
@@ -303,12 +303,12 @@ let try_add_new_coercion_with_source ref ~local poly ~source =
   try_add_new_coercion_core ref ~local poly (Some source) None false
 
 let add_coercion_hook poly local ref =
-  let stre = match local with
+  let local = match local with
+  | Discharge
   | Local -> true
   | Global -> false
-  | Discharge -> assert false
   in
-  let () = try_add_new_coercion ref ~local:stre poly in
+  let () = try_add_new_coercion ref ~local poly in
   let msg = pr_global_env Id.Set.empty ref ++ str " is now a coercion" in
   Flags.if_verbose Feedback.msg_info msg
 
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 3a01ce6df..e9d6ed9f6 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -79,27 +79,50 @@ GRAMMAR EXTEND Gram
       | IDENT "Redirect"; s = ne_string; c = located_vernac -> { VernacRedirect (s, c) }
       | IDENT "Timeout"; n = natural; v = vernac_control -> { VernacTimeout(n,v) }
       | IDENT "Fail"; v = vernac_control -> { VernacFail v }
-      | v = vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+      | v = decorated_vernac -> { let (f, v) = v in VernacExpr(f, v) } ]
+    ]
+  ;
+  decorated_vernac:
+    [ [ a = attributes ; fv = vernac -> { let (f, v) = fv in (List.append a f, v) }
+      | fv = vernac -> { fv } ]
+    ]
+  ;
+  attributes:
+    [ [ "#[" ; a = attribute_list ; "]" -> { a } ]
+    ]
+  ;
+  attribute_list:
+    [ [ a = LIST0 attribute SEP "," -> { a } ]
+    ]
+  ;
+  attribute:
+    [ [ k = ident ; v = attribute_value -> { Names.Id.to_string k, v } ]
+    ]
+  ;
+  attribute_value:
+    [ [ "=" ; v = string -> { VernacFlagLeaf v }
+      | "(" ; a = attribute_list ; ")" -> { VernacFlagList a }
+      | -> { VernacFlagEmpty } ]
     ]
   ;
   vernac:
-    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (VernacLocal true :: f, v) }
-      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (VernacLocal false :: f, v) }
+    [ [ IDENT "Local"; v = vernac_poly -> { let (f, v) = v in (("local", VernacFlagEmpty) :: f, v) }
+      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in (("global", VernacFlagEmpty) :: f, v) }
 
       | v = vernac_poly -> { v } ]
     ]
   ;
   vernac_poly:
-    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic true :: f, v) }
-      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (VernacPolymorphic false :: f, v) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux -> { let (f, v) = v in (("polymorphic", VernacFlagEmpty) :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in (("monomorphic", VernacFlagEmpty) :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
   vernac_aux:
     (* Better to parse "." here: in case of failure (e.g. in coerce_to_var), *)
     (* "." is still in the stream and discard_to_dot works correctly         *)
-    [ [ IDENT "Program"; g = gallina; "." -> { ([VernacProgram], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { ([VernacProgram], g) }
+    [ [ IDENT "Program"; g = gallina; "." -> { (["program", VernacFlagEmpty], g) }
+      | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) }
       | g = gallina; "." -> { ([], g) }
       | g = gallina_ext; "." -> { ([], g) }
       | c = command; "." -> { ([], c) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5fbe1f4e4..e5547d9b7 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -153,8 +153,6 @@ open Pputils
       | SearchAbout sl ->
          keyword "Search" ++ spc() ++ prlist_with_sep spc pr_search_about sl ++ pr_in_out_modules b
 
-  let pr_locality local = if local then keyword "Local" else keyword "Global"
-
   let pr_option_ref_value = function
     | QualidRefValue id -> pr_qualid id
     | StringRefValue s -> qs s
@@ -1195,21 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
-let pr_vernac_flag =
+let rec pr_vernac_flag (k, v) =
+  let k = keyword k 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
-  | VernacPolymorphic true -> keyword "Polymorphic"
-  | VernacPolymorphic false -> keyword "Monomorphic"
-  | VernacProgram -> keyword "Program"
-  | VernacLocal local -> pr_locality local
+  | [] -> mt ()
+  | flags ->  str "#[" ++ pr_vernac_flags flags ++ str "]" ++ cut ()
 
   let rec pr_vernac_control v =
     let return = tag_vernac v in
     match v with
-    | VernacExpr (f, v') ->
-      List.fold_right
-        (fun f a -> pr_vernac_flag f ++ spc() ++ a)
-        f
-        (pr_vernac_expr v' ++ sep_end v')
+    | VernacExpr (f, v') -> pr_vernac_attributes f ++ pr_vernac_expr v' ++ sep_end v'
     | VernacTime (_,{v}) ->
       return (keyword "Time" ++ spc() ++ pr_vernac_control v)
     | VernacRedirect (s, {v}) ->
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 5fda1a0da..27f2a740e 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2319,32 +2319,62 @@ let with_fail st b f =
       | _ -> assert false
   end
 
+let attributes_of_flags f atts =
+  let assert_empty k v =
+    if v <> VernacFlagEmpty
+    then user_err Pp.(str "Attribute " ++ str k ++ str " does not accept arguments")
+  in
+  List.fold_left
+    (fun (polymorphism, atts) (k, v) ->
+       match k with
+       | "program" when not atts.program ->
+         assert_empty k v;
+         (polymorphism, { atts with program = true })
+       | "program" ->
+         user_err Pp.(str "Program mode specified twice")
+       | "polymorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some true, atts)
+       | "monomorphic" when polymorphism = None ->
+         assert_empty k v;
+         (Some false, atts)
+       | ("polymorphic" | "monomorphic") ->
+         user_err Pp.(str "Polymorphism specified twice")
+       | "local" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some true })
+       | "global" when Option.is_empty atts.locality ->
+         assert_empty k v;
+         (polymorphism, { atts with locality = Some false })
+       | ("local" | "global") ->
+         user_err Pp.(str "Locality specified twice")
+       | "deprecated" when Option.is_empty atts.deprecated ->
+           begin match v with
+             | VernacFlagList [ "since", VernacFlagLeaf since ; "note", VernacFlagLeaf note ]
+             | VernacFlagList [ "note", VernacFlagLeaf note ; "since", VernacFlagLeaf since ] ->
+               let since = Some since and note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ~note ()) })
+             | VernacFlagList [ "since", VernacFlagLeaf since ] ->
+               let since = Some since in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~since ()) })
+             | VernacFlagList [ "note", VernacFlagLeaf note ] ->
+               let note = Some note in
+               (polymorphism, { atts with deprecated = Some (mk_deprecation ~note ()) })
+             |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+           end
+       | "deprecated" ->
+         user_err Pp.(str "Deprecation specified twice")
+       | _ -> user_err Pp.(str "Unknown attribute " ++ str k)
+    )
+    (None, atts)
+    f
+
 let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
   let orig_univ_poly = Flags.is_universe_polymorphism () in
   let orig_program_mode = Flags.is_program_mode () in
-  let flags f atts =
-    List.fold_left
-      (fun (polymorphism, atts) f ->
-         match f with
-         | VernacProgram when not atts.program ->
-           (polymorphism, { atts with program = true })
-         | VernacProgram ->
-           user_err Pp.(str "Program mode specified twice")
-         | VernacPolymorphic b when polymorphism = None ->
-           (Some b, atts)
-         | VernacPolymorphic _ ->
-           user_err Pp.(str "Polymorphism specified twice")
-         | VernacLocal b when Option.is_empty atts.locality ->
-           (polymorphism, { atts with locality = Some b })
-         | VernacLocal _ ->
-           user_err Pp.(str "Locality specified twice")
-      )
-      (None, atts)
-      f
-  in
   let rec control = function
   | VernacExpr (f, v) ->
-    let (polymorphism, atts) = flags f { loc; locality = None; polymorphic = false; program = orig_program_mode; } in
+    let (polymorphism, atts) = attributes_of_flags f (mk_atts ~program:orig_program_mode ()) in
     aux ~polymorphism ~atts v
   | VernacFail v -> with_fail st true (fun () -> control v)
   | VernacTimeout (n,v) ->
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 02a3b2bd6..79f9c05ad 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -38,3 +38,7 @@ val interp_redexp_hook : (Environ.env -> Evd.evar_map -> Genredexpr.raw_red_expr
   Evd.evar_map * Redexpr.red_expr) Hook.t
 
 val universe_polymorphism_option_name : string list
+
+(** Elaborate a [atts] record out of a list of flags.
+    Also returns whether polymorphism is explicitly (un)set. *)
+val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index f5f37339c..e97cac818 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -459,13 +459,14 @@ type nonrec vernac_expr =
   (* For extension *)
   | VernacExtend of extend_name * Genarg.raw_generic_argument list
 
-type nonrec vernac_flag =
-  | VernacProgram
-  | VernacPolymorphic of bool
-  | VernacLocal of bool
+type vernac_flags = (string * vernac_flag_value) list
+and vernac_flag_value =
+  | VernacFlagEmpty
+  | VernacFlagLeaf of string
+  | VernacFlagList of vernac_flags
 
 type vernac_control =
-  | VernacExpr of vernac_flag list * vernac_expr
+  | VernacExpr of vernac_flags * vernac_expr
   (* boolean is true when the `-time` batch-mode command line flag was set.
      the flag is used to print differently in `-time` vs `Time foo` *)
   | VernacTime of bool * vernac_control CAst.t
diff --git a/vernac/vernacinterp.ml b/vernac/vernacinterp.ml
index d4f2a753f..1bb1414f3 100644
--- a/vernac/vernacinterp.ml
+++ b/vernac/vernacinterp.ml
@@ -12,15 +12,22 @@ open Util
 open Pp
 open CErrors
 
-type deprecation = bool
+type deprecation = { since : string option ; note : string option }
+
+let mk_deprecation ?(since=None) ?(note=None) () =
+  { since ; note }
 
 type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : deprecation option;
 }
 
+let mk_atts ?(loc=None) ?(locality=None) ?(polymorphic=false) ?(program=false) ?(deprecated=None) () : atts =
+  { loc ; locality ; polymorphic ; program ; deprecated }
+
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
@@ -28,7 +35,7 @@ type plugin_args = Genarg.raw_generic_argument list
 (* Table of vernac entries *)
 let vernac_tab =
   (Hashtbl.create 211 :
-    (Vernacexpr.extend_name, deprecation * plugin_args vernac_command) Hashtbl.t)
+    (Vernacexpr.extend_name, bool * plugin_args vernac_command) Hashtbl.t)
 
 let vinterp_add depr s f =
   try
diff --git a/vernac/vernacinterp.mli b/vernac/vernacinterp.mli
index 935cacf77..46468b309 100644
--- a/vernac/vernacinterp.mli
+++ b/vernac/vernacinterp.mli
@@ -10,21 +10,27 @@
 
 (** Interpretation of extended vernac phrases. *)
 
-type deprecation = bool
+type deprecation = { since : string option ; note : string option }
+
+val mk_deprecation : ?since: string option -> ?note: string option -> unit -> deprecation
 
 type atts = {
   loc : Loc.t option;
   locality : bool option;
   polymorphic : bool;
   program : bool;
+  deprecated : deprecation option;
 }
 
+val mk_atts : ?loc: Loc.t option -> ?locality: bool option ->
+  ?polymorphic: bool -> ?program: bool -> ?deprecated: deprecation option -> unit -> atts
+
 type 'a vernac_command = 'a -> atts:atts -> st:Vernacstate.t -> Vernacstate.t
 
 type plugin_args = Genarg.raw_generic_argument list
 
 val vinterp_init : unit -> unit
-val vinterp_add : deprecation -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
+val vinterp_add : bool -> Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 val overwriting_vinterp_add : Vernacexpr.extend_name -> plugin_args vernac_command -> unit
 
 val call : Vernacexpr.extend_name -> plugin_args -> atts:atts -> st:Vernacstate.t -> Vernacstate.t