aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/constr.ml4
-rw-r--r--kernel/mod_subst.ml41
-rw-r--r--kernel/mod_subst.mli10
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/univ.ml9
-rw-r--r--kernel/univ.mli8
-rw-r--r--kernel/vars.ml5
-rw-r--r--kernel/vars.mli3
8 files changed, 49 insertions, 34 deletions
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 8e5d15dd2d..d67d15b23b 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -1361,7 +1361,7 @@ type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
-(* Sorts and sort family *)
+(** Minimalistic constr printer, typically for debugging *)
let debug_print_fix pr_constr ((t,i),(lna,tl,bl)) =
let open Pp in
@@ -1377,8 +1377,6 @@ let pr_puniverses p u =
if Univ.Instance.is_empty u then p
else Pp.(p ++ str"(*" ++ Univ.Instance.pr Univ.Level.pr u ++ str"*)")
-(* Minimalistic constr printer, typically for debugging *)
-
let rec debug_print c =
let open Pp in
match kind c with
diff --git a/kernel/mod_subst.ml b/kernel/mod_subst.ml
index 2a91c7dab0..52fb39e1d0 100644
--- a/kernel/mod_subst.ml
+++ b/kernel/mod_subst.ml
@@ -24,7 +24,7 @@ open Constr
is the term into which we should inline. *)
type delta_hint =
- | Inline of int * (Univ.AUContext.t * constr) option
+ | Inline of int * constr Univ.univ_abstracted option
| Equiv of KerName.t
(* NB: earlier constructor Prefix_equiv of ModPath.t
@@ -164,7 +164,7 @@ let find_prefix resolve mp =
(** Applying a resolver to a kernel name *)
-exception Change_equiv_to_inline of (int * (Univ.AUContext.t * constr))
+exception Change_equiv_to_inline of (int * constr Univ.univ_abstracted)
let solve_delta_kn resolve kn =
try
@@ -294,43 +294,34 @@ let subst_ind sub (ind,i as indi) =
let subst_pind sub (ind,u) =
(subst_ind sub ind, u)
-let subst_con0 sub (cst,u) =
+let subst_con0 sub cst =
let mpu,l = Constant.repr2 cst in
let mpc = KerName.modpath (Constant.canonical cst) in
let mpu,mpc,resolve,user = subst_dual_mp sub mpu mpc in
let knu = KerName.make mpu l in
let knc = if mpu == mpc then knu else KerName.make mpc l in
match search_delta_inline resolve knu knc with
- | Some (ctx, t) ->
+ | Some t ->
(* In case of inlining, discard the canonical part (cf #2608) *)
- let () = assert (Int.equal (Univ.AUContext.size ctx) (Univ.Instance.length u)) in
- Constant.make1 knu, Vars.subst_instance_constr u t
+ Constant.make1 knu, Some t
| None ->
let knc' =
progress (kn_of_delta resolve) (if user then knu else knc) ~orelse:knc
in
let cst' = Constant.make knu knc' in
- cst', mkConstU (cst',u)
+ cst', None
let subst_con sub cst =
try subst_con0 sub cst
- with No_subst -> fst cst, mkConstU cst
+ with No_subst -> cst, None
-let subst_con_kn sub con =
- subst_con sub (con,Univ.Instance.empty)
-
-let subst_pcon sub (_con,u as pcon) =
- try let con', _can = subst_con0 sub pcon in
+let subst_pcon sub (con,u as pcon) =
+ try let con', _can = subst_con0 sub con in
con',u
with No_subst -> pcon
-let subst_pcon_term sub (_con,u as pcon) =
- try let con', can = subst_con0 sub pcon in
- (con',u), can
- with No_subst -> pcon, mkConstU pcon
-
let subst_constant sub con =
- try fst (subst_con0 sub (con,Univ.Instance.empty))
+ try fst (subst_con0 sub con)
with No_subst -> con
let subst_proj_repr sub p =
@@ -351,7 +342,7 @@ let subst_evaluable_reference subst = function
let rec map_kn f f' c =
let func = map_kn f f' in
match kind c with
- | Const kn -> (try snd (f' kn) with No_subst -> c)
+ | Const kn -> (try f' kn with No_subst -> c)
| Proj (p,t) ->
let p' = Projection.map f p in
let t' = func t in
@@ -420,8 +411,14 @@ let rec map_kn f f' c =
| _ -> c
let subst_mps sub c =
+ let subst_pcon_term sub (con,u) =
+ let con', can = subst_con0 sub con in
+ match can with
+ | None -> mkConstU (con',u)
+ | Some t -> Vars.univ_instantiate_constr u t
+ in
if is_empty_subst sub then c
- else map_kn (subst_mind sub) (subst_con0 sub) c
+ else map_kn (subst_mind sub) (subst_pcon_term sub) c
let rec replace_mp_in_mp mpfrom mpto mp =
match mp with
@@ -486,7 +483,7 @@ let gen_subst_delta_resolver dom subst resolver =
| Equiv kequ ->
(try Equiv (subst_kn_delta subst kequ)
with Change_equiv_to_inline (lev,c) -> Inline (lev,Some c))
- | Inline (lev,Some (ctx, t)) -> Inline (lev,Some (ctx, subst_mps subst t))
+ | Inline (lev,Some t) -> Inline (lev,Some (Univ.map_univ_abstracted (subst_mps subst) t))
| Inline (_,None) -> hint
in
Deltamap.add_kn kkey' hint' rslv
diff --git a/kernel/mod_subst.mli b/kernel/mod_subst.mli
index 8416094063..ea391b3de7 100644
--- a/kernel/mod_subst.mli
+++ b/kernel/mod_subst.mli
@@ -28,7 +28,7 @@ val add_kn_delta_resolver :
KerName.t -> KerName.t -> delta_resolver -> delta_resolver
val add_inline_delta_resolver :
- KerName.t -> (int * (Univ.AUContext.t * constr) option) -> delta_resolver -> delta_resolver
+ KerName.t -> (int * constr Univ.univ_abstracted option) -> delta_resolver -> delta_resolver
val add_delta_resolver : delta_resolver -> delta_resolver -> delta_resolver
@@ -133,17 +133,11 @@ val subst_kn :
substitution -> KerName.t -> KerName.t
val subst_con :
- substitution -> pconstant -> Constant.t * constr
+ substitution -> Constant.t -> Constant.t * constr Univ.univ_abstracted option
val subst_pcon :
substitution -> pconstant -> pconstant
-val subst_pcon_term :
- substitution -> pconstant -> pconstant * constr
-
-val subst_con_kn :
- substitution -> Constant.t -> Constant.t * constr
-
val subst_constant :
substitution -> Constant.t -> Constant.t
diff --git a/kernel/modops.ml b/kernel/modops.ml
index f43dbd88f9..97ac3cdebb 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -403,7 +403,8 @@ let inline_delta_resolver env inl mp mbid mtb delta =
| Def body ->
let constr = Mod_subst.force_constr body in
let ctx = Declareops.constant_polymorphic_context constant in
- add_inline_delta_resolver kn (lev, Some (ctx, constr)) l
+ let constr = Univ.{univ_abstracted_value=constr; univ_abstracted_binder=ctx} in
+ add_inline_delta_resolver kn (lev, Some constr) l
with Not_found ->
error_no_such_label_sub (Constant.label con)
(ModPath.to_string (Constant.modpath con))
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 7b5ed05bda..93a91af1d7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -978,6 +978,15 @@ struct
end
+type 'a univ_abstracted = {
+ univ_abstracted_value : 'a;
+ univ_abstracted_binder : AUContext.t;
+}
+
+let map_univ_abstracted f {univ_abstracted_value;univ_abstracted_binder} =
+ let univ_abstracted_value = f univ_abstracted_value in
+ {univ_abstracted_value;univ_abstracted_binder}
+
let hcons_abstract_universe_context = AUContext.hcons
(** Universe info for cumulative inductive types: A context of
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 512f38cedd..8327ff1644 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -360,6 +360,14 @@ sig
end
+type 'a univ_abstracted = {
+ univ_abstracted_value : 'a;
+ univ_abstracted_binder : AUContext.t;
+}
+(** A value with bound universe levels. *)
+
+val map_univ_abstracted : ('a -> 'b) -> 'a univ_abstracted -> 'b univ_abstracted
+
(** Universe info for cumulative inductive types: A context of
universe levels with universe constraints, representing local
universe variables and constraints, together with an array of
diff --git a/kernel/vars.ml b/kernel/vars.ml
index f9c576ca4a..bd56d60053 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -295,6 +295,11 @@ let subst_instance_constr subst c =
in
aux c
+let univ_instantiate_constr u c =
+ let open Univ in
+ assert (Int.equal (Instance.length u) (AUContext.size c.univ_abstracted_binder));
+ subst_instance_constr u c.univ_abstracted_value
+
(* let substkey = CProfile.declare_profile "subst_instance_constr";; *)
(* let subst_instance_constr inst c = CProfile.profile2 substkey subst_instance_constr inst c;; *)
diff --git a/kernel/vars.mli b/kernel/vars.mli
index 7c928e2694..f2c32b3625 100644
--- a/kernel/vars.mli
+++ b/kernel/vars.mli
@@ -140,4 +140,7 @@ val subst_univs_level_context : Univ.universe_level_subst -> Constr.rel_context
val subst_instance_constr : Instance.t -> constr -> constr
val subst_instance_context : Instance.t -> Constr.rel_context -> Constr.rel_context
+val univ_instantiate_constr : Instance.t -> constr univ_abstracted -> constr
+(** Ignores the constraints carried by [univ_abstracted]. *)
+
val universes_of_constr : constr -> Univ.LSet.t
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:53:34 +0000