aboutsummaryrefslogtreecommitdiff
path: root/kernel
diff options
context:
space:
mode:
Diffstat (limited to 'kernel')
-rw-r--r--kernel/cooking.ml18
-rw-r--r--kernel/cooking.mli4
-rw-r--r--kernel/declarations.ml1
-rw-r--r--kernel/declareops.ml6
-rw-r--r--kernel/modops.ml1
-rw-r--r--kernel/opaqueproof.ml64
-rw-r--r--kernel/opaqueproof.mli17
-rw-r--r--kernel/safe_typing.ml38
-rw-r--r--kernel/term_typing.ml40
9 files changed, 113 insertions, 76 deletions
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 1336e3e8bf..fbc0822570 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -159,7 +159,6 @@ type 'opaque result = {
cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
cook_type : types;
cook_universes : universes;
- cook_private_univs : Univ.ContextSet.t option;
cook_relevance : Sorts.relevance;
cook_inline : inline;
cook_context : Constr.named_context option;
@@ -202,7 +201,7 @@ let lift_univs cb subst auctx0 =
let subst, auctx = discharge_abstract_universe_context subst auctx0 auctx in
subst, (Polymorphic auctx)
-let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, (c, priv)) =
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
let ainst = Instance.of_array (Array.init univs Level.var) in
@@ -211,7 +210,15 @@ let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
let hyps = Context.Named.map expmod abstract in
let hyps = abstract_context hyps in
let c = abstract_constant_body (expmod c) hyps in
- univs + AUContext.size abs_ctx, c
+ let priv = match priv with
+ | Opaqueproof.PrivateMonomorphic () ->
+ let () = assert (AUContext.is_empty abs_ctx) in
+ priv
+ | Opaqueproof.PrivatePolymorphic ctx ->
+ let ctx = on_snd (Univ.subst_univs_level_constraints (Univ.make_instance_subst usubst)) ctx in
+ Opaqueproof.PrivatePolymorphic ctx
+ in
+ univs + AUContext.size abs_ctx, (c, priv)
let cook_constr infos univs c =
let fold info (univs, c) = cook_constr info (univs, c) in
@@ -240,15 +247,10 @@ let cook_constant { 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_relevance = cb.const_relevance;
cook_inline = cb.const_inline_code;
cook_context = Some const_hyps;
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 934b7c6b50..c98fb0bc3a 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,14 +21,14 @@ type 'opaque result = {
cook_body : (constr Mod_subst.substituted, 'opaque) constant_def;
cook_type : types;
cook_universes : universes;
- cook_private_univs : Univ.ContextSet.t option;
cook_relevance : Sorts.relevance;
cook_inline : inline;
cook_context : Constr.named_context option;
}
val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int ->
+ (constr * unit Opaqueproof.delayed_universes) -> (constr * unit Opaqueproof.delayed_universes)
val cook_inductive :
Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 388b4f14bf..deb01589b6 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -94,7 +94,6 @@ type 'opaque constant_body = {
const_relevance : Sorts.relevance;
const_body_code : Cemitcodes.to_patch_substituted option;
const_universes : 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 de9a052096..a8ebed2326 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -113,7 +113,6 @@ 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_relevance = cb.const_relevance;
const_inline_code = cb.const_inline_code;
const_typing_flags = cb.const_typing_flags }
@@ -144,16 +143,11 @@ let hcons_universes cbu =
| Polymorphic ctx ->
Polymorphic (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_universes cb.const_universes;
- const_private_poly_univs = hcons_const_private_univs cb.const_private_poly_univs;
}
(** {6 Inductive types } *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index 472fddb829..fcd88fd543 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -329,7 +329,6 @@ let strengthen_const mp_from l cb resolver =
let u = Univ.make_abstract_instance (Declareops.constant_polymorphic_context cb) in
{ cb with
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/opaqueproof.ml b/kernel/opaqueproof.ml
index e18b726111..66c50c4b57 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -20,13 +20,24 @@ type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
type indirect_accessor = {
- access_proof : DirPath.t -> int -> constr option;
- access_discharge : cooking_info list -> int -> constr -> constr;
+ access_proof : DirPath.t -> int -> opaque_proofterm;
+ access_discharge : cooking_info list -> int -> (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
}
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+let drop_mono = function
+| PrivateMonomorphic _ -> PrivateMonomorphic ()
+| PrivatePolymorphic _ as ctx -> ctx
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
type universes = int
+
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
| Direct of universes * cooking_info list * proofterm
@@ -59,7 +70,10 @@ let turn_indirect dp o tab = match o with
hashconsing of their contents, potentially as a future. *)
let hcons (c, u) =
let c = Constr.hcons c in
- let u = Univ.hcons_universe_context_set u in
+ let u = match u with
+ | PrivateMonomorphic u -> PrivateMonomorphic (Univ.hcons_universe_context_set u)
+ | PrivatePolymorphic u -> PrivatePolymorphic (Univ.hcons_universe_context_set u)
+ in
(c, u)
in
let cu = Future.chain cu hcons in
@@ -97,34 +111,42 @@ let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (n, d, cu) ->
- let (c, _) = Future.force cu in
- access.access_discharge d n c
+ let (c, u) = Future.force cu in
+ access.access_discharge d n (c, drop_mono u)
| Indirect (l,dp,i) ->
- let c =
+ let c, u =
if DirPath.equal dp odp
then
let (n, d, cu) = Int.Map.find i prfs in
- let (c, _) = Future.force cu in
- access.access_discharge d n c
- else match access.access_proof dp i with
- | None -> not_here ()
- | Some v -> v
+ let (c, u) = Future.force cu in
+ access.access_discharge d n (c, drop_mono u)
+ else
+ let (n, d, cu) = access.access_proof dp i in
+ match cu with
+ | None -> not_here ()
+ | Some (c, u) -> access.access_discharge n d (c, u)
in
- force_constr (List.fold_right subst_substituted l (from_val c))
+ let c = force_constr (List.fold_right subst_substituted l (from_val c)) in
+ (c, u)
+
+let get_mono (_, u) = match u with
+| PrivateMonomorphic ctx -> ctx
+| PrivatePolymorphic _ -> Univ.ContextSet.empty
let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
| Direct (_,_,cu) ->
- snd(Future.force cu)
+ get_mono (Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
then
let (_, _, cu) = Int.Map.find i prfs in
- snd (Future.force cu)
+ get_mono (Future.force cu)
else Univ.ContextSet.empty
let get_direct_constraints = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
-| Direct (_, _, cu) -> Future.chain cu snd
+| Direct (_, _, cu) ->
+ Future.chain cu get_mono
module FMap = Future.UUIDMap
@@ -136,8 +158,14 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
let c =
if Future.is_val cu then
- let (c, _) = Future.force cu in
- Some c
+ let (c, priv) = Future.force cu in
+ let priv = match priv with
+ | PrivateMonomorphic _ ->
+ let () = assert (Int.equal univs 0) in
+ PrivateMonomorphic ()
+ | PrivatePolymorphic _ as priv -> priv
+ in
+ Some (c, priv)
else if Future.UUIDSet.mem uid except then None
else
CErrors.anomaly
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 6e275649cd..20c862c651 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -21,7 +21,11 @@ open Mod_subst
When it is [turn_indirect] the data is relocated to an opaque table
and the [opaque] is turned into an index. *)
-type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type 'a delayed_universes =
+| PrivateMonomorphic of 'a
+| PrivatePolymorphic of Univ.ContextSet.t
+
+type proofterm = (constr * Univ.ContextSet.t delayed_universes) Future.computation
type opaquetab
type opaque
@@ -42,9 +46,12 @@ type cooking_info = {
modlist : work_list;
abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+type opaque_proofterm = cooking_info list * int * (Constr.t * unit delayed_universes) option
+
type indirect_accessor = {
- access_proof : DirPath.t -> int -> constr option;
- access_discharge : cooking_info list -> int -> constr -> constr;
+ access_proof : DirPath.t -> int -> opaque_proofterm;
+ access_discharge : cooking_info list -> int ->
+ (Constr.t * unit delayed_universes) -> (Constr.t * unit delayed_universes);
}
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The two functions above activate
@@ -53,7 +60,7 @@ type indirect_accessor = {
(** From a [opaque] back to a [constr]. This might use the
indirect opaque accessor given as an argument. *)
-val force_proof : indirect_accessor -> opaquetab -> opaque -> constr
+val force_proof : indirect_accessor -> opaquetab -> opaque -> constr * unit delayed_universes
val force_constraints : indirect_accessor -> opaquetab -> opaque -> Univ.ContextSet.t
val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
@@ -65,5 +72,5 @@ val discharge_direct_opaque :
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : ?except:Future.UUIDSet.t -> opaquetab ->
- (cooking_info list * int * Constr.t option) array *
+ opaque_proofterm array *
int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 0b0f14eee7..596fcd210c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -725,11 +725,14 @@ let export_side_effects mb env (b_ctx, eff) =
let kn = eff.seff_constant in
let ce = constant_entry_of_side_effect eff in
let cb = Term_typing.translate_constant Term_typing.Pure env kn ce in
- let map cu =
+ let map cu =
let (c, u) = Future.force cu in
- let () = assert (Univ.ContextSet.is_empty u) in
+ let () = match u with
+ | Opaqueproof.PrivateMonomorphic ctx | Opaqueproof.PrivatePolymorphic ctx ->
+ assert (Univ.ContextSet.is_empty ctx)
+ in
c
- in
+ in
let cb = map_constant map cb in
let eff = { eff with seff_body = cb } in
(push_seff env eff, export_eff eff)
@@ -742,13 +745,16 @@ let export_side_effects mb env (b_ctx, eff) =
in
translate_seff trusted seff [] env
-let n_univs cb = match cb.const_universes with
-| Monomorphic _ -> 0
-| Polymorphic auctx -> Univ.AUContext.size auctx
-
let export_private_constants ~in_section ce senv =
let exported, ce = export_side_effects senv.revstruct senv.env ce in
- let map (kn, cb) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val (p, Univ.ContextSet.empty))) cb) in
+ let map univs p =
+ let univs, local = match univs with
+ | Monomorphic _ -> 0, Opaqueproof.PrivateMonomorphic Univ.ContextSet.empty
+ | Polymorphic auctx -> Univ.AUContext.size auctx, Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+ in
+ Opaqueproof.create ~univs (Future.from_val (p, local))
+ in
+ let map (kn, cb) = (kn, map_constant (fun c -> map cb.const_universes c) cb) in
let bodies = List.map map exported in
let exported = List.map (fun (kn, _) -> kn) exported in
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -775,7 +781,11 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
in
let senv =
- let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
+ let univs = match cb.const_universes with
+ | Monomorphic _ -> 0
+ | Polymorphic auctx -> Univ.AUContext.size auctx
+ in
+ let cb = map_constant (fun c -> Opaqueproof.create ~univs c) cb in
add_constant_aux ~in_section senv (kn, cb) in
let senv =
match decl with
@@ -791,14 +801,16 @@ let add_constant (type a) ~(side_effect : a effect_entry) ~in_section l decl sen
| (Primitive _ | Undef _) -> assert false
| Def c -> (Def c, cb.const_universes)
| OpaqueDef o ->
- let (b, ctx) = Future.force o in
- match cb.const_universes with
- | Monomorphic ctx' ->
+ let (b, delayed) = Future.force o in
+ match cb.const_universes, delayed with
+ | Monomorphic ctx', Opaqueproof.PrivateMonomorphic ctx ->
OpaqueDef b, Monomorphic (Univ.ContextSet.union ctx ctx')
- | Polymorphic auctx ->
+ | Polymorphic auctx, Opaqueproof.PrivatePolymorphic ctx ->
(* Upper layers enforce that there are no internal constraints *)
let () = assert (Univ.ContextSet.is_empty ctx) in
OpaqueDef b, Polymorphic auctx
+ | (Monomorphic _ | Polymorphic _), (Opaqueproof.PrivateMonomorphic _ | Opaqueproof.PrivatePolymorphic _) ->
+ assert false
in
let cb = { cb with const_body = body; const_universes = univs } in
let from_env = CEphemeron.create senv.revstruct in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index f984088f47..9ec3269375 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -79,7 +79,6 @@ 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_relevance = r;
cook_inline = false;
cook_context = ctx;
@@ -108,7 +107,6 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
{ Cooking.cook_body = cd;
cook_type = ty;
cook_universes = Monomorphic uctxt;
- cook_private_univs = None;
cook_inline = false;
cook_context = None;
cook_relevance = Sorts.Relevant;
@@ -124,7 +122,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let { const_entry_body = body; const_entry_feedback = feedback_id; _ } = c in
let tyj = Typeops.infer_type env typ in
let proofterm =
- Future.chain body (fun ((body,uctx),side_eff) ->
+ Future.chain body begin fun ((body,uctx),side_eff) ->
(* don't redeclare universes which are declared for the type *)
let uctx = Univ.ContextSet.diff uctx univs in
let j, uctx = match trust with
@@ -145,13 +143,13 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
in
let c = j.uj_val in
feedback_completion_typecheck feedback_id;
- c, uctx) in
+ c, Opaqueproof.PrivateMonomorphic uctx
+ end in
let def = OpaqueDef proofterm in
{
Cooking.cook_body = def;
cook_type = tyj.utj_val;
cook_universes = Monomorphic univs;
- cook_private_univs = None;
cook_relevance = Sorts.relevance_of_sort tyj.utj_type;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -168,8 +166,7 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let tj = Typeops.infer_type env typ in
let sbst, auctx = Univ.abstract_universes nas uctx in
let usubst = Univ.make_instance_subst sbst in
- let (def, private_univs) =
- let (body, ctx), side_eff = Future.join body in
+ let proofterm = Future.chain body begin fun ((body, ctx), side_eff) ->
let body, ctx = match trust with
| Pure -> body, ctx
| SideEffects handle ->
@@ -183,16 +180,15 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
let j = Typeops.infer env body in
let _ = Typeops.judge_of_cast env j DEFAULTcast tj in
let def = Vars.subst_univs_level_constr usubst j.uj_val in
- def, private_univs
- in
- let def = OpaqueDef (Future.from_val (def, Univ.ContextSet.empty)) in
+ let () = feedback_completion_typecheck feedback_id in
+ def, Opaqueproof.PrivatePolymorphic private_univs
+ end in
+ let def = OpaqueDef proofterm in
let typ = Vars.subst_univs_level_constr usubst tj.utj_val in
- feedback_completion_typecheck feedback_id;
{
Cooking.cook_body = def;
cook_type = typ;
cook_universes = Polymorphic auctx;
- cook_private_univs = Some private_univs;
cook_relevance = Sorts.relevance_of_sort tj.utj_type;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -211,22 +207,22 @@ let infer_declaration (type a) ~(trust : a trust) env (dcl : a constant_entry) =
body, ctx
| SideEffects _ -> assert false
in
- let env, usubst, univs, private_univs = match c.const_entry_universes with
+ let env, usubst, univs = match c.const_entry_universes with
| Monomorphic_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 ctx, None
+ env, Univ.empty_level_subst, Monomorphic ctx
| Polymorphic_entry (nas, uctx) ->
(** [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
- let env, local =
- if Univ.ContextSet.is_empty ctx then env, None
- else CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
+ let () =
+ if not (Univ.ContextSet.is_empty ctx) then
+ CErrors.anomaly Pp.(str "Local universes in non-opaque polymorphic definition.")
in
- env, sbst, Polymorphic auctx, local
+ env, sbst, Polymorphic auctx
in
let j = Typeops.infer env body in
let typ = match typ with
@@ -244,7 +240,6 @@ 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_relevance = Retypeops.relevance_of_term env j.uj_val;
cook_inline = c.const_entry_inline_code;
cook_context = c.const_entry_secctx;
@@ -341,7 +336,6 @@ let build_constant_declaration env result =
const_type = typ;
const_body_code = tps;
const_universes = univs;
- const_private_poly_univs = result.cook_private_univs;
const_relevance = result.cook_relevance;
const_inline_code = result.cook_inline;
const_typing_flags = Environ.typing_flags env }
@@ -368,7 +362,6 @@ let translate_recipe env _kn r =
const_type = result.cook_type;
const_body_code = tps;
const_universes = univs;
- const_private_poly_univs = result.cook_private_univs;
const_relevance = result.cook_relevance;
const_inline_code = result.cook_inline;
const_typing_flags = Environ.typing_flags env }
@@ -407,7 +400,10 @@ let translate_local_def env _id centry =
let (p, cst) = Future.force 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
+ let () = match cst with
+ | Opaqueproof.PrivateMonomorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+ | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+ in
p
| Undef _ | Primitive _ -> assert false
in
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 16:50:57 +0000