From 7cfc4e5146be5666419451bdd516f1f3f264d24a Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Sun, 25 Jan 2015 14:42:51 +0100 Subject: Imported Upstream version 8.5~beta1+dfsg --- checker/check.ml | 224 ++++++++++++++++++++++++++++++++++--------------------- 1 file changed, 141 insertions(+), 83 deletions(-) (limited to 'checker/check.ml') diff --git a/checker/check.ml b/checker/check.ml index 85ee28db..9a750858 100644 --- a/checker/check.ml +++ b/checker/check.ml @@ -1,31 +1,32 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* failwith "path_of_dirpath" | l::dir -> - {dirpath=List.map string_of_id dir;basename=string_of_id l} + {dirpath=List.map Id.to_string dir;basename=Id.to_string l} let pr_dirlist dp = prlist_with_sep (fun _ -> str".") str (List.rev dp) let pr_path sp = @@ -33,37 +34,26 @@ let pr_path sp = [] -> str sp.basename | sl -> pr_dirlist sl ++ str"." ++ str sp.basename -type library_objects - -type compilation_unit_name = dir_path - -type library_disk = { - md_name : compilation_unit_name; - md_compiled : Safe_typing.LightenLibrary.lightened_compiled_library; - md_objects : library_objects; - md_deps : (compilation_unit_name * Digest.t) list; - md_imports : compilation_unit_name list } - (************************************************************************) -(*s Modules on disk contain the following informations (after the magic - number, and before the digest). *) (*s Modules loaded in memory contain the following informations. They are kept in the global table [libraries_table]. *) type library_t = { - library_name : compilation_unit_name; - library_filename : System.physical_path; - library_compiled : Safe_typing.compiled_library; - library_deps : (compilation_unit_name * Digest.t) list; - library_digest : Digest.t } + library_name : Cic.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_extra_univs : Univ.constraints } module LibraryOrdered = struct - type t = dir_path + type t = DirPath.t let compare d1 d2 = Pervasives.compare - (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) + (List.rev (DirPath.repr d1)) (List.rev (DirPath.repr d2)) end module LibrarySet = Set.Make(LibraryOrdered) @@ -80,7 +70,7 @@ let find_library dir = let try_find_library dir = try find_library dir with Not_found -> - error ("Unknown library " ^ (string_of_dirpath dir)) + error ("Unknown library " ^ (DirPath.to_string dir)) let library_full_filename dir = (find_library dir).library_filename @@ -90,6 +80,29 @@ let library_full_filename dir = (find_library dir).library_filename let register_loaded_library m = libraries_table := LibraryMap.add m.library_name m !libraries_table +(* Map from library names to table of opaque terms *) +let opaque_tables = ref LibraryMap.empty +let opaque_univ_tables = ref LibraryMap.empty + +let access_opaque_table dp i = + let t = + try LibraryMap.find dp !opaque_tables + with Not_found -> assert false + in + assert (i < Array.length t); + Future.force 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.empty_constraint + + +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 md = m.library_compiled in @@ -98,22 +111,23 @@ let check_one_lib admit (dir,m) = also check if it carries a validation certificate (yet to be implemented). *) if LibrarySet.mem dir admit then - (Flags.if_verbose msgnl + (Flags.if_verbose ppnl (str "Admitting library: " ++ pr_dirpath dir); - Safe_typing.unsafe_import file md dig) + Safe_typing.unsafe_import file md m.library_extra_univs dig) else - (Flags.if_verbose msgnl + (Flags.if_verbose ppnl (str "Checking library: " ++ pr_dirpath dir); - Safe_typing.import file md dig); - Flags.if_verbose msg(fnl()); + Safe_typing.import file md m.library_extra_univs dig); + Flags.if_verbose pp (fnl()); + pp_flush (); register_loaded_library m (*************************************************************************) (*s Load path. Mapping from physical to logical paths etc.*) -type logical_path = dir_path +type logical_path = DirPath.t -let load_paths = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([],[] : CUnix.physical_path list * logical_path list) let get_load_paths () = fst !load_paths @@ -147,20 +161,23 @@ let canonical_path_name p = let find_logical_path phys_dir = let phys_dir = canonical_path_name phys_dir in - match list_filter2 (fun p d -> p = phys_dir) !load_paths with + let physical, logical = !load_paths in + match List.filter2 (fun p d -> p = phys_dir) physical logical with | _,[dir] -> dir | _,[] -> default_root_prefix - | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) + | _,l -> anomaly (Pp.str ("Two logical paths are associated to "^phys_dir)) let remove_load_path dir = - load_paths := list_filter2 (fun p d -> p <> dir) !load_paths + let physical, logical = !load_paths in + load_paths := List.filter2 (fun p d -> p <> dir) physical logical let add_load_path (phys_path,coq_path) = if !Flags.debug then - msgnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ + ppnl (str "path: " ++ pr_dirpath coq_path ++ str " ->" ++ spc() ++ str phys_path); let phys_path = canonical_path_name phys_path in - match list_filter2 (fun p d -> p = phys_path) !load_paths with + let physical, logical = !load_paths in + match List.filter2 (fun p d -> p = phys_path) physical logical with | _,[dir] -> if coq_path <> dir (* If this is not the default -I . to coqtop *) @@ -171,7 +188,7 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> default_root_prefix then - Flags.if_warn msg_warning + msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); @@ -180,10 +197,11 @@ let add_load_path (phys_path,coq_path) = end | _,[] -> load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths) - | _ -> anomaly ("Two logical paths are associated to "^phys_path) + | _ -> anomaly (Pp.str ("Two logical paths are associated to "^phys_path)) let load_paths_of_dir_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_paths) + let physical, logical = !load_paths in + fst (List.filter2 (fun p d -> d = dir) physical logical) (************************************************************************) (*s Locate absolute or partially qualified library names in the path *) @@ -197,7 +215,7 @@ let locate_absolute_library dir = let loadpath = load_paths_of_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try - let name = string_of_id base^".vo" in + let name = Id.to_string base^".vo" in let _, file = System.where_in_path ~warn:false loadpath name in (dir, file) with Not_found -> @@ -220,7 +238,7 @@ let locate_qualified_library qid = let name = qid.basename^".vo" in let path, file = System.where_in_path loadpath name in let dir = - extend_dirpath (find_logical_path path) (id_of_string qid.basename) in + extend_dirpath (find_logical_path path) (Id.of_string qid.basename) in (* Look if loaded *) try (dir, library_full_filename dir) @@ -228,28 +246,29 @@ let locate_qualified_library qid = (dir, file) with Not_found -> raise LibNotFound -let explain_locate_library_error qid = function - | LibUnmappedDir -> - let prefix = qid.dirpath in - errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ - str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) - | LibNotFound -> - errorlabstrm "load_absolute_library_from" - (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") - | e -> raise e +let error_unmapped_dir qid = + let prefix = qid.dirpath in + errorlabstrm "load_absolute_library_from" + (str "Cannot load " ++ pr_path qid ++ str ":" ++ spc () ++ + str "no physical path bound to" ++ spc () ++ pr_dirlist prefix ++ fnl ()) + +let error_lib_not_found qid = + errorlabstrm "load_absolute_library_from" + (str"Cannot find library " ++ pr_path qid ++ str" in loadpath") let try_locate_absolute_library dir = try locate_absolute_library dir - with e -> - explain_locate_library_error (path_of_dirpath dir) e + with + | LibUnmappedDir -> error_unmapped_dir (path_of_dirpath dir) + | LibNotFound -> error_lib_not_found (path_of_dirpath dir) let try_locate_qualified_library qid = try locate_qualified_library qid - with e -> - explain_locate_library_error qid e + with + | LibUnmappedDir -> error_unmapped_dir qid + | LibNotFound -> error_lib_not_found qid (************************************************************************) (*s Low-level interning/externing of libraries to files *) @@ -257,7 +276,7 @@ let try_locate_qualified_library qid = (*s Loading from disk to cache (preparation phase) *) let raw_intern_library = - snd (System.raw_extern_intern Coq_config.vo_magic_number ".vo") + snd (System.raw_extern_intern Coq_config.vo_magic_number) let with_magic_number_check f a = try f a @@ -270,12 +289,16 @@ let with_magic_number_check f a = (************************************************************************) (* Internalise libraries *) -let mk_library md f table digest = { +open Cic + +let mk_library md f table digest cst = { library_name = md.md_name; library_filename = f; - library_compiled = Safe_typing.LightenLibrary.load table md.md_compiled; + library_compiled = md.md_compiled; + library_opaques = table; library_deps = md.md_deps; - library_digest = digest } + library_digest = digest; + library_extra_univs = cst } let name_clash_message dir mdir f = str ("The file " ^ f ^ " contains library") ++ spc () ++ @@ -286,22 +309,56 @@ let name_clash_message dir mdir f = let depgraph = ref LibraryMap.empty let intern_from_file (dir, f) = - Flags.if_verbose msg (str"[intern "++str f++str" ..."); - let (md,table,digest) = + Flags.if_verbose pp (str"[intern "++str f++str" ..."); pp_flush (); + let (md,table,opaque_csts,digest) = try let ch = with_magic_number_check raw_intern_library f in - let (md:library_disk) = System.marshal_in f ch in - let digest = System.marshal_in f ch in - let table = (System.marshal_in f ch : Safe_typing.LightenLibrary.table) in - close_in ch; + let (md:Cic.library_disk), _, digest = 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 + let (table:Cic.opaque_table), pos, checksum = + System.marshal_in_segment f ch in + (* Verification of the final checksum *) + let () = close_in ch in + let ch = open_in f in + 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 - errorlabstrm "load_physical_library" + errorlabstrm "intern_from_file" (name_clash_message dir md.md_name f); - Flags.if_verbose msgnl(str" done]"); - md,table,digest - with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in + if tasks <> None || discharging <> None then + errorlabstrm "intern_from_file" + (str "The file "++str f++str " contains unfinished tasks"); + if opaque_csts <> None then begin + pp (str " (was a vio file) "); + Option.iter (fun (_,_,b) -> if not b then + errorlabstrm "intern_from_file" + (str "The file "++str f++str " is still a .vio")) + opaque_csts; + Validate.validate !Flags.debug Values.v_univopaques opaque_csts; + end; + (* Verification of the unmarshalled values *) + 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 + with e -> Flags.if_verbose ppnl (str" failed!]"); raise e in depgraph := LibraryMap.add md.md_name md.md_deps !depgraph; - mk_library md f table digest + opaque_tables := LibraryMap.add md.md_name table !opaque_tables; + Option.iter (fun (opaque_csts,_,_) -> + opaque_univ_tables := + LibraryMap.add md.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 let get_deps (dir, f) = try LibraryMap.find dir !depgraph @@ -317,14 +374,15 @@ let rec intern_library seen (dir, f) needed = try let _ = find_library dir in needed with Not_found -> (* Look if already listed and consequently its dependencies too *) - if List.mem_assoc dir needed then needed + if List.mem_assoc_f DirPath.equal dir needed then needed else (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file (dir,f) in let seen' = LibrarySet.add dir seen in let deps = - List.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps in - (dir,m) :: List.fold_right (intern_library seen') deps needed + Array.map (fun (d,_) -> try_locate_absolute_library d) m.library_deps + in + (dir,m) :: Array.fold_right (intern_library seen') deps needed (* Compute the reflexive transitive dependency closure *) let rec fold_deps seen ff (dir,f) (s,acc) = @@ -332,9 +390,9 @@ let rec fold_deps seen ff (dir,f) (s,acc) = if LibrarySet.mem dir s then (s,acc) else let deps = get_deps (dir,f) in - let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in + let deps = Array.map (fun (d,_) -> try_locate_absolute_library d) deps in let seen' = LibrarySet.add dir seen in - let (s',acc') = List.fold_right (fold_deps seen' ff) deps (s,acc) in + let (s',acc') = Array.fold_right (fold_deps seen' ff) deps (s,acc) in (LibrarySet.add dir s', ff dir acc') and fold_deps_list seen ff modl needed = @@ -358,14 +416,14 @@ let recheck_library ~norec ~admit ~check = let nochk = List.fold_right LibrarySet.remove (List.map fst (nrl@ml)) nochk in (* *) - Flags.if_verbose msgnl (fnl()++hv 2 (str "Ordered list:" ++ fnl() ++ + Flags.if_verbose ppnl (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 msgnl(str"Modules were successfully checked") + Flags.if_verbose ppnl (str"Modules were successfully checked") open Printf let mem s = let m = try_find_library s in - h 0 (str (sprintf "%dk" (size_kb m))) + h 0 (str (sprintf "%dk" (CObj.size_kb m))) -- cgit v1.2.3