aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/.merlin.in2
-rw-r--r--kernel/constr.ml4
-rw-r--r--kernel/indtypes.ml4
-rw-r--r--kernel/inductive.ml6
-rw-r--r--kernel/mod_subst.ml41
-rw-r--r--kernel/mod_subst.mli10
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/uGraph.ml2
-rw-r--r--kernel/univ.ml48
-rw-r--r--kernel/univ.mli29
-rw-r--r--kernel/vars.ml5
-rw-r--r--kernel/vars.mli3
12 files changed, 100 insertions, 57 deletions
diff --git a/kernel/.merlin.in b/kernel/.merlin.in
index 912ff61496..29da7d2cf6 100644
--- a/kernel/.merlin.in
+++ b/kernel/.merlin.in
@@ -1,4 +1,4 @@
-FLG -rectypes -thread -safe-string -w +a-4-44-50
+FLG -rectypes -thread -safe-string -w +a-4-44
S ../clib
B ../clib
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/indtypes.ml b/kernel/indtypes.ml
index a4a02791b4..68d44f8782 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -218,7 +218,9 @@ let check_subtyping_arity_constructor env (subst : constr -> constr) (arcn : typ
let check_subtyping cumi paramsctxt env_ar inds =
let numparams = Context.Rel.nhyps paramsctxt in
let uctx = CumulativityInfo.univ_context cumi in
- let new_levels = Array.init (UContext.size uctx) (Level.make DirPath.empty) in
+ let new_levels = Array.init (UContext.size uctx)
+ (fun i -> Level.make (Level.UGlobal.make DirPath.empty i))
+ in
let lmap = Array.fold_left2 (fun lmap u u' -> LMap.add u u' lmap)
LMap.empty (Instance.to_array @@ UContext.instance uctx) new_levels
in
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
index 9bbcf07f7e..05c5c0e821 100644
--- a/kernel/inductive.ml
+++ b/kernel/inductive.ml
@@ -593,10 +593,10 @@ let rec ienv_decompose_prod (env,_ as ienv) n c =
ienv_decompose_prod ienv' (n-1) b
| _ -> assert false
+let dummy_univ = Level.(make (UGlobal.make (DirPath.make [Id.of_string "implicit"]) 0))
+let dummy_implicit_sort = mkType (Universe.make dummy_univ)
let lambda_implicit_lift n a =
- let level = Level.make (DirPath.make [Id.of_string "implicit"]) 0 in
- let implicit_sort = mkType (Universe.make level) in
- let lambda_implicit a = mkLambda (Anonymous, implicit_sort, a) in
+ let lambda_implicit a = mkLambda (Anonymous, dummy_implicit_sort, a) in
iterate lambda_implicit n (lift n a)
(* This removes global parameters of the inductive types in lc (for
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/uGraph.ml b/kernel/uGraph.ml
index afdc8f1511..5fc8d0297f 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -921,7 +921,7 @@ let sort_universes g =
let types = Array.init (max_lvl + 1) (function
| 0 -> Level.prop
| 1 -> Level.set
- | n -> Level.make mp (n-2))
+ | n -> Level.make (Level.UGlobal.make mp (n-2)))
in
let g = Array.fold_left (fun g u ->
let g, u = safe_repr g u in
diff --git a/kernel/univ.ml b/kernel/univ.ml
index 2b3b4f9486..93a91af1d7 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -36,10 +36,26 @@ open Util
module RawLevel =
struct
open Names
+
+ module UGlobal = struct
+ type t = DirPath.t * int
+
+ let make dp i = (DirPath.hcons dp,i)
+
+ let equal (d, i) (d', i') = DirPath.equal d d' && Int.equal i i'
+
+ let hash (d,i) = Hashset.Combine.combine i (DirPath.hash d)
+
+ let compare (d, i) (d', i') =
+ let c = Int.compare i i' in
+ if Int.equal c 0 then DirPath.compare d d'
+ else c
+ end
+
type t =
| Prop
| Set
- | Level of int * DirPath.t
+ | Level of UGlobal.t
| Var of int
(* Hash-consing *)
@@ -49,8 +65,7 @@ struct
match x, y with
| Prop, Prop -> true
| Set, Set -> true
- | Level (n,d), Level (n',d') ->
- Int.equal n n' && DirPath.equal d d'
+ | Level l, Level l' -> UGlobal.equal l l'
| Var n, Var n' -> Int.equal n n'
| _ -> false
@@ -62,7 +77,7 @@ struct
| Set, Set -> 0
| Set, _ -> -1
| _, Set -> 1
- | Level (i1, dp1), Level (i2, dp2) ->
+ | Level (dp1, i1), Level (dp2, i2) ->
if i1 < i2 then -1
else if i1 > i2 then 1
else DirPath.compare dp1 dp2
@@ -83,9 +98,9 @@ struct
let hcons = function
| Prop as x -> x
| Set as x -> x
- | Level (n,d) as x ->
+ | Level (d,n) as x ->
let d' = Names.DirPath.hcons d in
- if d' == d then x else Level (n,d')
+ if d' == d then x else Level (d',n)
| Var _n as x -> x
open Hashset.Combine
@@ -94,18 +109,18 @@ struct
| Prop -> combinesmall 1 0
| Set -> combinesmall 1 1
| Var n -> combinesmall 2 n
- | Level (n, d) -> combinesmall 3 (combine n (Names.DirPath.hash d))
+ | Level (d, n) -> combinesmall 3 (combine n (Names.DirPath.hash d))
end
module Level = struct
- open Names
+ module UGlobal = RawLevel.UGlobal
type raw_level = RawLevel.t =
| Prop
| Set
- | Level of int * DirPath.t
+ | Level of UGlobal.t
| Var of int
(** Embed levels with their hash value *)
@@ -166,7 +181,7 @@ module Level = struct
match data x with
| Prop -> "Prop"
| Set -> "Set"
- | Level (n,d) -> Names.DirPath.to_string d^"."^string_of_int n
+ | Level (d,n) -> Names.DirPath.to_string d^"."^string_of_int n
| Var n -> "Var(" ^ string_of_int n ^ ")"
let pr u = str (to_string u)
@@ -185,11 +200,11 @@ module Level = struct
match data u with
| Var n -> Some n | _ -> None
- let make m n = make (Level (n, Names.DirPath.hcons m))
+ let make qid = make (Level qid)
let name u =
match data u with
- | Level (n, d) -> Some (d, n)
+ | Level (d, n) -> Some (d, n)
| _ -> None
end
@@ -963,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 de7b334ae4..8327ff1644 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -11,9 +11,22 @@
(** Universes. *)
module Level :
sig
+
+ module UGlobal : sig
+ type t
+
+ val make : Names.DirPath.t -> int -> t
+ val equal : t -> t -> bool
+ val hash : t -> int
+ val compare : t -> t -> int
+
+ end
+ (** Qualified global universe level *)
+
type t
(** Type of universe levels. A universe level is essentially a unique name
- that will be associated to constraints later on. *)
+ that will be associated to constraints later on. A level can be local to a
+ definition or global. *)
val set : t
val prop : t
@@ -34,9 +47,7 @@ sig
val hash : t -> int
- val make : Names.DirPath.t -> int -> t
- (** Create a new universe level from a unique identifier and an associated
- module path. *)
+ val make : UGlobal.t -> t
val pr : t -> Pp.t
(** Pretty-printing *)
@@ -48,7 +59,7 @@ sig
val var_index : t -> int option
- val name : t -> (Names.DirPath.t * int) option
+ val name : t -> UGlobal.t option
end
(** Sets of universe levels *)
@@ -349,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-05-01 08:37:45 +0000