diff options
Diffstat (limited to 'checker')
| -rw-r--r-- | checker/check.ml | 26 | ||||
| -rw-r--r-- | checker/cic.mli | 10 | ||||
| -rw-r--r-- | checker/values.ml | 7 | ||||
| -rw-r--r-- | checker/votour.ml | 1 |
4 files changed, 27 insertions, 17 deletions
diff --git a/checker/check.ml b/checker/check.ml index 3e22c4b18..c835cec82 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -291,12 +291,12 @@ let with_magic_number_check f a = open Cic -let mk_library md f table digest cst = { - library_name = md.md_name; +let mk_library sd md f table digest cst = { + library_name = sd.md_name; library_filename = f; library_compiled = md.md_compiled; library_opaques = table; - library_deps = md.md_deps; + library_deps = sd.md_deps; library_digest = digest; library_extra_univs = cst } @@ -310,10 +310,11 @@ let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); - let (md,table,opaque_csts,digest) = + let (sd,md,table,opaque_csts,digest) = try let ch = with_magic_number_check raw_intern_library f in - let (md:Cic.library_disk), _, digest = System.marshal_in_segment f ch in + let (sd:Cic.summary_disk), _, digest = System.marshal_in_segment f ch in + let (md:Cic.library_disk), _, _ = System.marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = System.marshal_in_segment f ch in let (discharging:'a option), _, _ = System.marshal_in_segment f ch in let (tasks:'a option), _, _ = System.marshal_in_segment f ch in @@ -325,9 +326,9 @@ let intern_from_file (dir, f) = if not (String.equal (Digest.channel ch pos) checksum) then errorlabstrm "intern_from_file" (str "Checksum mismatch"); let () = close_in ch in - if dir <> md.md_name then + if dir <> sd.md_name then errorlabstrm "intern_from_file" - (name_clash_message dir md.md_name f); + (name_clash_message dir sd.md_name f); if tasks <> None || discharging <> None then errorlabstrm "intern_from_file" (str "The file "++str f++str " contains unfinished tasks"); @@ -340,25 +341,26 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_univopaques opaque_csts; end; (* Verification of the unmarshalled values *) + Validate.validate !Flags.debug Values.v_libsum sd; Validate.validate !Flags.debug Values.v_lib md; Validate.validate !Flags.debug Values.v_opaques table; Flags.if_verbose ppnl (str" done]"); pp_flush (); let digest = if opaque_csts <> None then Cic.Dviovo (digest,udg) else (Cic.Dvo digest) in - md,table,opaque_csts,digest + sd,md,table,opaque_csts,digest with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in - depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; - opaque_tables := LibraryMap.add md.md_name table !opaque_tables; + depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; + opaque_tables := LibraryMap.add sd.md_name table !opaque_tables; Option.iter (fun (opaque_csts,_,_) -> opaque_univ_tables := - LibraryMap.add md.md_name opaque_csts !opaque_univ_tables) + LibraryMap.add sd.md_name opaque_csts !opaque_univ_tables) opaque_csts; let extra_cst = Option.default Univ.empty_constraint (Option.map (fun (_,cs,_) -> Univ.ContextSet.constraints cs) opaque_csts) in - mk_library md f table digest extra_cst + mk_library sd md f table digest extra_cst let get_deps (dir, f) = try LibraryMap.find dir !depgraph diff --git a/checker/cic.mli b/checker/cic.mli index 90a0e9feb..e875e40f0 100644 --- a/checker/cic.mli +++ b/checker/cic.mli @@ -417,12 +417,16 @@ type compiled_library = { type library_objects -type library_disk = { +type summary_disk = { md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : library_deps; +} + +type library_disk = { md_compiled : compiled_library; md_objects : library_objects; - md_deps : library_deps; - md_imports : compilation_unit_name array } +} type opaque_table = constr Future.computation array type univ_table = diff --git a/checker/values.ml b/checker/values.ml index cf93466b0..b2d74821d 100644 --- a/checker/values.ml +++ b/checker/values.ml @@ -13,7 +13,7 @@ To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli with a copy we maintain here: -MD5 0a174243f8b06535c9eecbbe8d339fe1 checker/cic.mli +MD5 f5fd749af797e08efee22122742bc740 checker/cic.mli *) @@ -350,8 +350,11 @@ let v_stm_seg = v_pair v_tasks v_counters (** Toplevel structures in a vo (see Cic.mli) *) +let v_libsum = + Tuple ("summary", [|v_dp;Array v_dp;v_deps|]) + let v_lib = - Tuple ("library",[|v_dp;v_compiled_lib;v_libraryobjs;v_deps;Array v_dp|]) + Tuple ("library",[|v_compiled_lib;v_libraryobjs|]) let v_opaques = Array (v_computation v_constr) let v_univopaques = diff --git a/checker/votour.ml b/checker/votour.ml index 01965bb4b..bb8e06702 100644 --- a/checker/votour.ml +++ b/checker/votour.ml @@ -249,6 +249,7 @@ let visit_vo f = Printf.printf "At prompt, <n> enters the <n>-th child, u goes up 1 level, x exits\n\n%!"; let segments = [| + make_seg "summary" Values.v_libsum; make_seg "library" Values.v_lib; make_seg "univ constraints of opaque proofs" Values.v_univopaques; make_seg "discharging info" (Opt Any); |