aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/cooking.ml22
-rw-r--r--kernel/indtypes.ml8
-rw-r--r--kernel/mod_typing.ml4
-rw-r--r--kernel/opaqueproof.ml2
-rw-r--r--kernel/opaqueproof.mli2
-rw-r--r--kernel/term_typing.ml1
-rw-r--r--kernel/univ.ml2
-rw-r--r--kernel/univ.mli4
-rw-r--r--library/lib.ml15
-rw-r--r--library/lib.mli4
-rw-r--r--vernac/record.ml1
11 files changed, 31 insertions, 34 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 31988ac1c..1f407fc29 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -168,13 +168,14 @@ let on_body ml hy f = function
{ Opaqueproof.modlist = ml; abstract = hy } o)
let expmod_constr_subst cache modlist subst c =
+ let subst = Univ.make_instance_subst subst in
let c = expmod_constr cache modlist c in
Vars.subst_univs_level_constr subst c
-let cook_constr { Opaqueproof.modlist ; abstract } c =
+let cook_constr { Opaqueproof.modlist ; abstract = (vars, subst, _) } c =
let cache = RefTable.create 13 in
- let expmod = expmod_constr_subst cache modlist (pi2 abstract) in
- let hyps = Context.Named.map expmod (pi1 abstract) in
+ let expmod = expmod_constr_subst cache modlist subst in
+ let hyps = Context.Named.map expmod vars in
abstract_constant_body (expmod c) hyps
let lift_univs cb subst auctx0 =
@@ -183,18 +184,13 @@ let lift_univs cb subst auctx0 =
assert (AUContext.is_empty auctx0);
subst, (Monomorphic_const ctx)
| Polymorphic_const auctx ->
- if (Univ.LMap.is_empty subst) then
+ if (Univ.Instance.is_empty subst) then
+ (** Still need to take the union for the constraints between globals *)
subst, (Polymorphic_const (AUContext.union auctx0 auctx))
else
- let len = Univ.LMap.cardinal subst in
- let rec gen_subst i acc =
- if i < 0 then acc
- else
- let acc = Univ.LMap.add (Level.var i) (Level.var (i + len)) acc in
- gen_subst (pred i) acc
- in
- let subst = gen_subst (Univ.AUContext.size auctx - 1) subst in
- let auctx' = Univ.subst_univs_level_abstract_universe_context subst auctx in
+ let ainst = Univ.make_abstract_instance auctx in
+ let subst = Instance.append subst ainst in
+ let auctx' = Univ.subst_univs_level_abstract_universe_context (Univ.make_instance_subst subst) auctx in
subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
let cook_constant ~hcons env { from = cb; info } =
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 1f2ae0b6c..b117f8714 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -879,9 +879,13 @@ 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)
+ let (inst, auctx) = Univ.abstract_universes ctx in
+ let inst = Univ.make_instance_subst inst in
+ (inst, Polymorphic_ind auctx)
| Cumulative_ind_entry cumi ->
- let (inst, acumi) = Univ.abstract_cumulativity_info cumi in (inst, Cumulative_ind acumi)
+ let (inst, acumi) = Univ.abstract_cumulativity_info cumi in
+ let inst = Univ.make_instance_subst inst 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
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index f7e755f00..b7eb481ee 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -94,8 +94,8 @@ let rec check_with_def env struc (idl,(c,ctx)) mp equiv =
let ctx = Univ.ContextSet.of_context ctx in
c', Monomorphic_const ctx, Univ.ContextSet.add_constraints cst ctx
| Polymorphic_const uctx ->
- let subst, ctx = Univ.abstract_universes ctx in
- let c = Vars.subst_univs_level_constr subst c in
+ let inst, ctx = Univ.abstract_universes ctx in
+ let c = Vars.subst_univs_level_constr (Univ.make_instance_subst inst) c in
let () =
if not (UGraph.check_subtype (Environ.universes env) uctx ctx) then
error_incorrect_with_constraint lab
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 45a62d55a..c2fcfbfd6 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.AUContext.t }
+ abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
type proofterm = (constr * Univ.ContextSet.t) 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 20d76ce23..c8339e6eb 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.AUContext.t }
+ abstract : Context.Named.t * Univ.Instance.t * Univ.AUContext.t }
(* The type has two caveats:
1) cook_constr is defined after
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 2e4426d62..cbc4ee2ec 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -232,6 +232,7 @@ let abstract_constant_universes = function
Univ.empty_level_subst, Monomorphic_const uctx
| Polymorphic_const_entry uctx ->
let sbst, auctx = Univ.abstract_universes uctx in
+ let sbst = Univ.make_instance_subst sbst in
sbst, Polymorphic_const auctx
let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 8cf9028fb..fee431ff4 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -1168,7 +1168,7 @@ let abstract_universes ctx =
(UContext.constraints ctx)
in
let ctx = UContext.make (instance, cstrs) in
- subst, ctx
+ instance, ctx
let abstract_cumulativity_info (univcst, substcst) =
let instance, univcst = abstract_universes univcst in
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 459394439..324167890 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -470,9 +470,9 @@ val subst_instance_universe : Instance.t -> Universe.t -> Universe.t
val make_instance_subst : Instance.t -> universe_level_subst
val make_inverse_instance_subst : Instance.t -> universe_level_subst
-val abstract_universes : UContext.t -> universe_level_subst * AUContext.t
+val abstract_universes : UContext.t -> Instance.t * AUContext.t
-val abstract_cumulativity_info : CumulativityInfo.t -> universe_level_subst * ACumulativityInfo.t
+val abstract_cumulativity_info : CumulativityInfo.t -> Instance.t * ACumulativityInfo.t
val make_abstract_instance : AUContext.t -> Instance.t
diff --git a/library/lib.ml b/library/lib.ml
index 16dd7fdd0..971089c17 100644
--- a/library/lib.ml
+++ b/library/lib.ml
@@ -419,7 +419,7 @@ type variable_info = Context.Named.Declaration.t * Decl_kinds.binding_kind
type variable_context = variable_info list
type abstr_info = {
abstr_ctx : variable_context;
- abstr_subst : Univ.universe_level_subst;
+ abstr_subst : Univ.Instance.t;
abstr_uctx : Univ.AUContext.t;
}
type abstr_list = abstr_info Names.Cmap.t * abstr_info Names.Mindmap.t
@@ -511,7 +511,7 @@ let section_segment_of_mutual_inductive kn =
let empty_segment = {
abstr_ctx = [];
- abstr_subst = Univ.LMap.empty;
+ abstr_subst = Univ.Instance.empty;
abstr_uctx = Univ.AUContext.empty;
}
@@ -672,13 +672,8 @@ let discharge_inductive (kn,i) =
let discharge_abstract_universe_context { abstr_subst = subst; abstr_uctx = abs_ctx } auctx =
let open Univ in
- let len = LMap.cardinal subst in
- let rec gen_subst i acc =
- if i < 0 then acc
- else
- let acc = LMap.add (Level.var i) (Level.var (i + len)) acc in
- gen_subst (pred i) acc
- in
- let subst = gen_subst (AUContext.size auctx - 1) subst in
+ let ainst = make_abstract_instance auctx in
+ let subst = Instance.append subst ainst in
+ let subst = make_instance_subst subst in
let auctx = Univ.subst_univs_level_abstract_universe_context subst auctx in
subst, AUContext.union abs_ctx auctx
diff --git a/library/lib.mli b/library/lib.mli
index 2f4d0d56f..cf75d5f8c 100644
--- a/library/lib.mli
+++ b/library/lib.mli
@@ -156,8 +156,8 @@ type variable_context = variable_info list
type abstr_info = private {
abstr_ctx : variable_context;
(** Section variables of this prefix *)
- abstr_subst : Univ.universe_level_subst;
- (** Abstract substitution: named universes are mapped to De Bruijn indices *)
+ abstr_subst : Univ.Instance.t;
+ (** Actual names of the abstracted variables *)
abstr_uctx : Univ.AUContext.t;
(** Universe quantification, same length as the substitution *)
}
diff --git a/vernac/record.ml b/vernac/record.ml
index d9dc16d96..1e464eb8b 100644
--- a/vernac/record.ml
+++ b/vernac/record.ml
@@ -531,6 +531,7 @@ let declare_class finite def cum ubinders univs id idbuild paramimpls params ari
match univs with
| Polymorphic_const_entry univs ->
let usubst, auctx = Univ.abstract_universes univs in
+ let usubst = Univ.make_instance_subst usubst in
let map c = Vars.subst_univs_level_constr usubst c in
let fields = Context.Rel.map map fields in
let ctx_context = on_snd (fun d -> Context.Rel.map map d) ctx_context in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-20 06:30:00 +0000