From b245a6c46bc3ef70142e8a165f6cde54265b941e Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Mon, 20 May 2019 11:51:31 +0200 Subject: Statically ensure the content of delayed proofs in vio file. Before, we would store futures, but it was actually ensured by the upper layers that they were either evaluated or stored by the STM somewhere else. We simply replace this type with an option, thus removing the Future.computation type from vo/vio files. This also enhances debug printing, as the latter is unable to properly print futures. --- library/library.ml | 22 ++++++---------------- library/library.mli | 4 ++-- 2 files changed, 8 insertions(+), 18 deletions(-) (limited to 'library') 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 *) -- cgit v1.2.3 From 2fa3dc389a58ca4a390b99995d82e6c089add163 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 21 May 2019 19:00:28 +0200 Subject: Move body_of_constant_body to Global and specialize its uses. This function is breaking the indirect opaque abstraction, so we move it outside of the kernel. Unluckily, there is no better place to put it, so we leave it in Global. The checker uses it in a fundamental way, so we reimplement it there, but this will eventually get removed. --- library/global.ml | 11 +++++++++++ 1 file changed, 11 insertions(+) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 58e2380440..827b062725 100644 --- a/library/global.ml +++ b/library/global.ml @@ -132,6 +132,17 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) +let body_of_constant_body env cb = + let open Declarations in + let otab = Environ.opaque_tables env in + match cb.const_body with + | Undef _ | Primitive _ -> + None + | Def c -> + Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) + | OpaqueDef o -> + Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + let body_of_constant_body ce = body_of_constant_body (env ()) ce let body_of_constant cst = body_of_constant_body (lookup_constant cst) -- cgit v1.2.3 From d3c931cd8c84d1b7d9d5763e20221d51700f0709 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 21 May 2019 19:22:30 +0200 Subject: Remove the indirect opaque accessor hooks from Opaqueproof. We simply pass them as arguments, now that they are not called by the kernel anymore. The checker definitely needs to access the opaque proofs. In order not to touch the API at all, I added a hook there, but it could also be provided as an additional argument, at the cost of changing all the upwards callers. --- library/global.ml | 8 ++++---- library/global.mli | 4 ++-- library/library.ml | 7 ++++--- library/library.mli | 3 +++ 4 files changed, 13 insertions(+), 9 deletions(-) (limited to 'library') diff --git a/library/global.ml b/library/global.ml index 827b062725..d5ffae7716 100644 --- a/library/global.ml +++ b/library/global.ml @@ -132,7 +132,7 @@ let exists_objlabel id = Safe_typing.exists_objlabel id (safe_env ()) let opaque_tables () = Environ.opaque_tables (env ()) -let body_of_constant_body env cb = +let body_of_constant_body access env cb = let open Declarations in let otab = Environ.opaque_tables env in match cb.const_body with @@ -141,11 +141,11 @@ let body_of_constant_body env cb = | Def c -> Some (Mod_subst.force_constr c, Declareops.constant_polymorphic_context cb) | OpaqueDef o -> - Some (Opaqueproof.force_proof otab o, Declareops.constant_polymorphic_context cb) + Some (Opaqueproof.force_proof access otab o, Declareops.constant_polymorphic_context cb) -let body_of_constant_body ce = body_of_constant_body (env ()) ce +let body_of_constant_body access ce = body_of_constant_body access (env ()) ce -let body_of_constant cst = body_of_constant_body (lookup_constant cst) +let body_of_constant access cst = body_of_constant_body access (lookup_constant cst) (** Operations on kernel names *) diff --git a/library/global.mli b/library/global.mli index 984d8c666c..aa9fc18477 100644 --- a/library/global.mli +++ b/library/global.mli @@ -100,13 +100,13 @@ val mind_of_delta_kn : KerName.t -> MutInd.t val opaque_tables : unit -> Opaqueproof.opaquetab -val body_of_constant : Constant.t -> (Constr.constr * Univ.AUContext.t) option +val body_of_constant : Opaqueproof.indirect_accessor -> Constant.t -> (Constr.constr * 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.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 * 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 3bc2e84054..039124635e 100644 --- a/library/library.ml +++ b/library/library.ml @@ -318,9 +318,10 @@ let access_univ_table dp i = access_table what univ_tables dp i with Not_found -> None -let () = - Opaqueproof.set_indirect_opaque_accessor access_opaque_table; - Opaqueproof.set_indirect_univ_accessor access_univ_table +let indirect_accessor = { + Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_constraints = access_univ_table; +} (************************************************************************) (* Internalise libraries *) diff --git a/library/library.mli b/library/library.mli index d2b0c4f202..2c0673c3b1 100644 --- a/library/library.mli +++ b/library/library.mli @@ -73,3 +73,6 @@ val overwrite_library_filenames : string -> unit (** {6 Native compiler. } *) val native_name_from_filename : string -> string + +(** {6 Opaque accessors} *) +val indirect_accessor : Opaqueproof.indirect_accessor -- cgit v1.2.3