summaryrefslogtreecommitdiff
path: root/checker/check.ml
diff options
context:
space:
mode:
Diffstat (limited to 'checker/check.ml')
-rw-r--r--checker/check.ml376
1 files changed, 376 insertions, 0 deletions
diff --git a/checker/check.ml b/checker/check.ml
new file mode 100644
index 00000000..f8844975
--- /dev/null
+++ b/checker/check.ml
@@ -0,0 +1,376 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(* $Id: library.ml 9679 2007-02-24 15:22:07Z herbelin $ *)
+
+open Pp
+open Util
+open Names
+
+let pr_id id = str (string_of_id id)
+let pr_dirpath dp = str (string_of_dirpath dp)
+let default_root_prefix = make_dirpath []
+let split_dirpath d =
+ let l = repr_dirpath d in (make_dirpath (List.tl l), List.hd l)
+let extend_dirpath p id = make_dirpath (id :: repr_dirpath p)
+
+type section_path = {
+ dirpath : string list ;
+ basename : string }
+let dir_of_path p =
+ make_dirpath
+ (id_of_string p.basename :: List.map id_of_string p.dirpath)
+let path_of_dirpath dir =
+ match repr_dirpath dir with
+ [] -> failwith "path_of_dirpath"
+ | l::dir ->
+ {dirpath=List.map string_of_id dir;basename=string_of_id l}
+let pr_dirlist dp =
+ prlist_with_sep (fun _ -> str".") str (List.rev dp)
+let pr_path sp =
+ match sp.dirpath with
+ [] -> 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.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 }
+
+module LibraryOrdered =
+ struct
+ type t = dir_path
+ let compare d1 d2 =
+ Pervasives.compare
+ (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2))
+ end
+
+module LibrarySet = Set.Make(LibraryOrdered)
+module LibraryMap = Map.Make(LibraryOrdered)
+
+(* This is a map from names to loaded libraries *)
+let libraries_table = ref LibraryMap.empty
+
+(* various requests to the tables *)
+
+let find_library dir =
+ LibraryMap.find dir !libraries_table
+
+let try_find_library dir =
+ try find_library dir
+ with Not_found ->
+ error ("Unknown library " ^ (string_of_dirpath dir))
+
+let library_full_filename dir = (find_library dir).library_filename
+
+ (* If a library is loaded several time, then the first occurrence must
+ be performed first, thus the libraries_loaded_list ... *)
+
+let register_loaded_library m =
+ libraries_table := LibraryMap.add m.library_name m !libraries_table
+
+let check_one_lib admit (dir,m) =
+ let file = m.library_filename in
+ 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 msgnl
+ (str "Admitting library: " ++ pr_dirpath dir);
+ Safe_typing.unsafe_import file md dig)
+ else
+ (Flags.if_verbose msgnl
+ (str "Checking library: " ++ pr_dirpath dir);
+ Safe_typing.import file md dig);
+ Flags.if_verbose msg(fnl());
+ register_loaded_library m
+
+(*************************************************************************)
+(*s Load path. Mapping from physical to logical paths etc.*)
+
+type logical_path = dir_path
+
+let load_paths = ref ([],[] : System.physical_path list * logical_path list)
+
+let get_load_paths () = fst !load_paths
+
+(* Hints to partially detects if two paths refer to the same repertory *)
+let rec remove_path_dot p =
+ let curdir = Filename.concat Filename.current_dir_name "" in (* Unix: "./" *)
+ let n = String.length curdir in
+ if String.length p > n && String.sub p 0 n = curdir then
+ remove_path_dot (String.sub p n (String.length p - n))
+ else
+ p
+
+let strip_path p =
+ let cwd = Filename.concat (Sys.getcwd ()) "" in (* Unix: "`pwd`/" *)
+ let n = String.length cwd in
+ if String.length p > n && String.sub p 0 n = cwd then
+ remove_path_dot (String.sub p n (String.length p - n))
+ else
+ remove_path_dot p
+
+let canonical_path_name p =
+ let current = Sys.getcwd () in
+ try
+ Sys.chdir p;
+ let p' = Sys.getcwd () in
+ Sys.chdir current;
+ p'
+ with Sys_error _ ->
+ (* We give up to find a canonical name and just simplify it... *)
+ strip_path 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
+ | _,[dir] -> dir
+ | _,[] -> default_root_prefix
+ | _,l -> anomaly ("Two logical paths are associated to "^phys_dir)
+
+let is_in_load_paths phys_dir =
+ let dir = canonical_path_name phys_dir in
+ let lp = get_load_paths () in
+ let check_p = fun p -> (String.compare dir p) == 0 in
+ List.exists check_p lp
+
+let remove_load_path dir =
+ load_paths := list_filter2 (fun p d -> p <> dir) !load_paths
+
+let add_load_path (phys_path,coq_path) =
+ let phys_path = canonical_path_name phys_path in
+ match list_filter2 (fun p d -> p = phys_path) !load_paths with
+ | _,[dir] ->
+ if coq_path <> dir
+ (* If this is not the default -I . to coqtop *)
+ && not
+ (phys_path = canonical_path_name Filename.current_dir_name
+ && coq_path = default_root_prefix)
+ then
+ begin
+ (* Assume the user is concerned by library naming *)
+ if dir <> default_root_prefix then
+ Flags.if_warn msg_warning
+ (str phys_path ++ strbrk " was previously bound to " ++
+ pr_dirpath dir ++ strbrk "; it is remapped to " ++
+ pr_dirpath coq_path);
+ remove_load_path phys_path;
+ load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths)
+ end
+ | _,[] ->
+ load_paths := (phys_path :: fst !load_paths, coq_path :: snd !load_paths)
+ | _ -> anomaly ("Two logical paths are associated to "^phys_path)
+
+let physical_paths (dp,lp) = dp
+
+let load_paths_of_dir_path dir =
+ fst (list_filter2 (fun p d -> d = dir) !load_paths)
+
+let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths)
+
+(************************************************************************)
+(*s Locate absolute or partially qualified library names in the path *)
+
+exception LibUnmappedDir
+exception LibNotFound
+
+let locate_absolute_library dir =
+ (* Search in loadpath *)
+ let pref, base = split_dirpath dir in
+ let loadpath = load_paths_of_dir_path pref in
+ if loadpath = [] then raise LibUnmappedDir;
+ try
+ let name = string_of_id base^".vo" in
+ let _, file = System.where_in_path loadpath name in
+ (dir, file)
+ with Not_found ->
+ (* Last chance, removed from the file system but still in memory *)
+ try
+ (dir, library_full_filename dir)
+ with Not_found ->
+ raise LibNotFound
+
+let locate_qualified_library qid =
+ try
+ let loadpath =
+ (* Search library in loadpath *)
+ if qid.dirpath=[] then get_load_paths ()
+ else
+ (* we assume dir is an absolute dirpath *)
+ load_paths_of_dir_path (dir_of_path qid)
+ in
+ if loadpath = [] then raise LibUnmappedDir;
+ 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
+ (* Look if loaded *)
+ try
+ (dir, library_full_filename dir)
+ with Not_found ->
+ (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 try_locate_absolute_library dir =
+ try
+ locate_absolute_library dir
+ with e ->
+ explain_locate_library_error (path_of_dirpath dir) e
+
+let try_locate_qualified_library qid =
+ try
+ locate_qualified_library qid
+ with e ->
+ explain_locate_library_error qid e
+
+(************************************************************************)
+(*s Low-level interning/externing of libraries to files *)
+
+(*s Loading from disk to cache (preparation phase) *)
+
+let vo_magic_number = 08190 (* trunk *)
+
+let (raw_extern_library, raw_intern_library) =
+ System.raw_extern_intern vo_magic_number ".vo"
+
+let with_magic_number_check f a =
+ try f a
+ with System.Bad_magic_number fname ->
+ errorlabstrm "with_magic_number_check"
+ (str"file " ++ str fname ++ spc () ++ str"has bad magic number." ++
+ spc () ++ str"It is corrupted" ++ spc () ++
+ str"or was compiled with another version of Coq.")
+
+(************************************************************************)
+(* Internalise libraries *)
+
+let mk_library md f digest = {
+ library_name = md.md_name;
+ library_filename = f;
+ library_compiled = md.md_compiled;
+ library_deps = md.md_deps;
+ library_digest = digest }
+
+let name_clash_message dir mdir f =
+ str ("The file " ^ f ^ " contains library") ++ spc () ++
+ pr_dirpath mdir ++ spc () ++ str "and not library" ++ spc() ++
+ pr_dirpath dir
+
+(* Dependency graph *)
+let depgraph = ref LibraryMap.empty
+
+let intern_from_file (dir, f) =
+ Flags.if_verbose msg (str"[intern "++str f++str" ...");
+ let (md,digest) =
+ try
+ let ch = with_magic_number_check raw_intern_library f in
+ let (md:library_disk) = System.marshal_in ch in
+ let digest = System.marshal_in ch in
+ close_in ch;
+ if dir <> md.md_name then
+ errorlabstrm "load_physical_library"
+ (name_clash_message dir md.md_name f);
+ Flags.if_verbose msgnl(str" done]");
+ md,digest
+ with e -> Flags.if_verbose msgnl(str" failed!]"); raise e in
+ depgraph := LibraryMap.add md.md_name md.md_deps !depgraph;
+ mk_library md f digest
+
+let get_deps (dir, f) =
+ try LibraryMap.find dir !depgraph
+ with Not_found ->
+ let _ = intern_from_file (dir,f) in
+ LibraryMap.find dir !depgraph
+
+(* Read a compiled library and all dependencies, in reverse order.
+ Do not include files that are already in the context. *)
+let rec intern_library (dir, f) needed =
+ (* Look if in the current logical environment *)
+ 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
+ else
+ (* [dir] is an absolute name which matches [f] which must be in loadpath *)
+ let m = intern_from_file (dir,f) in
+ (dir,m)::List.fold_right intern_mandatory_library m.library_deps needed
+
+(* digest error with checked modules could be a warning *)
+and intern_mandatory_library (dir,_) needed =
+ intern_library (try_locate_absolute_library dir) needed
+
+(* Compute the reflexive transitive dependency closure *)
+let rec fold_deps ff (dir,f) s =
+ if LibrarySet.mem dir s then s
+ else
+ let deps = get_deps (dir,f) in
+ let deps = List.map (fun (d,_) -> try_locate_absolute_library d) deps in
+ ff dir (List.fold_right (fold_deps ff) deps s)
+
+and fold_deps_list ff modl needed =
+ List.fold_right (fold_deps ff) modl needed
+
+let recheck_library ~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
+ let needed = List.rev (List.fold_right intern_library (ml@nrl) []) in
+ (* first compute the closure of norec, remove closure of check,
+ add closure of admit, and finally remove norec and check *)
+ let nochk = fold_deps_list LibrarySet.add nrl LibrarySet.empty in
+ let nochk = fold_deps_list LibrarySet.remove ml nochk in
+ let nochk = fold_deps_list LibrarySet.add al nochk in
+ (* explicitely required modules cannot be skipped... *)
+ 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() ++
+ prlist
+ (fun (dir,_) -> pr_dirpath dir ++ fnl()) needed));
+ List.iter (check_one_lib nochk) needed;
+ Flags.if_verbose msgnl(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)))
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-31 21:37:54 +0000