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)))