aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
diff options
context:
space:
mode:
authorGravatar Amin Timany <amintimany@gmail.com>2017-06-01 16:18:19 +0200
committerGravatar Emilio Jesus Gallego Arias <e+git@x80.org>2017-06-16 04:51:19 +0200
commitff918e4bb0ae23566e038f4b55d84dd2c343f95e (patch)
treeebab76cc4dedaf307f96088a3756d8292a341433 /kernel
parent3380f47d2bb38d549fcdac8fb073f9aa1f259a23 (diff)
Clean up universes of constants and inductives
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cbytegen.ml4
-rw-r--r--kernel/cbytegen.mli2
-rw-r--r--kernel/cooking.ml43
-rw-r--r--kernel/cooking.mli3
-rw-r--r--kernel/declarations.ml16
-rw-r--r--kernel/declareops.ml124
-rw-r--r--kernel/declareops.mli15
-rw-r--r--kernel/entries.mli9
-rw-r--r--kernel/environ.ml46
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/indtypes.ml69
-rw-r--r--kernel/indtypes.mli11
-rw-r--r--kernel/inductive.ml10
-rw-r--r--kernel/mod_typing.ml23
-rw-r--r--kernel/modops.ml11
-rw-r--r--kernel/modops.mli1
-rw-r--r--kernel/nativecode.ml7
-rw-r--r--kernel/opaqueproof.ml2
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/reduction.ml67
-rw-r--r--kernel/safe_typing.ml79
-rw-r--r--kernel/subtyping.ml87
-rw-r--r--kernel/term_typing.ml97
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/univ.ml66
-rw-r--r--kernel/univ.mli55
-rw-r--r--kernel/vconv.ml50
27 files changed, 568 insertions, 338 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 57b397e6f..02c6a2c71 100644
--- a/kernel/cbytegen.ml
+++ b/kernel/cbytegen.ml
@@ -992,8 +992,8 @@ let compile_constant_body fail_on_error env univs = function
let body = Mod_subst.force_constr sb in
let instance_size =
match univs with
- | None -> 0
- | Some univ -> Univ.UContext.size univ
+ | Monomorphic_const _ -> 0
+ | Polymorphic_const univ -> Univ.AUContext.size univ
in
match kind_of_term body with
| Const (kn',u) when is_univ_copy instance_size u ->
diff --git a/kernel/cbytegen.mli b/kernel/cbytegen.mli
index c0f48641c..48c2e4533 100644
--- a/kernel/cbytegen.mli
+++ b/kernel/cbytegen.mli
@@ -10,7 +10,7 @@ val compile : bool -> (* Fail on error with a nice user message, otherwise simpl
(** init, fun, fv *)
val compile_constant_body : bool ->
- env -> constant_universes option -> constant_def -> body_code option
+ env -> constant_universes -> 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 4deadff0a..000865364 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -153,8 +153,7 @@ type inline = bool
type result =
constant_def * constant_type * projection_body option *
- bool * constant_universes * inline
- * Context.Named.t option
+ constant_universes * inline * Context.Named.t option
let on_body ml hy f = function
| Undef _ as x -> x
@@ -179,17 +178,21 @@ let cook_constr { Opaqueproof.modlist ; abstract } c =
abstract_constant_body (expmod c) hyps
let lift_univs cb subst =
- if cb.const_polymorphic && not (Univ.LMap.is_empty subst) then
- let inst = Univ.UContext.instance cb.const_universes in
- let cstrs = Univ.UContext.constraints cb.const_universes in
- let len = Univ.LMap.cardinal subst in
- let subst =
- Array.fold_left_i (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
- subst (Univ.Instance.to_array inst)
- in
- let cstrs' = Univ.subst_univs_level_constraints subst cstrs in
- subst, Univ.UContext.make (inst,cstrs')
- else subst, cb.const_universes
+ match cb.const_universes with
+ | Monomorphic_const ctx -> subst, (Monomorphic_const ctx)
+ | Polymorphic_const auctx ->
+ if (Univ.LMap.is_empty subst) then
+ subst, (Polymorphic_const auctx)
+ else
+ let inst = Univ.AUContext.instance auctx in
+ let len = Univ.LMap.cardinal subst in
+ let subst =
+ Array.fold_left_i
+ (fun i acc v -> Univ.LMap.add (Level.var i) (Level.var (i + len)) acc)
+ subst (Univ.Instance.to_array inst)
+ in
+ let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
+ subst, (Polymorphic_const auctx')
let cook_constant ~hcons env { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
@@ -243,15 +246,15 @@ let cook_constant ~hcons env { from = cb; info } =
proj_eta = etab, etat;
proj_type = ty'; proj_body = c' }
in
- let univs =
- let abs' =
- if cb.const_polymorphic then abs_ctx
- else instantiate_univ_context abs_ctx
- in
- UContext.union abs' univs
+ let univs =
+ match univs with
+ | Monomorphic_const ctx ->
+ Monomorphic_const (UContext.union (instantiate_univ_context abs_ctx) ctx)
+ | Polymorphic_const auctx ->
+ Polymorphic_const (AUContext.union abs_ctx auctx)
in
(body, typ, Option.map projection cb.const_proj,
- cb.const_polymorphic, univs, cb.const_inline_code,
+ univs, cb.const_inline_code,
Some const_hyps)
(* let cook_constant_key = Profile.declare_profile "cook_constant" *)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 7d47eba23..9db85a4a1 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -18,8 +18,7 @@ type inline = bool
type result =
constant_def * constant_type * projection_body option *
- bool * constant_universes * inline
- * Context.Named.t option
+ constant_universes * inline * Context.Named.t option
val cook_constant : hcons:bool -> env -> recipe -> result
val cook_constr : Opaqueproof.cooking_info -> Term.constr -> Term.constr
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index ae4732456..f3b7ae2b2 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -64,7 +64,9 @@ type constant_def =
| Def of constr Mod_subst.substituted (** or a transparent global definition *)
| OpaqueDef of Opaqueproof.opaque (** or an opaque global definition *)
-type constant_universes = Univ.universe_context
+type constant_universes =
+ | Monomorphic_const of Univ.universe_context
+ | Polymorphic_const of Univ.abstract_universe_context
(** The [typing_flags] are instructions to the type-checker which
modify its behaviour. The typing flags used in the type-checking
@@ -83,7 +85,6 @@ type constant_body = {
const_body : constant_def;
const_type : constant_type;
const_body_code : Cemitcodes.to_patch_substituted option;
- const_polymorphic : bool; (** Is it polymorphic or not *)
const_universes : constant_universes;
const_proj : projection_body option;
const_inline_code : bool;
@@ -168,6 +169,11 @@ type one_inductive_body = {
mind_reloc_tbl : Cbytecodes.reloc_table;
}
+type abstrac_inductive_universes =
+ | Monomorphic_ind of Univ.universe_context
+ | Polymorphic_ind of Univ.abstract_universe_context
+ | Cumulative_ind of Univ.abstract_cumulativity_info
+
type mutual_inductive_body = {
mind_packets : one_inductive_body array; (** The component of the mutual inductive block *)
@@ -186,11 +192,7 @@ type mutual_inductive_body = {
mind_params_ctxt : Context.Rel.t; (** The context of parameters (includes let-in declaration) *)
- mind_polymorphic : bool; (** Is it polymorphic or not *)
-
- mind_cumulative : bool; (** Is it cumulative or not *)
-
- mind_universes : Univ.universe_info_ind; (** Local universe variables and constraints together with subtyping constraints *)
+ mind_universes : abstrac_inductive_universes; (** Information about monomorphic/polymorphic/cumulative inductives and their universes *)
mind_private : bool option; (** allow pattern-matching: Some true ok, Some false blocked *)
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 1d91b2d41..72b490768 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -45,14 +45,15 @@ let hcons_template_arity ar =
(** {6 Constants } *)
let instantiate cb c =
- if cb.const_polymorphic then
- Vars.subst_instance_constr (Univ.UContext.instance cb.const_universes) c
- else c
+ match cb.const_universes with
+ | Monomorphic_const _ -> c
+ | Polymorphic_const ctx ->
+ Vars.subst_instance_constr (Univ.AUContext.instance ctx) c
-let instantiate_constraints cb cst =
- if cb.const_polymorphic then
- Univ.subst_instance_constraints (Univ.UContext.instance cb.const_universes) cst
- else cst
+let constant_is_polymorphic cb =
+ match cb.const_universes with
+ | Monomorphic_const _ -> false
+ | Polymorphic_const _ -> true
let body_of_constant otab cb = match cb.const_body with
| Undef _ -> None
@@ -67,34 +68,55 @@ let type_of_constant cb =
| TemplateArity _ as x -> x
let constraints_of_constant otab cb =
- let cst = Univ.Constraint.union
- (Univ.UContext.constraints cb.const_universes)
- (match cb.const_body with
- | Undef _ -> Univ.empty_constraint
- | Def c -> Univ.empty_constraint
- | OpaqueDef o ->
- Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
- in instantiate_constraints cb cst
+ match cb.const_universes with
+ | Polymorphic_const ctx ->
+ Univ.UContext.constraints (Univ.instantiate_univ_context ctx)
+ | Monomorphic_const ctx ->
+ Univ.Constraint.union
+ (Univ.UContext.constraints ctx)
+ (match cb.const_body with
+ | Undef _ -> Univ.empty_constraint
+ | Def c -> Univ.empty_constraint
+ | OpaqueDef o ->
+ Univ.ContextSet.constraints (Opaqueproof.force_constraints otab o))
let universes_of_constant otab cb =
match cb.const_body with
- | Undef _ | Def _ -> cb.const_universes
+ | Undef _ | Def _ ->
+ begin
+ match cb.const_universes with
+ | Monomorphic_const ctx -> ctx
+ | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+ end
| OpaqueDef o ->
- let body_uctxs = Opaqueproof.force_constraints otab o in
- assert(not cb.const_polymorphic || Univ.ContextSet.is_empty body_uctxs);
- let uctxs = Univ.ContextSet.of_context cb.const_universes in
- Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+ let body_uctxs = Opaqueproof.force_constraints otab o in
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ let uctxs = Univ.ContextSet.of_context ctx in
+ Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs)
+ | Polymorphic_const ctx ->
+ assert(Univ.ContextSet.is_empty body_uctxs);
+ Univ.instantiate_univ_context ctx
let universes_of_polymorphic_constant otab cb =
- if cb.const_polymorphic then
- let univs = universes_of_constant otab cb in
- Univ.instantiate_univ_context univs
- else Univ.UContext.empty
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.UContext.empty
+ | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
let constant_has_body cb = match cb.const_body with
| Undef _ -> false
| Def _ | OpaqueDef _ -> true
+let constant_polymorphic_instance cb =
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.Instance.empty
+ | Polymorphic_const ctx -> Univ.AUContext.instance ctx
+
+let constant_polymorphic_context cb =
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.UContext.empty
+ | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
+
let is_opaque cb = match cb.const_body with
| OpaqueDef _ -> true
| Undef _ | Def _ -> false
@@ -142,7 +164,6 @@ let subst_const_body sub cb =
const_proj = proj';
const_body_code =
Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
- const_polymorphic = cb.const_polymorphic;
const_universes = cb.const_universes;
const_inline_code = cb.const_inline_code;
const_typing_flags = cb.const_typing_flags }
@@ -173,11 +194,18 @@ let hcons_const_def = function
Def (from_val (Term.hcons_constr constr))
| OpaqueDef _ as x -> x (* hashconsed when turned indirect *)
+let hcons_const_universes cbu =
+ match cbu with
+ | Monomorphic_const ctx ->
+ Monomorphic_const (Univ.hcons_universe_context ctx)
+ | Polymorphic_const ctx ->
+ Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
+
let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
const_type = hcons_const_type cb.const_type;
- const_universes = Univ.hcons_universe_context cb.const_universes }
+ const_universes = hcons_const_universes cb.const_universes }
(** {6 Inductive types } *)
@@ -266,22 +294,36 @@ let subst_mind_body sub mib =
mind_params_ctxt =
Context.Rel.map (subst_mps sub) mib.mind_params_ctxt;
mind_packets = Array.smartmap (subst_mind_packet sub) mib.mind_packets ;
- mind_polymorphic = mib.mind_polymorphic;
- mind_cumulative = mib.mind_cumulative;
mind_universes = mib.mind_universes;
mind_private = mib.mind_private;
mind_typing_flags = mib.mind_typing_flags;
}
-let inductive_instance mib =
- if mib.mind_polymorphic then
- Univ.UContext.instance (Univ.UInfoInd.univ_context mib.mind_universes)
- else Univ.Instance.empty
-
-let inductive_context mib =
- if mib.mind_polymorphic then
- Univ.instantiate_univ_context (Univ.UInfoInd.univ_context mib.mind_universes)
- else Univ.UContext.empty
+let inductive_polymorphic_instance mib =
+ match mib.mind_universes with
+ | Monomorphic_ind _ -> Univ.Instance.empty
+ | Polymorphic_ind ctx -> Univ.AUContext.instance ctx
+ | Cumulative_ind cumi ->
+ Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
+
+let inductive_polymorphic_context mib =
+ match mib.mind_universes with
+ | Monomorphic_ind _ -> Univ.UContext.empty
+ | Polymorphic_ind ctx -> Univ.instantiate_univ_context ctx
+ | Cumulative_ind cumi ->
+ Univ.instantiate_univ_context (Univ.ACumulativityInfo.univ_context cumi)
+
+let inductive_is_polymorphic mib =
+ match mib.mind_universes with
+ | Monomorphic_ind _ -> false
+ | Polymorphic_ind ctx -> true
+ | Cumulative_ind cumi -> true
+
+let inductive_is_cumulative mib =
+ match mib.mind_universes with
+ | Monomorphic_ind _ -> false
+ | Polymorphic_ind ctx -> false
+ | Cumulative_ind cumi -> true
(** {6 Hash-consing of inductive declarations } *)
@@ -309,11 +351,17 @@ 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 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.smartmap hcons_mind_packet mib.mind_packets;
mind_params_ctxt = hcons_rel_context mib.mind_params_ctxt;
- mind_universes = Univ.hcons_universe_info_ind mib.mind_universes }
+ mind_universes = hcons_mind_universes mib.mind_universes }
(** {6 Stm machinery } *)
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index 6650b6b7b..811a28aa6 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -27,6 +27,12 @@ val subst_const_body : substitution -> constant_body -> constant_body
val constant_has_body : constant_body -> bool
+val constant_polymorphic_instance : constant_body -> universe_instance
+val constant_polymorphic_context : constant_body -> universe_context
+
+(** Is the constant polymorphic? *)
+val constant_is_polymorphic : constant_body -> bool
+
(** Accessing const_body, forcing access to opaque proof term if needed.
Only use this function if you know what you're doing. *)
@@ -66,8 +72,13 @@ val subst_wf_paths : substitution -> wf_paths -> wf_paths
val subst_mind_body : substitution -> mutual_inductive_body -> mutual_inductive_body
-val inductive_instance : mutual_inductive_body -> universe_instance
-val inductive_context : mutual_inductive_body -> universe_context
+val inductive_polymorphic_instance : mutual_inductive_body -> universe_instance
+val inductive_polymorphic_context : mutual_inductive_body -> universe_context
+
+(** Is the inductive polymorphic? *)
+val inductive_is_polymorphic : mutual_inductive_body -> bool
+(** Is the inductive cumulative? *)
+val inductive_is_cumulative : mutual_inductive_body -> bool
(** {6 Kernel flags} *)
diff --git a/kernel/entries.mli b/kernel/entries.mli
index 9c17346f2..f133587c1 100644
--- a/kernel/entries.mli
+++ b/kernel/entries.mli
@@ -34,6 +34,11 @@ 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.universe_context
+ | Polymorphic_ind_entry of Univ.universe_context
+ | Cumulative_ind_entry of Univ.cumulativity_info
+
type one_inductive_entry = {
mind_entry_typename : Id.t;
mind_entry_arity : constr;
@@ -49,9 +54,7 @@ type mutual_inductive_entry = {
mind_entry_finite : Decl_kinds.recursivity_kind;
mind_entry_params : (Id.t * local_entry) list;
mind_entry_inds : one_inductive_entry list;
- mind_entry_polymorphic : bool;
- mind_entry_cumulative : bool;
- mind_entry_universes : Univ.universe_info_ind;
+ mind_entry_universes : inductive_universes;
(* universe constraints and the constraints for subtyping of
inductive types in the block. *)
mind_entry_private : bool option;
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 5727bf2ea..1ab5b7a8d 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -228,8 +228,10 @@ let add_constant kn cb env =
add_constant_key kn cb no_link_info env
let constraints_of cb u =
- let univs = cb.const_universes in
- Univ.subst_instance_constraints u (Univ.UContext.constraints univs)
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.Constraint.empty
+ | Polymorphic_const ctx ->
+ Univ.UContext.constraints (Univ.subst_instance_context u ctx)
let map_regular_arity f = function
| RegularArity a as ar ->
@@ -240,15 +242,23 @@ let map_regular_arity f = function
(* constant_type gives the type of a constant *)
let constant_type env (kn,u) =
let cb = lookup_constant kn env in
- if cb.const_polymorphic then
- let csts = constraints_of cb u in
- (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
- else cb.const_type, Univ.Constraint.empty
+ match cb.const_universes with
+ | Monomorphic_const _ -> cb.const_type, Univ.Constraint.empty
+ | Polymorphic_const ctx ->
+ let csts = constraints_of cb u in
+ (map_regular_arity (subst_instance_constr u) cb.const_type, csts)
+
+let constant_instance env kn =
+ let cb = lookup_constant kn env in
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.Instance.empty
+ | Polymorphic_const ctx -> Univ.AUContext.instance ctx
let constant_context env kn =
let cb = lookup_constant kn env in
- if cb.const_polymorphic then cb.const_universes
- else Univ.UContext.empty
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.UContext.empty
+ | Polymorphic_const ctx -> Univ.instantiate_univ_context ctx
type const_evaluation_result = NoBody | Opaque | IsProj
@@ -259,10 +269,14 @@ let constant_value env (kn,u) =
if cb.const_proj = None then
match cb.const_body with
| Def l_body ->
- if cb.const_polymorphic then
- let csts = constraints_of cb u in
- (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
- else Mod_subst.force_constr l_body, Univ.Constraint.empty
+ begin
+ match cb.const_universes with
+ | Monomorphic_const _ ->
+ (Mod_subst.force_constr l_body, Univ.Constraint.empty)
+ | Polymorphic_const _ ->
+ let csts = constraints_of cb u in
+ (subst_instance_constr u (Mod_subst.force_constr l_body), csts)
+ end
| OpaqueDef _ -> raise (NotEvaluableConst Opaque)
| Undef _ -> raise (NotEvaluableConst NoBody)
else raise (NotEvaluableConst IsProj)
@@ -273,7 +287,7 @@ let constant_opt_value env cst =
let constant_value_and_type env (kn, u) =
let cb = lookup_constant kn env in
- if cb.const_polymorphic then
+ if Declareops.constant_is_polymorphic cb then
let cst = constraints_of cb u in
let b' = match cb.const_body with
| Def l_body -> Some (subst_instance_constr u (Mod_subst.force_constr l_body))
@@ -295,7 +309,7 @@ let constant_value_and_type env (kn, u) =
(* constant_type gives the type of a constant *)
let constant_type_in env (kn,u) =
let cb = lookup_constant kn env in
- if cb.const_polymorphic then
+ if Declareops.constant_is_polymorphic cb then
map_regular_arity (subst_instance_constr u) cb.const_type
else cb.const_type
@@ -321,7 +335,7 @@ let evaluable_constant kn env =
| Undef _ -> false
let polymorphic_constant cst env =
- (lookup_constant cst env).const_polymorphic
+ Declareops.constant_is_polymorphic (lookup_constant cst env)
let polymorphic_pconstant (cst,u) env =
if Univ.Instance.is_empty u then false
@@ -353,7 +367,7 @@ let is_projection cst env =
let lookup_mind = lookup_mind
let polymorphic_ind (mind,i) env =
- (lookup_mind mind env).mind_polymorphic
+ Declareops.inductive_is_polymorphic (lookup_mind mind env)
let polymorphic_pind (ind,u) env =
if Univ.Instance.is_empty u then false
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b7431dbe5..ae3afcb35 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -161,6 +161,9 @@ val constant_value_and_type : env -> constant puniverses ->
(** The universe context associated to the constant, empty if not
polymorphic *)
val constant_context : env -> constant -> Univ.universe_context
+(** The universe isntance associated to the constant, empty if not
+ polymorphic *)
+val constant_instance : env -> constant -> Univ.universe_instance
(* These functions should be called under the invariant that [env]
already contains the constraints corresponding to the constant
@@ -256,7 +259,7 @@ type unsafe_type_judgment = types punsafe_type_judgment
(** {6 Compilation of global declaration } *)
-val compile_constant_body : env -> constant_universes option -> constant_def -> Cemitcodes.body_code option
+val compile_constant_body : env -> constant_universes -> constant_def -> Cemitcodes.body_code option
exception Hyp_not_found
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 5cfcbba60..00fbe27a7 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -231,23 +231,23 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Ter
(* Check that the subtyping information inferred for inductive types in the block is correct. *)
(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
-let check_subtyping mie paramsctxt env_ar inds =
+let check_subtyping cumi paramsctxt env_ar inds =
let numparams = Context.Rel.nhyps paramsctxt in
- let sbsubst = UInfoInd.subtyping_susbst mie.mind_entry_universes in
+ let sbsubst = CumulativityInfo.subtyping_susbst cumi in
let dosubst = subst_univs_level_constr sbsubst in
- let uctx = UInfoInd.univ_context mie.mind_entry_universes in
+ let uctx = CumulativityInfo.univ_context cumi in
let instance_other = Univ.subst_univs_level_instance sbsubst (Univ.UContext.instance uctx) in
let constraints_other = Univ.subst_univs_level_constraints sbsubst (Univ.UContext.constraints uctx) in
let uctx_other = Univ.UContext.make (instance_other, constraints_other) in
- let env' = Environ.push_context uctx env_ar in
- let env'' = Environ.push_context uctx_other env' in
- let envsb = push_context (UInfoInd.subtyp_context mie.mind_entry_universes) env'' in
+ let env = Environ.push_context uctx env_ar in
+ let env = Environ.push_context uctx_other env in
+ let env = push_context (CumulativityInfo.subtyp_context cumi) env in
(* process individual inductive types: *)
Array.iter (fun (id,cn,lc,(sign,arity)) ->
match arity with
| RegularArity (_, full_arity, _) ->
- check_subtyping_arity_constructor envsb dosubst full_arity numparams true;
- Array.iter (fun cnt -> check_subtyping_arity_constructor envsb dosubst cnt numparams false) lc
+ check_subtyping_arity_constructor env dosubst full_arity numparams true;
+ Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
| TemplateArity _ -> ()
) inds
@@ -264,7 +264,13 @@ let typecheck_inductive env mie =
(* Check unicity of names *)
mind_check_names mie;
(* Params are typed-checked here *)
- let env' = push_context (Univ.UInfoInd.univ_context mie.mind_entry_universes) env in
+ let univctx =
+ match mie.mind_entry_universes with
+ | Monomorphic_ind_entry ctx -> ctx
+ | Polymorphic_ind_entry ctx -> ctx
+ | Cumulative_ind_entry cumi -> Univ.CumulativityInfo.univ_context cumi
+ in
+ let env' = push_context univctx env in
let (env_params,paramsctxt) = infer_local_decls env' mie.mind_entry_params in
(* We first type arity of each inductive definition *)
(* This allows building the environment of arities and to share *)
@@ -383,16 +389,21 @@ let typecheck_inductive env mie =
| _ (* Not an explicit occurrence of Type *) ->
full_polymorphic ()
in
- let arity =
- if mie.mind_entry_polymorphic then full_polymorphic ()
- else template_polymorphic ()
+ let arity =
+ match mie.mind_entry_universes with
+ | Monomorphic_ind_entry _ -> template_polymorphic ()
+ | Polymorphic_ind_entry _ | Cumulative_ind_entry _ -> full_polymorphic ()
in
(id,cn,lc,(sign,arity)))
inds
in
(* Check that the subtyping information inferred for inductive types in the block is correct. *)
(* This check produces a value of the unit type if successful or raises an anomaly if check fails. *)
- let () = if mie.mind_entry_cumulative then check_subtyping mie paramsctxt env_arities inds
+ let () =
+ match mie.mind_entry_universes with
+ | Monomorphic_ind_entry _ -> ()
+ | Polymorphic_ind_entry _ -> ()
+ | Cumulative_ind_entry cumi -> check_subtyping cumi paramsctxt env_arities inds
in (env_arities, env_ar_par, paramsctxt, inds)
(************************************************************************)
@@ -864,14 +875,21 @@ let compute_projections ((kn, _ as ind), u as indu) n x nparamargs params
Array.of_list (List.rev kns),
Array.of_list (List.rev pbs)
-let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite inds nmr recargs =
+let abstract_inductive_universes iu =
+ match iu with
+ | Monomorphic_ind_entry ctx -> (Univ.empty_level_subst, Monomorphic_ind ctx)
+ | Polymorphic_ind_entry ctx ->
+ let (inst, auctx) = Univ.abstract_universes ctx in (inst, Polymorphic_ind auctx)
+ | Cumulative_ind_entry cumi ->
+ let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+
+let build_inductive env prv iu env_ar 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
let nparamargs = Context.Rel.nhyps paramsctxt in
let nparamsctxt = Context.Rel.length paramsctxt in
- let substunivs, ctxunivs = Univ.abstract_universes p (Univ.UInfoInd.univ_context ctx) in
- let substsubtyp, ctxsubtyp = Univ.abstract_universes p (Univ.UInfoInd.subtyp_context ctx) in
+ let substunivs, aiu = abstract_inductive_universes iu in
let paramsctxt = Vars.subst_univs_level_context substunivs paramsctxt in
let env_ar =
let ctxunivs = Environ.rel_context env_ar in
@@ -942,10 +960,14 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind
&& Array.length pkt.mind_consnames == 1
&& pkt.mind_consnrealargs.(0) > 0 ->
(** The elimination criterion ensures that all projections can be defined. *)
- let u =
- if p then
- subst_univs_level_instance substunivs (Univ.UContext.instance ctxunivs)
- else Univ.Instance.empty
+ let u =
+ let process auctx =
+ subst_univs_level_instance substunivs (Univ.AUContext.instance auctx)
+ in
+ match aiu with
+ | Monomorphic_ind _ -> Univ.Instance.empty
+ | Polymorphic_ind auctx -> process auctx
+ | Cumulative_ind acumi -> process (Univ.ACumulativityInfo.univ_context acumi)
in
let indsp = ((kn, 0), u) in
let rctx, indty = decompose_prod_assum (subst1 (mkIndU indsp) pkt.mind_nf_lc.(0)) in
@@ -968,9 +990,7 @@ let build_inductive env cum p prv ctx env_ar paramsctxt kn isrecord isfinite ind
mind_nparams_rec = nmr;
mind_params_ctxt = paramsctxt;
mind_packets = packets;
- mind_polymorphic = p;
- mind_cumulative = cum;
- mind_universes = Univ.UInfoInd.make (ctxunivs, ctxsubtyp);
+ mind_universes = aiu;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
@@ -985,7 +1005,6 @@ let check_inductive env kn mie =
let chkpos = (Environ.typing_flags env).check_guarded in
let (nmr,recargs) = check_positivity ~chkpos kn env_ar_par paramsctxt mie.mind_entry_finite inds in
(* Build the inductive packets *)
- build_inductive env mie.mind_entry_cumulative mie.mind_entry_polymorphic mie.mind_entry_private
- mie.mind_entry_universes
+ build_inductive env mie.mind_entry_private mie.mind_entry_universes
env_ar paramsctxt kn mie.mind_entry_record mie.mind_entry_finite
inds nmr recargs
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index 7b0f01794..5b4615399 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -32,17 +32,6 @@ type inductive_error =
exception InductiveError of inductive_error
-val check_subtyping_arity_constructor : Environ.env ->
-(Term.constr -> Term.constr) -> Term.types -> int -> bool -> unit
-
-(* This needs not be exposed. Exposing for debugging purposes! *)
-val check_subtyping : Entries.mutual_inductive_entry ->
-Context.Rel.t ->
-Environ.env ->
-('b * 'c * Term.types array *
- ('d * ('e * Term.types * 'f, 'g) Declarations.declaration_arity))
-array -> unit
-
(** The following function does checks on inductive declarations. *)
val check_inductive : env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 0f0dc0d60..e81a1cb58 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -54,9 +54,13 @@ let inductive_paramdecls (mib,u) =
Vars.subst_instance_context u mib.mind_params_ctxt
let instantiate_inductive_constraints mib u =
- if mib.mind_polymorphic then
- Univ.subst_instance_constraints u (Univ.UContext.constraints (Univ.UInfoInd.univ_context mib.mind_universes))
- else Univ.Constraint.empty
+ let process auctx =
+ Univ.UContext.constraints (Univ.subst_instance_context 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)
(************************************************************************)
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ff44f0f54..79016735b 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -74,12 +74,13 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
as long as they have the right type *)
let uctx = Declareops.universes_of_constant (opaque_tables env) cb in
let uctx = (* Context of the spec *)
- if cb.const_polymorphic then
- Univ.instantiate_univ_context uctx
- else uctx
+ match cb.const_universes with
+ | Monomorphic_const _ -> uctx
+ | Polymorphic_const auctx ->
+ Univ.instantiate_univ_context auctx
in
let c', univs, ctx' =
- if not cb.const_polymorphic then
+ if not (Declareops.constant_is_polymorphic cb) then
let env' = Environ.push_context ~strict:true uctx env' in
let env' = Environ.push_context ~strict:true ctx env' in
let c',cst = match cb.const_body with
@@ -92,7 +93,7 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
| Def cs ->
let c' = Mod_subst.force_constr cs in
c, Reduction.infer_conv env' (Environ.universes env') c c'
- in c', ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
+ in c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst (Univ.ContextSet.of_context ctx)
else
let cus, ccst = Univ.UContext.dest uctx in
let newus, cst = Univ.UContext.dest ctx in
@@ -122,21 +123,17 @@ 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;
- let subst, ctx = Univ.abstract_universes true ctx in
- Vars.subst_univs_level_constr subst c, ctx, Univ.ContextSet.empty
+ let subst, ctx = Univ.abstract_universes ctx in
+ Vars.subst_univs_level_constr subst c, Polymorphic_const ctx, Univ.ContextSet.empty
in
let def = Def (Mod_subst.from_val c') in
(* let ctx' = Univ.UContext.make (newus, cst) in *)
- let univs =
- if cb.const_polymorphic then Some cb.const_universes
- else None
- in
let cb' =
{ cb with
const_body = def;
- const_universes = ctx ;
+ const_universes = univs ;
const_body_code = Option.map Cemitcodes.from_val
- (compile_constant_body env' univs def) }
+ (compile_constant_body env' cb.const_universes def) }
in
before@(lab,SFBconst(cb'))::after, c', ctx'
else
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 1f8b97ae6..33d13f1ba 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -35,6 +35,7 @@ type signature_mismatch_error =
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of env * types * types
+ | CumulativeStatusExpected of bool
| PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
@@ -327,12 +328,10 @@ let strengthen_const mp_from l cb resolver =
|_ ->
let kn = KerName.make2 mp_from l in
let con = constant_of_delta_kn resolver kn in
- let u =
- if cb.const_polymorphic then
- let u = Univ.UContext.instance cb.const_universes in
- let s = Univ.make_instance_subst u in
- Univ.subst_univs_level_instance s u
- else Univ.Instance.empty
+ let u =
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.Instance.empty
+ | Polymorphic_const ctx -> Univ.make_abstract_instance ctx
in
{ cb with
const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
diff --git a/kernel/modops.mli b/kernel/modops.mli
index e9f3db6e9..4b533c7ef 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -94,6 +94,7 @@ type signature_mismatch_error =
| NotConvertibleConstructorField of Id.t
| NotConvertibleBodyField
| NotConvertibleTypeField of env * types * types
+ | CumulativeStatusExpected of bool
| PolymorphicStatusExpected of bool
| NotSameConstructorNamesField
| NotSameInductiveNameInBlockField
diff --git a/kernel/nativecode.ml b/kernel/nativecode.ml
index d3cd6b62a..4941d64d8 100644
--- a/kernel/nativecode.ml
+++ b/kernel/nativecode.ml
@@ -1863,8 +1863,9 @@ let compile_constant env sigma prefix ~interactive con cb =
match cb.const_proj with
| None ->
let u =
- if cb.const_polymorphic then Univ.UContext.instance cb.const_universes
- else Univ.Instance.empty
+ match cb.const_universes with
+ | Monomorphic_const _ -> Univ.Instance.empty
+ | Polymorphic_const ctx -> Univ.AUContext.instance ctx
in
begin match cb.const_body with
| Def t ->
@@ -1960,7 +1961,7 @@ let param_name = Name (id_of_string "params")
let arg_name = Name (id_of_string "arg")
let compile_mind prefix ~interactive mb mind stack =
- let u = Declareops.inductive_instance mb in
+ let u = Declareops.inductive_polymorphic_instance mb in
let f i stack ob =
let gtype = Gtype((mind, i), Array.map snd ob.mind_reloc_tbl) in
let j = push_symbol (SymbInd (mind,i)) in
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 59e90ca2e..3e15ff740 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,7 +16,7 @@ type work_list = (Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t }
type proofterm = (constr * Univ.universe_context_set) Future.computation
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 3897d5e51..be1f4b13f 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -49,7 +49,7 @@ type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
type cooking_info = {
modlist : work_list;
- abstract : Context.Named.t * Univ.universe_level_subst * Univ.UContext.t }
+ abstract : Context.Named.t * Univ.universe_level_subst * Univ.AUContext.t }
(* The type has two caveats:
1) cook_constr is defined after
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index ea583fdac..8bf95e5de 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -497,11 +497,12 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if eq_ind ind1 ind2 then
let mind = Environ.lookup_mind (fst ind1) env in
let cuniv =
- if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+ convert_instances ~flex:false u1 u2 cuniv
+ | Declarations.Cumulative_ind cumi ->
convert_inductives cv_pb (mind, snd ind1) u1 (CClosure.stack_args_size v1)
u2 (CClosure.stack_args_size v2) cuniv
- else
- convert_instances ~flex:false u1 u2 cuniv
in
convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -510,12 +511,13 @@ and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
if Int.equal j1 j2 && eq_ind ind1 ind2 then
let mind = Environ.lookup_mind (fst ind1) env in
let cuniv =
- if mind.Declarations.mind_polymorphic && mind.Declarations.mind_cumulative then
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+ convert_instances ~flex:false u1 u2 cuniv
+ | Declarations.Cumulative_ind _ ->
convert_constructors
(mind, snd ind1, j1) u1 (CClosure.stack_args_size v1)
u2 (CClosure.stack_args_size v2) cuniv
- else
- convert_instances ~flex:false u1 u2 cuniv
in
convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
@@ -637,22 +639,26 @@ let infer_check_conv_inductives
infer_check_convert_instances
infer_check_inductive_instances
cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
- if mind.Declarations.mind_polymorphic then
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+ infer_check_convert_instances ~flex:false u1 u2 univs
+ | Declarations.Cumulative_ind cumi ->
let num_param_arity =
mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
in
if not (num_param_arity = sv1 && num_param_arity = sv2) then
infer_check_convert_instances ~flex:false u1 u2 univs
else
- let uinfind = mind.Declarations.mind_universes in
- infer_check_inductive_instances cv_pb uinfind u1 u2 univs
- else infer_check_convert_instances ~flex:false u1 u2 univs
+ infer_check_inductive_instances cv_pb cumi u1 u2 univs
let infer_check_conv_constructors
infer_check_convert_instances
infer_check_inductive_instances
(mind, ind, cns) u1 sv1 u2 sv2 univs =
- if mind.Declarations.mind_polymorphic then
+ match mind.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ ->
+ infer_check_convert_instances ~flex:false u1 u2 univs
+ | Declarations.Cumulative_ind cumi ->
let num_cnstr_args =
let nparamsctxt =
mind.Declarations.mind_nparams + mind.Declarations.mind_packets.(ind).Declarations.mind_nrealargs
@@ -662,26 +668,30 @@ let infer_check_conv_constructors
if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
infer_check_convert_instances ~flex:false u1 u2 univs
else
- let uinfind = mind.Declarations.mind_universes in
- infer_check_inductive_instances CONV uinfind u1 u2 univs
- else infer_check_convert_instances ~flex:false u1 u2 univs
+ infer_check_inductive_instances CONV cumi u1 u2 univs
-let check_inductive_instances cv_pb uinfind u u' univs =
- let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
- let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let check_inductive_instances cv_pb cumi u u' univs =
+ let ind_instance =
+ Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi)
+ in
+ let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
(Univ.Instance.length ind_instance = Univ.Instance.length u')) then
anomaly (Pp.str "Invalid inductive subtyping encountered!")
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.subst_instance_constraints comp_subst ind_sbcst
+ Univ.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx)
in
let comp_cst =
match cv_pb with
CONV ->
- let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+ let comp_cst' =
+ let comp_subst = (Univ.Instance.append u' u) in
+ Univ.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx)
+ in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
in
@@ -746,22 +756,27 @@ let infer_convert_instances ~flex u u' (univs,cstrs) =
else Univ.enforce_eq_instances u u' cstrs
in (univs, cstrs')
-let infer_inductive_instances cv_pb uinfind u u' (univs, cstrs) =
- let ind_instance = Univ.UContext.instance (Univ.UInfoInd.univ_context uinfind) in
- let ind_sbcst = Univ.UContext.constraints (Univ.UInfoInd.subtyp_context uinfind) in
+let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
+ let ind_instance =
+ Univ.AUContext.instance (Univ.ACumulativityInfo.subtyp_context cumi)
+ in
+ let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
if not ((Univ.Instance.length ind_instance = Univ.Instance.length u) &&
(Univ.Instance.length ind_instance = Univ.Instance.length u')) then
anomaly (Pp.str "Invalid inductive subtyping encountered!")
else
let comp_cst =
let comp_subst = (Univ.Instance.append u u') in
- Univ.subst_instance_constraints comp_subst ind_sbcst
+ Univ.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx)
in
let comp_cst =
match cv_pb with
CONV ->
- let comp_subst = (Univ.Instance.append u' u) in
- let comp_cst' = (Univ.subst_instance_constraints comp_subst ind_sbcst) in
+ let comp_cst' =
+ let comp_subst = (Univ.Instance.append u' u) in
+ Univ.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx) in
Univ.Constraint.union comp_cst comp_cst'
| CUMUL -> comp_cst
in
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 1568fe0bf..946222ef2 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -237,20 +237,29 @@ let private_con_of_scheme ~kind env cl =
let universes_of_private eff =
let open Declarations in
- List.fold_left (fun acc { Entries.eff } ->
- match eff with
- | Entries.SEscheme (l,s) ->
- List.fold_left (fun acc (_,_,cb,c) ->
- let acc = match c with
- | `Nothing -> acc
- | `Opaque (_, ctx) -> ctx :: acc in
- if cb.const_polymorphic then acc
- else (Univ.ContextSet.of_context cb.const_universes) :: acc)
- acc l
- | Entries.SEsubproof (c, cb, e) ->
- if cb.const_polymorphic then acc
- else Univ.ContextSet.of_context cb.const_universes :: acc)
- [] (Term_typing.uniq_seff eff)
+ List.fold_left
+ (fun acc { Entries.eff } ->
+ match eff with
+ | Entries.SEscheme (l,s) ->
+ List.fold_left
+ (fun acc (_,_,cb,c) ->
+ let acc = match c with
+ | `Nothing -> acc
+ | `Opaque (_, ctx) -> ctx :: acc
+ in
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ (Univ.ContextSet.of_context ctx) :: acc
+ | Polymorphic_const _ -> acc
+ )
+ acc l
+ | Entries.SEsubproof (c, cb, e) ->
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ (Univ.ContextSet.of_context ctx) :: acc
+ | Polymorphic_const _ -> acc
+ )
+ [] (Term_typing.uniq_seff eff)
let env_of_safe_env senv = senv.env
let env_of_senv = env_of_safe_env
@@ -373,7 +382,11 @@ let safe_push_named d env =
let push_named_def (id,de) senv =
- let c,typ,univs = Term_typing.translate_local_def senv.revstruct senv.env id de in
+ let c,typ,univs =
+ match Term_typing.translate_local_def senv.revstruct senv.env id de with
+ | c, typ, Monomorphic_const ctx -> c, typ, ctx
+ | _, _, Polymorphic_const _ -> assert false
+ in
let poly = de.Entries.const_entry_polymorphic in
let univs = Univ.ContextSet.of_context univs in
let c, univs = match c with
@@ -410,26 +423,28 @@ let labels_of_mib mib =
get ()
let globalize_constant_universes env cb =
- if cb.const_polymorphic then
- [Now (true, Univ.ContextSet.empty)]
- else
- let cstrs = Univ.ContextSet.of_context cb.const_universes in
- Now (false, cstrs) ::
- (match cb.const_body with
- | (Undef _ | Def _) -> []
- | OpaqueDef lc ->
- match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
- | None -> []
- | Some fc ->
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ let cstrs = Univ.ContextSet.of_context ctx in
+ Now (false, cstrs) ::
+ (match cb.const_body with
+ | (Undef _ | Def _) -> []
+ | OpaqueDef lc ->
+ match Opaqueproof.get_constraints (Environ.opaque_tables env) lc with
+ | None -> []
+ | Some fc ->
match Future.peek_val fc with
- | None -> [Later fc]
- | Some c -> [Now (false, c)])
+ | None -> [Later fc]
+ | Some c -> [Now (false, c)])
+ | Polymorphic_const _ ->
+ [Now (true, Univ.ContextSet.empty)]
let globalize_mind_universes mb =
- if mb.mind_polymorphic then
- [Now (true, Univ.ContextSet.empty)]
- else
- [Now (false, Univ.ContextSet.of_context (Univ.UInfoInd.univ_context mb.mind_universes))]
+ match mb.mind_universes with
+ | Monomorphic_ind ctx ->
+ [Now (false, Univ.ContextSet.of_context ctx)]
+ | Polymorphic_ind _ -> [Now (true, Univ.ContextSet.empty)]
+ | Cumulative_ind _ -> [Now (true, Univ.ContextSet.empty)]
let constraints_of_sfb env sfb =
match sfb with
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 60e630a6d..1bd9d6e49 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -104,15 +104,21 @@ 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 poly =
- if not (mib1.mind_polymorphic == mib2.mind_polymorphic) then
- error (PolymorphicStatusExpected mib2.mind_polymorphic)
- else mib2.mind_polymorphic
- in
- let u =
- if poly then
- CErrors.user_err Pp.(str "Checking of subtyping of polymorphic inductive types not implemented")
- else Instance.empty
+ let u =
+ let process inst inst' =
+ if Univ.Instance.equal inst inst' then inst else error IncompatibleInstances
+ in
+ match mib1.mind_universes, mib2.mind_universes with
+ | Monomorphic_ind _, Monomorphic_ind _ -> Univ.Instance.empty
+ | Polymorphic_ind auctx, Polymorphic_ind auctx' ->
+ process
+ (Univ.AUContext.instance auctx) (Univ.AUContext.instance auctx')
+ | Cumulative_ind cumi, Cumulative_ind cumi' ->
+ process
+ (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+ (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi'))
+ | _ -> error
+ (CumulativeStatusExpected (Declareops.inductive_is_cumulative mib2))
in
let mib2 = Declareops.subst_mind_body subst2 mib2 in
let check_inductive_type cst name env t1 t2 =
@@ -148,7 +154,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
error (NotConvertibleInductiveField name)
| _ -> (s1, s2) in
check_conv (NotConvertibleInductiveField name)
- cst poly u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
+ cst (inductive_is_polymorphic mib1) u infer_conv_leq env (mkArity (ctx1,s1)) (mkArity (ctx2,s2))
in
let check_packet cst p1 p2 =
@@ -176,7 +182,7 @@ let check_inductive cst env mp1 l info1 mp2 mib2 spec2 subst1 subst2 reso1 reso2
let check_cons_types i cst p1 p2 =
Array.fold_left3
(fun cst id t1 t2 -> check_conv (NotConvertibleConstructorField id) cst
- poly u infer_conv env t1 t2)
+ (inductive_is_polymorphic mib1) u infer_conv env t1 t2)
cst
p2.mind_consnames
(arities_of_specif (mind,u) (mib1,p1))
@@ -293,37 +299,42 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
let cb2 = Declareops.subst_const_body subst2 cb2 in
(* Start by checking universes *)
let poly =
- if not (cb1.const_polymorphic == cb2.const_polymorphic) then
- error (PolymorphicStatusExpected cb2.const_polymorphic)
- else cb2.const_polymorphic
+ if not (Declareops.constant_is_polymorphic cb1
+ == Declareops.constant_is_polymorphic cb2) then
+ error (PolymorphicStatusExpected (Declareops.constant_is_polymorphic cb2))
+ else Declareops.constant_is_polymorphic cb2
in
- let cst', env', u =
- if poly then
- let ctx1 = Univ.instantiate_univ_context cb1.const_universes in
- let ctx2 = Univ.instantiate_univ_context cb2.const_universes in
- let inst1, ctx1 = Univ.UContext.dest ctx1 in
- let inst2, ctx2 = Univ.UContext.dest ctx2 in
+ let cst', env', u =
+ match cb1.const_universes, cb2.const_universes with
+ | Monomorphic_const _, Monomorphic_const _ ->
+ cst, env, Univ.Instance.empty
+ | Polymorphic_const auctx1, Polymorphic_const auctx2 ->
+ begin
+ let ctx1 = Univ.instantiate_univ_context auctx1 in
+ let ctx2 = Univ.instantiate_univ_context auctx2 in
+ let inst1, ctx1 = Univ.UContext.dest ctx1 in
+ let inst2, ctx2 = Univ.UContext.dest ctx2 in
if not (Univ.Instance.length inst1 == Univ.Instance.length inst2) then
error IncompatibleInstances
else
let cstrs = Univ.enforce_eq_instances inst1 inst2 cst in
let cstrs = Univ.Constraint.union cstrs ctx2 in
- try
- (* The environment with the expected universes plus equality
- of the body instances with the expected instance *)
- let ctxi = Univ.Instance.append inst1 inst2 in
- let ctx = Univ.UContext.make (ctxi, cstrs) in
- let env = Environ.push_context ctx env in
- (* Check that the given definition does not add any constraint over
- the expected ones, so that it can be used in place of
- the original. *)
- if UGraph.check_constraints ctx1 (Environ.universes env) then
- cstrs, env, inst2
- else error (IncompatibleConstraints ctx1)
- with Univ.UniverseInconsistency incon ->
- error (IncompatibleUniverses incon)
- else
- cst, env, Univ.Instance.empty
+ try
+ (* The environment with the expected universes plus equality
+ of the body instances with the expected instance *)
+ let ctxi = Univ.Instance.append inst1 inst2 in
+ let ctx = Univ.UContext.make (ctxi, cstrs) in
+ let env = Environ.push_context ctx env in
+ (* Check that the given definition does not add any constraint over
+ the expected ones, so that it can be used in place of
+ the original. *)
+ if UGraph.check_constraints ctx1 (Environ.universes env) then
+ cstrs, env, inst2
+ else error (IncompatibleConstraints ctx1)
+ with Univ.UniverseInconsistency incon ->
+ error (IncompatibleUniverses incon)
+ end
+ | _ -> assert false
in
(* Now check types *)
let typ1 = Typeops.type_of_constant_type env' cb1.const_type in
@@ -354,7 +365,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
"name."));
let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
- let u1 = inductive_instance mind1 in
+ let u1 = inductive_polymorphic_instance mind1 in
let arity1,cst1 = constrained_type_of_inductive env
((mind1,mind1.mind_packets.(i)),u1) in
let cst2 =
@@ -371,7 +382,7 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
"name."));
let () = assert (List.is_empty mind1.mind_hyps && List.is_empty cb2.const_hyps) in
if Declareops.constant_has_body cb2 then error DefinitionFieldExpected;
- let u1 = inductive_instance mind1 in
+ let u1 = inductive_polymorphic_instance mind1 in
let ty1,cst1 = constrained_type_of_constructor (cstr,u1) (mind1,mind1.mind_packets.(i)) in
let cst2 =
Declareops.constraints_of_constant (Environ.opaque_tables env) cb2 in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3cf2299d8..5370bcea4 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -121,18 +121,19 @@ let inline_side_effects env body ctx side_eff =
| OpaqueDef _, `Opaque (b,_) -> (b, true)
| _ -> assert false
in
- if cb.const_polymorphic then
- (** Inline the term to emulate universe polymorphism *)
- let data = (Univ.UContext.instance cb.const_universes, b) in
- let subst = Cmap_env.add c (Inl data) subst in
- (subst, var, ctx, args)
- else
+ match cb.const_universes with
+ | Monomorphic_const cnstctx ->
(** Abstract over the term at the top of the proof *)
let ty = Typeops.type_of_constant_type env cb.const_type in
let subst = Cmap_env.add c (Inr var) subst in
- let univs = Univ.ContextSet.of_context cb.const_universes in
+ let univs = Univ.ContextSet.of_context cnstctx in
let ctx = Univ.ContextSet.union ctx univs in
(subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
+ | Polymorphic_const auctx ->
+ (** Inline the term to emulate universe polymorphism *)
+ let data = (Univ.AUContext.instance auctx, b) in
+ let subst = Cmap_env.add c (Inl data) subst in
+ (subst, var, ctx, args)
in
let (subst, len, ctx, args) = List.fold_left fold (Cmap_env.empty, 1, ctx, []) side_eff in
(** Third step: inline the definitions *)
@@ -225,16 +226,25 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:state_id Feedback.Complete)
+let abstract_constant_universes abstract uctx =
+ if not abstract then
+ Univ.empty_level_subst, Monomorphic_const uctx
+ else
+ let sbst, auctx = Univ.abstract_universes uctx in
+ sbst, Polymorphic_const auctx
+
let infer_declaration ~trust env kn dcl =
match dcl with
| ParameterEntry (ctx,poly,(t,uctx),nl) ->
let env = push_context ~strict:(not poly) uctx env in
let j = infer env t in
let abstract = poly && not (Option.is_empty kn) in
- let usubst, univs = Univ.abstract_universes abstract uctx in
+ let usubst, univs =
+ abstract_constant_universes abstract uctx
+ in
let c = Typeops.assumption_of_judgment env j in
let t = hcons_constr (Vars.subst_univs_level_constr usubst c) in
- Undef nl, RegularArity t, None, poly, univs, false, ctx
+ Undef nl, RegularArity t, None, univs, false, ctx
(** Definition [c] is opaque (Qed), non polymorphic and with a specified type,
so we delay the typing and hash consing of its body.
@@ -264,9 +274,9 @@ let infer_declaration ~trust env kn dcl =
feedback_completion_typecheck feedback_id;
c, uctx) in
let def = OpaqueDef (Opaqueproof.create proofterm) in
- def, RegularArity typ, None, c.const_entry_polymorphic,
- c.const_entry_universes,
- c.const_entry_inline_code, c.const_entry_secctx
+ def, RegularArity typ, None,
+ (Monomorphic_const c.const_entry_universes),
+ c.const_entry_inline_code, c.const_entry_secctx
(** Other definitions have to be processed immediately. *)
| DefinitionEntry c ->
@@ -279,7 +289,8 @@ let infer_declaration ~trust env kn dcl =
let env = push_context_set ~strict:(not c.const_entry_polymorphic) ctx env in
let abstract = c.const_entry_polymorphic && not (Option.is_empty kn) in
let usubst, univs =
- Univ.abstract_universes abstract (Univ.ContextSet.to_context ctx) in
+ abstract_constant_universes abstract (Univ.ContextSet.to_context ctx)
+ in
let j = infer env body in
let typ = match typ with
| None ->
@@ -298,8 +309,7 @@ let infer_declaration ~trust env kn dcl =
else Def (Mod_subst.from_val def)
in
feedback_completion_typecheck feedback_id;
- def, typ, None, c.const_entry_polymorphic,
- univs, c.const_entry_inline_code, c.const_entry_secctx
+ def, typ, None, univs, c.const_entry_inline_code, c.const_entry_secctx
| ProjectionEntry {proj_entry_ind = ind; proj_entry_arg = i} ->
let mib, _ = Inductive.lookup_mind_specif env (ind,0) in
@@ -311,9 +321,16 @@ let infer_declaration ~trust env kn dcl =
else assert false
| _ -> assert false
in
+ let univs =
+ match mib.mind_universes with
+ | Monomorphic_ind ctx -> Monomorphic_const ctx
+ | Polymorphic_ind auctx -> Polymorphic_const auctx
+ | Cumulative_ind acumi ->
+ Polymorphic_const (Univ.ACumulativityInfo.univ_context acumi)
+ in
let term, typ = pb.proj_eta in
Def (Mod_subst.from_val (hcons_constr term)), RegularArity typ, Some pb,
- mib.mind_polymorphic, Univ.UInfoInd.univ_context mib.mind_universes, false, None
+ univs, false, None
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
@@ -337,7 +354,7 @@ let record_aux env s_ty s_bo suggested_expr =
let suggest_proof_using = ref (fun _ _ _ _ _ -> "")
let set_suggest_proof_using f = suggest_proof_using := f
-let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx) =
+let build_constant_declaration kn env (def,typ,proj,univs,inline_code,ctx) =
let check declared inferred =
let mk_set l = List.fold_right Id.Set.add (List.map NamedDecl.get_id l) Id.Set.empty in
let inferred_set, declared_set = mk_set inferred, mk_set declared in
@@ -409,9 +426,8 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
check declared inferred) lc) in
let tps =
let res =
- let comp_univs = if poly then Some univs else None in
match proj with
- | None -> compile_constant_body env comp_univs def
+ | None -> compile_constant_body env univs def
| Some pb ->
(* The compilation of primitive projections is a bit tricky, because
they refer to themselves (the body of p looks like fun c =>
@@ -425,14 +441,13 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
const_type = typ;
const_proj = proj;
const_body_code = None;
- const_polymorphic = poly;
const_universes = univs;
const_inline_code = inline_code;
const_typing_flags = Environ.typing_flags env;
}
in
let env = add_constant kn cb env in
- compile_constant_body env comp_univs def
+ compile_constant_body env univs def
in Option.map Cemitcodes.from_val res
in
{ const_hyps = hyps;
@@ -440,7 +455,6 @@ let build_constant_declaration kn env (def,typ,proj,poly,univs,inline_code,ctx)
const_type = typ;
const_proj = proj;
const_body_code = tps;
- const_polymorphic = poly;
const_universes = univs;
const_inline_code = inline_code;
const_typing_flags = Environ.typing_flags env }
@@ -452,6 +466,12 @@ let translate_constant mb env kn ce =
(infer_declaration ~trust:mb env (Some kn) ce)
let constant_entry_of_side_effect cb u =
+ let poly, univs =
+ match cb.const_universes with
+ | Monomorphic_const ctx -> false, ctx
+ | Polymorphic_const auctx ->
+ true, Univ.instantiate_univ_context auctx
+ in
let pt =
match cb.const_body, u with
| OpaqueDef _, `Opaque (b, c) -> b, c
@@ -463,8 +483,8 @@ let constant_entry_of_side_effect cb u =
const_entry_feedback = None;
const_entry_type =
(match cb.const_type with RegularArity t -> Some t | _ -> None);
- const_entry_polymorphic = cb.const_polymorphic;
- const_entry_universes = cb.const_universes;
+ const_entry_polymorphic = poly;
+ const_entry_universes = univs;
const_entry_opaque = Declareops.is_opaque cb;
const_entry_inline_code = cb.const_inline_code }
;;
@@ -508,16 +528,23 @@ let export_side_effects mb env ce =
let trusted = check_signatures mb signatures in
let push_seff env = function
| kn, cb, `Nothing, _ ->
- let env = Environ.add_constant kn cb env in
- if not cb.const_polymorphic then
- Environ.push_context ~strict:true cb.const_universes env
- else env
- | kn, cb, `Opaque(_, ctx), _ ->
- let env = Environ.add_constant kn cb env in
- if not cb.const_polymorphic then
- let env = Environ.push_context ~strict:true cb.const_universes env in
- Environ.push_context_set ~strict:true ctx env
- else env in
+ begin
+ let env = Environ.add_constant kn cb env in
+ match cb.const_universes with
+ | Monomorphic_const ctx ->
+ Environ.push_context ~strict:true ctx env
+ | Polymorphic_const _ -> env
+ end
+ | kn, cb, `Opaque(_, ctx), _ ->
+ begin
+ let env = Environ.add_constant kn cb env in
+ match cb.const_universes with
+ | Monomorphic_const cstctx ->
+ let env = Environ.push_context ~strict:true cstctx env in
+ Environ.push_context_set ~strict:true ctx env
+ | Polymorphic_const _ -> env
+ end
+ in
let rec translate_seff sl seff acc env =
match sl, seff with
| _, [] -> List.rev acc, ce
@@ -553,7 +580,7 @@ let translate_recipe env kn r =
build_constant_declaration kn env (Cooking.cook_constant ~hcons env r)
let translate_local_def mb env id centry =
- let def,typ,proj,poly,univs,inline_code,ctx =
+ let def,typ,proj,univs,inline_code,ctx =
infer_declaration ~trust:mb env None (DefinitionEntry centry) in
let typ = type_of_constant_type env typ in
if ctx = None && !Flags.compilation_mode = Flags.BuildVo then begin
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 1a07bb2fc..e08f3362d 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -555,7 +555,7 @@ let type_of_projection_constant env (p,u) =
let cb = lookup_constant cst env in
match cb.const_proj with
| Some pb ->
- if cb.const_polymorphic then
+ if Declareops.constant_is_polymorphic cb then
Vars.subst_instance_constr u pb.proj_type
else pb.proj_type
| None -> raise (Invalid_argument "type_of_projection: not a projection")
diff --git a/kernel/univ.ml b/kernel/univ.ml
index eb45f022e..8cbb20a05 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1031,7 +1031,13 @@ end
type universe_context = UContext.t
let hcons_universe_context = UContext.hcons
-(** Universe info for inductive types: A context of universe levels
+module AUContext = UContext
+
+type abstract_universe_context = AUContext.t
+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 a context of universe levels with
universe constraints, representing conditions for subtyping used
@@ -1040,7 +1046,7 @@ let hcons_universe_context = UContext.hcons
This data structure maintains the invariant that the context for
subtyping constraints is exactly twice as big as the context for
universe constraints. *)
-module UInfoInd =
+module CumulativityInfo =
struct
type t = universe_context * universe_context
@@ -1093,8 +1099,13 @@ struct
end
-type universe_info_ind = UInfoInd.t
-let hcons_universe_info_ind = UInfoInd.hcons
+type cumulativity_info = CumulativityInfo.t
+let hcons_cumulativity_info = CumulativityInfo.hcons
+
+module ACumulativityInfo = CumulativityInfo
+
+type abstract_cumulativity_info = ACumulativityInfo.t
+let hcons_abstract_cumulativity_info = ACumulativityInfo.hcons
(** A set of universes with universe constraints.
We linearize the set to a list after typechecking.
@@ -1200,6 +1211,9 @@ let subst_univs_level_constraints subst csts =
(fun c -> Option.fold_right Constraint.add (subst_univs_level_constraint subst c))
csts Constraint.empty
+let subst_univs_level_abstract_universe_context subst (inst, csts) =
+ inst, subst_univs_level_constraints subst csts
+
(** With level to universe substitutions. *)
type universe_subst_fn = universe_level -> universe
@@ -1272,12 +1286,9 @@ let instantiate_univ_context (ctx, csts) =
(ctx, subst_instance_constraints ctx csts)
(** Substitute instance inst for ctx in universe constraints and subtyping constraints *)
-let instantiate_univ_info_ind (univcst, subtpcst) =
+let instantiate_cumulativity_info (univcst, subtpcst) =
(instantiate_univ_context univcst, instantiate_univ_context subtpcst)
-let instantiate_univ_constraints u (_, csts) =
- subst_instance_constraints u csts
-
let make_instance_subst i =
let arr = Instance.to_array i in
Array.fold_left_i (fun i acc l ->
@@ -1290,16 +1301,22 @@ let make_inverse_instance_subst i =
LMap.add (Level.var i) l acc)
LMap.empty arr
-let abstract_universes poly ctx =
+let make_abstract_instance (ctx, _) =
+ Array.mapi (fun i l -> Level.var i) ctx
+
+let abstract_universes ctx =
let instance = UContext.instance ctx in
- if poly then
- let subst = make_instance_subst instance in
- let cstrs = subst_univs_level_constraints subst
- (UContext.constraints ctx)
- in
- let ctx = UContext.make (instance, cstrs) in
- subst, ctx
- else empty_level_subst, ctx
+ let subst = make_instance_subst instance in
+ let cstrs = subst_univs_level_constraints subst
+ (UContext.constraints ctx)
+ in
+ let ctx = UContext.make (instance, cstrs) in
+ subst, ctx
+
+let abstract_cumulativity_info (univcst, substcst) =
+ let instance, univcst = abstract_universes univcst in
+ let _, substcst = abstract_universes substcst in
+ (instance, (univcst, substcst))
(** Pretty-printing *)
@@ -1307,7 +1324,11 @@ let pr_constraints prl = Constraint.pr prl
let pr_universe_context = UContext.pr
-let pr_universe_info_ind = UInfoInd.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
@@ -1364,3 +1385,12 @@ let subst_instance_constraints =
let key = Profile.declare_profile "subst_instance_constraints" in
Profile.profile2 key subst_instance_constraints
else subst_instance_constraints
+
+let subst_instance_context =
+ let subst_instance_context_body inst (inner_inst, inner_constr) =
+ (inner_inst, subst_instance_constraints inst inner_constr)
+ in
+ if Flags.profile then
+ let key = Profile.declare_profile "subst_instance_constraints" in
+ Profile.profile2 key subst_instance_context_body
+ else subst_instance_context_body
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 53af80448..ecc72701d 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -315,6 +315,23 @@ end
type universe_context = UContext.t
+module AUContext :
+sig
+ type t
+
+ val empty : t
+
+ val instance : t -> Instance.t
+
+ val size : t -> int
+
+ (** Keeps the order of the instances *)
+ val union : t -> t -> t
+
+end
+
+type abstract_universe_context = AUContext.t
+
(** Universe info for inductive types: A context of universe levels
with universe constraints, representing local universe variables
and constraints, together with a context of universe levels with
@@ -324,7 +341,7 @@ type universe_context = UContext.t
This data structure maintains the invariant that the context for
subtyping constraints is exactly twice as big as the context for
universe constraints. *)
-module UInfoInd :
+module CumulativityInfo :
sig
type t
@@ -347,7 +364,17 @@ sig
end
-type universe_info_ind = UInfoInd.t
+type cumulativity_info = CumulativityInfo.t
+
+module ACumulativityInfo :
+sig
+ type t
+
+ val univ_context : t -> abstract_universe_context
+ val subtyp_context : t -> abstract_universe_context
+end
+
+type abstract_cumulativity_info = ACumulativityInfo.t
(** Universe contexts (as sets) *)
@@ -399,6 +426,8 @@ val is_empty_level_subst : universe_level_subst -> bool
val subst_univs_level_level : universe_level_subst -> universe_level -> universe_level
val subst_univs_level_universe : universe_level_subst -> universe -> universe
val subst_univs_level_constraints : universe_level_subst -> constraints -> constraints
+val subst_univs_level_abstract_universe_context :
+ universe_level_subst -> abstract_universe_context -> abstract_universe_context
val subst_univs_level_instance : universe_level_subst -> universe_instance -> universe_instance
(** Level to universe substitutions. *)
@@ -413,27 +442,31 @@ val subst_univs_constraints : universe_subst_fn -> constraints -> constraints
(** Substitution of instances *)
val subst_instance_instance : universe_instance -> universe_instance -> universe_instance
val subst_instance_universe : universe_instance -> universe -> universe
-val subst_instance_constraints : universe_instance -> constraints -> constraints
+val subst_instance_context : universe_instance -> abstract_universe_context -> universe_context
val make_instance_subst : universe_instance -> universe_level_subst
val make_inverse_instance_subst : universe_instance -> universe_level_subst
-val abstract_universes : bool -> universe_context -> universe_level_subst * universe_context
+val abstract_universes : universe_context -> universe_level_subst * abstract_universe_context
+
+val abstract_cumulativity_info : cumulativity_info -> universe_level_subst * abstract_cumulativity_info
+
+val make_abstract_instance : abstract_universe_context -> universe_instance
(** Get the instantiated graph. *)
-val instantiate_univ_context : universe_context -> universe_context
+val instantiate_univ_context : abstract_universe_context -> universe_context
(** Get the instantiated graphs for both universe constraints and subtyping constraints. *)
-val instantiate_univ_info_ind : universe_info_ind -> universe_info_ind
-
-val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+val instantiate_cumulativity_info : abstract_cumulativity_info -> cumulativity_info
(** {6 Pretty-printing of universes. } *)
val pr_constraint_type : constraint_type -> Pp.std_ppcmds
val pr_constraints : (Level.t -> Pp.std_ppcmds) -> constraints -> Pp.std_ppcmds
val pr_universe_context : (Level.t -> Pp.std_ppcmds) -> universe_context -> Pp.std_ppcmds
-val pr_universe_info_ind : (Level.t -> Pp.std_ppcmds) -> universe_info_ind -> Pp.std_ppcmds
+val pr_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> cumulativity_info -> Pp.std_ppcmds
+val pr_abstract_universe_context : (Level.t -> Pp.std_ppcmds) -> abstract_universe_context -> Pp.std_ppcmds
+val pr_abstract_cumulativity_info : (Level.t -> Pp.std_ppcmds) -> abstract_cumulativity_info -> Pp.std_ppcmds
val pr_universe_context_set : (Level.t -> Pp.std_ppcmds) -> universe_context_set -> Pp.std_ppcmds
val explain_universe_inconsistency : (Level.t -> Pp.std_ppcmds) ->
univ_inconsistency -> Pp.std_ppcmds
@@ -447,8 +480,10 @@ val hcons_univ : universe -> universe
val hcons_constraints : constraints -> constraints
val hcons_universe_set : universe_set -> universe_set
val hcons_universe_context : universe_context -> universe_context
+val hcons_abstract_universe_context : abstract_universe_context -> abstract_universe_context
val hcons_universe_context_set : universe_context_set -> universe_context_set
-val hcons_universe_info_ind : universe_info_ind -> universe_info_ind
+val hcons_cumulativity_info : cumulativity_info -> cumulativity_info
+val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info
(******)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index fa1662270..0e452621c 100644
--- a/kernel/vconv.ml
+++ b/kernel/vconv.ml
@@ -88,30 +88,34 @@ and conv_atom env pb k a1 stk1 a2 stk2 cu =
(* Pp.(msg_debug (str "conv_atom(" ++ pr_atom a1 ++ str ", " ++ pr_atom a2 ++ str ")")) ; *)
match a1, a2 with
| Aind ((mi,i) as ind1) , Aind ind2 ->
- if eq_ind ind1 ind2 && compare_stack stk1 stk2
- then
- if Environ.polymorphic_ind ind1 env
- then
- let mib = Environ.lookup_mind mi env in
- let ulen = Univ.UContext.size (Univ.UInfoInd.univ_context mib.Declarations.mind_universes) in
- match stk1 , stk2 with
- | [], [] -> assert (Int.equal ulen 0); cu
- | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
- assert (ulen <= nargs args1);
- assert (ulen <= nargs args2);
- let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
- let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
- let u1 = Univ.Instance.of_array u1 in
- let u2 = Univ.Instance.of_array u2 in
- let cu = convert_instances ~flex:false u1 u2 cu in
- conv_arguments env ~from:ulen k args1 args2
- (conv_stack env k stk1' stk2' cu)
- | _, _ -> assert false (* Should not happen if problem is well typed *)
- else
- conv_stack env k stk1 stk2 cu
- else raise NotConvertible
+ if eq_ind ind1 ind2 && compare_stack stk1 stk2 then
+ if Environ.polymorphic_ind ind1 env then
+ let mib = Environ.lookup_mind mi env in
+ let ulen =
+ match mib.Declarations.mind_universes with
+ | Declarations.Monomorphic_ind ctx -> Univ.UContext.size ctx
+ | Declarations.Polymorphic_ind auctx -> Univ.AUContext.size auctx
+ | Declarations.Cumulative_ind cumi ->
+ Univ.AUContext.size (Univ.ACumulativityInfo.univ_context cumi)
+ in
+ match stk1 , stk2 with
+ | [], [] -> assert (Int.equal ulen 0); cu
+ | Zapp args1 :: stk1' , Zapp args2 :: stk2' ->
+ assert (ulen <= nargs args1);
+ assert (ulen <= nargs args2);
+ let u1 = Array.init ulen (fun i -> uni_lvl_val (arg args1 i)) in
+ let u2 = Array.init ulen (fun i -> uni_lvl_val (arg args2 i)) in
+ let u1 = Univ.Instance.of_array u1 in
+ let u2 = Univ.Instance.of_array u2 in
+ let cu = convert_instances ~flex:false u1 u2 cu in
+ conv_arguments env ~from:ulen k args1 args2
+ (conv_stack env k stk1' stk2' cu)
+ | _, _ -> assert false (* Should not happen if problem is well typed *)
+ else
+ conv_stack env k stk1 stk2 cu
+ else raise NotConvertible
| Aid ik1, Aid ik2 ->
- if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
+ if Vars.eq_id_key ik1 ik2 && compare_stack stk1 stk2 then
conv_stack env k stk1 stk2 cu
else raise NotConvertible
| Atype _ , _ | _, Atype _ -> assert false