aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/values.ml4
-rw-r--r--interp/notation_ops.ml6
-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
-rw-r--r--library/globnames.ml20
-rw-r--r--library/globnames.mli4
-rw-r--r--pretyping/classops.ml8
-rw-r--r--pretyping/detyping.ml11
-rw-r--r--pretyping/heads.ml17
-rw-r--r--pretyping/patternops.ml10
-rw-r--r--pretyping/recordops.ml8
-rw-r--r--tactics/hints.ml12
18 files changed, 106 insertions, 77 deletions
diff --git a/checker/values.ml b/checker/values.ml
index dcb2bca81a..574019c06d 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -168,8 +168,10 @@ let v_section_ctxt = v_enum "emptylist" 1
(** kernel/mod_subst *)
+let v_univ_abstracted v = v_tuple "univ_abstracted" [|v;v_abs_context|]
+
let v_delta_hint =
- v_sum "delta_hint" 0 [|[|Int; Opt (v_pair v_abs_context v_constr)|];[|v_kn|]|]
+ v_sum "delta_hint" 0 [|[|Int; Opt (v_univ_abstracted v_constr)|];[|v_kn|]|]
let v_resolver =
v_tuple "delta_resolver"
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index 7a525f84a5..b41160f758 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -530,8 +530,10 @@ let rec subst_notation_constr subst bound raw =
match raw with
| NRef ref ->
let ref',t = subst_global subst ref in
- if ref' == ref then raw else
- fst (notation_constr_of_constr bound t)
+ if ref' == ref then raw else (match t with
+ | None -> NRef ref'
+ | Some t ->
+ fst (notation_constr_of_constr bound t.Univ.univ_abstracted_value))
| NVar _ -> raw
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 2b3b4f9486..1690bd7c70 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -963,6 +963,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 de7b334ae4..760ccbab04 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -349,6 +349,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
diff --git a/library/globnames.ml b/library/globnames.ml
index 9aca7788d2..db2e8bfaed 100644
--- a/library/globnames.ml
+++ b/library/globnames.ml
@@ -31,8 +31,8 @@ let destConstructRef = function ConstructRef ind -> ind | _ -> failwith "destCon
let subst_constructor subst (ind,j as ref) =
let ind' = subst_ind subst ind in
- if ind==ind' then ref, mkConstruct ref
- else (ind',j), mkConstruct (ind',j)
+ if ind==ind' then ref
+ else (ind',j)
let subst_global_reference subst ref = match ref with
| VarRef var -> ref
@@ -43,20 +43,20 @@ let subst_global_reference subst ref = match ref with
let ind' = subst_ind subst ind in
if ind==ind' then ref else IndRef ind'
| ConstructRef ((kn,i),j as c) ->
- let c',t = subst_constructor subst c in
- if c'==c then ref else ConstructRef c'
+ let c' = subst_constructor subst c in
+ if c'==c then ref else ConstructRef c'
let subst_global subst ref = match ref with
- | VarRef var -> ref, mkVar var
+ | VarRef var -> ref, None
| ConstRef kn ->
- let kn',t = subst_con_kn subst kn in
- if kn==kn' then ref, mkConst kn else ConstRef kn', t
+ let kn',t = subst_con subst kn in
+ if kn==kn' then ref, None else ConstRef kn', t
| IndRef ind ->
let ind' = subst_ind subst ind in
- if ind==ind' then ref, mkInd ind else IndRef ind', mkInd ind'
+ if ind==ind' then ref, None else IndRef ind', None
| ConstructRef ((kn,i),j as c) ->
- let c',t = subst_constructor subst c in
- if c'==c then ref,t else ConstructRef c', t
+ let c' = subst_constructor subst c in
+ if c'==c then ref,None else ConstructRef c', None
let canonical_gr = function
| ConstRef con -> ConstRef(Constant.make1 (Constant.canonical con))
diff --git a/library/globnames.mli b/library/globnames.mli
index a96a42ced2..d49ed453f5 100644
--- a/library/globnames.mli
+++ b/library/globnames.mli
@@ -36,8 +36,8 @@ val destConstructRef : GlobRef.t -> constructor
val is_global : GlobRef.t -> constr -> bool
-val subst_constructor : substitution -> constructor -> constructor * constr
-val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr
+val subst_constructor : substitution -> constructor -> constructor
+val subst_global : substitution -> GlobRef.t -> GlobRef.t * constr Univ.univ_abstracted option
val subst_global_reference : substitution -> GlobRef.t -> GlobRef.t
(** This constr is not safe to be typechecked, universe polymorphism is not
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index f18040accb..306a76e35e 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -192,9 +192,11 @@ let subst_cl_typ subst ct = match ct with
let c' = subst_proj_repr subst c in
if c' == c then ct else CL_PROJ c'
| CL_CONST c ->
- let c',t = subst_con_kn subst c in
- if c' == c then ct else
- pi1 (find_class_type Evd.empty (EConstr.of_constr t))
+ let c',t = subst_con subst c in
+ if c' == c then ct else (match t with
+ | None -> CL_CONST c'
+ | Some t ->
+ pi1 (find_class_type Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)))
| CL_IND i ->
let i' = subst_ind subst i in
if i' == i then ct else CL_IND i'
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 33ced6d6e0..bcfa2df56b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -933,10 +933,13 @@ let (f_subst_genarg, subst_genarg_hook) = Hook.make ()
let rec subst_glob_constr subst = DAst.map (function
| GRef (ref,u) as raw ->
let ref',t = subst_global subst ref in
- if ref' == ref then raw else
- let env = Global.env () in
- let evd = Evd.from_env env in
- DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t))
+ if ref' == ref then raw else (match t with
+ | None -> GRef (ref', u)
+ | Some t ->
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ let t = t.Univ.univ_abstracted_value in (* XXX This seems dangerous *)
+ DAst.get (detype Now false Id.Set.empty env evd (EConstr.of_constr t)))
| GSort _
| GVar _
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index e533930267..ccbb2934bc 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -147,13 +147,16 @@ let cache_head o =
let subst_head_approximation subst = function
| RigidHead (RigidParameter cst) as k ->
- let cst,c = subst_con_kn subst cst in
- if isConst c && Constant.equal (fst (destConst c)) cst then
- (* A change of the prefix of the constant *)
- k
- else
- (* A substitution of the constant by a functor argument *)
- kind_of_head (Global.env()) c
+ let cst',c = subst_con subst cst in
+ if cst == cst' then k
+ else
+ (match c with
+ | None ->
+ (* A change of the prefix of the constant *)
+ RigidHead (RigidParameter cst')
+ | Some c ->
+ (* A substitution of the constant by a functor argument *)
+ kind_of_head (Global.env()) c.Univ.univ_abstracted_value)
| x -> x
let subst_head (subst,(ref,k)) =
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3c1c470053..9c93f29e06 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -279,10 +279,12 @@ let rec subst_pattern subst pat =
match pat with
| PRef ref ->
let ref',t = subst_global subst ref in
- if ref' == ref then pat else
- let env = Global.env () in
- let evd = Evd.from_env env in
- pattern_of_constr env evd t
+ if ref' == ref then pat else (match t with
+ | None -> PRef ref'
+ | Some t ->
+ let env = Global.env () in
+ let evd = Evd.from_env env in
+ pattern_of_constr env evd t.Univ.univ_abstracted_value)
| PVar _
| PEvar _
| PRel _ -> pat
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index fe9b69dbbc..bc35bedd2c 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -71,12 +71,12 @@ let subst_structure (subst,((kn,i),id,kl,projs as obj)) =
(* invariant: struc.s_PROJ is an evaluable reference. Thus we can take *)
(* the first component of subst_con. *)
List.Smart.map
- (Option.Smart.map (fun kn -> fst (subst_con_kn subst kn)))
+ (Option.Smart.map (subst_constant subst))
projs
in
- let id' = fst (subst_constructor subst id) in
- if projs' == projs && kn' == kn && id' == id then obj else
- ((kn',i),id',kl,projs')
+ let id' = subst_constructor subst id in
+ if projs' == projs && kn' == kn && id' == id then obj else
+ ((kn',i),id',kl,projs')
let discharge_structure (_,x) = Some x
diff --git a/tactics/hints.ml b/tactics/hints.ml
index 77479f9efa..dc3b90211e 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1064,12 +1064,12 @@ let cache_autohint (kn, obj) =
let subst_autohint (subst, obj) =
let subst_key gr =
- let (lab'', elab') = subst_global subst gr in
- let elab' = EConstr.of_constr elab' in
- let gr' =
- (try head_constr_bound Evd.empty elab'
- with Bound -> lab'')
- in if gr' == gr then gr else gr'
+ let (gr', t) = subst_global subst gr in
+ match t with
+ | None -> gr'
+ | Some t ->
+ (try head_constr_bound Evd.empty (EConstr.of_constr t.Univ.univ_abstracted_value)
+ with Bound -> gr')
in
let subst_hint (k,data as hint) =
let k' = Option.Smart.map subst_key k in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:02:51 +0000