Make attributes more general to make defining #[universes(...)] easy

8 files changed, 122 insertions, 46 deletions

diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 4958f17212..f3961327d8 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -194,7 +194,7 @@ let classify_vernac e =
   in
   let rec static_control_classifier ~poly = function
     | VernacExpr (f, e) ->
-      let poly' = Attributes.(parse_drop_extra polymorphic f) in
+      let poly' = Attributes.(parse_drop_extra polymorphic_nowarn f) in
       static_classifier ~poly:(Option.default poly poly') e
     | VernacTimeout (_,e) -> static_control_classifier ~poly e
     | VernacTime (_,{v=e}) | VernacRedirect (_, {v=e}) ->
diff --git a/test-suite/success/Template.v b/test-suite/success/Template.v
index 1c6e2d81d8..cfc25c3346 100644
--- a/test-suite/success/Template.v
+++ b/test-suite/success/Template.v
@@ -25,7 +25,7 @@ Module AutoNo.
 End AutoNo.
 
 Module Yes.
-  #[template]
+  #[universes(template)]
   Inductive Box@{i} (A:Type@{i}) : Type@{i} := box : A -> Box A.
 
   About Box.
@@ -37,7 +37,7 @@ Module Yes.
 End Yes.
 
 Module No.
-  #[notemplate]
+  #[universes(notemplate)]
   Inductive Box (A:Type) : Type := box : A -> Box A.
 
   About Box.
diff --git a/test-suite/success/attribute_syntax.v b/test-suite/success/attribute_syntax.v
index 7b972f4ed9..f4f59a3c16 100644
--- a/test-suite/success/attribute_syntax.v
+++ b/test-suite/success/attribute_syntax.v
@@ -11,7 +11,7 @@ End Scope.
 
 Fail Check 0 = true :> nat.
 
-#[polymorphic]
+#[universes(polymorphic)]
 Definition ι T (x: T) := x.
 
 Check ι _ ι.
@@ -24,9 +24,9 @@ Reset f.
 Ltac foo := foo.
 
 Module M.
-  #[local] #[polymorphic] Definition zed := Type.
+  #[local] #[universes(polymorphic)] Definition zed := Type.
 
-  #[local, polymorphic] Definition kats := Type.
+  #[local, universes(polymorphic)] Definition kats := Type.
 End M.
 Check M.zed@{_}.
 Fail Check zed.
diff --git a/vernac/attributes.ml b/vernac/attributes.ml
index b35a4428f9..0413c7e55a 100644
--- a/vernac/attributes.ml
+++ b/vernac/attributes.ml
@@ -19,44 +19,41 @@ let unsupported_attributes ?loc = function
     let conj = match keys with [_] -> "this attribute: " | _ -> "these attributes: " in
     user_err ?loc Pp.(str "This command does not support " ++ str conj ++ prlist str keys ++ str".")
 
-type 'a key_parser = 'a option -> Vernacexpr.vernac_flag_value -> 'a
-
-type 'a attribute = ('a -> Vernacexpr.vernac_flag_value -> 'a) CString.Map.t * 'a
-
-let parse_drop_extra (p,v:'a attribute) (atts:vernac_flags) : 'a =
-  List.fold_left (fun v (k,args) ->
-      match CString.Map.find k p with
-      | exception Not_found -> v
-      | parser -> parser v args)
-    v atts
-
-let parse_with_extra (p,v:'a attribute) (atts:vernac_flags) : 'a * vernac_flags =
-  let v, extra = List.fold_left (fun (v,extra) (k,args as att) ->
-      match CString.Map.find k p with
-      | exception Not_found -> (v,att::extra)
-      | parser -> (parser v args, extra))
-      (v,[]) atts
-  in
-  v, List.rev extra
+type 'a key_parser = 'a option -> vernac_flag_value -> 'a
+
+type 'a attribute = ('a -> vernac_flags -> vernac_flags * 'a) * 'a
+
+type transform = unit attribute
+
+let parse_with_extra (p,v:'a attribute) (atts:vernac_flags) : vernac_flags * 'a =
+  p v atts
+
+let parse_drop_extra att atts =
+  snd (parse_with_extra att atts)
 
 let parse (p:'a attribute) atts : 'a =
-  let v, extra = parse_with_extra p atts in
+  let extra, v = parse_with_extra p atts in
   unsupported_attributes extra;
   v
 
 module Notations = struct
 
   let (++) (p1,v1:'a attribute) (p2,v2:'b attribute) : ('a*'b) attribute =
-    let p = CString.Map.merge (fun key p1 p2 -> match p1, p2 with
-        | Some p1, None -> Some (fun (x,y) args -> (p1 x args, y))
-        | None, Some p2 -> Some (fun (x,y) args -> (x, p2 y args))
-        | None, None -> None
-        | Some _, Some _ ->
-          anomaly Pp.(str "Attribute collision on " ++ str key))
-        p1 p2
+    let p (v1,v2) atts =
+      let atts, v1 = p1 v1 atts in
+      let atts, v2 = p2 v2 atts in
+      atts, (v1, v2)
     in
     p, (v1, v2)
 
+  let (|>) (p1,():transform) (p2,v2:'a attribute) : 'a attribute =
+    let p v2 atts =
+      let atts, () = p1 () atts in
+      let atts, v2 = p2 v2 atts in
+      atts, v2
+    in
+    p, v2
+
 end
 open Notations
 
@@ -82,8 +79,16 @@ let assert_once ~name prev =
     user_err Pp.(str "Attribute for " ++ str name ++ str " specified twice.")
 
 let attribute_of_list (l:(string * 'a key_parser) list) : 'a option attribute =
-  List.fold_left (fun acc (k,p) -> CString.Map.add k (fun prev args -> Some (p prev args)) acc)
-    CString.Map.empty l, None
+  let rec p extra v = function
+    | [] -> List.rev extra, v
+    | (key, attv as att) :: rem ->
+      (match CList.assoc_f String.equal key l with
+       | exception Not_found -> p (att::extra) v rem
+       | parser ->
+         let v = Some (parser v attv) in
+         p extra v rem)
+  in
+  p [], None
 
 let single_key_parser ~name ~key v prev args =
   assert_empty key args;
@@ -94,13 +99,56 @@ 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)]
 
-let polymorphic = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
+let qualify_attribute qual (parser, v:'a attribute) : 'a attribute =
+  let rec qualified extra v = function
+    | [] -> List.rev extra, v
+    | (key,attv) :: rem when String.equal key qual ->
+      (match attv with
+       | VernacFlagEmpty | VernacFlagLeaf _ ->
+         CErrors.user_err ~hdr:"qualified_attribute"
+           Pp.(str "Malformed attribute " ++ str qual ++ str ": attribute list expected.")
+       | VernacFlagList atts ->
+         let atts, v = parse_with_extra (parser, v) atts in
+         let extra = if atts = [] then extra else (key,VernacFlagList atts) :: extra in
+         qualified extra v rem)
+    | att :: rem -> qualified (att::extra) v rem
+  in
+  qualified [], v
+
+let polymorphic_base = bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
 
 let program = bool_attribute ~name:"Program mode" ~on:"program" ~off:"noprogram"
 
 let locality = bool_attribute ~name:"Locality" ~on:"local" ~off:"global"
 
-let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate"
+let warn_unqualified_univ_attr =
+  CWarnings.create ~name:"unqualified-univ-attr" ~category:"deprecated"
+    (fun key -> Pp.(str "Attribute " ++ str key ++
+                    str " should be qualified as \"universes("++str key++str")\"."))
+
+let ukey = "universes"
+let universe_transform ~warn_unqualified : transform =
+  let p () atts = List.map (fun (key,_ as att) ->
+      match key with
+      | "polymorphic" | "monomorphic"
+      | "template" | "notemplate" ->
+        if warn_unqualified then warn_unqualified_univ_attr key;
+        ukey, VernacFlagList [att]
+      | _ -> att) atts, () in
+  p, ()
+
+let polymorphic_nowarn =
+  universe_transform ~warn_unqualified:false |>
+  qualify_attribute ukey polymorphic_base
+
+let universe_poly_template =
+  let template = bool_attribute ~name:"Template" ~on:"template" ~off:"notemplate" in
+  universe_transform ~warn_unqualified:true |>
+  qualify_attribute ukey (polymorphic_base ++ template)
+
+let polymorphic =
+  universe_transform ~warn_unqualified:true |>
+  qualify_attribute ukey polymorphic_base
 
 let deprecation_parser : deprecation key_parser = fun orig args ->
   assert_once ~name:"deprecation" orig;
@@ -120,8 +168,8 @@ let deprecation_parser : deprecation key_parser = fun orig args ->
 let deprecation = attribute_of_list ["deprecated",deprecation_parser]
 
 let attributes_of_flags f =
-  let (((locality, template), deprecated), polymorphic), program =
-    parse (locality ++ template ++ deprecation ++ polymorphic ++ program) f
+  let ((locality, deprecated), (polymorphic, template)), program =
+    parse (locality ++ deprecation ++ universe_poly_template ++ program) f
   in
   let polymorphic = Option.default (Flags.is_universe_polymorphism()) polymorphic in
   let program = Option.default (Flags.is_program_mode()) program in
@@ -132,3 +180,7 @@ let only_locality atts = parse locality atts
 let only_polymorphism atts =
   let att = parse polymorphic atts in
   Option.default (Flags.is_universe_polymorphism ()) att
+
+
+let vernac_polymorphic_flag = ukey, VernacFlagList ["polymorphic", VernacFlagEmpty]
+let vernac_monomorphic_flag = ukey, VernacFlagList ["monomorphic", VernacFlagEmpty]
diff --git a/vernac/attributes.mli b/vernac/attributes.mli
index 5b03c26cb1..891dc1e735 100644
--- a/vernac/attributes.mli
+++ b/vernac/attributes.mli
@@ -12,7 +12,14 @@ open Vernacexpr
 
 type 'a attribute
 (** The type of attributes. When parsing attributes if an ['a
-   attribute] is present then an ['a] value will be produced. *)
+   attribute] is present then an ['a] value will be produced.
+    In the most general case, an attribute transforms the raw flags
+   along with its value. *)
+
+type transform = unit attribute
+(** An attribute which is used only for the transformation it applies
+   to the flags. For instance, transform [polymorphic] to
+   [universes(polymorphic)]. *)
 
 val parse : 'a attribute -> vernac_flags -> 'a
 (** Errors on unsupported attributes. *)
@@ -22,6 +29,8 @@ module Notations : sig
 
   val (++) : 'a attribute -> 'b attribute -> ('a * 'b) attribute
   (** Combine 2 attributes. If any keys are in common an error will be raised. *)
+
+  val (|>) : transform -> 'a attribute -> 'a attribute
 end
 
 (** Definitions for some standard attributes. *)
@@ -32,10 +41,13 @@ val mk_deprecation : ?since: string option -> ?note: string option -> unit -> de
 
 val polymorphic : bool option attribute
 val program : bool option attribute
-val template : bool option attribute
+val universe_poly_template : (bool option * bool option) attribute
 val locality : bool option attribute
 val deprecation : deprecation option attribute
 
+val polymorphic_nowarn : bool option attribute
+(** For internal use, avoid warning if not qualified as eg [universes(polymorphic)]. *)
+
 type t = {
   locality : bool option;
   polymorphic : bool;
@@ -61,7 +73,7 @@ val only_polymorphism : vernac_flags -> bool
 val parse_drop_extra : 'a attribute -> vernac_flags -> 'a
 (** Ignores unsupported attributes. *)
 
-val parse_with_extra : 'a attribute -> vernac_flags -> 'a * vernac_flags
+val parse_with_extra : 'a attribute -> vernac_flags -> vernac_flags * 'a
 (** Returns unsupported attributes. *)
 
 (** * Defining attributes. *)
@@ -82,6 +94,10 @@ val bool_attribute : name:string -> on:string -> off:string -> bool option attri
    provided and [false] when [off] is provided. The attribute may only
    be set once for a command. *)
 
+val qualify_attribute : string -> 'a attribute -> 'a attribute
+(** [qualified_attribute qual att] treats [#[qual(atts)]] like [att]
+   treats [atts]. *)
+
 (** Combinators to help define your own parsers. See the
    implementation of [bool_attribute] for practical use. *)
 
@@ -98,3 +114,7 @@ val single_key_parser : name:string -> key:string -> 'a -> 'a key_parser
 (** [single_key_parser ~name ~key v] makes a parser for attribute
     [name] giving the constant value [v] for key [key] taking no
     arguments. [name] may only be given once. *)
+
+(** Compatibility values for parsing [Polymorphic]. *)
+val vernac_polymorphic_flag : vernac_flag
+val vernac_monomorphic_flag : vernac_flag
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index d7229d32fe..1d0a5ab0a3 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -112,8 +112,10 @@ GRAMMAR EXTEND Gram
     ]
   ;
   vernac_poly:
-    [ [ 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) }
+    [ [ IDENT "Polymorphic"; v = vernac_aux ->
+        { let (f, v) = v in (Attributes.vernac_polymorphic_flag :: f, v) }
+      | IDENT "Monomorphic"; v = vernac_aux ->
+        { let (f, v) = v in (Attributes.vernac_monomorphic_flag :: f, v) }
       | v = vernac_aux -> { v } ]
     ]
   ;
diff --git a/vernac/vernac.mllib b/vernac/vernac.mllib
index 35ce8c726b..30fae756e9 100644
--- a/vernac/vernac.mllib
+++ b/vernac/vernac.mllib
@@ -1,4 +1,5 @@
 Vernacexpr
+Attributes
 Pvernac
 G_vernac
 G_proofs
@@ -7,7 +8,6 @@ Himsg
 ExplainErr
 Locality
 Egramml
-Attributes
 Vernacinterp
 Ppvernac
 Proof_using
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b02d482761..ac50afcf9b 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -2401,7 +2401,9 @@ let interp ?(verbosely=true) ?proof ~st {CAst.loc;v=c} =
     | VernacLoad (_,fname) -> vernac_load control fname
 
     | c ->
-      let poly, program = Attributes.(parse_drop_extra Notations.(polymorphic ++ program) atts) in
+      let poly, program = let open Attributes in
+        parse_drop_extra Notations.(polymorphic_nowarn ++ program) atts
+      in
       (* NB: we keep polymorphism and program in the attributes, we're
          just parsing them to do our option magic. *)
       check_vernac_supports_polymorphism c poly;