aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--interp/declare.ml21
-rw-r--r--kernel/entries.ml7
-rw-r--r--kernel/safe_typing.ml19
-rw-r--r--kernel/safe_typing.mli2
-rw-r--r--kernel/term_typing.ml50
-rw-r--r--kernel/term_typing.mli6
-rw-r--r--library/global.ml2
-rw-r--r--library/global.mli2
8 files changed, 65 insertions, 44 deletions
diff --git a/interp/declare.ml b/interp/declare.ml
index 8781c8719..5be07e09e 100644
--- a/interp/declare.ml
+++ b/interp/declare.ml
@@ -231,11 +231,24 @@ let cache_variable ((sp,_),o) =
| SectionLocalDef (de) ->
let (de, eff) = Global.export_private_constants ~in_section:true de in
let () = List.iter register_side_effect eff in
- let univs = Global.push_named_def (id,de) in
- let poly = match de.const_entry_universes with
- | Monomorphic_const_entry _ -> false
- | Polymorphic_const_entry _ -> true
+ (** The body should already have been forced upstream because it is a
+ section-local definition, but it's not enforced by typing *)
+ let (body, uctx), () = Future.force de.const_entry_body in
+ let poly, univs = match de.const_entry_universes with
+ | Monomorphic_const_entry uctx -> false, uctx
+ | Polymorphic_const_entry uctx -> true, Univ.ContextSet.of_context uctx
in
+ let univs = Univ.ContextSet.union uctx univs in
+ (** We must declare the universe constraints before type-checking the
+ term. *)
+ let () = Global.push_context_set (not poly) univs in
+ let se = {
+ secdef_body = body;
+ secdef_secctx = de.const_entry_secctx;
+ secdef_feedback = de.const_entry_feedback;
+ secdef_type = de.const_entry_type;
+ } in
+ let () = Global.push_named_def (id, se) in
Explicit, de.const_entry_opaque,
poly, univs in
Nametab.push (Nametab.Until 1) (restrict_path 0 sp) (VarRef id);
diff --git a/kernel/entries.ml b/kernel/entries.ml
index ca79de404..36b75668b 100644
--- a/kernel/entries.ml
+++ b/kernel/entries.ml
@@ -81,6 +81,13 @@ type 'a definition_entry = {
const_entry_opaque : bool;
const_entry_inline_code : bool }
+type section_def_entry = {
+ secdef_body : constr;
+ secdef_secctx : Context.Named.t option;
+ secdef_feedback : Stateid.t option;
+ secdef_type : types option;
+}
+
type inline = int option (* inlining level, None for no inlining *)
type parameter_entry =
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index fa984515a..93b8e278f 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -382,22 +382,9 @@ let safe_push_named d env =
let push_named_def (id,de) senv =
- let open Entries in
- let c,typ,univs = Term_typing.translate_local_def senv.env id de in
- let poly = match de.Entries.const_entry_universes with
- | Monomorphic_const_entry _ -> false
- | Polymorphic_const_entry _ -> true
- in
- let c, univs = match c with
- | Def c -> Mod_subst.force_constr c, univs
- | OpaqueDef o ->
- Opaqueproof.force_proof (Environ.opaque_tables senv.env) o,
- Univ.ContextSet.union univs
- (Opaqueproof.force_constraints (Environ.opaque_tables senv.env) o)
- | _ -> assert false in
- let senv' = push_context_set poly univs senv in
- let env'' = safe_push_named (LocalDef (id,c,typ)) senv'.env in
- univs, {senv' with env=env''}
+ let c, typ = Term_typing.translate_local_def senv.env id de in
+ let env'' = safe_push_named (LocalDef (id, c, typ)) senv.env in
+ { senv with env = env'' }
let push_named_assum ((id,t,poly),ctx) senv =
let senv' = push_context_set poly ctx senv in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index fbc398a2a..757b803a3 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -90,7 +90,7 @@ val push_named_assum :
(** Returns the full universe context necessary to typecheck the definition
(futures are forced) *)
val push_named_def :
- Id.t * unit Entries.definition_entry -> Univ.ContextSet.t safe_transformer
+ Id.t * Entries.section_def_entry -> safe_transformer0
(** Insertion of global axioms or definitions *)
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 761eab511..2e4426d62 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -227,17 +227,14 @@ let feedback_completion_typecheck =
Option.iter (fun state_id ->
feedback ~id:state_id Feedback.Complete)
-let abstract_constant_universes abstract = function
+let abstract_constant_universes = function
| Monomorphic_const_entry uctx ->
Univ.empty_level_subst, Monomorphic_const uctx
| Polymorphic_const_entry uctx ->
- if not abstract then
- Univ.empty_level_subst, Monomorphic_const (Univ.ContextSet.of_context uctx)
- else
- let sbst, auctx = Univ.abstract_universes uctx in
- sbst, Polymorphic_const auctx
+ let sbst, auctx = Univ.abstract_universes uctx in
+ sbst, Polymorphic_const auctx
-let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry) =
+let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
match dcl with
| ParameterEntry (ctx,(t,uctx),nl) ->
let env = match uctx with
@@ -245,10 +242,7 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| Polymorphic_const_entry uctx -> push_context ~strict:false uctx env
in
let j = infer env t in
- let abstract = not (Option.is_empty kn) in
- let usubst, univs =
- abstract_constant_universes abstract uctx
- in
+ let usubst, univs = abstract_constant_universes uctx in
let c = Typeops.assumption_of_judgment env j in
let t = Constr.hcons (Vars.subst_univs_level_constr usubst c) in
{
@@ -316,12 +310,11 @@ let infer_declaration (type a) ~(trust : a trust) env kn (dcl : a constant_entry
| SideEffects _ -> inline_side_effects env body ctx side_eff
in
let env = push_context_set ~strict:(not poly) ctx env in
- let abstract = not (Option.is_empty kn) in
let ctx = if poly
then Polymorphic_const_entry (Univ.ContextSet.to_context ctx)
else Monomorphic_const_entry ctx
in
- let usubst, univs = abstract_constant_universes abstract ctx in
+ let usubst, univs = abstract_constant_universes ctx in
let j = infer env body in
let typ = match typ with
| None ->
@@ -493,7 +486,7 @@ let build_constant_declaration kn env result =
let translate_constant mb env kn ce =
build_constant_declaration kn env
- (infer_declaration ~trust:mb env (Some kn) ce)
+ (infer_declaration ~trust:mb env ce)
let constant_entry_of_side_effect cb u =
let univs =
@@ -607,7 +600,17 @@ let translate_recipe env kn r =
let translate_local_def env id centry =
let open Cooking in
- let decl = infer_declaration ~trust:Pure env None (DefinitionEntry centry) in
+ let body = Future.from_val ((centry.secdef_body, Univ.ContextSet.empty), ()) in
+ let centry = {
+ const_entry_body = body;
+ const_entry_secctx = centry.secdef_secctx;
+ const_entry_feedback = centry.secdef_feedback;
+ const_entry_type = centry.secdef_type;
+ const_entry_universes = Monomorphic_const_entry Univ.ContextSet.empty;
+ const_entry_opaque = false;
+ const_entry_inline_code = false;
+ } in
+ let decl = infer_declaration ~trust:Pure env (DefinitionEntry centry) in
let typ = decl.cook_type in
if Option.is_empty decl.cook_context && !Flags.record_aux_file then begin
match decl.cook_body with
@@ -619,11 +622,22 @@ let translate_local_def env id centry =
(Opaqueproof.force_proof (opaque_tables env) lc) in
record_aux env ids_typ ids_def
end;
- let univs = match decl.cook_universes with
- | Monomorphic_const ctx -> ctx
+ let () = match decl.cook_universes with
+ | Monomorphic_const ctx -> assert (Univ.ContextSet.is_empty ctx)
| Polymorphic_const _ -> assert false
in
- decl.cook_body, typ, univs
+ let c = match decl.cook_body with
+ | Def c -> Mod_subst.force_constr c
+ | OpaqueDef o ->
+ let p = Opaqueproof.force_proof (Environ.opaque_tables env) o in
+ let cst = Opaqueproof.force_constraints (Environ.opaque_tables env) o in
+ (** Let definitions are ensured to have no extra constraints coming from
+ the body by virtue of the typing of [Entries.section_def_entry]. *)
+ let () = assert (Univ.ContextSet.is_empty cst) in
+ p
+ | Undef _ -> assert false
+ in
+ c, typ
(* Insertion of inductive types. *)
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index c771452a1..7bc029010 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -18,8 +18,8 @@ type _ trust =
| Pure : unit trust
| SideEffects : structure_body -> side_effects trust
-val translate_local_def : env -> Id.t -> unit definition_entry ->
- constant_def * types * Univ.ContextSet.t
+val translate_local_def : env -> Id.t -> section_def_entry ->
+ constr * types
val translate_local_assum : env -> types -> types
@@ -72,7 +72,7 @@ val translate_recipe : env -> Constant.t -> Cooking.recipe -> constant_body
(** Internal functions, mentioned here for debug purpose only *)
-val infer_declaration : trust:'a trust -> env -> Constant.t option ->
+val infer_declaration : trust:'a trust -> env ->
'a constant_entry -> Cooking.result
val build_constant_declaration :
diff --git a/library/global.ml b/library/global.ml
index ce37dfecf..ed847b7cd 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -81,7 +81,7 @@ let globalize_with_summary fs f =
let i2l = Label.of_id
let push_named_assum a = globalize0 (Safe_typing.push_named_assum a)
-let push_named_def d = globalize (Safe_typing.push_named_def d)
+let push_named_def d = globalize0 (Safe_typing.push_named_def d)
let add_constraints c = globalize0 (Safe_typing.add_constraints c)
let push_context_set b c = globalize0 (Safe_typing.push_context_set b c)
let push_context b c = globalize0 (Safe_typing.push_context b c)
diff --git a/library/global.mli b/library/global.mli
index 2a646386e..03bc945da 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -32,7 +32,7 @@ val set_typing_flags : Declarations.typing_flags -> unit
(** Variables, Local definitions, constants, inductive types *)
val push_named_assum : (Id.t * Constr.types * bool) Univ.in_universe_context_set -> unit
-val push_named_def : (Id.t * unit Entries.definition_entry) -> Univ.ContextSet.t
+val push_named_def : (Id.t * Entries.section_def_entry) -> unit
val export_private_constants : in_section:bool ->
Safe_typing.private_constants Entries.definition_entry ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 10:07:03 +0000