aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml7
-rw-r--r--checker/mod_checking.ml23
-rw-r--r--checker/values.ml6
-rw-r--r--doc/plugin_tutorial/tuto1/src/simple_print.ml2
-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
-rw-r--r--library/global.ml9
-rw-r--r--library/global.mli7
-rw-r--r--library/library.ml9
-rw-r--r--library/library.mli2
-rw-r--r--plugins/extraction/extraction.ml2
-rw-r--r--plugins/funind/functional_principles_proofs.ml4
-rw-r--r--plugins/funind/functional_principles_types.ml2
-rw-r--r--plugins/funind/indfun.ml2
-rw-r--r--printing/prettyp.ml12
-rw-r--r--printing/printmod.ml2
-rw-r--r--stm/stm.ml8
-rw-r--r--vernac/assumptions.ml4
-rw-r--r--vernac/lemmas.ml2
26 files changed, 172 insertions, 120 deletions
diff --git a/checker/check.ml b/checker/check.ml
index 903258daef..89cb834a4a 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -51,7 +51,7 @@ let pr_path sp =
type compilation_unit_name = DirPath.t
type seg_univ = Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
type library_t = {
library_name : compilation_unit_name;
@@ -98,10 +98,7 @@ let access_opaque_table dp i =
with Not_found -> assert false
in
assert (i < Array.length t);
- let (info, n, c) = t.(i) in
- match c with
- | None -> None
- | Some c -> Some (Cooking.cook_constr info n c)
+ t.(i)
let access_discharge = Cooking.cook_constr
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 0684623a81..7e49e741ad 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -31,16 +31,19 @@ let check_constant_declaration env kn cb =
in
let ty = cb.const_type in
let _ = infer_type env' ty in
- let env' = match cb.const_private_poly_univs, (cb.const_body, poly) with
- | None, _ -> env'
- | Some local, (OpaqueDef _, true) -> push_subgraph local env'
- | Some _, _ -> assert false
- in
- let otab = Environ.opaque_tables env in
- let body = match cb.const_body with
- | Undef _ | Primitive _ -> None
- | Def c -> Some (Mod_subst.force_constr c)
- | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
+ let otab = Environ.opaque_tables env' in
+ let body, env' = match cb.const_body with
+ | Undef _ | Primitive _ -> None, env'
+ | Def c -> Some (Mod_subst.force_constr c), env'
+ | OpaqueDef o ->
+ let c, u = Opaqueproof.force_proof !indirect_accessor otab o in
+ let env' = match u, cb.const_universes with
+ | Opaqueproof.PrivateMonomorphic (), Monomorphic _ -> env'
+ | Opaqueproof.PrivatePolymorphic local, Polymorphic _ ->
+ push_subgraph local env'
+ | _ -> assert false
+ in
+ Some c, env'
in
let () =
match body with
diff --git a/checker/values.ml b/checker/values.ml
index 4a4c8d803c..7b869cd130 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -230,7 +230,6 @@ let v_cb = v_tuple "constant_body"
v_relevance;
Any;
v_univs;
- Opt v_context_set;
v_bool;
v_typing_flags|]
@@ -399,6 +398,9 @@ let v_abstract =
let v_cooking_info =
Tuple ("cooking_info", [|v_work_list; v_abstract|])
-let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt v_constr |]))
+let v_delayed_universes =
+ Sum ("delayed_universes", 0, [| [| v_unit |]; [| v_context_set |] |])
+
+let v_opaques = Array (Tuple ("opaque", [| List v_cooking_info; Int; Opt (v_pair v_constr v_delayed_universes) |]))
let v_univopaques =
Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/doc/plugin_tutorial/tuto1/src/simple_print.ml b/doc/plugin_tutorial/tuto1/src/simple_print.ml
index 48b5f2214c..ba989b1bac 100644
--- a/doc/plugin_tutorial/tuto1/src/simple_print.ml
+++ b/doc/plugin_tutorial/tuto1/src/simple_print.ml
@@ -12,6 +12,6 @@ let simple_body_access gref =
| Globnames.ConstRef cst ->
let cb = Environ.lookup_constant cst (Global.env()) in
match Global.body_of_constant_body Library.indirect_accessor cb with
- | Some(e, _) -> EConstr.of_constr e
+ | Some(e, _, _) -> EConstr.of_constr e
| None -> failwith "This term has no value"
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
diff --git a/library/global.ml b/library/global.ml
index 3f30a63808..44e4a9b7e1 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -139,9 +139,14 @@ let body_of_constant_body access env cb =
| Undef _ | Primitive _ ->
None
| Def c ->
- Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb)
+ let u = match cb.const_universes with
+ | Monomorphic _ -> Opaqueproof.PrivateMonomorphic ()
+ | Polymorphic _ -> Opaqueproof.PrivatePolymorphic Univ.ContextSet.empty
+ in
+ Some (Mod_subst.force_constr c, u, Declareops.constant_polymorphic_context cb)
| OpaqueDef o ->
- Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb)
+ let c, u = Opaqueproof.force_proof access otab o in
+ Some (c, u, Declareops.constant_polymorphic_context cb)
let body_of_constant_body access ce = body_of_constant_body access (env ()) ce
diff --git a/library/global.mli b/library/global.mli
index c36cec3511..34b6c52833 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -100,13 +100,16 @@ val mind_of_delta_kn : KerName.t -> MutInd.t
val opaque_tables : unit -> Opaqueproof.opaquetab
-val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t ->
+ (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
(** Returns the body of the constant if it has any, and the polymorphic context
it lives in. For monomorphic constant, the latter is empty, and for
polymorphic constants, the term contains De Bruijn universe variables that
need to be instantiated. *)
-val body_of_constant_body : Opaqueproof.indirect_accessor -> Opaqueproof.opaque Declarations.constant_body -> (Constr.constr * Univ.AUContext.t) option
+val body_of_constant_body : Opaqueproof.indirect_accessor ->
+ Opaqueproof.opaque Declarations.constant_body ->
+ (Constr.constr * unit Opaqueproof.delayed_universes * Univ.AUContext.t) option
(** Same as {!body_of_constant} but on {!Declarations.constant_body}. *)
(** {6 Compiled libraries } *)
diff --git a/library/library.ml b/library/library.ml
index 1ac75d2fdc..a55fe33617 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,7 +280,7 @@ type 'a table_status =
| Fetched of 'a array
let opaque_tables =
- ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) table_status) LibraryMap.t)
+ ref (LibraryMap.empty : (Opaqueproof.opaque_proofterm table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,7 @@ let access_table what tables dp i =
let access_opaque_table dp i =
let what = "opaque proofs" in
- let (info, n, c) = access_table what opaque_tables dp i in
- match c with
- | None -> None
- | Some c -> Some (Cooking.cook_constr info n c)
+ access_table what opaque_tables dp i
let indirect_accessor = {
Opaqueproof.access_proof = access_opaque_table;
@@ -323,7 +320,7 @@ type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
let mk_library sd md digests univs =
{
diff --git a/library/library.mli b/library/library.mli
index 727eca10cf..de395fd3b4 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -35,7 +35,7 @@ type seg_sum
type seg_lib
type seg_univ = (* all_cst, finished? *)
Univ.ContextSet.t * bool
-type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t option) array
+type seg_proofs = Opaqueproof.opaque_proofterm array
(** Open a module (or a library); if the boolean is true then it's also
an export otherwise just a simple import *)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 051d1f8e0f..8c505eb202 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -115,7 +115,7 @@ let get_body lconstr = EConstr.of_constr (Mod_subst.force_constr lconstr)
let get_opaque env c =
EConstr.of_constr
- (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c)
+ (fst (Opaqueproof.force_proof Library.indirect_accessor (Environ.opaque_tables env) c))
let applistc c args = EConstr.mkApp (c, Array.of_list args)
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 17498c6384..ce3b5a82d6 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -951,7 +951,7 @@ let generate_equation_lemma evd fnames f fun_num nb_params nb_args rec_args_num
(* observe (str "rec_args_num := " ++ str (string_of_int (rec_args_num + 1) )); *)
let f_def = Global.lookup_constant (fst (destConst evd f)) in
let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
- let (f_body, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
+ let (f_body, _, _) = Option.get (Global.body_of_constant_body Library.indirect_accessor f_def) in
let f_body = EConstr.of_constr f_body in
let params,f_body_with_params = decompose_lam_n evd nb_params f_body in
let (_,num),(_,_,bodies) = destFix evd f_body_with_params in
@@ -1082,7 +1082,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
in
let get_body const =
match Global.body_of_constant Library.indirect_accessor const with
- | Some (body, _) ->
+ | Some (body, _, _) ->
let env = Global.env () in
let sigma = Evd.from_env env in
Tacred.cbv_norm_flags
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 8af5dc818b..53d303bb99 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -413,7 +413,7 @@ let get_funs_constant mp =
function const ->
let find_constant_body const =
match Global.body_of_constant Library.indirect_accessor const with
- | Some (body, _) ->
+ | Some (body, _, _) ->
let body = Tacred.cbv_norm_flags
(CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
(Global.env ())
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index ecf953bef1..0ecfbacb09 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -853,7 +853,7 @@ let make_graph (f_ref : GlobRef.t) =
in
(match Global.body_of_constant_body Library.indirect_accessor c_body with
| None -> error "Cannot build a graph over an axiom!"
- | Some (body, _) ->
+ | Some (body, _, _) ->
let env = Global.env () in
let extern_body,extern_type =
with_full_print (fun () ->
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index f55bfb504f..396c954b42 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -583,11 +583,15 @@ let print_constant with_values sep sp udecl =
str"*** [ " ++
print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++
str" ]" ++
- Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs
- | Some (c, ctx) ->
+ Printer.pr_universes sigma univs
+ | Some (c, priv, ctx) ->
+ let priv = match priv with
+ | Opaqueproof.PrivateMonomorphic () -> None
+ | Opaqueproof.PrivatePolymorphic ctx -> Some ctx
+ in
print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++
(if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++
- Printer.pr_universes sigma univs ?priv:cb.const_private_poly_univs)
+ Printer.pr_universes sigma univs ?priv)
let gallina_print_constant_with_infos sp udecl =
print_constant true " = " sp udecl ++
@@ -723,7 +727,7 @@ let print_full_pure_context env sigma =
| OpaqueDef lc ->
str "Theorem " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ str "." ++ fnl () ++
- str "Proof " ++ pr_lconstr_env env sigma (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc)
+ str "Proof " ++ pr_lconstr_env env sigma (fst (Opaqueproof.force_proof Library.indirect_accessor (Global.opaque_tables ()) lc))
| Def c ->
str "Definition " ++ print_basename con ++ cut () ++
str " : " ++ pr_ltype_env env sigma typ ++ cut () ++ str " := " ++
diff --git a/printing/printmod.ml b/printing/printmod.ml
index bd97104f60..52a3616152 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -297,7 +297,7 @@ let print_body is_impl extent env mp (l,body) =
hov 2 (str ":= " ++
Printer.pr_lconstr_env env sigma (Mod_subst.force_constr l))
| _ -> mt ()) ++ str "." ++
- Printer.pr_abstract_universe_ctx sigma ctx ?priv:cb.const_private_poly_univs)
+ Printer.pr_abstract_universe_ctx sigma ctx)
| SFBmind mib ->
match extent with
| WithContents ->
diff --git a/stm/stm.ml b/stm/stm.ml
index d77e37c910..bae51d1794 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1746,14 +1746,18 @@ end = struct (* {{{ *)
the call to [check_task_aux] above. *)
let uc = Opaqueproof.force_constraints Library.indirect_accessor (Global.opaque_tables ()) o in
let uc = Univ.hcons_universe_context_set uc in
- let (pr, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
+ let (pr, priv, ctx) = Option.get (Global.body_of_constant_body Library.indirect_accessor c) in
(* We only manipulate monomorphic terms here. *)
let () = assert (Univ.AUContext.is_empty ctx) in
+ let () = match priv with
+ | Opaqueproof.PrivateMonomorphic () -> ()
+ | Opaqueproof.PrivatePolymorphic ctx -> assert (Univ.ContextSet.is_empty ctx)
+ in
let pr = Constr.hcons pr in
let (ci, univs, dummy) = p.(bucket) in
let () = assert (Option.is_empty dummy) in
let () = assert (Int.equal (Univ.AUContext.size ctx) univs) in
- p.(bucket) <- ci, univs, Some pr;
+ p.(bucket) <- ci, univs, Some (pr, priv);
Univ.ContextSet.union cst uc, false
let check_task name l i =
diff --git a/vernac/assumptions.ml b/vernac/assumptions.ml
index 9353ef3902..5c6a282894 100644
--- a/vernac/assumptions.ml
+++ b/vernac/assumptions.ml
@@ -168,7 +168,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
let body () = id |> Global.lookup_named |> NamedDecl.get_value in
traverse_object accu body (VarRef id)
| Const (kn, _) ->
- let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
+ let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object accu body (ConstRef kn)
| Ind ((mind, _) as ind, _) ->
traverse_inductive accu mind (IndRef ind)
@@ -181,7 +181,7 @@ let rec traverse current ctx accu t = match Constr.kind t with
| Lambda(_,_,oty), Const (kn, _)
when Vars.noccurn 1 oty &&
not (Declareops.constant_has_body (lookup_constant kn)) ->
- let body () = Option.map fst (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
+ let body () = Option.map pi1 (Global.body_of_constant_body Library.indirect_accessor (lookup_constant kn)) in
traverse_object
~inhabits:(current,ctx,Vars.subst1 mkProp oty) accu body (ConstRef kn)
| _ ->
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml
index 7aba64fb93..cd8b17f681 100644
--- a/vernac/lemmas.ml
+++ b/vernac/lemmas.ml
@@ -93,7 +93,7 @@ let retrieve_first_recthm uctx = function
(* we get the right order somehow but surely it could be enforced in a better way *)
let uctx = UState.context uctx in
let inst = Univ.UContext.instance uctx in
- let map (c, ctx) = Vars.subst_instance_constr inst c in
+ let map (c, _, _) = Vars.subst_instance_constr inst c in
(Option.map map (Global.body_of_constant_body Library.indirect_accessor cb), is_opaque cb)
| _ -> assert false
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 18:59:56 +0000