aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/changelog/02-specification-language/11600-uniform-syntax.rst4
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst13
-rw-r--r--plugins/funind/glob_term_to_relation.ml2
-rw-r--r--test-suite/success/uniform_inductive_parameters.v25
-rw-r--r--vernac/comInductive.ml26
-rw-r--r--vernac/g_vernac.mlg3
-rw-r--r--vernac/ppvernac.ml5
-rw-r--r--vernac/vernacentries.ml43
-rw-r--r--vernac/vernacexpr.ml7
9 files changed, 82 insertions, 46 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 721c7a7a51..7ce4538a4d 100644
--- a/doc/sphinx/language/gallina-specification-language.rst
+++ b/doc/sphinx/language/gallina-specification-language.rst
@@ -1063,8 +1063,17 @@ 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.
+ 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 651247937d..e2b4694fff 100644
--- a/test-suite/success/uniform_inductive_parameters.v
+++ b/test-suite/success/uniform_inductive_parameters.v
@@ -1,23 +1,22 @@
-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)).
+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 97c9d23c68..882be6449d 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 0cf407619b..c6ba4e2c29 100644
--- a/vernac/ppvernac.ml
+++ b/vernac/ppvernac.ml
@@ -811,11 +811,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 e469323f50..63fc587f71 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -623,18 +623,16 @@ 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 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 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 vernac_record ~template udecl cum k poly finite records =
let cumulative = should_treat_as_cumulative cum poly in
@@ -682,6 +680,7 @@ 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
@@ -710,12 +709,14 @@ 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),
- { rf_subclass = coe' ; rf_priority = None ; rf_notation = [] ; rf_canonical = true }
- in
- let template, poly = Attributes.(parse Notations.(template ++ polymorphic) atts) in
+ { 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]]
else if List.for_all is_record indl then
(* Mutual record case *)
@@ -732,12 +733,15 @@ 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
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 *)
@@ -761,12 +765,9 @@ 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
- ComInductive.do_mutual_inductive ~template udecl indl ~cumulative ~poly
- ~private_ind:lo ~uniform finite
+ let uniform = should_treat_as_uniform () in
+ 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")
diff --git a/vernac/vernacexpr.ml b/vernac/vernacexpr.ml
index 3610240634..45018a246c 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 12:54:45 +0000