aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml15
-rw-r--r--checker/mod_checking.ml12
-rw-r--r--checker/mod_checking.mli2
-rw-r--r--checker/values.ml20
-rw-r--r--kernel/cooking.ml18
-rw-r--r--kernel/cooking.mli2
-rw-r--r--kernel/opaqueproof.ml59
-rw-r--r--kernel/opaqueproof.mli25
-rw-r--r--kernel/safe_typing.ml8
-rw-r--r--library/library.ml10
-rw-r--r--library/library.mli2
-rw-r--r--stm/stm.ml8
12 files changed, 112 insertions, 69 deletions
diff --git a/checker/check.ml b/checker/check.ml
index c5bc59e72a..747d7c43a1 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 = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.constr) option array
type library_t = {
library_name : compilation_unit_name;
@@ -98,9 +98,18 @@ let access_opaque_table dp i =
with Not_found -> assert false
in
assert (i < Array.length t);
- t.(i)
+ match t.(i) with
+ | None -> None
+ | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
-let () = Mod_checking.set_indirect_accessor access_opaque_table
+let access_discharge = Cooking.cook_constr
+
+let indirect_accessor = {
+ Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_discharge = access_discharge;
+}
+
+let () = Mod_checking.set_indirect_accessor indirect_accessor
let check_one_lib admit senv (dir,m) =
let md = m.library_compiled in
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index ccce0bd9a7..0684623a81 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -8,13 +8,13 @@ open Environ
(** {6 Checking constants } *)
-let get_proof = ref (fun _ _ -> assert false)
-let set_indirect_accessor f = get_proof := f
-
-let indirect_accessor = {
- Opaqueproof.access_proof = (fun dp n -> !get_proof dp n);
+let indirect_accessor = ref {
+ Opaqueproof.access_proof = (fun _ _ -> assert false);
+ Opaqueproof.access_discharge = (fun _ _ _ -> assert false);
}
+let set_indirect_accessor f = indirect_accessor := f
+
let check_constant_declaration env kn cb =
Flags.if_verbose Feedback.msg_notice (str " checking cst:" ++ Constant.print kn);
(* Locally set the oracle for further typechecking *)
@@ -40,7 +40,7 @@ let check_constant_declaration env kn cb =
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)
+ | OpaqueDef o -> Some (Opaqueproof.force_proof !indirect_accessor otab o)
in
let () =
match body with
diff --git a/checker/mod_checking.mli b/checker/mod_checking.mli
index dbc81c8507..7aa1f837a0 100644
--- a/checker/mod_checking.mli
+++ b/checker/mod_checking.mli
@@ -8,6 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-val set_indirect_accessor : (Names.DirPath.t -> int -> Constr.t option) -> unit
+val set_indirect_accessor : Opaqueproof.indirect_accessor -> unit
val check_module : Environ.env -> Names.ModPath.t -> Declarations.module_body -> unit
diff --git a/checker/values.ml b/checker/values.ml
index 031f05dd6b..6dbf281f49 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -131,7 +131,7 @@ let v_proj = v_tuple "projection" [|v_proj_repr; v_bool|]
let rec v_constr =
Sum ("constr",0,[|
[|Int|]; (* Rel *)
- [|Fail "Var"|]; (* Var *)
+ [|v_id|]; (* Var *)
[|Fail "Meta"|]; (* Meta *)
[|Fail "Evar"|]; (* Evar *)
[|v_sort|]; (* Sort *)
@@ -383,6 +383,22 @@ let v_libsum =
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
-let v_opaques = Array (Opt v_constr)
+let v_ndecl = v_sum "named_declaration" 0
+ [| [|v_binder_annot v_id; v_constr|]; (* LocalAssum *)
+ [|v_binder_annot v_id; v_constr; v_constr|] |] (* LocalDef *)
+
+let v_nctxt = List v_ndecl
+
+let v_work_list =
+ let v_abstr = v_pair v_instance (Array v_id) in
+ Tuple ("work_list", [|v_hmap v_cst v_abstr; v_hmap v_cst v_abstr|])
+
+let v_abstract =
+ Tuple ("abstract", [| v_nctxt; v_instance; v_abs_context |])
+
+let v_cooking_info =
+ Tuple ("cooking_info", [|v_work_list; v_abstract|])
+
+let v_opaques = Array (Opt (Tuple ("opaque", [| List v_cooking_info; Int; v_constr |])))
let v_univopaques =
Opt (Tuple ("univopaques",[|v_context_set;v_bool|]))
diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index 620efbafd6..1336e3e8bf 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -202,17 +202,21 @@ 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 } c =
+let cook_constr { Opaqueproof.modlist ; abstract } (univs, c) =
let cache = RefTable.create 13 in
let abstract, usubst, abs_ctx = abstract in
- (* For now the STM only handles deferred computation of monomorphic
- constants. The API will need to be adapted when it's not the case
- anymore. *)
- let () = assert (AUContext.is_empty abs_ctx) in
+ let ainst = Instance.of_array (Array.init univs Level.var) in
+ let usubst = Instance.append usubst ainst in
let expmod = expmod_constr_subst cache modlist usubst in
let hyps = Context.Named.map expmod abstract in
let hyps = abstract_context hyps in
- abstract_constant_body (expmod c) hyps
+ let c = abstract_constant_body (expmod c) hyps in
+ univs + AUContext.size abs_ctx, c
+
+let cook_constr infos univs c =
+ let fold info (univs, c) = cook_constr info (univs, c) in
+ let (_, c) = List.fold_right fold infos (univs, c) in
+ c
let cook_constant { from = cb; info } =
let { Opaqueproof.modlist; abstract } = info in
@@ -227,7 +231,7 @@ let cook_constant { from = cb; info } =
| Undef _ as x -> x
| Def cs -> Def (Mod_subst.from_val (map (Mod_subst.force_constr cs)))
| OpaqueDef o ->
- OpaqueDef (Opaqueproof.discharge_direct_opaque ~cook_constr:map info o)
+ OpaqueDef (Opaqueproof.discharge_direct_opaque info o)
| Primitive _ -> CErrors.anomaly (Pp.str "Primitives cannot be cooked")
in
let const_hyps =
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index abae3880d7..934b7c6b50 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -28,7 +28,7 @@ type 'opaque result = {
}
val cook_constant : recipe -> Opaqueproof.opaque result
-val cook_constr : Opaqueproof.cooking_info -> constr -> constr
+val cook_constr : Opaqueproof.cooking_info list -> int -> constr -> constr
val cook_inductive :
Opaqueproof.cooking_info -> mutual_inductive_body -> Entries.mutual_inductive_entry
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 1971c67c61..ee549dee4f 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -16,19 +16,22 @@ open Mod_subst
type work_list = (Instance.t * Id.t array) Cmap.t *
(Instance.t * Id.t array) Mindmap.t
+type cooking_info = {
+ modlist : work_list;
+ abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
+ access_discharge : cooking_info list -> int -> constr -> constr;
}
-type cooking_info = {
- modlist : work_list;
- abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
type proofterm = (constr * Univ.ContextSet.t) Future.computation
+type universes = int
type opaque =
| Indirect of substitution list * DirPath.t * int (* subst, lib, index *)
- | Direct of cooking_info list * proofterm
+ | Direct of universes * cooking_info list * proofterm
type opaquetab = {
- opaque_val : (cooking_info list * proofterm) Int.Map.t;
+ opaque_val : (int * cooking_info list * proofterm) Int.Map.t;
(** Actual proof terms *)
opaque_len : int;
(** Size of the above map *)
@@ -43,14 +46,14 @@ let empty_opaquetab = {
let not_here () =
CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
-let create cu = Direct ([],cu)
+let create ~univs cu = Direct (univs, [],cu)
let turn_indirect dp o tab = match o with
| Indirect (_,_,i) ->
if not (Int.Map.mem i tab.opaque_val)
then CErrors.anomaly (Pp.str "Indirect in a different table.")
else CErrors.anomaly (Pp.str "Already an indirect opaque.")
- | Direct (d,cu) ->
+ | Direct (nunivs, d, cu) ->
(* Invariant: direct opaques only exist inside sections, we turn them
indirect as soon as we are at toplevel. At this moment, we perform
hashconsing of their contents, potentially as a future. *)
@@ -61,7 +64,7 @@ let turn_indirect dp o tab = match o with
in
let cu = Future.chain cu hcons in
let id = tab.opaque_len in
- let opaque_val = Int.Map.add id (d,cu) tab.opaque_val in
+ let opaque_val = Int.Map.add id (nunivs, d,cu) tab.opaque_val in
let opaque_dir =
if DirPath.equal dp tab.opaque_dir then tab.opaque_dir
else if DirPath.equal tab.opaque_dir DirPath.initial then dp
@@ -74,10 +77,10 @@ let subst_opaque sub = function
| Indirect (s,dp,i) -> Indirect (sub::s,dp,i)
| Direct _ -> CErrors.anomaly (Pp.str "Substituting a Direct opaque.")
-let discharge_direct_opaque ~cook_constr ci = function
+let discharge_direct_opaque ci = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
- | Direct (d,cu) ->
- Direct (ci::d,Future.chain cu (fun (c, u) -> cook_constr c, u))
+ | Direct (n, d, cu) ->
+ Direct (n, ci :: d, cu)
let join except cu = match except with
| None -> ignore (Future.join cu)
@@ -86,36 +89,42 @@ let join except cu = match except with
else ignore (Future.join cu)
let join_opaque ?except { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> join except cu
+ | Direct (_,_,cu) -> join except cu
| Indirect (_,dp,i) ->
if DirPath.equal dp odp then
- let fp = snd (Int.Map.find i prfs) in
+ let (_, _, fp) = Int.Map.find i prfs in
join except fp
let force_proof access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) ->
- fst(Future.force cu)
+ | Direct (n, d, cu) ->
+ let (c, _) = Future.force cu in
+ access.access_discharge d n c
| Indirect (l,dp,i) ->
- let pt =
+ let c =
if DirPath.equal dp odp
- then Future.chain (snd (Int.Map.find i prfs)) fst
+ 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 -> Future.from_val v
+ | Some v -> v
in
- let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
let force_constraints _access { opaque_val = prfs; opaque_dir = odp; _ } = function
- | Direct (_,cu) -> snd(Future.force cu)
+ | Direct (_,_,cu) ->
+ snd(Future.force cu)
| Indirect (_,dp,i) ->
if DirPath.equal dp odp
- then snd (Future.force (snd (Int.Map.find i prfs)))
+ then
+ let (_, _, cu) = Int.Map.find i prfs in
+ snd (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 snd
module FMap = Future.UUIDMap
@@ -123,13 +132,15 @@ let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _
let opaque_table = Array.make n None in
let disch_table = Array.make n [] in
let f2t_map = ref FMap.empty in
- let iter n (d, cu) =
+ let iter n (univs, d, cu) =
let uid = Future.uuid cu in
let () = f2t_map := FMap.add (Future.uuid cu) n !f2t_map in
if Future.is_val cu then
let (c, _) = Future.force cu in
- opaque_table.(n) <- Some c
+ opaque_table.(n) <- Some (d, univs, c)
else if Future.UUIDSet.mem uid except then
+ (* Only monomorphic constraints can be delayed currently *)
+ let () = assert (Int.equal univs 0) in
disch_table.(n) <- d
else
CErrors.anomaly
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index 46b0500507..47439a787d 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -28,15 +28,23 @@ type opaque
val empty_opaquetab : opaquetab
(** From a [proofterm] to some [opaque]. *)
-val create : proofterm -> opaque
+val create : univs:int -> proofterm -> opaque
(** Turn a direct [opaque] into an indirect one. It is your responsibility to
hashcons the inner term beforehand. The integer is an hint of the maximum id
used so far *)
val turn_indirect : DirPath.t -> opaque -> opaquetab -> opaque * opaquetab
+type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
+ (Univ.Instance.t * Id.t array) Mindmap.t
+
+type cooking_info = {
+ modlist : work_list;
+ abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
+
type indirect_accessor = {
access_proof : DirPath.t -> int -> constr option;
+ access_discharge : cooking_info list -> int -> constr -> constr;
}
(** When stored indirectly, opaque terms are indexed by their library
dirpath and an integer index. The two functions above activate
@@ -51,23 +59,12 @@ val get_direct_constraints : opaque -> Univ.ContextSet.t Future.computation
val subst_opaque : substitution -> opaque -> opaque
-type work_list = (Univ.Instance.t * Id.t array) Cmap.t *
- (Univ.Instance.t * Id.t array) Mindmap.t
-
-type cooking_info = {
- modlist : work_list;
- abstract : Constr.named_context * Univ.Instance.t * Univ.AUContext.t }
-
-(* The type has two caveats:
- 1) cook_constr is defined after
- 2) we have to store the input in the [opaque] in order to be able to
- discharge it when turning a .vi into a .vo *)
val discharge_direct_opaque :
- cook_constr:(constr -> constr) -> cooking_info -> opaque -> opaque
+ cooking_info -> opaque -> opaque
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
val dump : ?except:Future.UUIDSet.t -> opaquetab ->
- Constr.t option array *
+ (cooking_info list * int * Constr.t) option array *
cooking_info list array *
int Future.UUIDMap.t
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 9f7466902d..759cbe22ee 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -749,9 +749,13 @@ 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 (Future.from_val p)) cb) in
+ let map (kn, cb, _) = (kn, map_constant (fun p -> Opaqueproof.create ~univs:(n_univs cb) (Future.from_val p)) cb) in
let bodies = List.map map exported in
let exported = List.map (fun (kn, _, r) -> (kn, r)) exported in
let senv = List.fold_left (add_constant_aux ~in_section) senv bodies in
@@ -778,7 +782,7 @@ let add_constant ?role ~in_section l decl senv =
Term_typing.translate_constant Term_typing.Pure senv.env kn ce
in
let senv =
- let cb = map_constant Opaqueproof.create cb in
+ let cb = map_constant (fun c -> Opaqueproof.create ~univs:(n_univs cb) c) cb in
add_constant_aux ~in_section senv (kn, cb) in
let senv =
match decl with
diff --git a/library/library.ml b/library/library.ml
index e3b8511af1..0a57a85c35 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -280,7 +280,7 @@ type 'a table_status =
| Fetched of 'a option array
let opaque_tables =
- ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
+ ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr) table_status) LibraryMap.t)
let add_opaque_table dp st =
opaque_tables := LibraryMap.add dp st !opaque_tables
@@ -306,10 +306,14 @@ let access_table what tables dp i =
let access_opaque_table dp i =
let what = "opaque proofs" in
- access_table what opaque_tables dp i
+ let ans = access_table what opaque_tables dp i in
+ match ans with
+ | None -> None
+ | Some (info, n, c) -> Some (Cooking.cook_constr info n c)
let indirect_accessor = {
Opaqueproof.access_proof = access_opaque_table;
+ Opaqueproof.access_discharge = Cooking.cook_constr;
}
(************************************************************************)
@@ -320,7 +324,7 @@ type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) option array
let mk_library sd md digests univs =
{
diff --git a/library/library.mli b/library/library.mli
index 142206e2c5..0c5d6e33c1 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -36,7 +36,7 @@ type seg_lib
type seg_univ = (* all_cst, finished? *)
Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr option array
+type seg_proofs = (Opaqueproof.cooking_info list * int * Constr.t) option 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/stm/stm.ml b/stm/stm.ml
index b2bfa552b4..8efb606ddc 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1732,7 +1732,6 @@ end = struct (* {{{ *)
| `ERROR_ADMITTED -> cst, false
| `OK_ADMITTED -> cst, false
| `OK (po,_) ->
- let discharge c = List.fold_right Cooking.cook_constr d.(bucket) c in
let con =
Nametab.locate_constant
(Libnames.qualid_of_ident po.Proof_global.id) in
@@ -1744,12 +1743,11 @@ 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
(* We only manipulate monomorphic terms here. *)
- let map (c, ctx) = assert (Univ.AUContext.is_empty ctx); c in
- let pr = map (Option.get (Global.body_of_constant_body Library.indirect_accessor c)) in
- let pr = discharge pr in
+ let () = assert (Univ.AUContext.is_empty ctx) in
let pr = Constr.hcons pr in
- p.(bucket) <- Some pr;
+ p.(bucket) <- Some (d.(bucket), Univ.AUContext.size ctx, pr);
Univ.ContextSet.union cst uc, false
let check_task name l i =
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 17:15:32 +0000