Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)

3 files changed, 38 insertions, 18 deletions

diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 09090ce89a..721c7a7a51 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,6 +1063,9 @@ Parameterized inductive types
         | cons3 : A -> list3 -> list3.
         End list3.
 
+     Attributes ``uniform`` and ``nonuniform`` respectively enable and
+     disable uniform parameters for a single inductive declaration block.
+
 .. seealso::
    Section :ref:`inductive-definitions` and the :tacn:`induction` tactic.
 
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..651247937d 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,13 +1,23 @@
+Module Att.
+  #[uniform] Inductive list (A : Type) :=
+  | nil : list
+  | cons : A -> list -> list.
+  Check (list : Type -> Type).
+  Check (cons : forall A, A -> list A -> list A).
+End Att.
+
 Set Uniform Inductive Parameters.
 
 Inductive list (A : Type) :=
-  | nil : list
-  | cons : A -> list -> list.
+| nil : list
+| cons : A -> list -> list.
 Check (list : Type -> Type).
 Check (cons : forall A, A -> list A -> list A).
 
 Inductive list2 (A : Type) (A' := prod A A) :=
-  | nil2 : list2
-  | cons2 : A' -> list2 -> list2.
+| nil2 : list2
+| cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
+
+#[nonuniform] Inductive bla (n:nat) := c (_ : bla (S n)).
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dec5a79892..e469323f50 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -623,16 +623,18 @@ let should_treat_as_cumulative cum poly =
     else user_err Pp.(str "The NonCumulative prefix can only be used in a polymorphic context.")
   | None -> poly && is_polymorphic_inductive_cumulativity ()
 
-let get_uniform_inductive_parameters =
-  Goptions.declare_bool_option_and_ref
-    ~depr:false
-    ~key:["Uniform"; "Inductive"; "Parameters"]
-    ~value:false
-
-let should_treat_as_uniform () =
-  if get_uniform_inductive_parameters ()
-  then ComInductive.UniformParameters
-  else ComInductive.NonUniformParameters
+let uniform_att =
+  let get_uniform_inductive_parameters =
+    Goptions.declare_bool_option_and_ref
+      ~depr:false
+      ~key:["Uniform"; "Inductive"; "Parameters"]
+      ~value:false
+  in
+  let open Attributes.Notations in
+  Attributes.bool_attribute ~name:"uniform" ~on:"uniform" ~off:"nonuniform" >>= fun u ->
+  let u = match u with Some u -> u | None -> get_uniform_inductive_parameters () in
+  let u = if u then ComInductive.UniformParameters else ComInductive.NonUniformParameters in
+  return u
 
 let vernac_record ~template udecl cum k poly finite records =
   let cumulative = should_treat_as_cumulative cum poly in
@@ -680,7 +682,6 @@ let finite_of_kind = let open Declarations in function
     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 open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
@@ -712,7 +713,9 @@ let vernac_inductive ~atts cum lo kind indl =
     let (coe, (lid, ce)) = l in
     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
+            { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true }
+    in
+    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
     vernac_record ~template udecl cum (Class true) poly finite [id, bl, c, None, [f]]
   else if List.for_all is_record indl then
     (* Mutual record case *)
@@ -734,6 +737,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
+    let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
     vernac_record ~template udecl cum kind poly finite recordl
   else if List.for_all is_constructor indl then
     (* Mutual inductive case *)
@@ -757,9 +761,12 @@ let vernac_inductive ~atts cum lo kind indl =
     | RecordDecl _ -> assert false (* ruled out above *)
     in
     let indl = List.map unpack indl in
+    let (template, poly), uniform =
+      Attributes.(parse Notations.(template ++ polymorphic ++ uniform_att) atts)
+    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:lo ~uniform finite
   else
     user_err (str "Mixed record-inductive definitions are not allowed")