aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
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.ml14
-rw-r--r--kernel/declareops.ml120
-rw-r--r--kernel/declareops.mli15
-rw-r--r--kernel/entries.mli10
-rw-r--r--kernel/environ.ml46
-rw-r--r--kernel/environ.mli5
-rw-r--r--kernel/indtypes.ml115
-rw-r--r--kernel/inductive.ml10
-rw-r--r--kernel/kernel.mllib2
-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.ml276
-rw-r--r--kernel/reduction.mli9
-rw-r--r--kernel/safe_typing.ml79
-rw-r--r--kernel/subtyping.ml88
-rw-r--r--kernel/term_typing.ml114
-rw-r--r--kernel/typeops.ml2
-rw-r--r--kernel/univ.ml126
-rw-r--r--kernel/univ.mli85
-rw-r--r--kernel/vars.ml44
-rw-r--r--kernel/vconv.ml50
29 files changed, 940 insertions, 368 deletions
diff --git a/kernel/cbytegen.ml b/kernel/cbytegen.ml
index 57b397e6f8..02c6a2c715 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 c0f48641ce..48c2e45332 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 4deadff0a7..0008653644 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 7d47eba23e..9db85a4a11 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 71e228b19c..21651b3e21 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 abstract_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,9 +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_universes : Univ.universe_context; (** Local universe variables and constraints *)
+ mind_universes : abstract_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 0a822d6fad..72b4907680 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -45,9 +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 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
@@ -61,33 +67,56 @@ let type_of_constant cb =
if t' == t then x else RegularArity t'
| TemplateArity _ as x -> x
-let constraints_of_constant otab cb = 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))
+let constraints_of_constant otab cb =
+ 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
@@ -135,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 }
@@ -166,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 } *)
@@ -259,21 +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_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 mib.mind_universes
- else Univ.Instance.empty
-
-let inductive_context mib =
- if mib.mind_polymorphic then
- Univ.instantiate_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 } *)
@@ -301,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_context 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 6650b6b7b0..811a28aa65 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 1e07c96909..f133587c16 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,8 +54,9 @@ 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_universes : Univ.universe_context;
+ 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 5727bf2ea1..1ab5b7a8d1 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 b7431dbe5f..ae3afcb355 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 1e13239bfc..00fbe27a70 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -207,6 +207,50 @@ let param_ccls paramsctxt =
in
List.fold_left fold [] paramsctxt
+(* Check arities and constructors *)
+let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : Term.types) numparams is_arity =
+ let numchecked = ref 0 in
+ let basic_check ev tp =
+ if !numchecked < numparams then () else conv_leq ev tp (subst tp);
+ numchecked := !numchecked + 1
+ in
+ let check_typ typ typ_env =
+ match typ with
+ | LocalAssum (_, typ') ->
+ begin
+ try
+ basic_check typ_env typ'; Environ.push_rel typ typ_env
+ with NotConvertible ->
+ anomaly ~label:"bad inductive subtyping relation" (Pp.str "Invalid subtyping relation")
+ end
+ | _ -> anomaly (Pp.str "")
+ in
+ let typs, codom = dest_prod env arcn in
+ let last_env = Context.Rel.fold_outside check_typ typs ~init:env in
+ if not is_arity then basic_check last_env codom else ()
+
+(* 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 cumi paramsctxt env_ar inds =
+ let numparams = Context.Rel.nhyps paramsctxt in
+ let sbsubst = CumulativityInfo.subtyping_susbst cumi in
+ let dosubst = subst_univs_level_constr sbsubst 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 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 env dosubst full_arity numparams true;
+ Array.iter (fun cnt -> check_subtyping_arity_constructor env dosubst cnt numparams false) lc
+ | TemplateArity _ -> ()
+ ) inds
+
(* Type-check an inductive definition. Does not check positivity
conditions. *)
(* TODO check that we don't overgeneralize construcors/inductive arities with
@@ -220,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 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 *)
@@ -339,12 +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 () =
+ 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)
(************************************************************************)
@@ -816,23 +875,31 @@ 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 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 subst, ctx = Univ.abstract_universes p ctx in
- let paramsctxt = Vars.subst_univs_level_context subst paramsctxt in
- let env_ar =
- let ctx = Environ.rel_context env_ar in
- let ctx' = Vars.subst_univs_level_context subst ctx in
- Environ.push_rel_context ctx' env
+ 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
+ let ctxunivs' = Vars.subst_univs_level_context substunivs ctxunivs in
+ Environ.push_rel_context ctxunivs' env
in
(* Check one inductive *)
let build_one_packet (id,cnames,lc,(ar_sign,ar_kind)) recarg =
(* Type of constructors in normal form *)
- let lc = Array.map (Vars.subst_univs_level_constr subst) lc in
+ let lc = Array.map (Vars.subst_univs_level_constr substunivs) lc in
let splayed_lc = Array.map (dest_prod_assum env_ar) lc in
let nf_lc = Array.map (fun (d,b) -> it_mkProd_or_LetIn b d) splayed_lc in
let consnrealdecls =
@@ -851,8 +918,8 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
let s = sort_of_univ defs in
let kelim = allowed_sorts info s in
let ar = RegularArity
- { mind_user_arity = Vars.subst_univs_level_constr subst ar;
- mind_sort = sort_of_univ (Univ.subst_univs_level_universe subst defs); } in
+ { mind_user_arity = Vars.subst_univs_level_constr substunivs ar;
+ mind_sort = sort_of_univ (Univ.subst_univs_level_universe substunivs defs); } in
ar, kelim in
(* Assigning VM tags to constructors *)
let nconst, nblock = ref 0, ref 0 in
@@ -871,7 +938,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
(* Build the inductive packet *)
{ mind_typename = id;
mind_arity = arkind;
- mind_arity_ctxt = Vars.subst_univs_level_context subst ar_sign;
+ mind_arity_ctxt = Vars.subst_univs_level_context substunivs ar_sign;
mind_nrealargs = Context.Rel.nhyps ar_sign - nparamargs;
mind_nrealdecls = Context.Rel.length ar_sign - nparamsctxt;
mind_kelim = kelim;
@@ -893,10 +960,14 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
&& 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 subst (Univ.UContext.instance ctx)
- 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
@@ -919,8 +990,7 @@ let build_inductive env p prv ctx env_ar paramsctxt kn isrecord isfinite inds nm
mind_nparams_rec = nmr;
mind_params_ctxt = paramsctxt;
mind_packets = packets;
- mind_polymorphic = p;
- mind_universes = ctx;
+ mind_universes = aiu;
mind_private = prv;
mind_typing_flags = Environ.typing_flags env;
}
@@ -935,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_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/inductive.ml b/kernel/inductive.ml
index f3b03252db..e81a1cb587 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 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/kernel.mllib b/kernel/kernel.mllib
index 2f49982ce2..0813315b5b 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -41,5 +41,5 @@ Nativelibrary
Safe_typing
Vm
Csymtable
-Vconv
Declarations
+Vconv
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index ff44f0f540..79016735bc 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 1f8b97ae6a..33d13f1ba0 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 e9f3db6e91..4b533c7efd 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 d3cd6b62a5..4941d64d82 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 59e90ca2e9..3e15ff7401 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 3897d5e51e..be1f4b13f0 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 427ce04c55..605e9f314c 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -191,6 +191,10 @@ type 'a universe_compare =
{ (* Might raise NotConvertible *)
compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+ conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+ Univ.Instance.t -> int -> 'a -> 'a;
+ conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+ Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
}
type 'a universe_state = 'a * 'a universe_compare
@@ -206,6 +210,12 @@ let sort_cmp_universes env pb s0 s1 (u, check) =
constructors. *)
let convert_instances ~flex u u' (s, check) =
(check.compare_instances ~flex u u' s, check)
+
+let convert_inductives cv_pb ind u1 sv1 u2 sv2 (s, check) =
+ (check.conv_inductives cv_pb ind u1 sv1 u2 sv2 s, check)
+
+let convert_constructors cons u1 sv1 u2 sv2 (s, check) =
+ (check.conv_constructors cons u1 sv1 u2 sv2 s, check)
let conv_table_key infos k1 k2 cuniv =
if k1 == k2 then cuniv else
@@ -299,11 +309,11 @@ let unfold_projection infos p c =
else None
(* Conversion between [lft1]term1 and [lft2]term2 *)
-let rec ccnv cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
- eqappr cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
+let rec ccnv env cv_pb l2r infos lft1 lft2 term1 term2 cuniv =
+ eqappr env cv_pb l2r infos (lft1, (term1,[])) (lft2, (term2,[])) cuniv
(* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
-and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
+and eqappr env cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
Control.check_for_interrupt ();
(* First head reduce both terms *)
let whd = whd_stack (infos_with_reds infos betaiotazeta) in
@@ -328,13 +338,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
sort_cmp_universes (env_of_infos infos) cv_pb s1 s2 cuniv
| (Meta n, Meta m) ->
if Int.equal n m
- then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| _ -> raise NotConvertible)
| (FEvar ((ev1,args1),env1), FEvar ((ev2,args2),env2)) ->
if Evar.equal ev1 ev2 then
- let cuniv = convert_stacks l2r infos lft1 lft2 v1 v2 cuniv in
- convert_vect l2r infos el1 el2
+ let cuniv = convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv in
+ convert_vect env l2r infos el1 el2
(Array.map (mk_clos env1) args1)
(Array.map (mk_clos env2) args2) cuniv
else raise NotConvertible
@@ -342,34 +352,34 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* 2 index known to be bound to no constant *)
| (FRel n, FRel m) ->
if Int.equal (reloc_rel n el1) (reloc_rel m el2)
- then convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ then convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* 2 constants, 2 local defined vars or 2 defined rels *)
| (FFlex fl1, FFlex fl2) ->
(try
let cuniv = conv_table_key infos fl1 fl2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
with NotConvertible | Univ.UniverseInconsistency _ ->
(* else the oracle tells which constant is to be expanded *)
let oracle = CClosure.oracle_of_infos infos in
let (app1,app2) =
if Conv_oracle.oracle_order Univ.out_punivs oracle l2r fl1 fl2 then
match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd def1 v1), appr2)
+ | Some def1 -> ((lft1, (def1, v1)), appr2)
| None ->
(match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd def2 v2))
+ | Some def2 -> (appr1, (lft2, (def2, v2)))
| None -> raise NotConvertible)
else
match unfold_reference infos fl2 with
- | Some def2 -> (appr1, (lft2, whd def2 v2))
+ | Some def2 -> (appr1, (lft2, (def2, v2)))
| None ->
(match unfold_reference infos fl1 with
- | Some def1 -> ((lft1, whd def1 v1), appr2)
+ | Some def1 -> ((lft1, (def1, v1)), appr2)
| None -> raise NotConvertible)
in
- eqappr cv_pb l2r infos app1 app2 cuniv)
+ eqappr env cv_pb l2r infos app1 app2 cuniv)
| (FProj (p1,c1), FProj (p2, c2)) ->
(* Projections: prefer unfolding to first-order unification,
@@ -377,42 +387,42 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
form *)
(match unfold_projection infos p1 c1 with
| Some (def1,s1) ->
- eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+ eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
| None ->
match unfold_projection infos p2 c2 with
| Some (def2,s2) ->
- eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+ eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
| None ->
if Constant.equal (Projection.constant p1) (Projection.constant p2)
&& compare_stack_shape v1 v2 then
- let u1 = ccnv CONV l2r infos el1 el2 c1 c2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 u1
+ let u1 = ccnv env CONV l2r infos el1 el2 c1 c2 cuniv in
+ convert_stacks env l2r infos lft1 lft2 v1 v2 u1
else (* Two projections in WHNF: unfold *)
raise NotConvertible)
| (FProj (p1,c1), t2) ->
(match unfold_projection infos p1 c1 with
| Some (def1,s1) ->
- eqappr cv_pb l2r infos (lft1, whd def1 (s1 :: v1)) appr2 cuniv
+ eqappr env cv_pb l2r infos (lft1, (def1, (s1 :: v1))) appr2 cuniv
| None ->
(match t2 with
| FFlex fl2 ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+ eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
| (t1, FProj (p2,c2)) ->
(match unfold_projection infos p2 c2 with
| Some (def2,s2) ->
- eqappr cv_pb l2r infos appr1 (lft2, whd def2 (s2 :: v2)) cuniv
+ eqappr env cv_pb l2r infos appr1 (lft2, (def2, (s2 :: v2))) cuniv
| None ->
(match t1 with
| FFlex fl1 ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+ eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None -> raise NotConvertible)
| _ -> raise NotConvertible))
@@ -424,15 +434,15 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given ill-typed terms (FLambda).");
let (_,ty1,bd1) = destFLambda mk_clos hd1 in
let (_,ty2,bd2) = destFLambda mk_clos hd2 in
- let cuniv = ccnv CONV l2r infos el1 el2 ty1 ty2 cuniv in
- ccnv CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
+ let cuniv = ccnv env CONV l2r infos el1 el2 ty1 ty2 cuniv in
+ ccnv env CONV l2r infos (el_lift el1) (el_lift el2) bd1 bd2 cuniv
| (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
if not (is_empty_stack v1 && is_empty_stack v2) then
anomaly (Pp.str "conversion was given ill-typed terms (FProd).");
(* Luo's system *)
- let cuniv = ccnv CONV l2r infos el1 el2 c1 c'1 cuniv in
- ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
+ let cuniv = ccnv env CONV l2r infos el1 el2 c1 c'1 cuniv in
+ ccnv env cv_pb l2r infos (el_lift el1) (el_lift el2) c2 c'2 cuniv
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
@@ -442,7 +452,7 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given unreduced term (FLambda).")
in
let (_,_ty1,bd1) = destFLambda mk_clos hd1 in
- eqappr CONV l2r infos
+ eqappr env CONV l2r infos
(el_lift lft1, (bd1, [])) (el_lift lft2, (hd2, eta_expand_stack v2)) cuniv
| (_, FLambda _) ->
let () = match v2 with
@@ -451,66 +461,88 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
anomaly (Pp.str "conversion was given unreduced term (FLambda).")
in
let (_,_ty2,bd2) = destFLambda mk_clos hd2 in
- eqappr CONV l2r infos
+ eqappr env CONV l2r infos
(el_lift lft1, (hd1, eta_expand_stack v1)) (el_lift lft2, (bd2, [])) cuniv
(* only one constant, defined var or defined rel *)
| (FFlex fl1, c2) ->
(match unfold_reference infos fl1 with
| Some def1 ->
- eqappr cv_pb l2r infos (lft1, whd def1 v1) appr2 cuniv
+ eqappr env cv_pb l2r infos (lft1, (def1, v1)) appr2 cuniv
| None ->
match c2 with
| FConstruct ((ind2,j2),u2) ->
(try
let v2, v1 =
eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
| (c1, FFlex fl2) ->
(match unfold_reference infos fl2 with
| Some def2 ->
- eqappr cv_pb l2r infos appr1 (lft2, whd def2 v2) cuniv
+ eqappr env cv_pb l2r infos appr1 (lft2, (def2, v2)) cuniv
| None ->
match c1 with
| FConstruct ((ind1,j1),u1) ->
(try let v1, v2 =
eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
- in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| _ -> raise NotConvertible)
(* Inductive types: MutInd MutConstruct Fix Cofix *)
-
| (FInd (ind1,u1), FInd (ind2,u2)) ->
- if eq_ind ind1 ind2
- then
- (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
- else raise NotConvertible
+ if eq_ind ind1 ind2 then
+ if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+ let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ else
+ let mind = Environ.lookup_mind (fst ind1) env in
+ let cuniv =
+ 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
+ in
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ else raise NotConvertible
| (FConstruct ((ind1,j1),u1), FConstruct ((ind2,j2),u2)) ->
- if Int.equal j1 j2 && eq_ind ind1 ind2
- then
- (let cuniv = convert_instances ~flex:false u1 u2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv)
- else raise NotConvertible
+ if Int.equal j1 j2 && eq_ind ind1 ind2 then
+ if Univ.Instance.length u1 = 0 || Univ.Instance.length u2 = 0 then
+ let cuniv = convert_instances ~flex:false u1 u2 cuniv in
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ else
+ let mind = Environ.lookup_mind (fst ind1) env in
+ let cuniv =
+ 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
+ in
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
+ else raise NotConvertible
(* Eta expansion of records *)
| (FConstruct ((ind1,j1),u1), _) ->
(try
let v1, v2 =
eta_expand_ind_stack (info_env infos) ind1 hd1 v1 (snd appr2)
- in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (_, FConstruct ((ind2,j2),u2)) ->
(try
let v2, v1 =
eta_expand_ind_stack (info_env infos) ind2 hd2 v2 (snd appr1)
- in convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ in convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
with Not_found -> raise NotConvertible)
| (FFix (((op1, i1),(_,tys1,cl1)),e1), FFix(((op2, i2),(_,tys2,cl2)),e2)) ->
@@ -521,11 +553,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+ let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
- convert_vect l2r infos
+ convert_vect env l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
| (FCoFix ((op1,(_,tys1,cl1)),e1), FCoFix((op2,(_,tys2,cl2)),e2)) ->
@@ -536,11 +568,11 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
let fty2 = Array.map (mk_clos e2) tys2 in
let fcl1 = Array.map (mk_clos (subs_liftn n e1)) cl1 in
let fcl2 = Array.map (mk_clos (subs_liftn n e2)) cl2 in
- let cuniv = convert_vect l2r infos el1 el2 fty1 fty2 cuniv in
+ let cuniv = convert_vect env l2r infos el1 el2 fty1 fty2 cuniv in
let cuniv =
- convert_vect l2r infos
+ convert_vect env l2r infos
(el_liftn n el1) (el_liftn n el2) fcl1 fcl2 cuniv in
- convert_stacks l2r infos lft1 lft2 v1 v2 cuniv
+ convert_stacks env l2r infos lft1 lft2 v1 v2 cuniv
else raise NotConvertible
(* Should not happen because both (hd1,v1) and (hd2,v2) are in whnf *)
@@ -551,13 +583,13 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
(* In all other cases, terms are not convertible *)
| _ -> raise NotConvertible
-and convert_stacks l2r infos lft1 lft2 stk1 stk2 cuniv =
+and convert_stacks env l2r infos lft1 lft2 stk1 stk2 cuniv =
compare_stacks
- (fun (l1,t1) (l2,t2) cuniv -> ccnv CONV l2r infos l1 l2 t1 t2 cuniv)
+ (fun (l1,t1) (l2,t2) cuniv -> ccnv env CONV l2r infos l1 l2 t1 t2 cuniv)
(eq_ind)
lft1 stk1 lft2 stk2 cuniv
-and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
+and convert_vect env l2r infos lft1 lft2 v1 v2 cuniv =
let lv1 = Array.length v1 in
let lv2 = Array.length v2 in
if Int.equal lv1 lv2
@@ -565,7 +597,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let rec fold n cuniv =
if n >= lv1 then cuniv
else
- let cuniv = ccnv CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
+ let cuniv = ccnv env CONV l2r infos lft1 lft2 v1.(n) v2.(n) cuniv in
fold (n+1) cuniv in
fold 0 cuniv
else raise NotConvertible
@@ -573,7 +605,7 @@ and convert_vect l2r infos lft1 lft2 v1 v2 cuniv =
let clos_gen_conv trans cv_pb l2r evars env univs t1 t2 =
let reds = CClosure.RedFlags.red_add_transparent betaiotazeta trans in
let infos = create_clos_infos ~evars reds env in
- ccnv cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
+ ccnv env cv_pb l2r infos el_id el_id (inject t1) (inject t2) univs
let check_eq univs u u' =
@@ -610,9 +642,88 @@ let check_convert_instances ~flex u u' univs =
if UGraph.check_eq_instances univs u u' then univs
else raise NotConvertible
+(* general conversion and inference functions *)
+let infer_check_conv_inductives
+ infer_check_convert_instances
+ infer_check_inductive_instances
+ cv_pb (mind, ind) u1 sv1 u2 sv2 univs =
+ 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
+ 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 =
+ 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
+ (* Context.Rel.length mind.Declarations.mind_params_ctxt *) in
+ nparamsctxt + mind.Declarations.mind_packets.(ind).Declarations.mind_consnrealargs.(cns - 1)
+ in
+ if not (num_cnstr_args = sv1 && num_cnstr_args = sv2) then
+ infer_check_convert_instances ~flex:false u1 u2 univs
+ else
+ infer_check_inductive_instances CONV cumi u1 u2 univs
+
+let check_inductive_instances cv_pb cumi u u' univs =
+ let length_ind_instance =
+ Univ.Instance.length
+ (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+ in
+ let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
+ if not ((length_ind_instance = Univ.Instance.length u) &&
+ (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.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx)
+ in
+ let comp_cst =
+ match cv_pb with
+ CONV ->
+ 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
+ if (UGraph.check_constraints comp_cst univs) then univs
+ else raise NotConvertible
+
+let check_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+ infer_check_conv_inductives
+ check_convert_instances
+ check_inductive_instances
+ cv_pb ind u1 sv1 u2 sv2 univs
+
+let check_conv_constructors cns u1 sv1 u2 sv2 univs =
+ infer_check_conv_constructors
+ check_convert_instances
+ check_inductive_instances
+ cns u1 sv1 u2 sv2 univs
+
let checked_universes =
{ compare = checked_sort_cmp_universes;
- compare_instances = check_convert_instances }
+ compare_instances = check_convert_instances;
+ conv_inductives = check_conv_inductives;
+ conv_constructors = check_conv_constructors}
let infer_eq (univs, cstrs as cuniv) u u' =
if UGraph.check_eq univs u u' then cuniv
@@ -647,11 +758,58 @@ let infer_cmp_universes env pb s0 s1 univs =
else univs
let infer_convert_instances ~flex u u' (univs,cstrs) =
- (univs, Univ.enforce_eq_instances u u' cstrs)
-
+ let cstrs' =
+ if flex then
+ if UGraph.check_eq_instances univs u u' then cstrs
+ else raise NotConvertible
+ else Univ.enforce_eq_instances u u' cstrs
+ in (univs, cstrs')
+
+let infer_inductive_instances cv_pb cumi u u' (univs, cstrs) =
+ let length_ind_instance =
+ Univ.Instance.length
+ (Univ.AUContext.instance (Univ.ACumulativityInfo.univ_context cumi))
+ in
+ let ind_subtypctx = Univ.ACumulativityInfo.subtyp_context cumi in
+ if not ((length_ind_instance = Univ.Instance.length u) &&
+ (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.UContext.constraints
+ (Univ.subst_instance_context comp_subst ind_subtypctx)
+ in
+ let comp_cst =
+ match cv_pb with
+ CONV ->
+ 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
+ (univs, Univ.Constraint.union cstrs comp_cst)
+
+
+let infer_conv_inductives cv_pb ind u1 sv1 u2 sv2 univs =
+ infer_check_conv_inductives
+ infer_convert_instances
+ infer_inductive_instances
+ cv_pb ind u1 sv1 u2 sv2 univs
+
+let infer_conv_constructors cns u1 sv1 u2 sv2 univs =
+ infer_check_conv_constructors
+ infer_convert_instances
+ infer_inductive_instances
+ cns u1 sv1 u2 sv2 univs
+
let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
{ compare = infer_cmp_universes;
- compare_instances = infer_convert_instances }
+ compare_instances = infer_convert_instances;
+ conv_inductives = infer_conv_inductives;
+ conv_constructors = infer_conv_constructors}
let gen_conv cv_pb l2r reds env evars univs t1 t2 =
let b =
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 8a2b2469d6..b6d88c2b9b 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -36,10 +36,13 @@ type 'a extended_conversion_function =
type conv_pb = CONV | CUMUL
type 'a universe_compare =
- { (* Might raise NotConvertible or UnivInconsistency *)
+ { (* Might raise NotConvertible *)
compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a;
- compare_instances: flex:bool ->
- Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+ compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a;
+ conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int ->
+ Univ.Instance.t -> int -> 'a -> 'a;
+ conv_constructors : (Declarations.mutual_inductive_body * int * int) ->
+ Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a;
}
type 'a universe_state = 'a * 'a universe_compare
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index f5e8e86530..946222ef2f 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 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 f779f68be4..1bd9d6e495 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -90,6 +90,7 @@ let check_conv_error error why cst poly u f env a1 a2 =
else error (IncompatiblePolymorphism (env, a1, a2))
else Constraint.union cst cst'
with NotConvertible -> error why
+ | Univ.UniverseInconsistency e -> error (IncompatibleUniverses e)
(* for now we do not allow reorderings *)
@@ -103,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 =
@@ -147,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 =
@@ -175,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))
@@ -292,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
@@ -353,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 =
@@ -370,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 eeb9c421a1..5370bcea43 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, mib.mind_universes, false, None
+ univs, false, None
let global_vars_set_constant_type env = function
| RegularArity t -> global_vars_set env t
@@ -337,18 +354,25 @@ 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
if not (Id.Set.subset inferred_set declared_set) then
let l = Id.Set.elements (Idset.diff inferred_set declared_set) in
let n = List.length l in
- user_err (Pp.(str "The following section " ++
- str (String.plural n "variable") ++
- str " " ++ str (String.conjugate_verb_to_be n) ++
- str " used but not declared:" ++
- fnl () ++ pr_sequence Id.print (List.rev l) ++ str ".")) in
+ let declared_vars = Pp.pr_sequence Id.print (Idset.elements declared_set) in
+ let inferred_vars = Pp.pr_sequence Id.print (Idset.elements inferred_set) in
+ let missing_vars = Pp.pr_sequence Id.print (List.rev l) in
+ user_err Pp.(prlist str
+ ["The following section "; (String.plural n "variable"); " ";
+ (String.conjugate_verb_to_be n); " used but not declared:"] ++ fnl () ++
+ missing_vars ++ str "." ++ fnl () ++ fnl () ++
+ str "You can either update your proof to not depend on " ++ missing_vars ++
+ str ", or you can update your Proof line from" ++ fnl () ++
+ str "Proof using " ++ declared_vars ++ fnl () ++
+ str "to" ++ fnl () ++
+ str "Proof using " ++ inferred_vars) in
let sort evn l =
List.filter (fun decl ->
let id = NamedDecl.get_id decl in
@@ -402,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 =>
@@ -418,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;
@@ -433,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 }
@@ -445,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
@@ -456,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 }
;;
@@ -501,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
@@ -546,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 1a07bb2fc6..e08f3362db 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 d53dd8e733..8cbb20a051 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -725,8 +725,11 @@ struct
pp_std ++ prl u1 ++ pr_constraint_type op ++
prl u2 ++ fnl () ) c (str "")
+ let universes_of c =
+ fold (fun (u1, op, u2) unvs -> LSet.add u2 (LSet.add u1 unvs)) c LSet.empty
end
+let universes_of_constraints = Constraint.universes_of
let empty_constraint = Constraint.empty
let union_constraint = Constraint.union
let eq_constraint = Constraint.equal
@@ -1028,6 +1031,82 @@ end
type universe_context = UContext.t
let hcons_universe_context = UContext.hcons
+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
+ for inductive types.
+
+ This data structure maintains the invariant that the context for
+ subtyping constraints is exactly twice as big as the context for
+ universe constraints. *)
+module CumulativityInfo =
+struct
+ type t = universe_context * universe_context
+
+ let make x =
+ if (Instance.length (UContext.instance (snd x))) =
+ (Instance.length (UContext.instance (fst x))) * 2 then x
+ else anomaly (Pp.str "Invalid subtyping information encountered!")
+
+ let empty = (UContext.empty, UContext.empty)
+ let is_empty (univcst, subtypcst) = UContext.is_empty univcst && UContext.is_empty subtypcst
+
+ let halve_context ctx =
+ let len = Array.length (Instance.to_array ctx) in
+ let halflen = len / 2 in
+ (Instance.of_array (Array.sub (Instance.to_array ctx) 0 halflen),
+ Instance.of_array (Array.sub (Instance.to_array ctx) halflen halflen))
+
+ let pr prl (univcst, subtypcst) =
+ if UContext.is_empty univcst then mt() else
+ let (ctx, ctx') = halve_context (UContext.instance subtypcst) in
+ (UContext.pr prl univcst) ++ fnl () ++ fnl () ++
+ h 0 (str "~@{" ++ Instance.pr prl ctx ++ str "} <= ~@{" ++ Instance.pr prl ctx' ++ str "} iff ")
+ ++ fnl () ++ h 0 (v 0 (Constraint.pr prl (UContext.constraints subtypcst)))
+
+ let hcons (univcst, subtypcst) =
+ (UContext.hcons univcst, UContext.hcons subtypcst)
+
+ let univ_context (univcst, subtypcst) = univcst
+ let subtyp_context (univcst, subtypcst) = subtypcst
+
+ let create_trivial_subtyping ctx ctx' =
+ CArray.fold_left_i
+ (fun i cst l -> Constraint.add (l, Eq, Array.get ctx' i) cst)
+ Constraint.empty (Instance.to_array ctx)
+
+ (** This function takes a universe context representing constraints
+ of an inductive and a Instance.t of fresh universe names for the
+ subtyping (with the same length as the context in the given
+ universe context) and produces a UInfoInd.t that with the
+ trivial subtyping relation. *)
+ let from_universe_context univcst freshunivs =
+ let inst = (UContext.instance univcst) in
+ assert (Instance.length freshunivs = Instance.length inst);
+ (univcst, UContext.make (Instance.append inst freshunivs,
+ create_trivial_subtyping inst freshunivs))
+
+ let subtyping_susbst (univcst, subtypcst) =
+ let (ctx, ctx') = (halve_context (UContext.instance subtypcst))in
+ Array.fold_left2 (fun subst l1 l2 -> LMap.add l1 l2 subst) LMap.empty ctx ctx'
+
+end
+
+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.
Beware, representation could change.
@@ -1132,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
@@ -1203,8 +1285,9 @@ let subst_instance_constraints s csts =
let instantiate_univ_context (ctx, csts) =
(ctx, subst_instance_constraints ctx csts)
-let instantiate_univ_constraints u (_, csts) =
- subst_instance_constraints u csts
+(** Substitute instance inst for ctx in universe constraints and subtyping constraints *)
+let instantiate_cumulativity_info (univcst, subtpcst) =
+ (instantiate_univ_context univcst, instantiate_univ_context subtpcst)
let make_instance_subst i =
let arr = Instance.to_array i in
@@ -1218,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 *)
@@ -1235,6 +1324,12 @@ 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 =
@@ -1290,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 1ccdebd501..ecc72701d4 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -315,6 +315,67 @@ 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
+ universe constraints, representing conditions for subtyping used
+ for inductive types.
+
+ This data structure maintains the invariant that the context for
+ subtyping constraints is exactly twice as big as the context for
+ universe constraints. *)
+module CumulativityInfo :
+sig
+ type t
+
+ val make : universe_context * universe_context -> t
+
+ val empty : t
+ val is_empty : t -> bool
+
+ val univ_context : t -> universe_context
+ val subtyp_context : t -> universe_context
+
+ (** This function takes a universe context representing constraints
+ of an inductive and a Instance.t of fresh universe names for the
+ subtyping (with the same length as the context in the given
+ universe context) and produces a UInfoInd.t that with the
+ trivial subtyping relation. *)
+ val from_universe_context : universe_context -> universe_instance -> t
+
+ val subtyping_susbst : t -> universe_level_subst
+
+end
+
+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) *)
module ContextSet :
@@ -365,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. *)
@@ -379,23 +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
-val instantiate_univ_constraints : universe_instance -> universe_context -> constraints
+(** Get the instantiated graphs for both universe constraints and subtyping 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_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
@@ -409,7 +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_cumulativity_info : cumulativity_info -> cumulativity_info
+val hcons_abstract_cumulativity_info : abstract_cumulativity_info -> abstract_cumulativity_info
(******)
@@ -419,3 +493,6 @@ val eq_levels : universe_level -> universe_level -> bool
(** deprecated: Equality of formal universe expressions. *)
val equal_universes : universe -> universe -> bool
+
+(** Universes of constraints *)
+val universes_of_constraints : constraints -> universe_set
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 629de80f7c..baf8fa31f6 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -319,35 +319,33 @@ let subst_instance_constr subst c =
if Univ.Instance.is_empty subst then c
else
let f u = Univ.subst_instance_instance subst u in
- let changed = ref false in
- let rec aux t =
+ let rec aux t =
match kind t with
- | Const (c, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; mkConstU (c, u'))
+ | Const (c, u) ->
+ if Univ.Instance.is_empty u then t
+ else
+ let u' = f u in
+ if u' == u then t
+ else (mkConstU (c, u'))
| Ind (i, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; mkIndU (i, u'))
+ if Univ.Instance.is_empty u then t
+ else
+ let u' = f u in
+ if u' == u then t
+ else (mkIndU (i, u'))
| Construct (c, u) ->
- if Univ.Instance.is_empty u then t
- else
- let u' = f u in
- if u' == u then t
- else (changed := true; mkConstructU (c, u'))
- | Sort (Sorts.Type u) ->
+ if Univ.Instance.is_empty u then t
+ else
+ let u' = f u in
+ if u' == u then t
+ else (mkConstructU (c, u'))
+ | Sort (Sorts.Type u) ->
let u' = Univ.subst_instance_universe subst u in
- if u' == u then t else
- (changed := true; mkSort (Sorts.sort_of_univ u'))
+ if u' == u then t else
+ (mkSort (Sorts.sort_of_univ u'))
| _ -> Constr.map aux t
in
- let c' = aux c in
- if !changed then c' else c
+ aux c
(* let substkey = Profile.declare_profile "subst_instance_constr";; *)
(* let subst_instance_constr inst c = Profile.profile2 substkey subst_instance_constr inst c;; *)
diff --git a/kernel/vconv.ml b/kernel/vconv.ml
index 74d956bef0..0e452621c8 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 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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-02 02:21:39 +0000