New syntax [Inductive Acc A R | x : Prop := ...]

to control uniform parameters.

This replaces the attribute.

9 files changed, 66 insertions, 10 deletions

diff --git a/doc/changelog/02-specification-language/11600-uniform-syntax.rst b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
new file mode 100644
index 0000000000..3fa3f80301
--- /dev/null
+++ b/doc/changelog/02-specification-language/11600-uniform-syntax.rst
@@ -0,0 +1,4 @@
+- **Added:**
+  New syntax :g:`Inductive Acc A R | x : Prop := ...` to specify which
+  parameters of an inductive are uniform.
+  (`#11600 <https://github.com/coq/coq/pull/11600>`_, by Gaëtan Gilbert).
diff --git a/doc/sphinx/language/gallina-specification-language.rst b/doc/sphinx/language/gallina-specification-language.rst
index 09090ce89a..7ce4538a4d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,6 +1063,18 @@ Parameterized inductive types
         | cons3 : A -> list3 -> list3.
         End list3.
 
+     For finer control, you can use a ``|`` between the uniform and
+     the non-uniform parameters:
+
+     .. coqtop:: in reset
+
+        Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
+          := Acc_in : (forall y, R y x -> Acc y) -> Acc x.
+
+     The flag can then be seen as deciding whether the ``|`` is at the
+     beginning (when the flag is unset) or at the end (when it is set)
+     of the parameters when not explicitly given.
+
 .. 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 fdbad2ab9e..c7dfe69fb1 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -1476,7 +1476,7 @@ let do_build_inductive
   in
   let rel_ind i ext_rel_constructors =
     ((CAst.make @@ relnames.(i)),
-    rel_params,
+    (rel_params,None),
     Some rel_arities.(i),
     ext_rel_constructors),[]
   in
diff --git a/test-suite/success/uniform_inductive_parameters.v b/test-suite/success/uniform_inductive_parameters.v
index 42236a5313..e2b4694fff 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -11,3 +11,12 @@ Inductive list2 (A : Type) (A' := prod A A) :=
   | cons2 : A' -> list2 -> list2.
 Check (list2 : Type -> Type).
 Check (cons2 : forall A (A' := prod A A), A' -> list2 A -> list2 A).
+
+Inductive list3 | A := nil3 | cons3 : A -> list3 (A * A)%type -> list3 A.
+
+Unset Uniform Inductive Parameters.
+
+Inductive list4 A | := nil4 | cons4 : A -> list4 -> list4.
+
+Inductive Acc {A:Type} (R:A->A->Prop) | (x:A) : Prop
+  := Acc_in : (forall y, R y x -> Acc y) -> Acc x.
diff --git a/vernac/comInductive.ml b/vernac/comInductive.ml
index d711c9aea0..85f2bf3708 100644
--- a/vernac/comInductive.ml
+++ b/vernac/comInductive.ml
@@ -456,9 +456,19 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
   let sigma, arities = List.fold_left_map (pretype_ind_arity env_params) sigma arities in
   let arities, relevances, arityconcl, indimpls = List.split4 arities in
 
-  let fullarities = List.map (fun c -> EConstr.it_mkProd_or_LetIn c ctx_params) arities in
+  let lift1_ctx ctx =
+    let t = EConstr.it_mkProd_or_LetIn EConstr.mkProp ctx in
+    let t = EConstr.Vars.lift 1 t in
+    let ctx, _ = EConstr.decompose_prod_assum sigma t in
+    ctx
+  in
+  let ctx_params_lifted, fullarities = CList.fold_left_map
+      (fun ctx_params c -> lift1_ctx ctx_params, EConstr.it_mkProd_or_LetIn c ctx_params)
+      ctx_params
+      arities
+  in
   let env_ar = push_types env_uparams indnames relevances fullarities in
-  let env_ar_params = EConstr.push_rel_context ctx_params env_ar in
+  let env_ar_params = EConstr.push_rel_context ctx_params_lifted env_ar in
 
   (* Compute interpretation metadatas *)
   let indimpls = List.map (fun impls -> userimpls @ impls) indimpls in
@@ -509,6 +519,9 @@ let interp_mutual_inductive_gen env0 ~template udecl (uparamsl,paramsl,indl) not
 let eq_local_binders bl1 bl2 =
   List.equal local_binder_eq bl1 bl2
 
+let eq_params (up1,p1) (up2,p2) =
+  eq_local_binders up1 up2 && Option.equal eq_local_binders p1 p2
+
 let extract_coercions indl =
   let mkqid (_,({CAst.v=id},_)) = qualid_of_ident id in
   let extract lc = List.filter (fun (iscoe,_) -> iscoe) lc in
@@ -519,7 +532,7 @@ let extract_params indl =
   match paramsl with
   | [] -> anomaly (Pp.str "empty list of inductive types.")
   | params::paramsl ->
-      if not (List.for_all (eq_local_binders params) paramsl) then user_err Pp.(str
+      if not (List.for_all (eq_params params) paramsl) then user_err Pp.(str
         "Parameters should be syntactically the same for each inductive type.");
       params
 
@@ -544,7 +557,12 @@ type uniform_inductive_flag =
 let do_mutual_inductive ~template udecl indl ~cumulative ~poly ~private_ind ~uniform finite =
   let (params,indl),coes,ntns = extract_mutual_inductive_declaration_components indl in
   (* Interpret the types *)
-  let indl = match uniform with UniformParameters -> (params, [], indl) | NonUniformParameters -> ([], params, indl) in
+  let indl = match params with
+    | uparams, Some params -> (uparams, params, indl)
+    | params, None -> match uniform with
+      | UniformParameters -> (params, [], indl)
+      | NonUniformParameters -> ([], params, indl)
+  in
   let mie,pl,impls = interp_mutual_inductive_gen (Global.env()) ~template udecl indl ntns ~cumulative ~poly ~private_ind finite in
   (* Declare the mutual inductive block with its associated schemes *)
   ignore (DeclareInd.declare_mutual_inductive_with_eliminations mie pl impls);
diff --git a/vernac/g_vernac.mlg b/vernac/g_vernac.mlg
index 74249301d7..728c678055 100644
--- a/vernac/g_vernac.mlg
+++ b/vernac/g_vernac.mlg
@@ -395,9 +395,10 @@ GRAMMAR EXTEND Gram
   ;
   inductive_definition:
     [ [ oc = opt_coercion; id = ident_decl; indpar = binders;
+        extrapar = OPT [ "|"; p = binders -> { p } ];
         c = OPT [ ":"; c = lconstr -> { c } ];
         lc=opt_constructors_or_fields; ntn = decl_notation ->
-           { (((oc,id),indpar,c,lc),ntn) } ] ]
+           { (((oc,id),(indpar,extrapar),c,lc),ntn) } ] ]
   ;
   constructor_list_or_record_decl:
     [ [ "|"; l = LIST1 constructor SEP "|" -> { Constructors l }
diff --git a/vernac/ppvernac.ml b/vernac/ppvernac.ml
index 6240120cb0..b31ecea112 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -812,11 +812,12 @@ let string_of_definition_object_kind = let open Decls in function
           | RecordDecl (c,fs) ->
             pr_record_decl c fs
         in
-        let pr_oneind key (((coe,iddecl),indpar,s,lc),ntn) =
+        let pr_oneind key (((coe,iddecl),(indupar,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_and_type_binders_arg indupar ++
+              pr_opt (fun p -> str "|" ++ spc() ++ pr_and_type_binders_arg p) indpar ++
               pr_opt (fun s -> str":" ++ spc() ++ pr_lconstr_expr env sigma s) s ++
               str" :=") ++ pr_constructor_list lc ++
             prlist (pr_decl_notation @@ pr_constr env sigma) ntn
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index dec5a79892..63fc587f71 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -709,6 +709,10 @@ let vernac_inductive ~atts cum lo kind indl =
   if Option.has_some is_defclass then
     (* Definitional class case *)
     let (id, bl, c, l) = Option.get is_defclass in
+    let bl = match bl with
+      | bl, None -> bl
+      | _ -> CErrors.user_err Pp.(str "Definitional classes do not support the \"|\" syntax.")
+    in
     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),
@@ -729,6 +733,10 @@ let vernac_inductive ~atts cum lo kind indl =
     let () = List.iter check_where indl in
     let unpack ((id, bl, c, decl), _) = match decl with
     | RecordDecl (oc, fs) ->
+      let bl = match bl with
+        | bl, None -> bl
+        | _ -> CErrors.user_err Pp.(str "Records do not support the \"|\" syntax.")
+      in
       (id, bl, c, oc, fs)
     | Constructors _ -> assert false (* ruled out above *)
     in
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 8ead56dfdf..f9cde7a005 100644
--- a/vernac/vernacexpr.ml
+++ b/vernac/vernacexpr.ml
@@ -163,12 +163,15 @@ type constructor_expr = (lident * constr_expr) with_coercion
 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_params_expr = local_binder_expr list * local_binder_expr list option
+(** If the option is nonempty the "|" marker was used *)
+
 type inductive_expr =
-  ident_decl with_coercion * local_binder_expr list * constr_expr option *
+  ident_decl with_coercion * inductive_params_expr * constr_expr option *
     constructor_list_or_record_decl_expr
 
 type one_inductive_expr =
-  lident * local_binder_expr list * constr_expr option * constructor_expr list
+  lident * inductive_params_expr * constr_expr option * constructor_expr list
 
 type typeclass_constraint = name_decl * Glob_term.binding_kind * constr_expr
 and typeclass_context = typeclass_constraint list