aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/context.ml8
-rw-r--r--kernel/context.mli2
-rw-r--r--kernel/cooking.ml4
-rw-r--r--kernel/declarations.ml1
-rw-r--r--kernel/declareops.ml3
-rw-r--r--kernel/indTyping.ml16
-rw-r--r--kernel/safe_typing.ml10
-rw-r--r--kernel/safe_typing.mli4
-rw-r--r--kernel/type_errors.ml7
-rw-r--r--kernel/type_errors.mli12
10 files changed, 37 insertions, 30 deletions
diff --git a/kernel/context.ml b/kernel/context.ml
index 7e394da2ed..500ed20343 100644
--- a/kernel/context.ml
+++ b/kernel/context.ml
@@ -196,12 +196,10 @@ struct
(** Return a new rel-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
- (** Return the number of {e local declarations} in a given context. *)
+ (** Return the number of {e local declarations} in a given rel-context. *)
let length = List.length
- (** [extended_rel_list n Γ] builds an instance [args] such that [Γ,Δ ⊢ args:Γ]
- with n = |Δ| and with the local definitions of [Γ] skipped in
- [args]. Example: for [x:T,y:=c,z:U] and [n]=2, it gives [Rel 5, Rel 3]. *)
+ (** Return the number of {e local assumptions} in a given rel-context. *)
let nhyps ctx =
let open Declaration in
let rec nhyps acc = function
@@ -413,7 +411,7 @@ struct
(** empty named-context *)
let empty = []
- (** empty named-context *)
+ (** Return a new named-context enriched by with a given inner-most declaration. *)
let add d ctx = d :: ctx
(** Return the number of {e local declarations} in a given named-context. *)
diff --git a/kernel/context.mli b/kernel/context.mli
index 8f233613da..04aa039a01 100644
--- a/kernel/context.mli
+++ b/kernel/context.mli
@@ -129,7 +129,7 @@ sig
(** Return a new rel-context enriched by with a given inner-most declaration. *)
val add : ('c, 't) Declaration.pt -> ('c, 't) pt -> ('c, 't) pt
- (** Return the number of {e local declarations} in a given context. *)
+ (** Return the number of {e local declarations} in a given rel-context. *)
val length : ('c, 't) pt -> int
(** Check whether given two rel-contexts are equal. *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index cebbfe4986..f1eb000c88 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -312,14 +312,14 @@ let cook_one_ind ~template_check ~ntypes
let arity = abstract_as_type (expmod arity) hyps in
let sort = destSort (expmod (mkSort sort)) in
RegularArity {mind_user_arity=arity; mind_sort=sort}
- | TemplateArity {template_param_levels=levels;template_level} ->
+ | TemplateArity {template_param_levels=levels;template_level;template_context} ->
let sec_levels = CList.map_filter (fun d ->
if RelDecl.is_local_assum d then Some (template_level_of_var ~template_check d)
else None)
section_decls
in
let levels = List.rev_append sec_levels levels in
- TemplateArity {template_param_levels=levels;template_level}
+ TemplateArity {template_param_levels=levels;template_level;template_context}
in
let mind_arity_ctxt =
let ctx = Context.Rel.map expmod mip.mind_arity_ctxt in
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 0b6e59bd5e..c550b0d432 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -32,6 +32,7 @@ type engagement = set_predicativity
type template_arity = {
template_param_levels : Univ.Level.t option list;
template_level : Univ.Universe.t;
+ template_context : Univ.ContextSet.t;
}
type ('a, 'b) declaration_arity =
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 27e3f84464..047027984d 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,7 +49,8 @@ let map_decl_arity f g = function
let hcons_template_arity ar =
{ template_param_levels = ar.template_param_levels;
(* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
- template_level = Univ.hcons_univ ar.template_level }
+ template_level = Univ.hcons_univ ar.template_level;
+ template_context = Univ.hcons_universe_context_set ar.template_context }
let universes_context = function
| Monomorphic _ -> Univ.AUContext.empty
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 591cd050a5..113ee787f2 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -66,7 +66,9 @@ let mind_check_names mie =
type univ_info = { ind_squashed : bool; ind_has_relevant_arg : bool;
ind_min_univ : Universe.t option; (* Some for template *)
- ind_univ : Universe.t }
+ ind_univ : Universe.t;
+ missing : Universe.Set.t; (* missing u <= ind_univ constraints *)
+ }
let check_univ_leq ?(is_real_arg=false) env u info =
let ind_univ = info.ind_univ in
@@ -78,9 +80,8 @@ let check_univ_leq ?(is_real_arg=false) env u info =
if type_in_type env || Univ.Universe.is_sprop u || UGraph.check_leq (universes env) u ind_univ
then { info with ind_min_univ = Option.map (Universe.sup u) info.ind_min_univ }
else if is_impredicative_univ env ind_univ
- then if Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
- else raise (InductiveError BadUnivs)
- else raise (InductiveError BadUnivs)
+ && Option.is_empty info.ind_min_univ then { info with ind_squashed = true }
+ else {info with missing = Universe.Set.add u info.missing}
let check_context_univs ~ctor env info ctx =
let check_one d (info,env) =
@@ -109,6 +110,7 @@ let check_arity env_params env_ar ind =
ind_has_relevant_arg=false;
ind_min_univ;
ind_univ=Sorts.univ_of_sort ind_sort;
+ missing=Universe.Set.empty;
}
in
let univ_info = check_indices_matter env_params univ_info indices in
@@ -174,7 +176,7 @@ let check_record data =
(* - all_sorts in case of small, unitary Prop (not smashed) *)
(* - logical_sorts in case of large, unitary Prop (smashed) *)
-let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_} =
+let allowed_sorts {ind_squashed;ind_univ;ind_min_univ=_;ind_has_relevant_arg=_;missing=_} =
if not ind_squashed then InType
else Sorts.family (Sorts.sort_of_univ ind_univ)
@@ -224,6 +226,8 @@ let template_polymorphic_univs ~template_check ~ctor_levels uctx paramsctxt conc
params, univs
let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,splayed_lc),univ_info) =
+ if not (Universe.Set.is_empty univ_info.missing)
+ then raise (InductiveError (MissingConstraints (univ_info.missing,univ_info.ind_univ)));
let arity = Vars.subst_univs_level_constr usubst arity in
let lc = Array.map (Vars.subst_univs_level_constr usubst) lc in
let indices = Vars.subst_univs_level_context usubst indices in
@@ -270,7 +274,7 @@ let abstract_packets ~template_check univs usubst params ((arity,lc),(indices,sp
CErrors.user_err
Pp.(strbrk "Ill-formed template inductive declaration: not polymorphic on any universe.")
else
- TemplateArity {template_param_levels = param_levels; template_level = min_univ}
+ TemplateArity {template_param_levels = param_levels; template_level = min_univ; template_context = ctx }
in
let kelim = allowed_sorts univ_info in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index e8adde2605..8db8a044a8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -759,7 +759,7 @@ let translate_direct_opaque env kn ce =
let () = assert (is_empty_private u) in
{ cb with const_body = OpaqueDef c }
-let export_side_effects mb env (b_ctx, eff) =
+let export_side_effects mb env eff =
let not_exists e = not (Environ.mem_constant e.seff_constant env) in
let aux (acc,sl) e =
if not (not_exists e) then acc, sl
@@ -776,7 +776,7 @@ let export_side_effects mb env (b_ctx, eff) =
in
let rec translate_seff sl seff acc env =
match seff with
- | [] -> List.rev acc, b_ctx
+ | [] -> List.rev acc
| eff :: rest ->
if Int.equal sl 0 then
let env, cb =
@@ -805,8 +805,8 @@ let push_opaque_proof pf senv =
let senv = { senv with env = Environ.set_opaque_tables senv.env otab } in
senv, o
-let export_private_constants ce senv =
- let exported, ce = export_side_effects senv.revstruct senv.env ce in
+let export_private_constants eff senv =
+ let exported = export_side_effects senv.revstruct senv.env eff in
let map senv (kn, c) = match c.const_body with
| OpaqueDef p ->
let local = empty_private c.const_universes in
@@ -819,7 +819,7 @@ let export_private_constants ce senv =
let exported = List.map (fun (kn, _) -> kn) exported in
(* No delayed constants to declare *)
let senv = List.fold_left add_constant_aux senv bodies in
- (ce, exported), senv
+ exported, senv
let add_constant l decl senv =
let kn = Constant.make2 senv.modpath l in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index e6f2fc4a5d..e472dfd5e5 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -86,8 +86,8 @@ type side_effect_declaration =
type exported_private_constant = Constant.t
val export_private_constants :
- private_constants Entries.proof_output ->
- (Constr.constr Univ.in_universe_context_set * exported_private_constant list) safe_transformer
+ private_constants ->
+ exported_private_constant list safe_transformer
(** returns the main constant *)
val add_constant :
diff --git a/kernel/type_errors.ml b/kernel/type_errors.ml
index f221ac7a4f..c2cdf98ee8 100644
--- a/kernel/type_errors.ml
+++ b/kernel/type_errors.ml
@@ -12,6 +12,7 @@ open Names
open Constr
open Environ
open Reduction
+open Univ
(* Type errors. *)
@@ -63,8 +64,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -83,7 +84,7 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
exception InductiveError of inductive_error
diff --git a/kernel/type_errors.mli b/kernel/type_errors.mli
index ae6fd31762..0f29717f12 100644
--- a/kernel/type_errors.mli
+++ b/kernel/type_errors.mli
@@ -11,6 +11,7 @@
open Names
open Constr
open Environ
+open Univ
(** Type errors. {% \label{typeerrors} %} *)
@@ -64,8 +65,8 @@ type ('constr, 'types) ptype_error =
| IllFormedRecBody of 'constr pguard_error * Name.t Context.binder_annot array * int * env * ('constr, 'types) punsafe_judgment array
| IllTypedRecBody of
int * Name.t Context.binder_annot array * ('constr, 'types) punsafe_judgment array * 'types array
- | UnsatisfiedConstraints of Univ.Constraint.t
- | UndeclaredUniverse of Univ.Level.t
+ | UnsatisfiedConstraints of Constraint.t
+ | UndeclaredUniverse of Level.t
| DisallowedSProp
| BadRelevance
@@ -86,7 +87,8 @@ type inductive_error =
| NotAnArity of env * constr
| BadEntry
| LargeNonPropInductiveNotInType
- | BadUnivs
+ | MissingConstraints of (Universe.Set.t * Universe.t)
+ (* each universe in the set should have been <= the other one *)
exception InductiveError of inductive_error
@@ -133,9 +135,9 @@ val error_ill_typed_rec_body :
val error_elim_explain : Sorts.family -> Sorts.family -> arity_error
-val error_unsatisfied_constraints : env -> Univ.Constraint.t -> 'a
+val error_unsatisfied_constraints : env -> Constraint.t -> 'a
-val error_undeclared_universe : env -> Univ.Level.t -> 'a
+val error_undeclared_universe : env -> Level.t -> 'a
val error_disallowed_sprop : env -> 'a
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 11:22:16 +0000