aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml6
-rw-r--r--kernel/cbytegen.mli2
-rw-r--r--kernel/cooking.ml12
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/declarations.ml17
-rw-r--r--kernel/declareops.ml56
-rw-r--r--kernel/declareops.mli4
-rw-r--r--kernel/entries.ml24
-rw-r--r--kernel/indTyping.ml50
-rw-r--r--kernel/indTyping.mli3
-rw-r--r--kernel/indtypes.ml13
-rw-r--r--kernel/inductive.ml7
-rw-r--r--kernel/mod_typing.ml8
-rw-r--r--kernel/modops.ml7
-rw-r--r--kernel/modops.mli1
-rw-r--r--kernel/nativecode.ml6
-rw-r--r--kernel/reduction.ml22
-rw-r--r--kernel/safe_typing.ml29
-rw-r--r--kernel/subtyping.ml63
-rw-r--r--kernel/term_typing.ml34
-rw-r--r--kernel/univ.ml70
-rw-r--r--kernel/univ.mli44
22 files changed, 153 insertions, 327 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index b95a940c14..718584b3d4 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -881,11 +881,7 @@ let compile_constant_body ~fail_on_error env univs = function
| Undef _ | OpaqueDef _ | Primitive _ -> Some BCconstant
| Def sb ->
let body = Mod_subst.force_constr sb in
- let instance_size =
- match univs with
- | Monomorphic_const _ -> 0
- | Polymorphic_const univ -> Univ.AUContext.size univ
- in
+ let instance_size = Univ.AUContext.size (Declareops.universes_context univs) in
match kind body with
| Const (kn',u) when is_univ_copy instance_size u ->
(* we use the canonical name of the constant*)
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index b1b55aef48..6a9550342c 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -20,7 +20,7 @@ val compile : fail_on_error:bool ->
(** init, fun, fv *)
val compile_constant_body : fail_on_error:bool ->
- env -> constant_universes -> Constr.t Mod_subst.substituted constant_def ->
+ env -> universes -> Constr.t Mod_subst.substituted constant_def ->
body_code option
(** Shortcut of the previous function used during module strengthening *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 88586352f6..22de9bfad5 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -157,7 +157,7 @@ type inline = bool
type result = {
cook_body : constr Mod_subst.substituted constant_def;
cook_type : types;
- cook_universes : constant_universes;
+ cook_universes : universes;
cook_private_univs : Univ.ContextSet.t option;
cook_inline : inline;
cook_context : Constr.named_context option;
@@ -185,10 +185,10 @@ let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
let lift_univs cb subst auctx0 =
match cb.const_universes with
- | Monomorphic_const ctx ->
+ | Monomorphic ctx ->
assert (AUContext.is_empty auctx0);
- subst, (Monomorphic_const ctx)
- | Polymorphic_const auctx ->
+ subst, (Monomorphic ctx)
+ | Polymorphic auctx ->
(** Given a named instance [subst := uā‚€ ... uā‚™ā‚‹ā‚] together with an abstract
context [auctx0 := 0 ... n - 1 |= C{0, ..., n - 1}] of the same length,
and another abstract context relative to the former context
@@ -202,13 +202,13 @@ let lift_univs cb subst auctx0 =
*)
if (Univ.Instance.is_empty subst) then
(** Still need to take the union for the constraints between globals *)
- subst, (Polymorphic_const (AUContext.union auctx0 auctx))
+ subst, (Polymorphic (AUContext.union auctx0 auctx))
else
let ainst = Univ.make_abstract_instance auctx in
let subst = Instance.append subst ainst in
let substf = Univ.make_instance_subst subst in
let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
- subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
+ subst, (Polymorphic (AUContext.union auctx0 auctx'))
let cook_constant ~hcons { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 07c6f37fab..89b5c60ad5 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -20,7 +20,7 @@ type inline = bool
type result = {
cook_body : constr Mod_subst.substituted constant_def;
cook_type : types;
- cook_universes : constant_universes;
+ cook_universes : universes;
cook_private_univs : Univ.ContextSet.t option;
cook_inline : inline;
cook_context : Constr.named_context option;
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 1008492825..6777e0c223 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -53,9 +53,9 @@ type 'a constant_def =
| OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
| Primitive of CPrimitives.t (** or a primitive operation *)
-type constant_universes =
- | Monomorphic_const of Univ.ContextSet.t
- | Polymorphic_const of Univ.AUContext.t
+type universes =
+ | Monomorphic of Univ.ContextSet.t
+ | Polymorphic of Univ.AUContext.t
(** The [typing_flags] are instructions to the type-checker which
modify its behaviour. The typing flags used in the type-checking
@@ -92,7 +92,7 @@ type constant_body = {
const_body : Constr.t Mod_subst.substituted constant_def;
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
- const_universes : constant_universes;
+ const_universes : universes;
const_private_poly_univs : Univ.ContextSet.t option;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
@@ -185,11 +185,6 @@ type one_inductive_body = {
mind_reloc_tbl : Vmvalues.reloc_table;
}
-type abstract_inductive_universes =
- | Monomorphic_ind of Univ.ContextSet.t
- | Polymorphic_ind of Univ.AUContext.t
- | Cumulative_ind of Univ.ACumulativityInfo.t
-
type recursivity_kind =
| Finite (** = inductive *)
| CoFinite (** = coinductive *)
@@ -213,7 +208,9 @@ type mutual_inductive_body = {
mind_params_ctxt : Constr.rel_context; (** The context of parameters (includes let-in declaration) *)
- mind_universes : abstract_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+ mind_universes : universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
+
+ mind_variance : Univ.Variance.t array option; (** Variance info, [None] when non-cumulative. *)
mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 5686c4071d..9e0230c3ba 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -49,12 +49,24 @@ let hcons_template_arity ar =
(* List.Smart.map (Option.Smart.map Univ.hcons_univ_level) ar.template_param_levels; *)
template_level = Univ.hcons_univ ar.template_level }
+let universes_context = function
+ | Monomorphic _ -> Univ.AUContext.empty
+ | Polymorphic ctx -> ctx
+
+let abstract_universes = function
+ | Entries.Monomorphic_entry ctx ->
+ Univ.empty_level_subst, Monomorphic ctx
+ | Entries.Polymorphic_entry (nas, ctx) ->
+ let (inst, auctx) = Univ.abstract_universes nas ctx in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Polymorphic auctx)
+
(** {6 Constants } *)
let constant_is_polymorphic cb =
match cb.const_universes with
- | Monomorphic_const _ -> false
- | Polymorphic_const _ -> true
+ | Monomorphic _ -> false
+ | Polymorphic _ -> true
let constant_has_body cb = match cb.const_body with
@@ -62,9 +74,7 @@ let constant_has_body cb = match cb.const_body with
| Def _ | OpaqueDef _ -> true
let constant_polymorphic_context cb =
- match cb.const_universes with
- | Monomorphic_const _ -> Univ.AUContext.empty
- | Polymorphic_const ctx -> ctx
+ universes_context cb.const_universes
let is_opaque cb = match cb.const_body with
| OpaqueDef _ -> true
@@ -126,12 +136,12 @@ let hcons_const_def = function
Def (from_val (Constr.hcons constr))
| OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
-let hcons_const_universes cbu =
+let hcons_universes cbu =
match cbu with
- | Monomorphic_const ctx ->
- Monomorphic_const (Univ.hcons_universe_context_set ctx)
- | Polymorphic_const ctx ->
- Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
+ | Monomorphic ctx ->
+ Monomorphic (Univ.hcons_universe_context_set ctx)
+ | Polymorphic ctx ->
+ Polymorphic (Univ.hcons_abstract_universe_context ctx)
let hcons_const_private_univs = function
| None -> None
@@ -141,7 +151,7 @@ let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
const_type = Constr.hcons cb.const_type;
- const_universes = hcons_const_universes cb.const_universes;
+ const_universes = hcons_universes cb.const_universes;
const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
}
@@ -239,27 +249,21 @@ let subst_mind_body sub mib =
Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.Smart.map (subst_mind_packet sub) mib.mind_packets ;
mind_universes = mib.mind_universes;
+ mind_variance = mib.mind_variance;
mind_private = mib.mind_private;
mind_typing_flags = mib.mind_typing_flags;
}
let inductive_polymorphic_context mib =
- match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.AUContext.empty
- | Polymorphic_ind ctx -> ctx
- | Cumulative_ind cumi -> Univ.ACumulativityInfo.univ_context cumi
+ universes_context mib.mind_universes
let inductive_is_polymorphic mib =
match mib.mind_universes with
- | Monomorphic_ind _ -> false
- | Polymorphic_ind _ctx -> true
- | Cumulative_ind _cumi -> true
+ | Monomorphic _ -> false
+ | Polymorphic _ctx -> true
let inductive_is_cumulative mib =
- match mib.mind_universes with
- | Monomorphic_ind _ -> false
- | Polymorphic_ind _ctx -> false
- | Cumulative_ind _cumi -> true
+ Option.has_some mib.mind_variance
let inductive_make_projection ind mib ~proj_arg =
match mib.mind_record with
@@ -306,17 +310,11 @@ let hcons_mind_packet oib =
mind_user_lc = user;
mind_nf_lc = nf }
-let hcons_mind_universes miu =
- match miu with
- | Monomorphic_ind ctx -> Monomorphic_ind (Univ.hcons_universe_context_set ctx)
- | Polymorphic_ind ctx -> Polymorphic_ind (Univ.hcons_abstract_universe_context ctx)
- | Cumulative_ind cui -> Cumulative_ind (Univ.hcons_abstract_cumulativity_info cui)
-
let hcons_mind mib =
{ mib with
mind_packets = Array.Smart.map hcons_mind_packet mib.mind_packets;
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
- mind_universes = hcons_mind_universes mib.mind_universes }
+ mind_universes = hcons_universes mib.mind_universes }
(** Hashconsing of modules *)
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 35490ceef9..23a44433b3 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -15,6 +15,10 @@ open Univ
(** Operations concerning types in [Declarations] :
[constant_body], [mutual_inductive_body], [module_body] ... *)
+val universes_context : universes -> AUContext.t
+
+val abstract_universes : Entries.universes_entry -> Univ.universe_level_subst * universes
+
(** {6 Arities} *)
val map_decl_arity : ('a -> 'c) -> ('b -> 'd) ->
diff --git a/kernel/entries.ml b/kernel/entries.ml
index 013327599d..a3d32267a7 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -16,6 +16,12 @@ open Constr
constants/axioms, mutual inductive definitions, modules and module
types *)
+type universes_entry =
+ | Monomorphic_entry of Univ.ContextSet.t
+ | Polymorphic_entry of Name.t array * Univ.UContext.t
+
+type 'a in_universes_entry = 'a * universes_entry
+
(** {6 Declaration of inductive types. } *)
(** Assume the following definition in concrete syntax:
@@ -28,11 +34,6 @@ then, in i{^ th} block, [mind_entry_params] is [xn:Xn;...;x1:X1];
[mind_entry_lc] is [Ti1;...;Tini], defined in context [[A'1;...;A'p;x1:X1;...;xn:Xn]] where [A'i] is [Ai] generalized over [[x1:X1;...;xn:Xn]].
*)
-type inductive_universes =
- | Monomorphic_ind_entry of Univ.ContextSet.t
- | Polymorphic_ind_entry of Name.t array * Univ.UContext.t
- | Cumulative_ind_entry of Name.t array * Univ.CumulativityInfo.t
-
type one_inductive_entry = {
mind_entry_typename : Id.t;
mind_entry_arity : constr;
@@ -48,7 +49,8 @@ type mutual_inductive_entry = {
mind_entry_finite : Declarations.recursivity_kind;
mind_entry_params : Constr.rel_context;
mind_entry_inds : one_inductive_entry list;
- mind_entry_universes : inductive_universes;
+ mind_entry_universes : universes_entry;
+ mind_entry_variance : Univ.Variance.t array option;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
mind_entry_private : bool option;
@@ -58,12 +60,6 @@ type mutual_inductive_entry = {
type 'a proof_output = constr Univ.in_universe_context_set * 'a
type 'a const_entry_body = 'a proof_output Future.computation
-type constant_universes_entry =
- | Monomorphic_const_entry of Univ.ContextSet.t
- | Polymorphic_const_entry of Name.t array * Univ.UContext.t
-
-type 'a in_constant_universes_entry = 'a * constant_universes_entry
-
type 'a definition_entry = {
const_entry_body : 'a const_entry_body;
(* List of section variables *)
@@ -71,7 +67,7 @@ type 'a definition_entry = {
(* State id on which the completion of type checking is reported *)
const_entry_feedback : Stateid.t option;
const_entry_type : types option;
- const_entry_universes : constant_universes_entry;
+ const_entry_universes : universes_entry;
const_entry_opaque : bool;
const_entry_inline_code : bool }
@@ -85,7 +81,7 @@ type section_def_entry = {
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
- Constr.named_context option * types in_constant_universes_entry * inline
+ Constr.named_context option * types in_universes_entry * inline
type primitive_entry = {
prim_entry_type : types option;
diff --git a/kernel/indTyping.ml b/kernel/indTyping.ml
index 6976b2019d..a5dafc5ab5 100644
--- a/kernel/indTyping.ml
+++ b/kernel/indTyping.ml
@@ -87,23 +87,28 @@ let check_subtyping_arity_constructor env subst arcn numparams is_arity =
let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
if not is_arity then basic_check last_env codom else ()
-let check_cumulativity univs env_ar params data =
+let check_cumulativity univs variances env_ar params data =
+ let uctx = match univs with
+ | Monomorphic_entry _ -> raise (InductiveError BadUnivs)
+ | Polymorphic_entry (_,uctx) -> uctx
+ in
+ let instance = UContext.instance uctx in
+ if Instance.length instance != Array.length variances then raise (InductiveError BadUnivs);
let numparams = Context.Rel.nhyps params in
- let uctx = CumulativityInfo.univ_context univs in
- let new_levels = Array.init (UContext.size uctx)
+ let new_levels = Array.init (Instance.length instance)
(fun i -> Level.(make (UGlobal.make DirPath.empty i)))
in
let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
- LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
+ LMap.empty (Instance.to_array instance) new_levels
in
let dosubst = Vars.subst_univs_level_constr lmap in
let instance_other = Instance.of_array new_levels in
- let constraints_other = Univ.subst_univs_level_constraints lmap (Univ.UContext.constraints uctx) in
+ let constraints_other = Univ.subst_univs_level_constraints lmap (UContext.constraints uctx) in
let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
let env = Environ.push_context uctx_other env_ar in
let subtyp_constraints =
- CumulativityInfo.leq_constraints univs
- (UContext.instance uctx) instance_other
+ Univ.enforce_leq_variance_instances variances
+ instance instance_other
Constraint.empty
in
let env = Environ.add_constraints subtyp_constraints env in
@@ -236,8 +241,8 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
| None -> RegularArity {mind_user_arity=arity;mind_sort=Sorts.sort_of_univ ind_univ}
| Some min_univ ->
((match univs with
- | Monomorphic_ind _ -> ()
- | Polymorphic_ind _ | Cumulative_ind _ ->
+ | Monomorphic _ -> ()
+ | Polymorphic _ ->
CErrors.anomaly ~label:"polymorphic_template_ind"
Pp.(strbrk "Template polymorphism and full polymorphism are incompatible."));
TemplateArity {template_param_levels=param_ccls params; template_level=min_univ})
@@ -246,17 +251,6 @@ let abstract_packets univs usubst params ((arity,lc),(indices,splayed_lc),univ_i
let kelim = allowed_sorts univ_info in
(arity,lc), (indices,splayed_lc), kelim
-let abstract_inductive_universes = function
- | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
- | Polymorphic_ind_entry (nas, ctx) ->
- let (inst, auctx) = Univ.abstract_universes nas ctx in
- let inst = Univ.make_instance_subst inst in
- (inst, Polymorphic_ind auctx)
- | Cumulative_ind_entry (nas, cumi) ->
- let (inst, acumi) = Univ.abstract_cumulativity_info nas cumi in
- let inst = Univ.make_instance_subst inst in
- (inst, Cumulative_ind acumi)
-
let typecheck_inductive env (mie:mutual_inductive_entry) =
let () = match mie.mind_entry_inds with
| [] -> CErrors.anomaly Pp.(str "empty inductive types declaration.")
@@ -269,9 +263,8 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
(* universes *)
let env_univs =
match mie.mind_entry_universes with
- | Monomorphic_ind_entry ctx -> push_context_set ctx env
- | Polymorphic_ind_entry (_, ctx) -> push_context ctx env
- | Cumulative_ind_entry (_, cumi) -> push_context (Univ.CumulativityInfo.univ_context cumi) env
+ | Monomorphic_entry ctx -> push_context_set ctx env
+ | Polymorphic_entry (_, ctx) -> push_context ctx env
in
(* Params *)
@@ -287,13 +280,14 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
mie.mind_entry_inds data
in
- let () = match mie.mind_entry_universes with
- | Cumulative_ind_entry (_,univs) -> check_cumulativity univs env_ar params (List.map pi1 data)
- | Monomorphic_ind_entry _ | Polymorphic_ind_entry _ -> ()
+ let () = match mie.mind_entry_variance with
+ | None -> ()
+ | Some variances ->
+ check_cumulativity mie.mind_entry_universes variances env_ar params (List.map pi1 data)
in
(* Abstract universes *)
- let usubst, univs = abstract_inductive_universes mie.mind_entry_universes in
+ let usubst, univs = Declareops.abstract_universes mie.mind_entry_universes in
let params = Vars.subst_univs_level_context usubst params in
let data = List.map (abstract_packets univs usubst params) data in
@@ -304,4 +298,4 @@ let typecheck_inductive env (mie:mutual_inductive_entry) =
Environ.push_rel_context ctx env
in
- env_ar_par, univs, params, Array.of_list data
+ env_ar_par, univs, mie.mind_entry_variance, params, Array.of_list data
diff --git a/kernel/indTyping.mli b/kernel/indTyping.mli
index 8841e38636..2598548f3f 100644
--- a/kernel/indTyping.mli
+++ b/kernel/indTyping.mli
@@ -16,6 +16,7 @@ open Declarations
Returns:
- environment with inductives + parameters in rel context
- abstracted universes
+ - checked variance info
- parameters
- for each inductive,
(arity * constructors) (with params)
@@ -24,7 +25,7 @@ open Declarations
*)
val typecheck_inductive : env -> mutual_inductive_entry ->
env
- * abstract_inductive_universes
+ * universes * Univ.Variance.t array option
* Constr.rel_context
* ((inductive_arity * Constr.types array) *
(Constr.rel_context * (Constr.rel_context * Constr.types) array) *
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 674d7a2a91..8f06e1e4b8 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -414,11 +414,7 @@ exception UndefinableExpansion
a substitution of the form [params, x : ind params] *)
let compute_projections (kn, i as ind) mib =
let pkt = mib.mind_packets.(i) in
- let u = match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.Instance.empty
- | Polymorphic_ind auctx -> Univ.make_abstract_instance auctx
- | Cumulative_ind acumi -> Univ.make_abstract_instance (Univ.ACumulativityInfo.univ_context acumi)
- in
+ let u = Univ.make_abstract_instance (Declareops.inductive_polymorphic_context mib) in
let subst = List.init mib.mind_ntypes (fun i -> mkIndU ((kn, mib.mind_ntypes - i - 1), u)) in
let rctx, _ = decompose_prod_assum (substl subst pkt.mind_nf_lc.(0)) in
let ctx, paramslet = List.chop pkt.mind_consnrealdecls.(0) rctx in
@@ -471,7 +467,7 @@ let compute_projections (kn, i as ind) mib =
Array.of_list (List.rev labs),
Array.of_list (List.rev pbs)
-let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr recargs =
+let build_inductive env names prv univs variance paramsctxt kn isrecord isfinite inds nmr recargs =
let ntypes = Array.length inds in
(* Compute the set of used section variables *)
let hyps = used_section_variables env inds in
@@ -529,6 +525,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr
mind_params_ctxt = paramsctxt;
mind_packets = packets;
mind_universes = univs;
+ mind_variance = variance;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
@@ -563,7 +560,7 @@ let build_inductive env names prv univs paramsctxt kn isrecord isfinite inds nmr
let check_inductive env kn mie =
(* First type-check the inductive definition *)
- let (env_ar_par, univs, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
+ let (env_ar_par, univs, variance, paramsctxt, inds) = IndTyping.typecheck_inductive env mie in
(* Then check positivity conditions *)
let chkpos = (Environ.typing_flags env).check_guarded in
let names = Array.map_of_list (fun entry -> entry.mind_entry_typename, entry.mind_entry_consnames)
@@ -574,6 +571,6 @@ let check_inductive env kn mie =
(Array.map (fun ((_,lc),(indices,_),_) -> Context.Rel.nhyps indices,lc) inds)
in
(* Build the inductive packets *)
- build_inductive env names mie.mind_entry_private univs
+ build_inductive env names mie.mind_entry_private univs variance
paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index c62d0e7ded..848ae65c51 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -56,12 +56,7 @@ let inductive_paramdecls (mib,u) =
Vars.subst_instance_context u mib.mind_params_ctxt
let instantiate_inductive_constraints mib u =
- let process auctx = Univ.AUContext.instantiate u auctx in
- match mib.mind_universes with
- | Monomorphic_ind _ -> Univ.Constraint.empty
- | Polymorphic_ind auctx -> process auctx
- | Cumulative_ind cumi -> process (Univ.ACumulativityInfo.univ_context cumi)
-
+ Univ.AUContext.instantiate u (Declareops.inductive_polymorphic_context mib)
(************************************************************************)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f68dd158c2..421d932d9a 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -76,7 +76,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
as long as they have the right type *)
let c', univs, ctx' =
match cb.const_universes, ctx with
- | Monomorphic_const _, None ->
+ | Monomorphic _, None ->
let c',cst = match cb.const_body with
| Undef _ | OpaqueDef _ ->
let j = Typeops.infer env' c in
@@ -90,8 +90,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
| Primitive _ ->
error_incorrect_with_constraint lab
in
- c', Monomorphic_const Univ.ContextSet.empty, cst
- | Polymorphic_const uctx, Some ctx ->
+ c', Monomorphic Univ.ContextSet.empty, cst
+ | Polymorphic uctx, Some ctx ->
let () =
if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
@@ -114,7 +114,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
in
if not (Univ.Constraint.is_empty cst) then
error_incorrect_with_constraint lab;
- c, Polymorphic_const ctx, Univ.Constraint.empty
+ c, Polymorphic ctx, Univ.Constraint.empty
| _ -> error_incorrect_with_constraint lab
in
let def = Def (Mod_subst.from_val c') in
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1dc8eec0da..4f992d3972 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -50,6 +50,7 @@ type signature_mismatch_error =
| IncompatibleUniverses of Univ.univ_inconsistency
| IncompatiblePolymorphism of env * types * types
| IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
+ | IncompatibleVariance
type module_typing_error =
| SignatureMismatch of
@@ -325,11 +326,7 @@ let strengthen_const mp_from l cb resolver =
|_ ->
let kn = KerName.make mp_from l in
let con = constant_of_delta_kn resolver kn in
- let u =
- match cb.const_universes with
- | Monomorphic_const _ -> Univ.Instance.empty
- | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
- in
+ let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
const_private_poly_univs = None;
diff --git a/kernel/modops.mli b/kernel/modops.mli
index bb97f0171e..119ce2b359 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -111,6 +111,7 @@ type signature_mismatch_error =
| IncompatibleUniverses of Univ.univ_inconsistency
| IncompatiblePolymorphism of env * types * types
| IncompatibleConstraints of { got : Univ.AUContext.t; expect : Univ.AUContext.t }
+ | IncompatibleVariance
type module_typing_error =
| SignatureMismatch of
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index c32bdb85d6..df60899b95 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1851,11 +1851,7 @@ and compile_named env sigma univ auxdefs id =
Glet(Gnamed id, MLprimitive (Mk_var id))::auxdefs
let compile_constant env sigma prefix ~interactive con cb =
- let no_univs =
- match cb.const_universes with
- | Monomorphic_const _ -> true
- | Polymorphic_const ctx -> Int.equal (Univ.AUContext.size ctx) 0
- in
+ let no_univs = 0 = Univ.AUContext.size (Declareops.constant_polymorphic_context cb) in
begin match cb.const_body with
| Def t ->
let t = Mod_subst.force_constr t in
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 61051c001d..b583d33e29 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -244,18 +244,14 @@ let inductive_cumulativity_arguments (mind,ind) =
mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
let convert_inductives_gen cmp_instances cmp_cumul cv_pb (mind,ind) nargs u1 u2 s =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
- s
- | Declarations.Polymorphic_ind _ ->
- cmp_instances u1 u2 s
- | Declarations.Cumulative_ind cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> cmp_instances u1 u2 s
+ | Some variances ->
let num_param_arity = inductive_cumulativity_arguments (mind,ind) in
if not (Int.equal num_param_arity nargs) then
cmp_instances u1 u2 s
else
- cmp_cumul cv_pb (Univ.ACumulativityInfo.variance cumi) u1 u2 s
+ cmp_cumul cv_pb variances u1 u2 s
let convert_inductives cv_pb ind nargs u1 u2 (s, check) =
convert_inductives_gen (check.compare_instances ~flex:false) check.compare_cumul_instances
@@ -266,13 +262,9 @@ let constructor_cumulativity_arguments (mind, ind, ctor) =
mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(ctor - 1)
let convert_constructors_gen cmp_instances cmp_cumul (mind, ind, cns) nargs u1 u2 s =
- match mind.Declarations.mind_universes with
- | Declarations.Monomorphic_ind _ ->
- assert (Univ.Instance.length u1 = 0 && Univ.Instance.length u2 = 0);
- s
- | Declarations.Polymorphic_ind _ ->
- cmp_instances u1 u2 s
- | Declarations.Cumulative_ind _cumi ->
+ match mind.Declarations.mind_variance with
+ | None -> cmp_instances u1 u2 s
+ | Some _ ->
let num_cnstr_args = constructor_cumulativity_arguments (mind,ind,cns) in
if not (Int.equal num_cnstr_args nargs) then
cmp_instances u1 u2 s
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 18a257047d..dc15d9d25e 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -312,8 +312,8 @@ let universes_of_private eff =
| `Opaque (_, ctx) -> ctx :: acc
in
match eff.seff_body.const_universes with
- | Monomorphic_const ctx -> ctx :: acc
- | Polymorphic_const _ -> acc
+ | Monomorphic ctx -> ctx :: acc
+ | Polymorphic _ -> acc
in
List.fold_left fold [] (side_effects_of_private_constants eff)
@@ -465,7 +465,7 @@ let labels_of_mib mib =
let globalize_constant_universes env cb =
match cb.const_universes with
- | Monomorphic_const cstrs ->
+ | Monomorphic cstrs ->
Now (false, cstrs) ::
(match cb.const_body with
| (Undef _ | Def _ | Primitive _) -> []
@@ -476,15 +476,14 @@ let globalize_constant_universes env cb =
match Future.peek_val fc with
| None -> [Later fc]
| Some c -> [Now (false, c)])
- | Polymorphic_const _ ->
+ | Polymorphic _ ->
[Now (true, Univ.ContextSet.empty)]
let globalize_mind_universes mb =
match mb.mind_universes with
- | Monomorphic_ind ctx ->
+ | Monomorphic ctx ->
[Now (false, ctx)]
- | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
- | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
+ | Polymorphic _ -> [Now (true, Univ.ContextSet.empty)]
let constraints_of_sfb env sfb =
match sfb with
@@ -612,13 +611,13 @@ let inline_side_effects env body side_eff =
| _ -> assert false
in
match cb.const_universes with
- | Monomorphic_const univs ->
+ | Monomorphic univs ->
(** Abstract over the term at the top of the proof *)
let ty = cb.const_type in
let subst = Cmap_env.add c (Inr var) subst in
let ctx = Univ.ContextSet.union ctx univs in
(subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
- | Polymorphic_const _ ->
+ | Polymorphic _ ->
(** Inline the term to emulate universe polymorphism *)
let subst = Cmap_env.add c (Inl b) subst in
(subst, var, ctx, args)
@@ -700,10 +699,10 @@ let constant_entry_of_side_effect cb u =
let open Entries in
let univs =
match cb.const_universes with
- | Monomorphic_const uctx ->
- Monomorphic_const_entry uctx
- | Polymorphic_const auctx ->
- Polymorphic_const_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
+ | Monomorphic uctx ->
+ Monomorphic_entry uctx
+ | Polymorphic auctx ->
+ Polymorphic_entry (Univ.AUContext.names auctx, Univ.AUContext.repr auctx)
in
let pt =
match cb.const_body, u with
@@ -756,8 +755,8 @@ let export_side_effects mb env c =
let { seff_constant = kn; seff_body = cb ; _ } = eff in
let env = Environ.add_constant kn cb env in
match cb.const_universes with
- | Polymorphic_const _ -> env
- | Monomorphic_const ctx ->
+ | Polymorphic _ -> env
+ | Monomorphic ctx ->
let ctx = match eff.seff_env with
| `Nothing -> ctx
| `Opaque(_, ctx') -> Univ.ContextSet.union ctx' ctx
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 2fc3aa99b5..dea72e8b59 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -92,11 +92,25 @@ let check_conv_error error why cst poly f env a1 a2 =
with NotConvertible -> error why
| Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
-let check_polymorphic_instance error env auctx1 auctx2 =
- if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
- error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
- else
- Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+let check_universes error env u1 u2 =
+ match u1, u2 with
+ | Monomorphic _, Monomorphic _ -> env
+ | Polymorphic auctx1, Polymorphic auctx2 ->
+ if not (UGraph.check_subtype (Environ.universes env) auctx2 auctx1) then
+ error (IncompatibleConstraints { got = auctx1; expect = auctx2; } )
+ else
+ Environ.push_context ~strict:false (Univ.AUContext.repr auctx2) env
+ | Monomorphic _, Polymorphic _ -> error (PolymorphicStatusExpected true)
+ | Polymorphic _, Monomorphic _ -> error (PolymorphicStatusExpected false)
+
+let check_variance error v1 v2 =
+ match v1, v2 with
+ | None, None -> ()
+ | Some v1, Some v2 ->
+ if not (Array.for_all2 Variance.check_subtype v2 v1) then
+ error IncompatibleVariance
+ | None, Some _ -> error (CumulativeStatusExpected true)
+ | Some _, None -> error (CumulativeStatusExpected false)
(* for now we do not allow reorderings *)
@@ -110,29 +124,9 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
| IndType ((_,0), mib) -> Declareops.subst_mind_body subst1 mib
| _ -> error (InductiveFieldExpected mib2)
in
- let env, inst =
- match mib1.mind_universes, mib2.mind_universes with
- | Monomorphic_ind _, Monomorphic_ind _ -> env, Univ.Instance.empty
- | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
- let env = check_polymorphic_instance error env auctx auctx' in
- env, Univ.make_abstract_instance auctx'
- | Cumulative_ind cumi, Cumulative_ind cumi' ->
- (** Currently there is no way to control variance of inductive types, but
- just in case we require that they are in a subtyping relation. *)
- let () =
- let v = ACumulativityInfo.variance cumi in
- let v' = ACumulativityInfo.variance cumi' in
- if not (Array.for_all2 Variance.check_subtype v' v) then
- CErrors.anomaly Pp.(str "Variance of " ++ KerName.print kn1 ++
- str " is not compatible with the one of " ++ KerName.print kn2)
- in
- let auctx = Univ.ACumulativityInfo.univ_context cumi in
- let auctx' = Univ.ACumulativityInfo.univ_context cumi' in
- let env = check_polymorphic_instance error env auctx auctx' in
- env, Univ.make_abstract_instance auctx'
- | _ -> error
- (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
- in
+ let env = check_universes error env mib1.mind_universes mib2.mind_universes in
+ let () = check_variance error mib1.mind_variance mib2.mind_variance in
+ let inst = make_abstract_instance (Declareops.inductive_polymorphic_context mib1) in
let mib2 = Declareops.subst_mind_body subst2 mib2 in
let check_inductive_type cst name t1 t2 =
check_conv (NotConvertibleInductiveField name)
@@ -235,17 +229,8 @@ let check_constant cst env l info1 cb2 spec2 subst1 subst2 =
let cb1 = Declareops.subst_const_body subst1 cb1 in
let cb2 = Declareops.subst_const_body subst2 cb2 in
(* Start by checking universes *)
- let poly, env =
- match cb1.const_universes, cb2.const_universes with
- | Monomorphic_const _, Monomorphic_const _ ->
- false, env
- | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
- true, check_polymorphic_instance error env auctx1 auctx2
- | Monomorphic_const _, Polymorphic_const _ ->
- error (PolymorphicStatusExpected true)
- | Polymorphic_const _, Monomorphic_const _ ->
- error (PolymorphicStatusExpected false)
- in
+ let env = check_universes error env cb1.const_universes cb2.const_universes in
+ let poly = Declareops.constant_is_polymorphic cb1 in
(* Now check types *)
let typ1 = cb1.const_type in
let typ2 = cb2.const_type in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3cb5d17d34..929f1c13a3 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -65,23 +65,15 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
Feedback.feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes = function
- | Monomorphic_const_entry uctx ->
- Univ.empty_level_subst, Monomorphic_const uctx
- | Polymorphic_const_entry (nas, uctx) ->
- let sbst, auctx = Univ.abstract_universes nas uctx in
- let sbst = Univ.make_instance_subst sbst in
- sbst, Polymorphic_const auctx
-
let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
match dcl with
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
- | Monomorphic_const_entry uctx -> push_context_set ~strict:true uctx env
- | Polymorphic_const_entry (_, uctx) -> push_context ~strict:false uctx env
+ | Monomorphic_entry uctx -> push_context_set ~strict:true uctx env
+ | Polymorphic_entry (_, uctx) -> push_context ~strict:false uctx env
in
let j = infer env t in
- let usubst, univs = abstract_constant_universes uctx in
+ let usubst, univs = Declareops.abstract_universes uctx in
let c = Typeops.assumption_of_judgment env j in
let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
{
@@ -115,7 +107,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
| CPrimitives.OT_type _ -> Undef None in
{ Cooking.cook_body = cd;
cook_type = ty;
- cook_universes = Monomorphic_const uctxt;
+ cook_universes = Monomorphic uctxt;
cook_private_univs = None;
cook_inline = false;
cook_context = None
@@ -134,7 +126,7 @@ the polymorphic case
*)
| DefinitionEntry ({ const_entry_type = Some typ;
const_entry_opaque = true;
- const_entry_universes = Monomorphic_const_entry univs; _ } as c) ->
+ const_entry_universes = Monomorphic_entry univs; _ } as c) ->
let env = push_context_set ~strict:true univs env in
let { const_entry_body = body; const_entry_feedback = feedback_id ; _ } = c in
let tyj = infer_type env typ in
@@ -165,7 +157,7 @@ the polymorphic case
{
Cooking.cook_body = def;
cook_type = typ;
- cook_universes = Monomorphic_const univs;
+ cook_universes = Monomorphic univs;
cook_private_univs = None;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -183,11 +175,11 @@ the polymorphic case
body, Univ.ContextSet.union ctx ctx'
in
let env, usubst, univs, private_univs = match c.const_entry_universes with
- | Monomorphic_const_entry univs ->
+ | Monomorphic_entry univs ->
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
- env, Univ.empty_level_subst, Monomorphic_const ctx, None
- | Polymorphic_const_entry (nas, uctx) ->
+ env, Univ.empty_level_subst, Monomorphic ctx, None
+ | Polymorphic_entry (nas, uctx) ->
(** [ctx] must contain local universes, such that it has no impact
on the rest of the graph (up to transitivity). *)
let env = push_context ~strict:false uctx env in
@@ -200,7 +192,7 @@ the polymorphic case
if Univ.ContextSet.is_empty ctx then env, None
else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
in
- env, sbst, Polymorphic_const auctx, local
+ env, sbst, Polymorphic auctx, local
in
let j = infer env body in
let typ = match typ with
@@ -342,7 +334,7 @@ let translate_local_def env _id centry =
const_entry_secctx = centry.secdef_secctx;
const_entry_feedback = centry.secdef_feedback;
const_entry_type = centry.secdef_type;
- const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
+ const_entry_universes = Monomorphic_entry Univ.ContextSet.empty;
const_entry_opaque = false;
const_entry_inline_code = false;
} in
@@ -360,8 +352,8 @@ let translate_local_def env _id centry =
record_aux env ids_typ ids_def
end;
let () = match decl.cook_universes with
- | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
- | Polymorphic_const _ -> assert false
+ | Monomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+ | Polymorphic _ -> assert false
in
let c = match decl.cook_body with
| Def c -> Mod_subst.force_constr c
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8940c0337e..09bf695915 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -989,68 +989,6 @@ let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
let hcons_abstract_universe_context = AUContext.hcons
-(** Universe info for cumulative inductive types: A context of
- universe levels with universe constraints, representing local
- universe variables and constraints, together with an array of
- Variance.t.
-
- This data structure maintains the invariant that the variance
- array has the same length as the universe instance. *)
-module CumulativityInfo =
-struct
- type t = universe_context * Variance.t array
-
- let make x =
- if (Instance.length (UContext.instance (fst x))) =
- (Array.length (snd x)) then x
- else anomaly (Pp.str "Invalid subtyping information encountered!")
-
- let empty = (UContext.empty, [||])
- let is_empty (univs, variance) = UContext.is_empty univs && Array.is_empty variance
-
- let pr prl (univs, variance) =
- UContext.pr prl ~variance univs
-
- let hcons (univs, variance) = (* should variance be hconsed? *)
- (UContext.hcons univs, variance)
-
- let univ_context (univs, _subtypcst) = univs
- let variance (_univs, variance) = variance
-
- (** This function takes a universe context representing constraints
- of an inductive and produces a CumulativityInfo.t with the
- trivial subtyping relation. *)
- let from_universe_context univs =
- (univs, Array.init (UContext.size univs) (fun _ -> Variance.Invariant))
-
- let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
- let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
-
-end
-
-let hcons_cumulativity_info = CumulativityInfo.hcons
-
-module ACumulativityInfo =
-struct
- type t = AUContext.t * Variance.t array
-
- let repr (auctx,var) = AUContext.repr auctx, var
-
- let pr prl (univs, variance) =
- AUContext.pr prl ~variance univs
-
- let hcons (univs, variance) = (* should variance be hconsed? *)
- (AUContext.hcons univs, variance)
-
- let univ_context (univs, _subtypcst) = univs
- let variance (_univs, variance) = variance
-
- let leq_constraints (_,variance) u u' csts = Variance.leq_constraints variance u u' csts
- let eq_constraints (_,variance) u u' csts = Variance.eq_constraints variance u u' csts
-end
-
-let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
-
(** A set of universes with universe constraints.
We linearize the set to a list after typechecking.
Beware, representation could change.
@@ -1211,10 +1149,6 @@ let abstract_universes nas ctx =
let ctx = (nas, cstrs) in
instance, ctx
-let abstract_cumulativity_info nas (univs, variance) =
- let subst, univs = abstract_universes nas univs in
- subst, (univs, variance)
-
let rec compact_univ s vars i u =
match u with
| [] -> (s, List.rev vars)
@@ -1235,12 +1169,8 @@ let pr_constraints prl = Constraint.pr prl
let pr_universe_context = UContext.pr
-let pr_cumulativity_info = CumulativityInfo.pr
-
let pr_abstract_universe_context = AUContext.pr
-let pr_abstract_cumulativity_info = ACumulativityInfo.pr
-
let pr_universe_context_set = ContextSet.pr
let pr_universe_subst =
diff --git a/kernel/univ.mli b/kernel/univ.mli
index b83251e983..1fbebee350 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -368,45 +368,6 @@ type 'a univ_abstracted = {
val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
-(** Universe info for cumulative inductive types: A context of
- universe levels with universe constraints, representing local
- universe variables and constraints, together with an array of
- Variance.t.
-
- This data structure maintains the invariant that the variance
- array has the same length as the universe instance. *)
-module CumulativityInfo :
-sig
- type t
-
- val make : UContext.t * Variance.t array -> t
-
- val empty : t
- val is_empty : t -> bool
-
- val univ_context : t -> UContext.t
- val variance : t -> Variance.t array
-
- (** This function takes a universe context representing constraints
- of an inductive and produces a CumulativityInfo.t with the
- trivial subtyping relation. *)
- val from_universe_context : UContext.t -> t
-
- val leq_constraints : t -> Instance.t constraint_function
- val eq_constraints : t -> Instance.t constraint_function
-end
-
-module ACumulativityInfo :
-sig
- type t
-
- val repr : t -> CumulativityInfo.t
- val univ_context : t -> AUContext.t
- val variance : t -> Variance.t array
- val leq_constraints : t -> Instance.t constraint_function
- val eq_constraints : t -> Instance.t constraint_function
-end
-
(** Universe contexts (as sets) *)
(** A set of universes with universe Constraint.t.
@@ -487,7 +448,6 @@ val make_instance_subst : Instance.t -> universe_level_subst
val make_inverse_instance_subst : Instance.t -> universe_level_subst
val abstract_universes : Names.Name.t array -> UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : Names.Name.t array -> CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
(** TODO: move universe abstraction out of the kernel *)
val make_abstract_instance : AUContext.t -> Instance.t
@@ -505,10 +465,8 @@ val pr_constraint_type : constraint_type -> Pp.t
val pr_constraints : (Level.t -> Pp.t) -> Constraint.t -> Pp.t
val pr_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
UContext.t -> Pp.t
-val pr_cumulativity_info : (Level.t -> Pp.t) -> CumulativityInfo.t -> Pp.t
val pr_abstract_universe_context : (Level.t -> Pp.t) -> ?variance:Variance.t array ->
AUContext.t -> Pp.t
-val pr_abstract_cumulativity_info : (Level.t -> Pp.t) -> ACumulativityInfo.t -> Pp.t
val pr_universe_context_set : (Level.t -> Pp.t) -> ContextSet.t -> Pp.t
val explain_universe_inconsistency : (Level.t -> Pp.t) ->
univ_inconsistency -> Pp.t
@@ -524,5 +482,3 @@ val hcons_universe_set : LSet.t -> LSet.t
val hcons_universe_context : UContext.t -> UContext.t
val hcons_abstract_universe_context : AUContext.t -> AUContext.t
val hcons_universe_context_set : ContextSet.t -> ContextSet.t
-val hcons_cumulativity_info : CumulativityInfo.t -> CumulativityInfo.t
-val hcons_abstract_cumulativity_info : ACumulativityInfo.t -> ACumulativityInfo.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 15:09:15 +0000