[vernac] Generic syntax for flags/attributes

5 files changed, 68 insertions, 66 deletions

diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 49fcda849..92c685741 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -87,50 +87,42 @@ GRAMMAR EXTEND Gram
   | fv = vernac -> fv
   ]]
   ;
-  attributes: [[ "#[" ; a = LIST1 attribute SEP "," ; "]" -> a ]]
-  ;
-  attribute:
-  [[
-    IDENT "polymorphic" -> VernacPolymorphic true
-  | IDENT "monomorphic" -> VernacPolymorphic false
-  | IDENT "program" -> VernacProgram
-  | IDENT "local" -> VernacLocal true
-  | IDENT "global" -> VernacLocal false
-  | IDENT "coercion" -> VernacCoercion
-  | IDENT "deprecated" ; v = attribute_value ->
-    match v with
-    | `List [ k1, `Leaf since ; k2, `Leaf note ] when Names.Id.equal k1 (Names.Id.of_string "since") && Names.Id.equal k2 (Names.Id.of_string "note") -> VernacDeprecated (since, note)
-    |  _ -> CErrors.user_err (Pp.str "Ill formed “deprecated” attribute")
+  attributes:
+  [[ "#[" ; a = attribute_list ; "]" -> a
   ]]
   ;
-  attribute_value:
-  [[ "=" ; v = string -> `Leaf v
-   | "(" ; m = LIST0 attribute_pair SEP "," ; ")" -> `List m
-   | -> `Empty
+  attribute_list:
+  [[ a = LIST0 attribute SEP "," -> a
   ]]
   ;
-  attribute_pair:
+  attribute:
   [[ k = ident ; v = attribute_value -> (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 ((Names.Id.of_string "local", VernacFlagEmpty) :: f, v) }
+      | IDENT "Global"; v = vernac_poly -> { let (f, v) = v in ((Names.Id.of_string "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 ((Names.Id.of_string "polymorphic", VernacFlagEmpty) :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux -> { let (f, v) = v in ((Names.Id.of_string "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; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
+      | IDENT "Program"; g = gallina_ext; "." -> { ([Names.Id.of_string "program", VernacFlagEmpty], g) }
       | g = gallina; "." -> { ([], g) }
       | g = gallina_ext; "." -> { ([], g) }
       | c = command; "." -> { ([], c) }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index f9237c775..024c145aa 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -1193,34 +1193,24 @@ open Pputils
       | VernacEndSubproof ->
         return (str "}")
 
-let rec pr_vernac_flag_data (k, v) =
-  let k = keyword k in
+let rec pr_vernac_flag (k, v) =
+  let k = keyword (Names.Id.to_string k) in
   match v with
-  | `Empty -> k
-  | `Leaf v -> k ++ str " = " ++ qs v
-  | `Node m -> k ++ str "( " ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag_data m ++ str " )"
-
-let pr_vernac_flag f =
-  match f with
-  | VernacPolymorphic true -> keyword "polymorphic"
-  | VernacPolymorphic false -> keyword "monomorphic"
-  | VernacProgram -> keyword "program"
-  | VernacLocal true -> keyword "local"
-  | VernacLocal false -> keyword "global"
-  | VernacDeprecated (since, note) ->
-    pr_vernac_flag_data ("deprecated", `Node [
-        "since", `Leaf since; "note", `Leaf note
-      ])
-
-let pr_vernac_flag_list =
+  | 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 "#[" ++ prlist_with_sep (fun () -> str ", ") pr_vernac_flag flags ++ str "]" ++ cut ()
+  | 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') -> pr_vernac_flag_list 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 af0f19834..e61687290 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2320,25 +2320,45 @@ let with_fail st b f =
   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) f ->
-       match f with
-       | VernacProgram when not atts.program ->
+    (fun (polymorphism, atts) (k, v) ->
+       let k = Names.Id.to_string k in
+       match k with
+       | "program" when not atts.program ->
+         assert_empty k v;
          (polymorphism, { atts with program = true })
-       | VernacProgram ->
+       | "program" ->
          user_err Pp.(str "Program mode specified twice")
-       | VernacPolymorphic b when polymorphism = None ->
-         (Some b, atts)
-       | VernacPolymorphic _ ->
+       | "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")
-       | VernacLocal b when Option.is_empty atts.locality ->
-         (polymorphism, { atts with locality = Some b })
-       | VernacLocal _ ->
+       | "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")
-       | VernacDeprecated (since, note) when Option.is_empty atts.deprecated ->
-         (polymorphism, { atts with deprecated = Some (since, note) })
-       | VernacDeprecated _ ->
+       | "deprecated" when Option.is_empty atts.deprecated ->
+           begin match v with
+             | VernacFlagList [ k1, VernacFlagLeaf since ; k2, VernacFlagLeaf note ]
+               when Names.Id.(equal k1 (of_string "since") && equal k2 (of_string "note")) ->
+               (polymorphism, { atts with deprecated = Some (since, 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
diff --git a/vernac/vernacentries.mli b/vernac/vernacentries.mli
index 79f9b602a..79f9c05ad 100644
--- a/vernac/vernacentries.mli
+++ b/vernac/vernacentries.mli
@@ -41,4 +41,4 @@ 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_flag list -> Vernacinterp.atts -> bool option * Vernacinterp.atts
+val attributes_of_flags : Vernacexpr.vernac_flags -> Vernacinterp.atts -> bool option * Vernacinterp.atts
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 57ccb6006..2287630c7 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -459,14 +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
-  | VernacDeprecated of string * string (* Since, Note *)
+type vernac_flags = (Names.Id.t * 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