diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 34 | ||||
| -rw-r--r-- | library/library.mli | 5 |
2 files changed, 18 insertions, 21 deletions
diff --git a/library/library.ml b/library/library.ml index e3b8511af1..1ac75d2fdc 100644 --- a/library/library.ml +++ b/library/library.ml @@ -276,11 +276,11 @@ let in_import_library : DirPath.t list * bool -> obj = (** Delayed / available tables of opaque terms *) type 'a table_status = - | ToFetch of 'a option array delayed - | Fetched of 'a option array + | ToFetch of 'a array delayed + | Fetched of 'a array let opaque_tables = - ref (LibraryMap.empty : (Constr.constr table_status) LibraryMap.t) + ref (LibraryMap.empty : ((Opaqueproof.cooking_info list * int * Constr.constr option) 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 (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) let indirect_accessor = { Opaqueproof.access_proof = access_opaque_table; + Opaqueproof.access_discharge = Cooking.cook_constr; } (************************************************************************) @@ -319,8 +323,7 @@ type seg_sum = summary_disk 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 = { @@ -344,7 +347,6 @@ let intern_from_file f = let ((lmd : seg_lib delayed), digest_lmd) = in_delayed f ch in let (univs : seg_univ option), _, digest_u = System.marshal_in_segment f ch in let _ = System.skip_in_segment f ch in - let _ = System.skip_in_segment f ch in let ((del_opaque : seg_proofs delayed),_) = in_delayed f ch in close_in ch; register_library_filename lsd.md_name f; @@ -527,15 +529,13 @@ let load_library_todo f = let (s0 : seg_sum), _, _ = System.marshal_in_segment f ch in let (s1 : seg_lib), _, _ = System.marshal_in_segment f ch in let (s2 : seg_univ option), _, _ = System.marshal_in_segment f ch in - let (s3 : seg_discharge option), _, _ = System.marshal_in_segment f ch in let tasks, _, _ = System.marshal_in_segment f ch in - let (s5 : seg_proofs), _, _ = System.marshal_in_segment f ch in + let (s4 : seg_proofs), _, _ = System.marshal_in_segment f ch in close_in ch; if tasks = None then user_err ~hdr:"restart" (str"not a .vio file"); if s2 = None then user_err ~hdr:"restart" (str"not a .vio file"); - if s3 = None then user_err ~hdr:"restart" (str"not a .vio file"); if snd (Option.get s2) then user_err ~hdr:"restart" (str"not a .vio file"); - s0, s1, Option.get s2, Option.get s3, Option.get tasks, s5 + s0, s1, Option.get s2, Option.get tasks, s4 (************************************************************************) (*s [save_library dir] ends library [dir] and save it to the disk. *) @@ -578,10 +578,10 @@ 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, disch_table, f2t_map = Opaqueproof.dump ~except otab in - let tasks, utab, dtab = + let opaque_table, f2t_map = Opaqueproof.dump ~except otab in + let tasks, utab = match todo with - | None -> None, None, None + | None -> None, None | Some (tasks, rcbackup) -> let tasks = List.map Stateid.(fun (r,b) -> @@ -589,8 +589,8 @@ let save_library_to ?todo ~output_native_objects dir f otab = with Not_found -> assert b; { r with uuid = -1 }, b) tasks in Some (tasks,rcbackup), - Some (Univ.ContextSet.empty,false), - Some disch_table in + Some (Univ.ContextSet.empty,false) + in let sd = { md_name = dir; md_deps = Array.of_list (current_deps ()); @@ -610,7 +610,6 @@ let save_library_to ?todo ~output_native_objects dir f otab = System.marshal_out_segment f' ch (sd : seg_sum); System.marshal_out_segment f' ch (md : seg_lib); System.marshal_out_segment f' ch (utab : seg_univ option); - System.marshal_out_segment f' ch (dtab : seg_discharge option); System.marshal_out_segment f' ch (tasks : 'tasks option); System.marshal_out_segment f' ch (opaque_table : seg_proofs); close_out ch; @@ -630,7 +629,6 @@ let save_library_raw f sum lib univs proofs = System.marshal_out_segment f ch (sum : seg_sum); System.marshal_out_segment f ch (lib : seg_lib); System.marshal_out_segment f ch (Some univs : seg_univ option); - System.marshal_out_segment f ch (None : seg_discharge option); System.marshal_out_segment f ch (None : 'tasks option); System.marshal_out_segment f ch (proofs : seg_proofs); close_out ch diff --git a/library/library.mli b/library/library.mli index 142206e2c5..727eca10cf 100644 --- a/library/library.mli +++ b/library/library.mli @@ -35,8 +35,7 @@ type seg_sum 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 *) @@ -51,7 +50,7 @@ val save_library_to : val load_library_todo : CUnix.physical_path - -> seg_sum * seg_lib * seg_univ * seg_discharge * 'tasks * seg_proofs + -> seg_sum * seg_lib * seg_univ * 'tasks * seg_proofs val save_library_raw : string -> seg_sum -> seg_lib -> seg_univ -> seg_proofs -> unit |