Merge PR #11584: Add #[uniform] and #[nonuniform] (for Uniform Inductive Parameters)

Reviewed-by: Matafou
Reviewed-by: Zimmi48
Reviewed-by: maximedenes

8 files changed, 83 insertions, 75 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/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index 84f09c385f..fdbad2ab9e 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1512,12 +1512,12 @@ let do_build_inductive
         let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
         let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
                           rel_inds
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             msg
         in
@@ -1527,12 +1527,12 @@ let do_build_inductive
         let _time3 = System.get_time () in
 (* 	Pp.msgnl (str "error : "++ str (string_of_float (System.time_difference time2 time3))); *)
         let repacked_rel_inds =
-          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c , Vernacexpr.Inductive_kw, Vernacexpr.Constructors l),ntn )
+          List.map  (fun ((a , b , c , l),ntn) -> ((false,(a,None)) , b, c, Vernacexpr.Constructors l),ntn )
                           rel_inds
         in
         let msg =
           str "while trying to define"++ spc () ++
-            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Declarations.Finite,repacked_rel_inds)})
+            Ppvernac.pr_vernac (CAst.make @@ Vernacexpr.{ control = []; attrs = []; expr = VernacInductive(None,false,Vernacexpr.Inductive_kw,repacked_rel_inds)})
             ++ fnl () ++
             CErrors.print reraise
         in
diff --git a/stm/vernac_classifier.ml b/stm/vernac_classifier.ml
index c5b3e0931b..65ef2ca8c6 100644
--- a/stm/vernac_classifier.ml
+++ b/stm/vernac_classifier.ml
@@ -131,7 +131,7 @@ let classify_vernac e =
         VtSideff ([id.CAst.v], VtLater)
     | VernacDefinition (_,({v=id},_),DefineBody _) -> VtSideff (idents_of_name id, VtLater)
     | VernacInductive (_, _,_,l) ->
-        let ids = List.map (fun (((_,({v=id},_)),_,_,_,cl),_) -> id :: match cl with
+        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] | _ -> []) @
            CList.map_filter (function
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/g_vernac.mlg b/vernac/g_vernac.mlg
index d0374bc4fa..74249301d7 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -21,7 +21,6 @@ open Constrexpr_ops
 open Extend
 open Decls
 open Declaremods
-open Declarations
 open Namegen
 open Tok (* necessary for camlp5 *)
 
@@ -200,9 +199,7 @@ GRAMMAR EXTEND Gram
       (* Gallina inductive declarations *)
       | cum = OPT cumulativity_token; priv = private_token; f = finite_token;
         indl = LIST1 inductive_definition SEP "with" ->
-          { let (k,f) = f in
-          let indl=List.map (fun ((a,b,c,d),e) -> ((a,b,c,k,d),e)) indl in
-          VernacInductive (cum, priv,f,indl) }
+          { VernacInductive (cum, priv, f, indl) }
       | "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
           { VernacFixpoint (NoDischarge, recs) }
       | IDENT "Let"; "Fixpoint"; recs = LIST1 rec_definition SEP "with" ->
@@ -337,12 +334,12 @@ GRAMMAR EXTEND Gram
   ] ]
   ;
   finite_token:
-    [ [ IDENT "Inductive" -> { (Inductive_kw,Finite) }
-      | IDENT "CoInductive" -> { (CoInductive,CoFinite) }
-      | IDENT "Variant" -> { (Variant,BiFinite) }
-      | IDENT "Record" -> { (Record,BiFinite) }
-      | IDENT "Structure" -> { (Structure,BiFinite) }
-      | IDENT "Class" -> { (Class true,BiFinite) } ] ]
+    [ [ IDENT "Inductive" -> { Inductive_kw }
+      | IDENT "CoInductive" -> { CoInductive }
+      | IDENT "Variant" -> { Variant }
+      | IDENT "Record" -> { Record }
+      | IDENT "Structure" -> { Structure }
+      | IDENT "Class" -> { Class true } ] ]
   ;
   cumulativity_token:
     [ [ IDENT "Cumulative" -> { VernacCumulative }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 82132a1af6..6240120cb0 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -476,7 +476,7 @@ let string_of_theorem_kind = let open Decls in function
     let prpri = match pri with None -> mt() | Some i -> str "| " ++ int i in
     prx ++ prpri ++ prlist (pr_decl_notation @@ pr_constr env sigma) ntn
 
-  let pr_record_decl b c fs =
+  let pr_record_decl c fs =
     pr_opt pr_lident c ++ (if c = None then str"{" else str" {") ++
       hv 0 (prlist_with_sep pr_semicolon pr_record_field fs ++ str"}")
 
@@ -802,7 +802,7 @@ let string_of_definition_object_kind = let open Decls in function
                    (if coe then str":>" else str":") ++
                    Flags.without_option Flags.beautify pr_spc_lconstr c)
         in
-        let pr_constructor_list b l = match l with
+        let pr_constructor_list l = match l with
           | Constructors [] -> mt()
           | Constructors l ->
             let fst_sep = match l with [_] -> "   " | _ -> " | " in
@@ -810,21 +810,20 @@ let string_of_definition_object_kind = let open Decls in function
               fnl() ++ str fst_sep ++
               prlist_with_sep (fun _ -> fnl() ++ str" | ") pr_constructor l
           | RecordDecl (c,fs) ->
-            pr_record_decl b c fs
+            pr_record_decl c fs
         in
-        let pr_oneind key (((coe,iddecl),indpar,s,k,lc),ntn) =
+        let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) =
           hov 0 (
             str key ++ spc() ++
               (if coe then str"> " else str"") ++ pr_ident_decl iddecl ++
               pr_and_type_binders_arg indpar ++
               pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
-              str" :=") ++ pr_constructor_list k lc ++
+              str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
         in
         let key =
-          let (_,_,_,k,_),_ = List.hd l in
           let kind =
-            match k with Record -> "Record" | Structure -> "Structure"
+            match f with Record -> "Record" | Structure -> "Structure"
                        | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive"
                        | Class _ -> "Class" | Variant -> "Variant"
           in
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index f8eef68997..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
@@ -661,25 +663,29 @@ let vernac_record ~template udecl cum k poly finite records =
 let extract_inductive_udecl (indl:(inductive_expr * decl_notation list) list) =
   match indl with
   | [] -> assert false
-  | (((coe,(id,udecl)),b,c,k,d),e) :: rest ->
-    let rest = List.map (fun (((coe,(id,udecl)),b,c,k,d),e) ->
+  | (((coe,(id,udecl)),b,c,d),e) :: rest ->
+    let rest = List.map (fun (((coe,(id,udecl)),b,c,d),e) ->
         if Option.has_some udecl
         then user_err ~hdr:"inductive udecl" Pp.(strbrk "Universe binders must be on the first inductive of the block.")
-        else (((coe,id),b,c,k,d),e))
+        else (((coe,id),b,c,d),e))
         rest
     in
-    udecl, (((coe,id),b,c,k,d),e) :: rest
+    udecl, (((coe,id),b,c,d),e) :: rest
+
+let finite_of_kind = let open Declarations in function
+  | Inductive_kw -> Finite
+  | 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 finite indl =
-  let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+let vernac_inductive ~atts cum lo kind indl =
   let open Pp in
   let udecl, indl = extract_inductive_udecl indl in
   if Dumpglob.dump () then
-    List.iter (fun (((coe,lid), _, _, _, cstrs), _) ->
+    List.iter (fun (((coe,lid), _, _, cstrs), _) ->
       match cstrs with
         | Constructors cstrs ->
             Dumpglob.dump_definition lid false "ind";
@@ -688,16 +694,17 @@ let vernac_inductive ~atts cum lo finite indl =
         | _ -> () (* dumping is done by vernac_record (called below) *) )
       indl;
 
+  let finite = finite_of_kind kind in
   let is_record = function
-  | ((_ , _ , _ , _, RecordDecl _), _) -> true
+  | ((_ , _ , _ , RecordDecl _), _) -> true
   | _ -> false
   in
   let is_constructor = function
-  | ((_ , _ , _ , _, Constructors _), _) -> true
+  | ((_ , _ , _ , Constructors _), _) -> true
   | _ -> false
   in
-  let is_defclass = match indl with
-  | [ ( id , bl , c , Class _, Constructors [l]), [] ] -> Some (id, bl, c, l)
+  let is_defclass = match kind, indl with
+  | Class _, [ ( id , bl , c , Constructors [l]), [] ] -> Some (id, bl, c, l)
   | _ -> None
   in
   if Option.has_some is_defclass then
@@ -706,42 +713,42 @@ let vernac_inductive ~atts cum lo finite 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 *)
-    let check_kind ((_, _, _, kind, _), _) = match kind with
-    | Variant ->
-      user_err (str "The Variant keyword does not support syntax { ... }.")
-    | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
+    let () = match kind with
+      | Variant ->
+        user_err (str "The Variant keyword does not support syntax { ... }.")
+      | Record | Structure | Class _ | Inductive_kw | CoInductive -> ()
     in
-    let () = List.iter check_kind indl in
-    let check_where ((_, _, _, _, _), wh) = match wh with
+    let check_where ((_, _, _, _), wh) = match wh with
     | [] -> ()
     | _ :: _ ->
       user_err (str "where clause not supported for records")
     in
     let () = List.iter check_where indl in
-    let unpack ((id, bl, c, _, decl), _) = match decl with
+    let unpack ((id, bl, c, decl), _) = match decl with
     | RecordDecl (oc, fs) ->
       (id, bl, c, oc, fs)
     | Constructors _ -> assert false (* ruled out above *)
     in
-    let ((_, _, _, kind, _), _) = List.hd 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 *)
-    let check_kind ((_, _, _, kind, _), _) = match kind with
+    let () = match kind with
     | (Record | Structure) ->
       user_err (str "The Record keyword is for types defined using the syntax { ... }.")
     | Class _ ->
       user_err (str "Inductive classes not supported")
     | Variant | Inductive_kw | CoInductive -> ()
     in
-    let () = List.iter check_kind indl in
-    let check_name ((na, _, _, _, _), _) = match na with
+    let check_name ((na, _, _, _), _) = match na with
     | (true, _) ->
       user_err (str "Variant types do not handle the \"> Name\" \
         syntax, which is reserved for records. Use the \":>\" \
@@ -749,26 +756,19 @@ let vernac_inductive ~atts cum lo finite indl =
     | _ -> ()
     in
     let () = List.iter check_name indl in
-    let unpack (((_, id) , bl, c, _, decl), ntn) = match decl with
+    let unpack (((_, id) , bl, c, decl), ntn) = match decl with
     | Constructors l -> (id, bl, c, l), ntn
     | 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")
-(*
-
-  match indl with
-  | [ ( id , bl , c , Class _, Constructors [l]), [] ] ->
-      let f =
-        let (coe, ({loc;v=id}, ce)) = l in
-        let coe' = if coe then Some true else None in
-          (((coe', AssumExpr ((make ?loc @@ Name id), ce)), None), [])
-      in vernac_record cum (Class true) atts.polymorphic finite [id, bl, c, None, [f]]
-    *)
 
 let vernac_fixpoint_common ~atts discharge l =
   if Dumpglob.dump () then
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 22a8de7f99..8ead56dfdf 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -104,7 +104,6 @@ type coercion_flag  = bool (* true = AddCoercion    false = NoCoercion     *)
 type instance_flag  = bool option
   (* Some true = Backward instance; Some false = Forward instance, None = NoInstance *)
 type export_flag    = bool (* true = Export;        false = Import         *)
-type inductive_flag = Declarations.recursivity_kind
 type onlyparsing_flag = { onlyparsing : bool }
  (* Some v = Parse only;  None = Print also.
     If v<>Current, it contains the name of the coq version
@@ -165,7 +164,7 @@ type constructor_list_or_record_decl_expr =
   | Constructors of constructor_expr list
   | RecordDecl of lident option * (local_decl_expr * record_field_attr) list
 type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option * inductive_kind *
+  ident_decl with_coercion * local_binder_expr list * constr_expr option *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
@@ -306,7 +305,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_flag * (inductive_expr * decl_notation list) list
+  | VernacInductive of vernac_cumulative option * bool (* private *) * 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