From a608c8e1bffa032ed67f6f2dd406017b6aca9eb9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Sun, 6 Feb 2005 13:03:51 +0000 Subject: Nettoyage et documentation de Library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6692 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.ml | 262 ++++++++++++++++++++++------------------------------ library/library.mli | 88 ++++++++---------- library/states.ml | 2 +- 3 files changed, 153 insertions(+), 199 deletions(-) (limited to 'library') diff --git a/library/library.ml b/library/library.ml index 388580eab..fee383233 100644 --- a/library/library.ml +++ b/library/library.ml @@ -25,9 +25,9 @@ open Declaremods type logical_path = dir_path -let load_path = ref ([],[] : System.physical_path list * logical_path list) +let load_paths = ref ([],[] : System.physical_path list * logical_path list) -let get_load_path () = fst !load_path +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 = @@ -60,17 +60,17 @@ 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_path with + match list_filter2 (fun p d -> p = phys_dir) !load_paths with | _,[dir] -> dir | _,[] -> Nameops.default_root_prefix | _,l -> anomaly ("Two logical paths are associated to "^phys_dir) -let remove_path dir = - load_path := list_filter2 (fun p d -> p <> dir) !load_path +let remove_load_path dir = + load_paths := list_filter2 (fun p d -> p <> dir) !load_paths -let add_load_path_entry (phys_path,coq_path) = +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_path with + 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 *) @@ -85,19 +85,19 @@ let add_load_path_entry (phys_path,coq_path) = ^(string_of_dirpath dir) ^("\nIt is remapped to "^(string_of_dirpath coq_path))); flush_all ()); - remove_path phys_path; - load_path := (phys_path::fst !load_path, coq_path::snd !load_path) + remove_load_path phys_path; + load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end | _,[] -> - load_path := (phys_path :: fst !load_path, coq_path :: snd !load_path) + 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_path_of_logical_path dir = - fst (list_filter2 (fun p d -> d = dir) !load_path) +let load_paths_of_dir_path dir = + fst (list_filter2 (fun p d -> d = dir) !load_paths) -let get_full_load_path () = List.combine (fst !load_path) (snd !load_path) +let get_full_load_paths () = List.combine (fst !load_paths) (snd !load_paths) (************************************************************************) (*s Modules on disk contain the following informations (after the magic @@ -124,7 +124,7 @@ type library_t = { library_imports : compilation_unit_name list; library_digest : Digest.t } -module CompilingLibraryOrdered = +module LibraryOrdered = struct type t = dir_path let compare d1 d2 = @@ -132,12 +132,12 @@ module CompilingLibraryOrdered = (List.rev (repr_dirpath d1)) (List.rev (repr_dirpath d2)) end -module CompilingLibraryMap = Map.Make(CompilingLibraryOrdered) +module LibraryMap = Map.Make(LibraryOrdered) -(* This is a map from names to libraries *) -let libraries_table = ref CompilingLibraryMap.empty +(* This is a map from names to loaded libraries *) +let libraries_table = ref LibraryMap.empty -(* These are the _ordered_ lists of loaded, imported and exported libraries *) +(* These are the _ordered_ sets of loaded, imported and exported libraries *) let libraries_loaded_list = ref [] let libraries_imports_list = ref [] let libraries_exports_list = ref [] @@ -155,7 +155,7 @@ let unfreeze (mt,mo,mi,me) = libraries_exports_list := me let init () = - libraries_table := CompilingLibraryMap.empty; + libraries_table := LibraryMap.empty; libraries_loaded_list := []; libraries_imports_list := []; libraries_exports_list := [] @@ -168,18 +168,32 @@ let _ = Summary.survive_module = false; Summary.survive_section = false } -let find_library s = - CompilingLibraryMap.find s !libraries_table +(* cache for libraries loaded in memory but not necessarily in environment *) +let compunit_cache = ref LibraryMap.empty -let try_find_library s = - try find_library s +let _ = + Summary.declare_summary "MODULES-CACHE" + { Summary.freeze_function = (fun () -> !compunit_cache); + Summary.unfreeze_function = (fun cu -> compunit_cache := cu); + Summary.init_function = + (fun () -> compunit_cache := LibraryMap.empty); + Summary.survive_module = true; + Summary.survive_section = true } + +(* 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 s)) + error ("Unknown library " ^ (string_of_dirpath dir)) -let library_full_filename m = (find_library m).library_filename +let library_full_filename dir = (find_library dir).library_filename let library_is_loaded dir = - try let _ = CompilingLibraryMap.find dir !libraries_table in true + try let _ = LibraryMap.find dir !libraries_table in true with Not_found -> false let library_is_opened dir = @@ -203,7 +217,7 @@ let register_loaded_library m = | m'::_ as l when m'.library_name = m.library_name -> l | m'::l' -> m' :: aux l' in libraries_loaded_list := aux !libraries_loaded_list; - libraries_table := CompilingLibraryMap.add m.library_name m !libraries_table + libraries_table := LibraryMap.add m.library_name m !libraries_table (* ... while if a library is imported/exported several time, then only the last occurrence is really needed - though the imported @@ -225,10 +239,8 @@ let register_open_library export m = (************************************************************************) (*s Opening libraries *) -(*s [open_library s] opens a library. The library [s] and all - libraries needed by [s] are assumed to be already loaded. When - opening [s] we recursively open all the libraries needed by [s] - and tagged [exported]. *) +(* [open_library export explicit m] opens library [m] if not already + opened _or_ if explicitly asked to be (re)opened *) let eq_lib_name m1 m2 = m1.library_name = m2.library_name @@ -246,6 +258,9 @@ let open_library export explicit_libs m = 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 + a library that is re-exported many times *) + let open_libraries export modl = let to_open_list = List.fold_left @@ -288,6 +303,8 @@ let (in_import, out_import) = (************************************************************************) +(*s Low-level interning/externing of libraries to files *) + (*s Loading from disk to cache (preparation phase) *) let vo_magic_number7 = 07992 (* V8.0 final old syntax *) @@ -314,23 +331,16 @@ let raw_intern_library a = let raw_extern_library = if !Options.v7 then raw_extern_library7 else raw_extern_library8 -(* cache for loaded libraries *) -let compunit_cache = ref CompilingLibraryMap.empty - -let _ = - Summary.declare_summary "MODULES-CACHE" - { Summary.freeze_function = (fun () -> !compunit_cache); - Summary.unfreeze_function = (fun cu -> compunit_cache := cu); - Summary.init_function = - (fun () -> compunit_cache := CompilingLibraryMap.empty); - Summary.survive_module = true; - Summary.survive_section = true } +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.") -(*s [load_library s] loads the library [s] from the disk, and [find_library s] - returns the library of name [s], loading it if necessary. - The boolean [doexp] specifies if we open the libraries which are declared - exported in the dependencies (it is [true] at the highest level; - then same value as for caller is reused in recursive loadings). *) +(************************************************************************) +(*s Locate absolute or partially qualified library names in the path *) exception LibUnmappedDir exception LibNotFound @@ -339,7 +349,7 @@ type library_location = LibLoaded | LibInPath let locate_absolute_library dir = (* Search in loadpath *) let pref, base = split_dirpath dir in - let loadpath = load_path_of_logical_path pref in + let loadpath = load_paths_of_dir_path pref in if loadpath = [] then raise LibUnmappedDir; try let name = (string_of_id base)^".vo" in @@ -352,13 +362,29 @@ let locate_absolute_library dir = with Not_found -> raise LibNotFound -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.") +let locate_qualified_library qid = + try + (* Search library in loadpath *) + let dir, base = repr_qualid qid in + let loadpath = + if repr_dirpath dir = [] then get_load_paths () + else + (* we assume dir is an absolute dirpath *) + load_paths_of_dir_path dir + in + if loadpath = [] then raise LibUnmappedDir; + let name = (string_of_id base)^".vo" in + let path, file = System.where_in_path loadpath name in + let dir = extend_dirpath (find_logical_path path) base in + (* Look if loaded *) + try + (LibLoaded, dir, library_full_filename dir) + with Not_found -> + (LibInPath, dir, file) + with Not_found -> raise LibNotFound + +(************************************************************************) +(* Internalise libraries *) let lighten_library m = if !Options.dont_load_proofs then lighten_library m else m @@ -382,11 +408,11 @@ let intern_from_file f = let rec intern_library (dir, f) = try (* Look if in the current logical environment *) - CompilingLibraryMap.find dir !libraries_table + LibraryMap.find dir !libraries_table with Not_found -> try (* Look if already loaded in cache and consequently its dependencies *) - CompilingLibraryMap.find dir !compunit_cache + LibraryMap.find dir !compunit_cache with Not_found -> (* [dir] is an absolute name which matches [f] which must be in loadpath *) let m = intern_from_file f in @@ -398,12 +424,12 @@ let rec intern_library (dir, f) = intern_and_cache_library dir m and intern_and_cache_library dir m = - compunit_cache := CompilingLibraryMap.add dir m !compunit_cache; + compunit_cache := LibraryMap.add dir m !compunit_cache; try List.iter (intern_mandatory_library dir) m.library_deps; m with e -> - compunit_cache := CompilingLibraryMap.remove dir !compunit_cache; + compunit_cache := LibraryMap.remove dir !compunit_cache; raise e and intern_mandatory_library caller (dir,d) = @@ -443,7 +469,7 @@ let rec_intern_by_filename_only id f = check_library_short_name f m.library_name id; (* We check no other file containing same library is loaded *) try - let m' = CompilingLibraryMap.find m.library_name !libraries_table in + let m' = LibraryMap.find m.library_name !libraries_table in Options.if_verbose warning ((string_of_dirpath m.library_name)^" is already loaded from file "^ m'.library_filename); @@ -452,27 +478,6 @@ let rec_intern_by_filename_only id f = let m = intern_and_cache_library m.library_name m in m.library_name -let locate_qualified_library qid = - try - (* Search library in loadpath *) - let dir, base = repr_qualid qid in - let loadpath = - if repr_dirpath dir = [] then get_load_path () - else - (* we assume dir is an absolute dirpath *) - load_path_of_logical_path dir - in - if loadpath = [] then raise LibUnmappedDir; - let name = (string_of_id base)^".vo" in - let path, file = System.where_in_path loadpath name in - let dir = extend_dirpath (find_logical_path path) base in - (* Look if loaded *) - try - (LibLoaded, dir, library_full_filename dir) - with Not_found -> - (LibInPath, dir, file) - with Not_found -> raise LibNotFound - let rec_intern_qualified_library (loc,qid) = try let (_,dir,f) = locate_qualified_library qid in @@ -491,7 +496,7 @@ let rec_intern_qualified_library (loc,qid) = let rec_intern_library_from_file idopt f = (* A name is specified, we have to check it contains library id *) - let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in + let _, f = System.find_file_in_path (get_load_paths ()) (f^".vo") in rec_intern_by_filename_only idopt f (**********************************************************************) @@ -519,11 +524,11 @@ let string_of_library (_,dir,_) = string_of_id (List.hd (repr_dirpath dir)) let rec load_library dir = try (* Look if loaded in current env (and consequently its dependencies) *) - CompilingLibraryMap.find dir !libraries_table + LibraryMap.find dir !libraries_table with Not_found -> (* [dir] is an absolute name matching [f] which must be in loadpath *) let m = - try CompilingLibraryMap.find dir !compunit_cache + try LibraryMap.find dir !compunit_cache with Not_found -> anomaly ((string_of_dirpath dir)^" should be in cache") in @@ -556,57 +561,39 @@ let (in_require, out_require) = export_function = export_require; classify_function = (fun (_,o) -> Anticipate o) } +(* Require libraries, import them if [export <> None], mark them for export + if [export = Some true] *) + +(* read = require without opening *) + let xml_require = ref (fun d -> ()) let set_xml_require f = xml_require := f -let require_library spec qidl export = -(* - if sections_are_opened () && Options.verbose () then - warning ("Objets of "^(string_of_library modref)^ - " not surviving sections (e.g. Grammar \nand Hints)\n"^ - "will be removed at the end of the section"); -*) +let require_library qidl export = let modrefl = List.map rec_intern_qualified_library qidl in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require (modrefl,None)); - List.iter - (fun dir -> - add_anonymous_leaf (in_import (dir, export))) - modrefl + option_iter (fun exp -> + List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + export end else - add_anonymous_leaf (in_require (modrefl,Some export)); + add_anonymous_leaf (in_require (modrefl,export)); if !Options.xml_export then List.iter !xml_require modrefl; add_frozen_state () -let require_library_from_file spec idopt file export = +let require_library_from_file idopt file export = let modref = rec_intern_library_from_file idopt file in if Lib.is_modtype () || Lib.is_module () then begin add_anonymous_leaf (in_require ([modref],None)); - add_anonymous_leaf (in_import (modref, export)) + option_iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + export end else - add_anonymous_leaf (in_require ([modref],Some export)); + add_anonymous_leaf (in_require ([modref],export)); if !Options.xml_export then !xml_require modref; add_frozen_state () - -(* read = require without opening *) - -let read_library qid = - let modref = rec_intern_qualified_library qid in - add_anonymous_leaf (in_require ([modref],None)); - if !Options.xml_export then !xml_require modref; - add_frozen_state () - -let read_library_from_file f = - let _, f = System.find_file_in_path (get_load_path ()) (f^".vo") in - let modref = rec_intern_by_filename_only None f in - add_anonymous_leaf (in_require ([modref],None)); - if !Options.xml_export then !xml_require modref; - add_frozen_state () - - (* called at end of section *) let reload_library modrefl = @@ -617,7 +604,7 @@ let reload_library modrefl = (* the function called by Vernacentries.vernac_import *) -let import_library export (loc,qid) = +let import_module export (loc,qid) = try match Nametab.locate_module qid with MPfile dir -> @@ -634,27 +621,30 @@ let import_library export (loc,qid) = str ((string_of_qualid qid)^" is not a module")) (************************************************************************) -(*s [save_library s] saves the library [m] to the disk. *) +(*s Initializing the compilation of a library. *) let start_library f = let _,longf = - System.find_file_in_path (get_load_path ()) (f^".v") in + System.find_file_in_path (get_load_paths ()) (f^".v") in let ldir0 = find_logical_path (Filename.dirname longf) in let id = id_of_string (Filename.basename f) in let ldir = extend_dirpath ldir0 id in Declaremods.start_library ldir; ldir,longf +(************************************************************************) +(*s [save_library dir] ends library [dir] and save it to the disk. *) + let current_deps () = List.map (fun m -> (m.library_name, m.library_digest)) !libraries_loaded_list let current_reexports () = List.map (fun m -> m.library_name) !libraries_exports_list -let save_library_to s f = - let cenv, seg = Declaremods.end_library s in +let save_library_to dir f = + let cenv, seg = Declaremods.end_library dir in let md = { - md_name = s; + md_name = dir; md_compiled = cenv; md_objects = seg; md_deps = current_deps (); @@ -668,33 +658,7 @@ let save_library_to s f = close_out ch with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) -(*s Pretty-printing of libraries state. *) - -(* this function is not used... *) -let fmt_libraries_state () = - let opened = opened_libraries () - and loaded = loaded_libraries () in - (str "Imported (open) Modules: " ++ - prlist_with_sep pr_spc pr_dirpath opened ++ fnl () ++ - str "Loaded Modules: " ++ - prlist_with_sep pr_spc pr_dirpath loaded ++ fnl ()) - - -(*s For tactics/commands requiring vernacular libraries *) - -let check_required_library d = - let d' = List.map id_of_string d in - let dir = make_dirpath (List.rev d') in - if not (library_is_loaded dir) then -(* Loading silently ... - let m, prefix = list_sep_last d' in - read_library - (dummy_loc,make_qualid (make_dirpath (List.rev prefix)) m) -*) -(* or failing ...*) - error ("Library "^(list_last d)^" has to be required first") - - +(************************************************************************) (*s Display the memory use of a library. *) open Printf diff --git a/library/library.mli b/library/library.mli index 02f01967c..4ecc76809 100644 --- a/library/library.mli +++ b/library/library.mli @@ -15,65 +15,58 @@ open Libnames open Libobject (*i*) -(*s This module is the heart of the library. It provides low level - functions to load, open and save libraries. Libraries are saved - onto the disk with checksums (obtained with the [Digest] module), - which are checked at loading time to prevent inconsistencies - between files written at various dates. It also provides a high - level function [require] which corresponds to the vernacular - command [Require]. *) +(*s This module provides functions to load, open and save + libraries. Libraries correspond to the subclass of modules that + coincide with a file on disk (the ".vo" files). Libraries on the + disk comes with checksums (obtained with the [Digest] module), which + are checked at loading time to prevent inconsistencies between files + written at various dates. +*) + +(*s Require = load in the environment + open (if the optional boolean + is not [None]); mark also for export if the boolean is [Some true] *) +val require_library : qualid located list -> bool option -> unit +val require_library_from_file : + identifier option -> System.physical_path -> bool option -> unit -val read_library : qualid located -> unit +(*s Open a module (or a library); if the boolean is true then it's also + an export otherwise just a simple import *) +val import_module : bool -> qualid located -> unit -val read_library_from_file : System.physical_path -> unit +(*s Start the compilation of a library *) +val start_library : string -> dir_path * string -(* [import_library true qid] = [export qid] *) - -val import_library : bool -> qualid located -> unit +(*s End the compilation of a library and save it to a ".vo" file *) +val save_library_to : dir_path -> string -> unit +(*s Interrogate the status of libraries *) + + (* - Tell if a library is loaded or opened *) val library_is_loaded : dir_path -> bool val library_is_opened : dir_path -> bool + (* - Tell which libraries are loaded or imported *) val loaded_libraries : unit -> dir_path list val opened_libraries : unit -> dir_path list -val fmt_libraries_state : unit -> Pp.std_ppcmds - -(*s Require. The command [require_library spec m file export] loads and opens - a library [m]. [file] specifies the filename, if not [None]. [spec] - specifies to look for a specification ([true]) or for an implementation - ([false]), if not [None]. And [export] specifies if the library must be - exported. *) - -val require_library : - bool option -> qualid located list -> bool -> unit - -val require_library_from_file : - bool option -> identifier option -> System.physical_path -> bool -> unit - -val set_xml_require : (dir_path -> unit) -> unit - -(*s [save_library_to s f] saves the current environment as a library [s] - in the file [f]. *) - -val start_library : string -> dir_path * string -val save_library_to : dir_path -> string -> unit - -(* [library_full_filename] returns the full filename of a loaded library. *) - + (* - Return the full filename of a loaded library. *) val library_full_filename : dir_path -> string +(*s Hook for the xml exportation of libraries *) +val set_xml_require : (dir_path -> unit) -> unit -(*s Global load path *) -type logical_path = dir_path +(*s Global load paths: a load path is a physical path in the file + system; to each load path is associated a Coq [dir_path] (the "logical" + path of the physical path) *) -val get_load_path : unit -> System.physical_path list -val get_full_load_path : unit -> (System.physical_path * logical_path) list -val add_load_path_entry : System.physical_path * logical_path -> unit -val remove_path : System.physical_path -> unit -val find_logical_path : System.physical_path -> logical_path -val load_path_of_logical_path : dir_path -> System.physical_path list +val get_load_paths : unit -> System.physical_path list +val get_full_load_paths : unit -> (System.physical_path * dir_path) list +val add_load_path : System.physical_path * dir_path -> unit +val remove_load_path : System.physical_path -> unit +val find_logical_path : System.physical_path -> dir_path +val load_paths_of_dir_path : dir_path -> System.physical_path list +(*s Locate a library in the load paths *) exception LibUnmappedDir exception LibNotFound type library_location = LibLoaded | LibInPath @@ -81,13 +74,10 @@ type library_location = LibLoaded | LibInPath val locate_qualified_library : qualid -> library_location * dir_path * System.physical_path - -val check_required_library : string list -> unit - -(*s Displays the memory use of a library. *) +(*s Statistics: display the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds -(* For discharge *) +(*s For discharge *) type library_reference val out_require : Libobject.obj -> library_reference diff --git a/library/states.ml b/library/states.ml index 0fa62265a..2a34c8753 100644 --- a/library/states.ml +++ b/library/states.ml @@ -24,7 +24,7 @@ let state_magic_number = 19764 let (extern_state,intern_state) = let (raw_extern, raw_intern) = extern_intern state_magic_number ".coq" in (fun s -> raw_extern s (get_state())), - (fun s -> set_state (raw_intern (Library.get_load_path ()) s)) + (fun s -> set_state (raw_intern (Library.get_load_paths ()) s)) (* Rollback. *) -- cgit v1.2.3