diff options
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 117 |
1 files changed, 56 insertions, 61 deletions
diff --git a/library/library.ml b/library/library.ml index 2c6d02ae..d066ff89 100644 --- a/library/library.ml +++ b/library/library.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: library.ml 13175 2010-06-22 06:28:37Z herbelin $ *) +(* $Id$ *) open Pp open Util @@ -39,7 +39,7 @@ let is_in_load_paths phys_dir = let dir = System.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 + List.exists check_p lp let remove_load_path dir = load_paths := List.filter (fun (p,d,_) -> p <> dir) !load_paths @@ -48,7 +48,7 @@ let add_load_path isroot (phys_path,coq_path) = let phys_path = System.canonical_path_name phys_path in match List.filter (fun (p,d,_) -> p = phys_path) !load_paths with | [_,dir,_] -> - if coq_path <> dir + if coq_path <> dir (* If this is not the default -I . to coqtop *) && not (phys_path = System.canonical_path_name Filename.current_dir_name @@ -71,7 +71,7 @@ let add_load_path isroot (phys_path,coq_path) = let physical_paths (dp,lp) = dp let extend_path_with_dirpath p dir = - List.fold_left Filename.concat p + List.fold_left Filename.concat p (List.map string_of_id (List.rev (repr_dirpath dir))) let root_paths_matching_dir_path dir = @@ -112,12 +112,12 @@ let loadpaths_matching_dir_path dir = let get_full_load_paths () = List.map (fun (a,b,c) -> (a,b)) !load_paths (************************************************************************) -(*s Modules on disk contain the following informations (after the magic +(*s Modules on disk contain the following informations (after the magic number, and before the digest). *) type compilation_unit_name = dir_path -type library_disk = { +type library_disk = { md_name : compilation_unit_name; md_compiled : compiled_library; md_objects : Declaremods.library_objects; @@ -135,7 +135,7 @@ type library_t = { library_imports : compilation_unit_name list; library_digest : Digest.t } -module LibraryOrdered = +module LibraryOrdered = struct type t = dir_path let compare d1 d2 = @@ -164,7 +164,7 @@ let freeze () = !libraries_imports_list, !libraries_exports_list -let unfreeze (mt,mo,mi,me) = +let unfreeze (mt,mo,mi,me) = libraries_table := mt; libraries_loaded_list := mo; libraries_imports_list := mi; @@ -176,13 +176,11 @@ let init () = libraries_imports_list := []; libraries_exports_list := [] -let _ = +let _ = Summary.declare_summary "MODULES" { Summary.freeze_function = freeze; Summary.unfreeze_function = unfreeze; - Summary.init_function = init; - Summary.survive_module = false; - Summary.survive_section = false } + Summary.init_function = init } (* various requests to the tables *) @@ -197,7 +195,7 @@ let try_find_library dir = let register_library_filename dir f = (* Not synchronized: overwrite the previous binding if one existed *) (* from a previous play of the session *) - libraries_filename_table := + libraries_filename_table := LibraryFilenameMap.add dir f !libraries_filename_table let library_full_filename dir = @@ -214,13 +212,13 @@ let library_is_loaded dir = try let _ = find_library dir in true with Not_found -> false -let library_is_opened dir = +let library_is_opened dir = List.exists (fun m -> m.library_name = dir) !libraries_imports_list let library_is_exported dir = List.exists (fun m -> m.library_name = dir) !libraries_exports_list -let loaded_libraries () = +let loaded_libraries () = List.map (fun m -> m.library_name) !libraries_loaded_list let opened_libraries () = @@ -251,7 +249,7 @@ let rec remember_last_of_each l m = let register_open_library export m = libraries_imports_list := remember_last_of_each !libraries_imports_list m; - if export then + if export then libraries_exports_list := remember_last_of_each !libraries_exports_list m (************************************************************************) @@ -273,14 +271,14 @@ let open_library export explicit_libs m = Declaremods.really_import_module (MPfile m.library_name) end else - if export then + if export then libraries_exports_list := remember_last_of_each !libraries_exports_list m -(* open_libraries recursively open a list of libraries but opens only once +(* open_libraries recursively open a list of libraries but opens only once a library that is re-exported many times *) let open_libraries export modl = - let to_open_list = + let to_open_list = List.fold_left (fun l m -> let subimport = @@ -301,19 +299,16 @@ let open_import i (_,(dir,export)) = (* if not (library_is_opened dir) then *) open_libraries export [try_find_library dir] -let cache_import obj = +let cache_import obj = open_import 1 obj -let subst_import (_,_,o) = o +let subst_import (_,o) = o -let export_import o = Some o - -let classify_import (_,(_,export as obj)) = +let classify_import (_,export as obj) = if export then Substitute obj else Dispose - let (in_import, out_import) = - declare_object {(default_object "IMPORT LIBRARY") with + declare_object {(default_object "IMPORT LIBRARY") with cache_function = cache_import; open_function = open_import; subst_function = subst_import; @@ -359,7 +354,7 @@ let locate_qualified_library warn qid = if loadpath = [] then raise LibUnmappedDir; let name = string_of_id base ^ ".vo" in let lpath, file = System.where_in_path ~warn (List.map fst loadpath) name in - let dir = extend_dirpath (List.assoc lpath loadpath) base in + let dir = add_dirpath_suffix (List.assoc lpath loadpath) base in (* Look if loaded *) if library_is_loaded dir then (LibLoaded, dir, library_full_filename dir) (* Otherwise, look for it in the file system *) @@ -370,7 +365,7 @@ let explain_locate_library_error qid = function | LibUnmappedDir -> let prefix, _ = repr_qualid qid in errorlabstrm "load_absolute_library_from" - (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ + (str "Cannot load " ++ pr_qualid qid ++ str ":" ++ spc () ++ str "no physical path bound to" ++ spc () ++ pr_dirpath prefix ++ fnl ()) | LibNotFound -> errorlabstrm "load_absolute_library_from" @@ -387,14 +382,14 @@ let try_locate_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library (Flags.is_verbose()) qid in dir,f - with e -> + with e -> explain_locate_library_error qid e (************************************************************************) (* Internalise libraries *) -let lighten_library m = +let lighten_library m = if !Flags.dont_load_proofs then lighten_library m else m let mk_library md digest = { @@ -458,7 +453,7 @@ let rec_intern_by_filename_only id f = (* We check no other file containing same library is loaded *) if library_is_loaded m.library_name then begin - Flags.if_verbose warning + Flags.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ library_full_filename m.library_name); m.library_name, [] @@ -470,15 +465,15 @@ let rec_intern_by_filename_only id f = let rec_intern_library_from_file idopt f = (* A name is specified, we have to check it contains library id *) let paths = get_load_paths () in - let _, f = + let _, f = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".vo") in rec_intern_by_filename_only idopt f (**********************************************************************) -(*s [require_library] loads and possibly opens a library. This is a +(*s [require_library] loads and possibly opens a library. This is a synchronized operation. It is performed as follows: - preparation phase: (functions require_library* ) the library and its + preparation phase: (functions require_library* ) the library and its dependencies are read from to disk (using intern_* ) [they are read from disk to ensure that at section/module discharging time, the physical library referred to outside the @@ -486,8 +481,8 @@ let rec_intern_library_from_file idopt f = the section/module] execution phase: (through add_leaf and cache_require) - the library is loaded in the environment and Nametab, the objects are - registered etc, using functions from Declaremods (via load_library, + the library is loaded in the environment and Nametab, the objects are + registered etc, using functions from Declaremods (via load_library, which recursively loads its dependencies) *) @@ -495,14 +490,14 @@ type library_reference = dir_path list * bool option let register_library (dir,m) = Declaremods.register_library - m.library_name - m.library_compiled - m.library_objects + m.library_name + m.library_compiled + m.library_objects m.library_digest; register_loaded_library m (* Follow the semantics of Anticipate object: - - called at module or module type closing when a Require occurs in + - called at module or module type closing when a Require occurs in the module or module type - not called from a library (i.e. a module identified with a file) *) let load_require _ (_,(needed,modl,_)) = @@ -517,22 +512,17 @@ let cache_require o = load_require 1 o; open_require 1 o - (* keeps the require marker for closed section replay but removes - OS dependent fields from .vo files for cross-platform compatibility *) -let export_require (_,l,e) = Some ([],l,e) - let discharge_require (_,o) = Some o -(* open_function is never called from here because an Anticipate object *) +(* open_function is never called from here because an Anticipate object *) let (in_require, out_require) = declare_object {(default_object "REQUIRE") with cache_function = cache_require; load_function = load_require; open_function = (fun _ _ -> assert false); - export_function = export_require; discharge_function = discharge_require; - classify_function = (fun (_,o) -> Anticipate o) } + classify_function = (fun o -> Anticipate o) } (* Require libraries, import them if [export <> None], mark them for export if [export = Some true] *) @@ -540,11 +530,10 @@ let (in_require, out_require) = let xml_require = ref (fun d -> ()) let set_xml_require f = xml_require := f -let require_library qidl export = - let modrefl = List.map try_locate_qualified_library qidl in +let require_library_from_dirpath modrefl export = let needed = List.rev (List.fold_left rec_intern_library [] modrefl) in let modrefl = List.map fst modrefl in - if Lib.is_modtype () || Lib.is_module () then + if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> @@ -556,6 +545,10 @@ let require_library qidl export = if !Flags.xml_export then List.iter !xml_require modrefl; add_frozen_state () +let require_library qidl export = + let modrefl = List.map try_locate_qualified_library qidl in + require_library_from_dirpath modrefl export + let require_library_from_file idopt file export = let modref,needed = rec_intern_library_from_file idopt file in let needed = List.rev needed in @@ -574,7 +567,7 @@ let require_library_from_file idopt file export = let import_module export (loc,qid) = try match Nametab.locate_module qid with - | MPfile dir -> + | MPfile dir -> if Lib.is_modtype () || Lib.is_module () || not export then add_anonymous_leaf (in_import (dir, export)) else @@ -586,23 +579,25 @@ let import_module export (loc,qid) = user_err_loc (loc,"import_library", str ((string_of_qualid qid)^" is not a module")) - + (************************************************************************) (*s Initializing the compilation of a library. *) -let check_coq_overwriting p = +let check_coq_overwriting p id = let l = repr_dirpath p in if not !Flags.boot && l <> [] && string_of_id (list_last l) = "Coq" then - errorlabstrm "" (strbrk ("Name "^string_of_dirpath p^" starts with prefix \"Coq\" which is reserved for the Coq library.")) + errorlabstrm "" + (strbrk ("Cannot build module "^string_of_dirpath p^"."^string_of_id id^ + ": it starts with prefix \"Coq\" which is reserved for the Coq library.")) -let start_library f = +let start_library f = let paths = get_load_paths () in let _,longf = System.find_file_in_path ~warn:(Flags.is_verbose()) paths (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in - check_coq_overwriting ldir0; let id = id_of_string (Filename.basename f) in - let ldir = extend_dirpath ldir0 id in + check_coq_overwriting ldir0 id; + let ldir = add_dirpath_suffix ldir0 id in Declaremods.start_library ldir; ldir,longf @@ -617,15 +612,15 @@ let current_reexports () = let error_recursively_dependent_library dir = errorlabstrm "" - (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ + (strbrk "Unable to use logical name " ++ pr_dirpath dir ++ strbrk " to save current library because" ++ strbrk " it already depends on a library of this name.") (* Security weakness: file might have been changed on disk between - writing the content and computing the checksum... *) + writing the content and computing the checksum... *) let save_library_to dir f = let cenv, seg = Declaremods.end_library dir in - let md = { + let md = { md_name = dir; md_compiled = cenv; md_objects = seg; @@ -650,5 +645,5 @@ open Printf let mem s = let m = try_find_library s in h 0 (str (sprintf "%dk (cenv = %dk / seg = %dk)" - (size_kb m) (size_kb m.library_compiled) + (size_kb m) (size_kb m.library_compiled) (size_kb m.library_objects))) |