diff options
Diffstat (limited to 'checker/check.ml')
| -rw-r--r-- | checker/check.ml | 84 |
1 files changed, 52 insertions, 32 deletions
diff --git a/checker/check.ml b/checker/check.ml index 4bb485d29e..e3a4bda8ec 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -13,7 +13,7 @@ open CErrors open Util open Names -let chk_pp = Pp.pp_with Format.std_formatter +let chk_pp = Feedback.msg_notice let pr_dirpath dp = str (DirPath.to_string dp) let default_root_prefix = DirPath.empty @@ -48,13 +48,17 @@ let pr_path sp = (*s Modules loaded in memory contain the following informations. They are kept in the global table [libraries_table]. *) +type compilation_unit_name = DirPath.t + +type seg_proofs = Constr.constr Future.computation array + type library_t = { - library_name : Cic.compilation_unit_name; + library_name : compilation_unit_name; library_filename : CUnix.physical_path; - library_compiled : Cic.compiled_library; - library_opaques : Cic.opaque_table; - library_deps : Cic.library_deps; - library_digest : Cic.vodigest; + library_compiled : Safe_typing.compiled_library; + library_opaques : seg_proofs; + library_deps : (compilation_unit_name * Safe_typing.vodigest) array; + library_digest : Safe_typing.vodigest; library_extra_univs : Univ.ContextSet.t } module LibraryOrdered = @@ -94,35 +98,36 @@ let access_opaque_table dp i = with Not_found -> assert false in assert (i < Array.length t); - Future.force t.(i) + t.(i) let access_opaque_univ_table dp i = try let t = LibraryMap.find dp !opaque_univ_tables in assert (i < Array.length t); - Future.force t.(i) - with Not_found -> Univ.ContextSet.empty + Some t.(i) + with Not_found -> None +let () = + Opaqueproof.set_indirect_opaque_accessor access_opaque_table; + Opaqueproof.set_indirect_univ_accessor access_opaque_univ_table -let _ = Declarations.indirect_opaque_access := access_opaque_table -let _ = Declarations.indirect_opaque_univ_access := access_opaque_univ_table - -let check_one_lib admit (dir,m) = - let file = m.library_filename in +let check_one_lib admit senv (dir,m) = let md = m.library_compiled in let dig = m.library_digest in (* Look up if the library is to be admitted correct. We could also check if it carries a validation certificate (yet to be implemented). *) - if LibrarySet.mem dir admit then - (Flags.if_verbose Feedback.msg_notice - (str "Admitting library: " ++ pr_dirpath dir); - Safe_typing.unsafe_import file md m.library_extra_univs dig) - else - (Flags.if_verbose Feedback.msg_notice - (str "Checking library: " ++ pr_dirpath dir); - Safe_typing.import file md m.library_extra_univs dig); - register_loaded_library m + let senv = + if LibrarySet.mem dir admit then + (Flags.if_verbose Feedback.msg_notice + (str "Admitting library: " ++ pr_dirpath dir); + Safe_checking.unsafe_import senv md m.library_extra_univs dig) + else + (Flags.if_verbose Feedback.msg_notice + (str "Checking library: " ++ pr_dirpath dir); + Safe_checking.import senv md m.library_extra_univs dig) + in + register_loaded_library m; senv (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) @@ -284,7 +289,21 @@ let raw_intern_library f = (************************************************************************) (* Internalise libraries *) -open Cic +type summary_disk = { + md_name : compilation_unit_name; + md_imports : compilation_unit_name array; + md_deps : (compilation_unit_name * Safe_typing.vodigest) array; +} + +module Dyn = Dyn.Make () +type obj = Dyn.t (* persistent dynamic objects *) +type lib_objects = (Id.t * obj) list +type library_objects = lib_objects * lib_objects + +type library_disk = { + md_compiled : Safe_typing.compiled_library; + md_objects : library_objects; +} let mk_library sd md f table digest cst = { library_name = sd.md_name; @@ -317,12 +336,12 @@ let intern_from_file (dir, f) = let (sd,md,table,opaque_csts,digest) = try let ch = System.with_magic_number_check raw_intern_library f in - let (sd:Cic.summary_disk), _, digest = marshal_in_segment f ch in - let (md:Cic.library_disk), _, digest = marshal_in_segment f ch in + let (sd:summary_disk), _, digest = marshal_in_segment f ch in + let (md:library_disk), _, digest = marshal_in_segment f ch in let (opaque_csts:'a option), _, udg = marshal_in_segment f ch in let (discharging:'a option), _, _ = marshal_in_segment f ch in let (tasks:'a option), _, _ = marshal_in_segment f ch in - let (table:Cic.opaque_table), pos, checksum = + let (table:seg_proofs), pos, checksum = marshal_in_segment f ch in (* Verification of the final checksum *) let () = close_in ch in @@ -350,8 +369,8 @@ let intern_from_file (dir, f) = Validate.validate !Flags.debug Values.v_opaques table; Flags.if_verbose chk_pp (str" done]" ++ fnl ()); let digest = - if opaque_csts <> None then Cic.Dviovo (digest,udg) - else (Cic.Dvo digest) in + if opaque_csts <> None then Safe_typing.Dvivo (digest,udg) + else (Safe_typing.Dvo_or_vi digest) in sd,md,table,opaque_csts,digest with e -> Flags.if_verbose chk_pp (str" failed!]" ++ fnl ()); raise e in depgraph := LibraryMap.add sd.md_name sd.md_deps !depgraph; @@ -406,7 +425,7 @@ and fold_deps_list seen ff modl needed = let fold_deps_list ff modl acc = snd (fold_deps_list LibrarySet.empty ff modl (LibrarySet.empty,acc)) -let recheck_library ~norec ~admit ~check = +let recheck_library senv ~norec ~admit ~check = let ml = List.map try_locate_qualified_library check in let nrl = List.map try_locate_qualified_library norec in let al = List.map try_locate_qualified_library admit in @@ -424,5 +443,6 @@ let recheck_library ~norec ~admit ~check = Flags.if_verbose Feedback.msg_notice (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ prlist (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed)); - List.iter (check_one_lib nochk) needed; - Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked") + let senv = List.fold_left (check_one_lib nochk) senv needed in + Flags.if_verbose Feedback.msg_notice (str"Modules were successfully checked"); + senv |