aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/sphinx/language/gallina-specification-language.rst3
-rw-r--r--plugins/funind/glob_term_to_relation.ml8
-rw-r--r--stm/vernac_classifier.ml2
-rw-r--r--test-suite/success/uniform_inductive_parameters.v18
-rw-r--r--vernac/g_vernac.mlg17
-rw-r--r--vernac/ppvernac.ml13
-rw-r--r--vernac/vernacentries.ml92
-rw-r--r--vernac/vernacexpr.ml5
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 13:24:39 +0000