diff options
Diffstat (limited to 'library/library.ml')
-rw-r--r-- | library/library.ml | 71 |
1 files changed, 42 insertions, 29 deletions
diff --git a/library/library.ml b/library/library.ml index 16dedf565..be0c25997 100644 --- a/library/library.ml +++ b/library/library.ml @@ -172,28 +172,32 @@ let open_libraries export modl = (**********************************************************************) -(* import and export - synchronous operations*) +(* import and export of libraries - synchronous operations *) +(* at the end similar to import and export of modules except that it *) +(* is optimized: when importing several libraries at the same time *) +(* which themselves indirectly imports the very same modules, these *) +(* ones are imported only ones *) -let open_import i (_,(dir,export)) = +let open_import_library i (_,(modl,export)) = if Int.equal i 1 then (* even if the library is already imported, we re-import it *) (* if not (library_is_opened dir) then *) - open_libraries export [try_find_library dir] + open_libraries export (List.map try_find_library modl) -let cache_import obj = - open_import 1 obj +let cache_import_library obj = + open_import_library 1 obj -let subst_import (_,o) = o +let subst_import_library (_,o) = o -let classify_import (_,export as obj) = +let classify_import_library (_,export as obj) = if export then Substitute obj else Dispose -let in_import : DirPath.t * bool -> obj = +let in_import_library : DirPath.t list * bool -> obj = declare_object {(default_object "IMPORT LIBRARY") with - cache_function = cache_import; - open_function = open_import; - subst_function = subst_import; - classify_function = classify_import } + cache_function = cache_import_library; + open_function = open_import_library; + subst_function = subst_import_library; + classify_function = classify_import_library } (************************************************************************) @@ -540,7 +544,7 @@ let require_library_from_dirpath modrefl export = begin add_anonymous_leaf (in_require (needed,modrefl,None)); Option.iter (fun exp -> - List.iter (fun dir -> add_anonymous_leaf (in_import(dir,exp))) modrefl) + add_anonymous_leaf (in_import_library (modrefl,exp))) export end else @@ -556,7 +560,7 @@ let require_library_from_file idopt file export = let needed = List.rev_map snd needed in if Lib.is_module_or_modtype () then begin add_anonymous_leaf (in_require (needed,[modref],None)); - Option.iter (fun exp -> add_anonymous_leaf (in_import (modref,exp))) + Option.iter (fun exp -> add_anonymous_leaf (in_import_library ([modref],exp))) export end else @@ -565,21 +569,30 @@ let require_library_from_file idopt file export = (* the function called by Vernacentries.vernac_import *) -let import_module export (loc,qid) = - try - match Nametab.locate_module qid with - | MPfile dir -> - if Lib.is_module_or_modtype () || not export then - add_anonymous_leaf (in_import (dir, export)) - else - add_anonymous_leaf (in_import (dir, export)) - | mp -> - Declaremods.import_module export mp - with - Not_found -> - user_err_loc - (loc,"import_library", - str ((string_of_qualid qid)^" is not a module")) +let safe_locate_module (loc,qid) = + try Nametab.locate_module qid + with Not_found -> + user_err_loc + (loc,"import_library", str (string_of_qualid qid ^ " is not a module")) + +let import_module export modl = + (* Optimization: libraries in a raw in the list are imported + "globally". If there is non-library in the list; it breaks the + optimization For instance: "Import Arith MyModule Zarith" will + not be optimized (possibly resulting in redefinitions, but + "Import MyModule Arith Zarith" and "Import Arith Zarith MyModule" + will have the submodules imported by both Arith and ZArith + imported only once *) + let flush = function + | [] -> () + | modl -> add_anonymous_leaf (in_import_library (List.rev modl, export)) in + let rec aux acc = function + | m :: l -> + (match safe_locate_module m with + | MPfile dir -> aux (dir::acc) l + | mp -> flush acc; Declaremods.import_module export mp; aux [] l) + | [] -> flush acc + in aux [] modl (************************************************************************) (*s Initializing the compilation of a library. *) |