Make Cumulative, NonCumulative and Private attributes.

- Legacy attributes can now be specified in any order.
- Legacy attribute Cumulative maps to universes(cumulative).
- Legacy attribute NonCumulative maps to universes(noncumulative).
- Legacy attribute Private maps to private(matching).

We use "private(matching)" and not "private(match)" because we cannot
use keywords within attributes.

6 files changed, 93 insertions, 81 deletions

diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index c7dfe69fb1..e08ad9af3a 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1517,7 +1517,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             msg
         in
@@ -1532,7 +1532,7 @@ let do_build_inductive
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             CErrors.print reraise
         in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index 15e839c612..567acb1c73 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -130,7 +130,7 @@ let classify_vernac e =
     | VernacPrimitive (id,_,_) ->
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
-    | VernacInductive (_, _,_,l) ->
+    | VernacInductive (_,l) ->
         let ids = List.map (fun (((_,({v=id},_)),_,_,cl),_) -> id :: match cl with
         | Constructors l -> List.map (fun (_,({v=id},_)) -> id) l
         | RecordDecl (oid,l) -> (match oid with Some {v=x} -> [x] | _ -> []) @
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 77423fbadf..dd75693c5b 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -107,35 +107,40 @@ GRAMMAR EXTEND Gram
       | -> { VernacFlagEmpty } ]
     ]
   ;
-  vernac:
-    [ [ 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 } ]
-    ]
+  legacy_attr:
+    [ [ IDENT "Local" ->
+        { ("local", VernacFlagEmpty) }
+      | IDENT "Global" ->
+        { ("global", VernacFlagEmpty) }
+      | IDENT "Polymorphic" ->
+        { Attributes.vernac_polymorphic_flag }
+      | IDENT "Monomorphic" ->
+        { Attributes.vernac_monomorphic_flag }
+      | IDENT "Cumulative" ->
+        { ("universes", VernacFlagList ["cumulative", VernacFlagEmpty]) }
+      | IDENT "NonCumulative" ->
+        { ("universes", VernacFlagList ["noncumulative", VernacFlagEmpty]) }
+      | IDENT "Private" ->
+        { ("private", VernacFlagList ["matching", VernacFlagEmpty]) }
+      | IDENT "Program" ->
+        { ("program", VernacFlagEmpty) }
+      ] ]
   ;
-  vernac_poly:
-    [ [ 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 } ]
-    ]
+  vernac:
+    [ [ attrs = LIST0 legacy_attr; v = vernac_aux -> { (attrs, 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; "." -> { (["program", VernacFlagEmpty], g) }
-      | IDENT "Program"; g = gallina_ext; "." -> { (["program", VernacFlagEmpty], g) }
-      | g = gallina; "." -> { ([], g) }
-      | g = gallina_ext; "." -> { ([], g) }
-      | c = command; "." -> { ([], c) }
-      | c = syntax; "." -> { ([], c) }
-      | c = subprf -> { ([], c) }
+    [ [ g = gallina; "." -> { g }
+      | g = gallina_ext; "." -> { g }
+      | c = command; "." -> { c }
+      | c = syntax; "." -> { c }
+      | c = subprf -> { c }
     ] ]
   ;
   vernac_aux: LAST
-    [ [ prfcom = command_entry -> { ([], prfcom) } ] ]
+    [ [ prfcom = command_entry -> { prfcom } ] ]
   ;
   noedit_mode:
     [ [ c = query_command -> { c None } ] ]
@@ -197,9 +202,8 @@ GRAMMAR EXTEND Gram
       | IDENT "Let"; id = identref; b = def_body ->
           { VernacDefinition ((DoDischarge, Let), (lname_of_lident id, None), b) }
       (* Gallina inductive declarations *)
-      | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
-        indl = LIST1 inductive_definition SEP "with" ->
-          { VernacInductive (cum, priv, f, indl) }
+      | f = finite_token; indl = LIST1 inductive_definition SEP "with" ->
+          { VernacInductive (f, indl) }
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           { VernacFixpoint (NoDischarge, recs) }
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -341,13 +345,6 @@ GRAMMAR EXTEND Gram
       | IDENT "Structure" -> { Structure }
       | IDENT "Class" -> { Class true } ] ]
   ;
-  cumulativity_token:
-    [ [ IDENT "Cumulative" -> { VernacCumulative }
-      | IDENT "NonCumulative" -> { VernacNonCumulative } ] ]
-  ;
-  private_token:
-    [ [ IDENT "Private" -> { true } | -> { false } ] ]
-  ;
   (* Simple definitions *)
   def_body:
     [ [ bl = binders; ":="; red = reduce; c = lconstr ->
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 5808c55cfc..a3de88d4dc 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -804,7 +804,7 @@ let string_of_definition_object_kind = let open Decls in function
         let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in
         return (hov 2 (pr_assumption_token (n > 1) discharge kind ++
                        pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions))
-      | VernacInductive (cum, p,f,l) ->
+      | VernacInductive (f,l) ->
         let pr_constructor (coe,(id,c)) =
           hov 2 (pr_lident id ++ str" " ++
                    (if coe then str":>" else str":") ++
@@ -830,24 +830,14 @@ let string_of_definition_object_kind = let open Decls in function
               str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
         in
-        let key =
-          let kind =
-            match f with Record -> "Record" | Structure -> "Structure"
-                       | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
-                       | Class _ -> "Class" | Variant -> "Variant"
-          in
-          if p then
-            let cm =
-              match cum with
-              | Some VernacCumulative -> "Cumulative"
-              | Some VernacNonCumulative -> "NonCumulative"
-              | None -> ""
-            in
-            cm ^ " " ^ kind
-          else kind
+        let kind =
+          match f with
+          | Record -> "Record" | Structure -> "Structure"
+          | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
+          | Class _ -> "Class" | Variant -> "Variant"
         in
         return (
-          hov 1 (pr_oneind key (List.hd l)) ++
+          hov 1 (pr_oneind kind (List.hd l)) ++
           (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l))
         )
 
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index b5ecd62dad..1ea4d6cb02 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -604,17 +604,39 @@ let vernac_assumption ~atts discharge kind l nl =
 
 let is_polymorphic_inductive_cumulativity =
   declare_bool_option_and_ref ~depr:false ~value:false
-    ~key:["Polymorphic"; "Inductive"; "Cumulativity"]
-
-let should_treat_as_cumulative cum poly =
-  match cum with
-  | Some VernacCumulative ->
-    if poly then true
-    else user_err Pp.(str "The Cumulative prefix can only be used in a polymorphic context.")
-  | Some VernacNonCumulative ->
-    if poly then false
-    else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
-  | None -> poly && is_polymorphic_inductive_cumulativity ()
+    ~key:["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.");
+  in
+  let open Attributes in
+  let open Notations in
+  qualify_attribute "universes"
+    (bool_attribute ~name:"Polymorphism" ~on:"polymorphic" ~off:"monomorphic"
+     ++ bool_attribute ~name:"Cumulativity" ~on:"cumulative" ~off:"noncumulative")
+  >>= function
+  | Some poly, Some cum ->
+     (* Case of Polymorphic|Monomorphic Cumulative|NonCumulative Inductive
+        and #[ universes(polymorphic|monomorphic,cumulative|noncumulative) ] Inductive *)
+     if poly then return (true, cum)
+     else error_poly_context ()
+  | Some poly, None ->
+     (* Case of Polymorphic|Monomorphic Inductive
+        and #[ universes(polymorphic|monomorphic) ] Inductive *)
+     if poly then return (true, is_polymorphic_inductive_cumulativity ())
+     else return (false, false)
+  | None, Some cum ->
+     (* Case of Cumulative|NonCumulative Inductive *)
+     if is_universe_polymorphism () then return (true, cum)
+     else error_poly_context ()
+  | None, None ->
+     (* Case of Inductive *)
+     if is_universe_polymorphism () then
+       return (true, is_polymorphic_inductive_cumulativity ())
+     else
+       return (false, false)
 
 let get_uniform_inductive_parameters =
   Goptions.declare_bool_option_and_ref
@@ -627,8 +649,7 @@ let should_treat_as_uniform () =
   then ComInductive.UniformParameters
   else ComInductive.NonUniformParameters
 
-let vernac_record ~template udecl cum k poly finite records =
-  let cumulative = should_treat_as_cumulative cum poly in
+let vernac_record ~template udecl ~cumulative k ~poly finite records =
   let map ((coe, id), binders, sort, nameopt, cfs) =
     let const = match nameopt with
     | None -> Nameops.add_prefix "Build_" id.v
@@ -668,12 +689,21 @@ let finite_of_kind = let open Declarations in function
   | CoInductive -> CoFinite
   | Variant | Record | Structure | Class _ -> BiFinite
 
-(** When [poly] is true the type is declared polymorphic. When [lo] is true,
-    then the type is declared private (as per the [Private] keyword). [finite]
-    indicates whether the type is inductive, co-inductive or
-    neither. *)
-let vernac_inductive ~atts cum lo kind indl =
-  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+let private_ind =
+  let open Attributes in
+  let open Notations in
+  attribute_of_list
+    [ "matching"
+    , single_key_parser ~name:"Private (matching) inductive type" ~key:"matching" ()
+    ]
+  |> qualify_attribute "private"
+  >>= function
+  | Some () -> return true
+  | None -> return false
+
+let vernac_inductive ~atts kind indl =
+  let (template, (poly, cumulative)), private_ind = Attributes.(
+      parse Notations.(template ++ polymorphic_cumulative ++ private_ind) atts) in
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -710,7 +740,7 @@ let vernac_inductive ~atts cum lo kind indl =
     let coe' = if coe then Some true else None in
     let f = AssumExpr ((make ?loc:lid.loc @@ Name lid.v), ce),
             { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true } in
-    vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
+    vernac_record ~template udecl ~cumulative (Class true) ~poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
     let () = match kind with
@@ -735,7 +765,7 @@ let vernac_inductive ~atts cum lo kind indl =
     in
     let kind = match kind with Class _ -> Class false | _ -> kind in
     let recordl = List.map unpack indl in
-    vernac_record ~template udecl cum kind poly finite recordl
+    vernac_record ~template udecl ~cumulative kind ~poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
     let () = match kind with
@@ -758,9 +788,8 @@ let vernac_inductive ~atts cum lo kind indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
-    let cumulative = should_treat_as_cumulative cum poly in
     let uniform = should_treat_as_uniform () in
-    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind:lo ~uniform finite
+    ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")
 
@@ -2008,8 +2037,8 @@ let translate_vernac ~atts v = let open Vernacextend in match v with
         vernac_declare_module_type lid bl mtys mtyo)
   | VernacAssumption ((discharge,kind),nl,l) ->
     VtDefault(fun () -> with_def_attributes ~atts vernac_assumption discharge kind l nl)
-  | VernacInductive (cum, priv, finite, l) ->
-    VtDefault(fun () -> vernac_inductive ~atts cum priv finite l)
+  | VernacInductive (finite, l) ->
+    VtDefault(fun () -> vernac_inductive ~atts finite l)
   | VernacFixpoint (discharge, l) ->
     let opens = List.exists (fun { body_def } -> Option.is_empty body_def) l in
     if opens then
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index efae1b8dfd..67e1fb9495 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -250,10 +250,6 @@ type register_kind =
 type module_ast_inl = module_ast * Declaremods.inline
 type module_binder = bool option * lident list * module_ast_inl
 
-(** [Some b] if locally enabled/disabled according to [b], [None] if
-    we should use the global flag. *)
-type vernac_cumulative = VernacCumulative | VernacNonCumulative
-
 (** {6 The type of vernacular expressions} *)
 
 type vernac_one_argument_status = {
@@ -312,7 +308,7 @@ type nonrec vernac_expr =
   | VernacExactProof of constr_expr
   | VernacAssumption of (discharge * Decls.assumption_object_kind) *
       Declaremods.inline * (ident_decl list * constr_expr) with_coercion list
-  | VernacInductive of vernac_cumulative option * bool (* private *) * inductive_kind * (inductive_expr * decl_notation list) list
+  | VernacInductive of inductive_kind * (inductive_expr * decl_notation list) list
   | VernacFixpoint of discharge * fixpoint_expr list
   | VernacCoFixpoint of discharge * cofixpoint_expr list
   | VernacScheme of (lident option * scheme) list