aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cClosure.ml17
-rw-r--r--kernel/cClosure.mli2
-rw-r--r--kernel/constr.ml72
-rw-r--r--kernel/constr.mli11
-rw-r--r--kernel/cooking.ml9
-rw-r--r--kernel/cooking.mli1
-rw-r--r--kernel/declarations.ml29
-rw-r--r--kernel/declareops.ml12
-rw-r--r--kernel/dune2
-rw-r--r--kernel/environ.ml16
-rw-r--r--kernel/environ.mli7
-rw-r--r--kernel/indtypes.ml10
-rw-r--r--kernel/indtypes.mli5
-rw-r--r--kernel/modops.ml3
-rw-r--r--kernel/reduction.ml4
-rw-r--r--kernel/safe_typing.ml23
-rw-r--r--kernel/safe_typing.mli1
-rw-r--r--kernel/term_typing.ml27
-rw-r--r--kernel/typeops.ml51
-rw-r--r--kernel/uGraph.ml17
-rw-r--r--kernel/uGraph.mli7
-rw-r--r--kernel/vars.ml17
22 files changed, 233 insertions, 110 deletions
diff --git a/kernel/cClosure.ml b/kernel/cClosure.ml
index 7e73609996..1f61bcae2e 100644
--- a/kernel/cClosure.ml
+++ b/kernel/cClosure.ml
@@ -300,7 +300,7 @@ and fterm =
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
- | FProd of Name.t * fconstr * fconstr
+ | FProd of Name.t * fconstr * constr * fconstr subs
| FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FLIFT of int * fconstr
@@ -584,9 +584,12 @@ let rec to_constr lfts v =
let tys = List.mapi (fun i (na, c) -> na, subst_constr (subs_liftn i subs) c) tys in
let f = subst_constr (subs_liftn len subs) f in
Term.compose_lam (List.rev tys) f
- | FProd (n,t,c) ->
- mkProd (n, to_constr lfts t,
- to_constr (el_lift lfts) c)
+ | FProd (n, t, c, e) ->
+ if is_subs_id e && is_lift_id lfts then
+ mkProd (n, to_constr lfts t, c)
+ else
+ let subs' = comp_subs lfts e in
+ mkProd (n, to_constr lfts t, subst_constr (subs_lift subs') c)
| FLetIn (n,b,t,f,e) ->
let subs = comp_subs (el_lift lfts) (subs_lift e) in
mkLetIn (n, to_constr lfts b,
@@ -869,7 +872,7 @@ and knht info e t stk =
| CoFix cfx -> { norm = Cstr; term = FCoFix (cfx,e) }, stk
| Lambda _ -> { norm = Cstr; term = mk_lambda e t }, stk
| Prod (n, t, c) ->
- { norm = Whnf; term = FProd (n, mk_clos e t, mk_clos (subs_lift e) c) }, stk
+ { norm = Whnf; term = FProd (n, mk_clos e t, c, e) }, stk
| LetIn (n,b,t,c) ->
{ norm = Red; term = FLetIn (n, mk_clos e b, mk_clos e t, c, e) }, stk
| Evar ev -> { norm = Red; term = FEvar (ev, e) }, stk
@@ -992,8 +995,8 @@ and norm_head info tab m =
| FLetIn(na,a,b,f,e) ->
let c = mk_clos (subs_lift e) f in
mkLetIn(na, kl info tab a, kl info tab b, kl info tab c)
- | FProd(na,dom,rng) ->
- mkProd(na, kl info tab dom, kl info tab rng)
+ | FProd(na,dom,rng,e) ->
+ mkProd(na, kl info tab dom, kl info tab (mk_clos (subs_lift e) rng))
| FCoFix((n,(na,tys,bds)),e) ->
let ftys = Array.Fun1.map mk_clos e tys in
let fbds =
diff --git a/kernel/cClosure.mli b/kernel/cClosure.mli
index b6c87b3732..c2d53eed47 100644
--- a/kernel/cClosure.mli
+++ b/kernel/cClosure.mli
@@ -114,7 +114,7 @@ type fterm =
| FCoFix of cofixpoint * fconstr subs
| FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
| FLambda of int * (Name.t * constr) list * constr * fconstr subs
- | FProd of Name.t * fconstr * fconstr
+ | FProd of Name.t * fconstr * constr * fconstr subs
| FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
| FEvar of existential * fconstr subs
| FLIFT of int * fconstr
diff --git a/kernel/constr.ml b/kernel/constr.ml
index 704e6de6b8..8e5d15dd2d 100644
--- a/kernel/constr.ml
+++ b/kernel/constr.ml
@@ -452,27 +452,6 @@ let fold f acc c = match kind c with
| CoFix (_,(_lna,tl,bl)) ->
Array.fold_left2 (fun acc t b -> f (f acc t) b) acc tl bl
-let fold_with_full_binders g f n acc c =
- let open Context.Rel.Declaration in
- match kind c with
- | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
- | Cast (c,_, t) -> f n (f n acc c) t
- | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
- | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
- | App (c,l) -> Array.fold_left (f n) (f n acc c) l
- | Proj (_,c) -> f n acc c
- | Evar (_,l) -> Array.fold_left (f n) acc l
- | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
- | Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
- let fd = Array.map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
- | CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c n t -> g (LocalAssum (n,t)) c) n lna tl in
- let fd = Array.map2 (fun t b -> (t,b)) tl bl in
- Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
-
(* [iter f c] iters [f] on the immediate subterms of [c]; it is
not recursive and the order with which subterms are processed is
not specified *)
@@ -534,12 +513,12 @@ let fold_constr_with_binders g f n acc c =
| Proj (_p,c) -> f n acc c
| Evar (_,l) -> Array.fold_left (f n) acc l
| Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
- | Fix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
+ | Fix (_,(_,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
- | CoFix (_,(lna,tl,bl)) ->
- let n' = CArray.fold_left2 (fun c _n _t -> g c) n lna tl in
+ | CoFix (_,(_,tl,bl)) ->
+ let n' = iterate g (Array.length tl) n in
let fd = Array.map2 (fun t b -> (t,b)) tl bl in
Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
@@ -799,6 +778,49 @@ let map_with_binders g f l c0 = match kind c0 with
let bl' = Array.Fun1.Smart.map f l' bl in
mkCoFix (ln,(lna,tl',bl'))
+(*********************)
+(* Lifting *)
+(*********************)
+
+(* The generic lifting function *)
+let rec exliftn el c =
+ let open Esubst in
+ match kind c with
+ | Rel i -> mkRel(reloc_rel i el)
+ | _ -> map_with_binders el_lift exliftn el c
+
+(* Lifting the binding depth across k bindings *)
+
+let liftn n k c =
+ let open Esubst in
+ match el_liftn (pred k) (el_shft n el_id) with
+ | ELID -> c
+ | el -> exliftn el c
+
+let lift n = liftn n 1
+
+let fold_with_full_binders g f n acc c =
+ let open Context.Rel.Declaration in
+ match kind c with
+ | Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ | Construct _ -> acc
+ | Cast (c,_, t) -> f n (f n acc c) t
+ | Prod (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | Lambda (na,t,c) -> f (g (LocalAssum (na,t)) n) (f n acc t) c
+ | LetIn (na,b,t,c) -> f (g (LocalDef (na,b,t)) n) (f n (f n acc b) t) c
+ | App (c,l) -> Array.fold_left (f n) (f n acc c) l
+ | Proj (_,c) -> f n acc c
+ | Evar (_,l) -> Array.fold_left (f n) acc l
+ | Case (_,p,c,bl) -> Array.fold_left (f n) (f n (f n acc p) c) bl
+ | Fix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+ | CoFix (_,(lna,tl,bl)) ->
+ let n' = CArray.fold_left2_i (fun i c n t -> g (LocalAssum (n,lift i t)) c) n lna tl in
+ let fd = Array.map2 (fun t b -> (t,b)) tl bl in
+ Array.fold_left (fun acc (t,b) -> f n' (f n acc t) b) acc fd
+
+
type 'univs instance_compare_fn = GlobRef.t -> int ->
'univs -> 'univs -> bool
diff --git a/kernel/constr.mli b/kernel/constr.mli
index 1be1f63ff7..f2cedcdabb 100644
--- a/kernel/constr.mli
+++ b/kernel/constr.mli
@@ -383,6 +383,17 @@ type rel_context = rel_declaration list
type named_context = named_declaration list
type compacted_context = compacted_declaration list
+(** {6 Relocation and substitution } *)
+
+(** [exliftn el c] lifts [c] with lifting [el] *)
+val exliftn : Esubst.lift -> constr -> constr
+
+(** [liftn n k c] lifts by [n] indexes above or equal to [k] in [c] *)
+val liftn : int -> int -> constr -> constr
+
+(** [lift n c] lifts by [n] the positive indexes in [c] *)
+val lift : int -> constr -> constr
+
(** {6 Functionals working on expressions canonically abstracted over
a local context (possibly with let-ins)} *)
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index b39aed01e8..f4b4834d98 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -158,6 +158,7 @@ type result = {
cook_body : constant_def;
cook_type : types;
cook_universes : constant_universes;
+ cook_private_univs : Univ.ContextSet.t option;
cook_inline : inline;
cook_context : Constr.named_context option;
}
@@ -204,7 +205,8 @@ let lift_univs cb subst auctx0 =
else
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
+ let substf = Univ.make_instance_subst subst in
+ let auctx' = Univ.subst_univs_level_abstract_universe_context substf auctx in
subst, (Polymorphic_const (AUContext.union auctx0 auctx'))
let cook_constant ~hcons { from = cb; info } =
@@ -229,10 +231,15 @@ let cook_constant ~hcons { from = cb; info } =
hyps)
hyps0 ~init:cb.const_hyps in
let typ = abstract_constant_type (expmod cb.const_type) hyps in
+ let private_univs = Option.map (on_snd (Univ.subst_univs_level_constraints
+ (Univ.make_instance_subst usubst)))
+ cb.const_private_poly_univs
+ in
{
cook_body = body;
cook_type = typ;
cook_universes = univs;
+ cook_private_univs = private_univs;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
}
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 6ebe691b83..7ff4b657d3 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,6 +21,7 @@ type result = {
cook_body : constant_def;
cook_type : types;
cook_universes : constant_universes;
+ cook_private_univs : Univ.ContextSet.t option;
cook_inline : inline;
cook_context : Constr.named_context option;
}
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index c1b38b4156..016b63be09 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -61,13 +61,27 @@ type constant_universes =
of a constant are tracked in their {!constant_body} so that they
can be displayed to the user. *)
type typing_flags = {
- check_guarded : bool; (** If [false] then fixed points and co-fixed
- points are assumed to be total. *)
- check_universes : bool; (** If [false] universe constraints are not checked *)
- conv_oracle : Conv_oracle.oracle; (** Unfolding strategies for conversion *)
- share_reduction : bool; (** Use by-need reduction algorithm *)
- enable_VM : bool; (** If [false], all VM conversions fall back to interpreted ones *)
- enable_native_compiler : bool; (** If [false], all native conversions fall back to VM ones *)
+ check_guarded : bool;
+ (** If [false] then fixed points and co-fixed points are assumed to
+ be total. *)
+
+ check_universes : bool;
+ (** If [false] universe constraints are not checked *)
+
+ conv_oracle : Conv_oracle.oracle;
+ (** Unfolding strategies for conversion *)
+
+ share_reduction : bool;
+ (** Use by-need reduction algorithm *)
+
+ enable_VM : bool;
+ (** If [false], all VM conversions fall back to interpreted ones *)
+
+ enable_native_compiler : bool;
+ (** If [false], all native conversions fall back to VM ones *)
+
+ indices_matter: bool;
+ (** The universe of an inductive type must be above that of its indices. *)
}
(* some contraints are in constant_constraints, some other may be in
@@ -78,6 +92,7 @@ type constant_body = {
const_type : types;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : constant_universes;
+ const_private_poly_univs : Univ.ContextSet.t option;
const_inline_code : bool;
const_typing_flags : typing_flags; (** The typing options which
were used for
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 3ed599c538..707c46048b 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -24,6 +24,7 @@ let safe_flags oracle = {
share_reduction = true;
enable_VM = true;
enable_native_compiler = true;
+ indices_matter = true;
}
(** {6 Arities } *)
@@ -101,6 +102,7 @@ let subst_const_body sub cb =
const_body_code =
Option.map (Cemitcodes.subst_to_patch_subst sub) cb.const_body_code;
const_universes = cb.const_universes;
+ const_private_poly_univs = cb.const_private_poly_univs;
const_inline_code = cb.const_inline_code;
const_typing_flags = cb.const_typing_flags }
@@ -126,14 +128,20 @@ let hcons_const_universes cbu =
match cbu with
| Monomorphic_const ctx ->
Monomorphic_const (Univ.hcons_universe_context_set ctx)
- | Polymorphic_const ctx ->
+ | Polymorphic_const ctx ->
Polymorphic_const (Univ.hcons_abstract_universe_context ctx)
+let hcons_const_private_univs = function
+ | None -> None
+ | Some univs -> Some (Univ.hcons_universe_context_set univs)
+
let hcons_const_body cb =
{ cb with
const_body = hcons_const_def cb.const_body;
const_type = Constr.hcons cb.const_type;
- const_universes = hcons_const_universes cb.const_universes }
+ const_universes = hcons_const_universes cb.const_universes;
+ const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
+ }
(** {6 Inductive types } *)
diff --git a/kernel/dune b/kernel/dune
index a503238907..4f2e0e4e28 100644
--- a/kernel/dune
+++ b/kernel/dune
@@ -4,7 +4,7 @@
(public_name coq.kernel)
(wrapped false)
(modules_without_implementation cinstr nativeinstr)
- (libraries clib config lib byterun))
+ (libraries lib byterun))
(rule
(targets copcodes.ml)
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 019c0a6819..38a428d9a1 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -241,6 +241,8 @@ let is_impredicative_set env =
let type_in_type env = not (typing_flags env).check_universes
let deactivated_guard env = not (typing_flags env).check_guarded
+let indices_matter env = env.env_typing_flags.indices_matter
+
let universes env = env.env_stratification.env_universes
let named_context env = env.env_named_context.env_named_ctx
let named_context_val env = env.env_named_context
@@ -380,6 +382,18 @@ let add_universes_set strict ctx g =
let push_context_set ?(strict=false) ctx env =
map_universes (add_universes_set strict ctx) env
+let push_subgraph (levels,csts) env =
+ let add_subgraph g =
+ let newg = Univ.LSet.fold (fun v g -> UGraph.add_universe v false g) levels g in
+ let newg = UGraph.merge_constraints csts newg in
+ (if not (Univ.Constraint.is_empty csts) then
+ let restricted = UGraph.constraints_for ~kept:(UGraph.domain g) newg in
+ (if not (UGraph.check_constraints restricted g) then
+ CErrors.anomaly Pp.(str "Local constraints imply new transitive constraints.")));
+ newg
+ in
+ map_universes add_subgraph env
+
let set_engagement c env = (* Unsafe *)
{ env with env_stratification =
{ env.env_stratification with env_engagement = c } }
@@ -389,6 +403,7 @@ let same_flags {
check_guarded;
check_universes;
conv_oracle;
+ indices_matter;
share_reduction;
enable_VM;
enable_native_compiler;
@@ -396,6 +411,7 @@ let same_flags {
check_guarded == alt.check_guarded &&
check_universes == alt.check_universes &&
conv_oracle == alt.conv_oracle &&
+ indices_matter == alt.indices_matter &&
share_reduction == alt.share_reduction &&
enable_VM == alt.enable_VM &&
enable_native_compiler == alt.enable_native_compiler
diff --git a/kernel/environ.mli b/kernel/environ.mli
index c285f907fc..8a2efb2477 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -96,6 +96,7 @@ val typing_flags : env -> typing_flags
val is_impredicative_set : env -> bool
val type_in_type : env -> bool
val deactivated_guard : env -> bool
+val indices_matter : env -> bool
(** is the local context empty *)
val empty_context : env -> bool
@@ -268,6 +269,12 @@ val push_context : ?strict:bool -> Univ.UContext.t -> env -> env
val push_context_set : ?strict:bool -> Univ.ContextSet.t -> env -> env
val push_constraints_to_env : 'a Univ.constrained -> env -> env
+val push_subgraph : Univ.ContextSet.t -> env -> env
+(** [push_subgraph univs env] adds the universes and constraints in
+ [univs] to [env] as [push_context_set ~strict:false univs env], and
+ also checks that they do not imply new transitive constraints
+ between pre-existing universes in [env]. *)
+
val set_engagement : engagement -> env -> env
val set_typing_flags : typing_flags -> env -> env
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml
index 20c90bc05a..a4a02791b4 100644
--- a/kernel/indtypes.ml
+++ b/kernel/indtypes.ml
@@ -35,14 +35,6 @@ env_ar_par = env_ar + declaration of parameters
nmr = ongoing computation of recursive parameters
*)
-(* Tell if indices (aka real arguments) contribute to size of inductive type *)
-(* If yes, this is compatible with the univalent model *)
-
-let indices_matter = ref false
-
-let enforce_indices_matter () = indices_matter := true
-let is_indices_matter () = !indices_matter
-
(* [weaker_noccur_between env n nvars t] (defined above), checks that
no de Bruijn indices between [n] and [n+nvars] occur in [t]. If
some such occurrences are found, then reduction is performed
@@ -303,7 +295,7 @@ let typecheck_inductive env mie =
let inflev =
(* The level of the inductive includes levels of indices if
in indices_matter mode *)
- if !indices_matter
+ if indices_matter env
then Some (cumulate_arity_large_levels env_params sign)
else None
in
diff --git a/kernel/indtypes.mli b/kernel/indtypes.mli
index a827c17683..840e23ed69 100644
--- a/kernel/indtypes.mli
+++ b/kernel/indtypes.mli
@@ -50,8 +50,3 @@ val check_positivity : chkpos:bool ->
(** The following function does checks on inductive declarations. *)
val check_inductive : env -> MutInd.t -> mutual_inductive_entry -> mutual_inductive_body
-
-(** The following enforces a system compatible with the univalent model *)
-
-val enforce_indices_matter : unit -> unit
-val is_indices_matter : unit -> bool
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 0dde1c7e75..f43dbd88f9 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -338,7 +338,8 @@ let strengthen_const mp_from l cb resolver =
| Polymorphic_const ctx -> Univ.make_abstract_instance ctx
in
{ cb with
- const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+ const_body = Def (Mod_subst.from_val (mkConstU (con,u)));
+ const_private_poly_univs = None;
const_body_code = Some (Cemitcodes.from_val (Cbytegen.compile_alias con)) }
let rec strengthen_mod mp_from mp_to mb =
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index fbb481424f..97cd4c00d7 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -438,14 +438,14 @@ and eqappr cv_pb l2r infos (lft1,st1) (lft2,st2) cuniv =
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
- | (FProd (_,c1,c2), FProd (_,c'1,c'2)) ->
+ | (FProd (_, c1, c2, e), FProd (_, c'1, c'2, e')) ->
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 el1 = el_stack lft1 v1 in
let el2 = el_stack lft2 v2 in
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
+ ccnv cv_pb l2r infos (el_lift el1) (el_lift el2) (mk_clos (subs_lift e) c2) (mk_clos (subs_lift e') c'2) cuniv
(* Eta-expansion on the fly *)
| (FLambda _, _) ->
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 2464df799e..df9e253135 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -196,6 +196,9 @@ let set_typing_flags c senv =
if env == senv.env then senv
else { senv with env }
+let set_indices_matter indices_matter senv =
+ set_typing_flags { (Environ.typing_flags senv.env) with indices_matter } senv
+
let set_share_reduction b senv =
let flags = Environ.typing_flags senv.env in
set_typing_flags { flags with share_reduction = b } senv
@@ -498,7 +501,7 @@ type generic_name =
| M (** name already known, cf the mod_mp field *)
| MT (** name already known, cf the mod_mp field *)
-let add_field ((l,sfb) as field) gn senv =
+let add_field ?(is_include=false) ((l,sfb) as field) gn senv =
let mlabs,olabs = match sfb with
| SFBmind mib ->
let l = labels_of_mib mib in
@@ -508,8 +511,18 @@ let add_field ((l,sfb) as field) gn senv =
| SFBmodule _ | SFBmodtype _ ->
check_modlabel l senv; (Label.Set.singleton l, Label.Set.empty)
in
- let cst = constraints_of_sfb senv.env sfb in
- let senv = add_constraints_list cst senv in
+ let senv =
+ if is_include then
+ (* Universes and constraints were added when the included module
+ was defined eg in [Include F X.] (one of the trickier
+ versions of Include) the constraints on the fields are
+ exactly those of the fields of F which was defined
+ separately. *)
+ senv
+ else
+ let cst = constraints_of_sfb senv.env sfb in
+ add_constraints_list cst senv
+ in
let env' = match sfb, gn with
| SFBconst cb, C con -> Environ.add_constant con cb senv.env
| SFBmind mib, I mind -> Environ.add_mind mind mib senv.env
@@ -599,7 +612,7 @@ let inline_side_effects env body side_eff =
let subst = Cmap_env.add c (Inr var) subst in
let ctx = Univ.ContextSet.union ctx univs in
(subst, var + 1, ctx, (cname c, b, ty, opaque) :: args)
- | Polymorphic_const _auctx ->
+ | Polymorphic_const _ ->
(** Inline the term to emulate universe polymorphism *)
let subst = Cmap_env.add c (Inl b) subst in
(subst, var, ctx, args)
@@ -1049,7 +1062,7 @@ let add_include me is_module inl senv =
| SFBmodule _ -> M
| SFBmodtype _ -> MT
in
- add_field field new_name senv
+ add_field ~is_include:true field new_name senv
in
resolver, List.fold_left add senv str
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index 7af773e3bc..57b01f15e3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -136,6 +136,7 @@ val add_constraints :
(** Setting the type theory flavor *)
val set_engagement : Declarations.engagement -> safe_transformer0
+val set_indices_matter : bool -> safe_transformer0
val set_typing_flags : Declarations.typing_flags -> safe_transformer0
val set_share_reduction : bool -> safe_transformer0
val set_VM : bool -> safe_transformer0
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 35fa871b4e..f9fdbdd68e 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -88,6 +88,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
Cooking.cook_body = Undef nl;
cook_type = t;
cook_universes = univs;
+ cook_private_univs = None;
cook_inline = false;
cook_context = ctx;
}
@@ -130,6 +131,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
Cooking.cook_body = def;
cook_type = typ;
cook_universes = Monomorphic_const univs;
+ cook_private_univs = None;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
@@ -145,24 +147,25 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let body, ctx', _ = handle env body side_eff in
body, Univ.ContextSet.union ctx ctx'
in
- let env, usubst, univs = match c.const_entry_universes with
+ let env, usubst, univs, private_univs = match c.const_entry_universes with
| Monomorphic_const_entry univs ->
let ctx = Univ.ContextSet.union univs ctx in
let env = push_context_set ~strict:true ctx env in
- env, Univ.empty_level_subst, Monomorphic_const ctx
+ env, Univ.empty_level_subst, Monomorphic_const ctx, None
| Polymorphic_const_entry (nas, uctx) ->
- (** Ensure not to generate internal constraints in polymorphic mode.
- The only way for this to happen would be that either the body
- contained deferred universes, or that it contains monomorphic
- side-effects. The first property is ruled out by upper layers,
- and the second one is ensured by the fact we currently
- unconditionally export side-effects from polymorphic definitions,
- i.e. [trust] is always [Pure]. *)
- let () = assert (Univ.ContextSet.is_empty ctx) in
+ (** [ctx] must contain local universes, such that it has no impact
+ on the rest of the graph (up to transitivity). *)
let env = push_context ~strict:false uctx env in
let sbst, auctx = Univ.abstract_universes nas uctx in
let sbst = Univ.make_instance_subst sbst in
- env, sbst, Polymorphic_const auctx
+ let env, local =
+ if opaque then
+ push_subgraph ctx env, Some (on_snd (Univ.subst_univs_level_constraints sbst) ctx)
+ else
+ if Univ.ContextSet.is_empty ctx then env, None
+ else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+ in
+ env, sbst, Polymorphic_const auctx, local
in
let j = infer env body in
let typ = match typ with
@@ -183,6 +186,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
Cooking.cook_body = def;
cook_type = typ;
cook_universes = univs;
+ cook_private_univs = private_univs;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
}
@@ -277,6 +281,7 @@ let build_constant_declaration _kn env result =
const_type = typ;
const_body_code = tps;
const_universes = univs;
+ const_private_poly_univs = result.cook_private_univs;
const_inline_code = result.cook_inline;
const_typing_flags = Environ.typing_flags env }
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index c8fd83c8a9..c9acd168e8 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -151,28 +151,41 @@ let type_of_abstraction _env name var ty =
let make_judgev c t =
Array.map2 make_judge c t
+let rec check_empty_stack = function
+| [] -> true
+| CClosure.Zupdate _ :: s -> check_empty_stack s
+| _ -> false
+
let type_of_apply env func funt argsv argstv =
+ let open CClosure in
let len = Array.length argsv in
- let rec apply_rec i typ =
- if Int.equal i len then typ
- else
- (match kind (whd_all env typ) with
- | Prod (_,c1,c2) ->
- let arg = argsv.(i) and argt = argstv.(i) in
- (try
- let () = conv_leq false env argt c1 in
- apply_rec (i+1) (subst1 arg c2)
- with NotConvertible ->
- error_cant_apply_bad_type env
- (i+1,c1,argt)
- (make_judge func funt)
- (make_judgev argsv argstv))
-
+ let infos = create_clos_infos all env in
+ let tab = create_tab () in
+ let rec apply_rec i typ =
+ if Int.equal i len then term_of_fconstr typ
+ else
+ let typ, stk = whd_stack infos tab typ [] in
+ (** The return stack is known to be empty *)
+ let () = assert (check_empty_stack stk) in
+ match fterm_of typ with
+ | FProd (_, c1, c2, e) ->
+ let arg = argsv.(i) in
+ let argt = argstv.(i) in
+ let c1 = term_of_fconstr c1 in
+ begin match conv_leq false env argt c1 with
+ | () -> apply_rec (i+1) (mk_clos (Esubst.subs_cons ([| inject arg |], e)) c2)
+ | exception NotConvertible ->
+ error_cant_apply_bad_type env
+ (i+1,c1,argt)
+ (make_judge func funt)
+ (make_judgev argsv argstv)
+ end
| _ ->
- error_cant_apply_not_functional env
- (make_judge func funt)
- (make_judgev argsv argstv))
- in apply_rec 0 funt
+ error_cant_apply_not_functional env
+ (make_judge func funt)
+ (make_judgev argsv argstv)
+ in
+ apply_rec 0 (inject funt)
(* Type of product *)
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml
index 9083156745..afdc8f1511 100644
--- a/kernel/uGraph.ml
+++ b/kernel/uGraph.ml
@@ -866,6 +866,23 @@ let constraints_for ~kept g =
arc.ltle csts)
kept csts
+let domain g = LMap.domain g.entries
+
+let choose p g u =
+ let exception Found of Level.t in
+ let ru = (repr g u).univ in
+ if p ru then Some ru
+ else
+ try LMap.iter (fun v -> function
+ | Canonical _ -> () (* we already tried [p ru] *)
+ | Equiv v' ->
+ let rv = (repr g v').univ in
+ if rv == ru && p v then raise (Found v)
+ (* NB: we could also try [p v'] but it will come up in the
+ rest of the iteration regardless. *)
+ ) g.entries; None
+ with Found v -> Some v
+
(** [sort_universes g] builds a totally ordered universe graph. The
output graph should imply the input graph (and the implication
will be strict most of the time), but is not necessarily minimal.
diff --git a/kernel/uGraph.mli b/kernel/uGraph.mli
index a2cc5b3116..4dbfac5c73 100644
--- a/kernel/uGraph.mli
+++ b/kernel/uGraph.mli
@@ -73,12 +73,19 @@ val sort_universes : t -> t
of the universes into equivalence classes. *)
val constraints_of_universes : t -> Constraint.t * LSet.t list
+val choose : (Level.t -> bool) -> t -> Level.t -> Level.t option
+(** [choose p g u] picks a universe verifying [p] and equal
+ to [u] in [g]. *)
+
(** [constraints_for ~kept g] returns the constraints about the
universes [kept] in [g] up to transitivity.
eg if [g] is [a <= b <= c] then [constraints_for ~kept:{a, c} g] is [a <= c]. *)
val constraints_for : kept:LSet.t -> t -> Constraint.t
+val domain : t -> LSet.t
+(** Known universes *)
+
val check_subtype : AUContext.t check_function
(** [check_subtype univ ctx1 ctx2] checks whether [ctx2] is an instance of
[ctx1]. *)
diff --git a/kernel/vars.ml b/kernel/vars.ml
index 7380a860dd..f9c576ca4a 100644
--- a/kernel/vars.ml
+++ b/kernel/vars.ml
@@ -9,7 +9,6 @@
(************************************************************************)
open Names
-open Esubst
module RelDecl = Context.Rel.Declaration
@@ -80,19 +79,9 @@ let noccur_with_meta n m term =
(* Lifting *)
(*********************)
-(* The generic lifting function *)
-let rec exliftn el c = match Constr.kind c with
- | Constr.Rel i -> Constr.mkRel(reloc_rel i el)
- | _ -> Constr.map_with_binders el_lift exliftn el c
-
-(* Lifting the binding depth across k bindings *)
-
-let liftn n k c =
- match el_liftn (pred k) (el_shft n el_id) with
- | ELID -> c
- | el -> exliftn el c
-
-let lift n = liftn n 1
+let exliftn = Constr.exliftn
+let liftn = Constr.liftn
+let lift = Constr.lift
(*********************)
(* Substituting *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 02:36:45 +0000