aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--checker/check.ml2
-rw-r--r--checker/values.ml12
-rw-r--r--kernel/opaqueproof.ml44
-rw-r--r--kernel/opaqueproof.mli10
-rw-r--r--library/library.ml22
-rw-r--r--library/library.mli4
-rw-r--r--stm/stm.ml9
7 files changed, 43 insertions, 60 deletions
diff --git a/checker/check.ml b/checker/check.ml
index a2c8a0f25d..cc5ad0af4c 100644
--- a/checker/check.ml
+++ b/checker/check.ml
@@ -50,7 +50,7 @@ let pr_path sp =
type compilation_unit_name = DirPath.t
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
type library_t = {
library_name : compilation_unit_name;
diff --git a/checker/values.ml b/checker/values.ml
index 5cbf0ff298..4b651cafb6 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -53,7 +53,6 @@ let v_enum name n = Sum(name,n,[||])
let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
let v_bool = v_enum "bool" 2
let v_unit = v_enum "unit" 1
-let v_ref v = v_tuple "ref" [|v|]
let v_set v =
let rec s = Sum ("Set.t",1,
@@ -70,13 +69,6 @@ let v_hmap vk vd = v_map Int (v_map vk vd)
let v_pred v = v_pair v_bool (v_set v)
-(* lib/future *)
-let v_computation f =
- Annot ("Future.computation",
- v_ref
- (v_sum "Future.comput" 0
- [| [| Fail "Future.ongoing" |]; [| f |] |]))
-
(** kernel/names *)
let v_id = String
@@ -391,6 +383,6 @@ let v_libsum =
let v_lib =
Tuple ("library",[|v_compiled_lib;v_libraryobjs|])
-let v_opaques = Array (v_computation v_constr)
+let v_opaques = Array (Opt v_constr)
let v_univopaques =
- Opt (Tuple ("univopaques",[|Array (v_computation v_context_set);v_context_set;v_bool|]))
+ Opt (Tuple ("univopaques",[|Array (Opt v_context_set);v_context_set;v_bool|]))
diff --git a/kernel/opaqueproof.ml b/kernel/opaqueproof.ml
index 5584b74b36..9f148ee248 100644
--- a/kernel/opaqueproof.ml
+++ b/kernel/opaqueproof.ml
@@ -43,6 +43,8 @@ let default_get_univ dp _ =
CErrors.user_err (Pp.pr_sequence Pp.str [
"Cannot access universe constraints of opaque proofs in library ";
DirPath.to_string dp])
+let not_here () =
+ CErrors.user_err Pp.(str "Cannot access opaque delayed proof")
let get_opaque = ref default_get_opaque
let get_univ = ref default_get_univ
@@ -102,7 +104,10 @@ let force_proof { opaque_val = prfs; opaque_dir = odp; _ } = function
let pt =
if DirPath.equal dp odp
then Future.chain (snd (Int.Map.find i prfs)) fst
- else !get_opaque dp i in
+ else match !get_opaque dp i with
+ | None -> not_here ()
+ | Some v -> Future.from_val v
+ in
let c = Future.force pt in
force_constr (List.fold_right subst_substituted l (from_val c))
@@ -113,7 +118,7 @@ let force_constraints { opaque_val = prfs; opaque_dir = odp; _ } = function
then snd (Future.force (snd (Int.Map.find i prfs)))
else match !get_univ dp i with
| None -> Univ.ContextSet.empty
- | Some u -> Future.force u
+ | Some u -> u
let get_direct_constraints = function
| Indirect _ -> CErrors.anomaly (Pp.str "Not a direct opaque.")
@@ -121,22 +126,23 @@ let get_direct_constraints = function
module FMap = Future.UUIDMap
-let a_constr = Future.from_val (mkRel 1)
-let a_univ = Future.from_val Univ.ContextSet.empty
-let a_discharge : cooking_info list = []
-
-let dump { opaque_val = otab; opaque_len = n; _ } =
- let opaque_table = Array.make n a_constr in
- let univ_table = Array.make n a_univ in
- let disch_table = Array.make n a_discharge in
+let dump ?(except = Future.UUIDSet.empty) { opaque_val = otab; opaque_len = n; _ } =
+ let opaque_table = Array.make n None in
+ let univ_table = Array.make n None in
+ let disch_table = Array.make n [] in
let f2t_map = ref FMap.empty in
- Int.Map.iter (fun n (d,cu) ->
- let c, u = Future.split2 cu in
- Future.sink u;
- Future.sink c;
- opaque_table.(n) <- c;
- univ_table.(n) <- u;
- disch_table.(n) <- d;
- f2t_map := FMap.add (Future.uuid cu) n !f2t_map)
- otab;
+ let iter n (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, u) = Future.force cu in
+ let () = univ_table.(n) <- Some u in
+ opaque_table.(n) <- Some c
+ else if Future.UUIDSet.mem uid except then
+ disch_table.(n) <- d
+ else
+ CErrors.anomaly
+ Pp.(str"Proof object "++int n++str" is not checked nor to be checked")
+ in
+ let () = Int.Map.iter iter otab in
opaque_table, univ_table, disch_table, !f2t_map
diff --git a/kernel/opaqueproof.mli b/kernel/opaqueproof.mli
index b84aeaf35a..3b61ec71ef 100644
--- a/kernel/opaqueproof.mli
+++ b/kernel/opaqueproof.mli
@@ -59,9 +59,9 @@ val discharge_direct_opaque :
val join_opaque : ?except:Future.UUIDSet.t -> opaquetab -> opaque -> unit
-val dump : opaquetab ->
- Constr.t Future.computation array *
- Univ.ContextSet.t Future.computation array *
+val dump : ?except:Future.UUIDSet.t -> opaquetab ->
+ Constr.t option array *
+ Univ.ContextSet.t option array *
cooking_info list array *
int Future.UUIDMap.t
@@ -73,7 +73,7 @@ val dump : opaquetab ->
*)
val set_indirect_opaque_accessor :
- (DirPath.t -> int -> constr Future.computation) -> unit
+ (DirPath.t -> int -> constr option) -> unit
val set_indirect_univ_accessor :
- (DirPath.t -> int -> Univ.ContextSet.t Future.computation option) -> unit
+ (DirPath.t -> int -> Univ.ContextSet.t option) -> unit
diff --git a/library/library.ml b/library/library.ml
index 9f4eb531ed..3bc2e84054 100644
--- a/library/library.ml
+++ b/library/library.ml
@@ -276,8 +276,8 @@ let in_import_library : DirPath.t list * bool -> obj =
(** Delayed / available tables of opaque terms *)
type 'a table_status =
- | ToFetch of 'a Future.computation array delayed
- | Fetched of 'a Future.computation array
+ | ToFetch of 'a option array delayed
+ | Fetched of 'a option array
let opaque_tables =
ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t)
@@ -315,7 +315,7 @@ let access_opaque_table dp i =
let access_univ_table dp i =
try
let what = "universe contexts of opaque proofs" in
- Some (access_table what univ_tables dp i)
+ access_table what univ_tables dp i
with Not_found -> None
let () =
@@ -328,9 +328,9 @@ let () =
type seg_sum = summary_disk
type seg_lib = library_disk
type seg_univ = (* true = vivo, false = vi *)
- Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+ Univ.ContextSet.t option array * Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr option array
let mk_library sd md digests univs =
{
@@ -590,7 +590,7 @@ let save_library_to ?todo ~output_native_objects dir f otab =
List.fold_left (fun e (r,_) -> Future.UUIDSet.add r.Stateid.uuid e)
Future.UUIDSet.empty l in
let cenv, seg, ast = Declaremods.end_library ~output_native_objects ~except dir in
- let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump otab in
+ let opaque_table, univ_table, disch_table, f2t_map = Opaqueproof.dump ~except otab in
let tasks, utab, dtab =
match todo with
| None -> None, None, None
@@ -603,16 +603,6 @@ let save_library_to ?todo ~output_native_objects dir f otab =
Some (tasks,rcbackup),
Some (univ_table,Univ.ContextSet.empty,false),
Some disch_table in
- let except =
- Future.UUIDSet.fold (fun uuid acc ->
- try Int.Set.add (Future.UUIDMap.find uuid f2t_map) acc
- with Not_found -> acc)
- except Int.Set.empty in
- let is_done_or_todo i x = Future.is_val x || Int.Set.mem i except in
- Array.iteri (fun i x ->
- if not(is_done_or_todo i x) then CErrors.user_err ~hdr:"library"
- Pp.(str"Proof object "++int i++str" is not checked nor to be checked"))
- opaque_table;
let sd = {
md_name = dir;
md_deps = Array.of_list (current_deps ());
diff --git a/library/library.mli b/library/library.mli
index f3186d847f..d2b0c4f202 100644
--- a/library/library.mli
+++ b/library/library.mli
@@ -34,9 +34,9 @@ val require_library_from_dirpath
type seg_sum
type seg_lib
type seg_univ = (* cst, all_cst, finished? *)
- Univ.ContextSet.t Future.computation array * Univ.ContextSet.t * bool
+ Univ.ContextSet.t option array * Univ.ContextSet.t * bool
type seg_discharge = Opaqueproof.cooking_info list array
-type seg_proofs = Constr.constr Future.computation array
+type seg_proofs = Constr.constr 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 9e9d23ba93..30cf8a0622 100644
--- a/stm/stm.ml
+++ b/stm/stm.ml
@@ -1846,13 +1846,8 @@ end = struct (* {{{ *)
let pr = map (Option.get (Global.body_of_constant_body c)) in
let pr = discharge pr in
let pr = Constr.hcons pr in
- let return c =
- let fc = Future.from_val c in
- let _ = Future.join fc in
- fc
- in
- u.(bucket) <- return uc;
- p.(bucket) <- return pr;
+ u.(bucket) <- Some uc;
+ p.(bucket) <- Some pr;
u, 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 12:50:29 +0000