From 12965209478bd99dfbe57f07d5b525e51b903f22 Mon Sep 17 00:00:00 2001 From: coq Date: Fri, 2 Aug 2002 17:17:42 +0000 Subject: Modules dans COQ\!\!\!\! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7 --- library/library.mli | 68 ++++++++++++++++++++++++++--------------------------- 1 file changed, 33 insertions(+), 35 deletions(-) (limited to 'library/library.mli') diff --git a/library/library.mli b/library/library.mli index dc34ec72e..43d73d241 100644 --- a/library/library.mli +++ b/library/library.mli @@ -11,61 +11,59 @@ (*i*) open Util open Names +open Libnames open Libobject (*i*) (*s This module is the heart of the library. It provides low level functions to - load, open and save modules. Modules are saved onto the disk with checksums + load, open and save libraries. Modules 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]. *) -val read_module : Nametab.qualid located -> unit -val read_module_from_file : System.physical_path -> unit -val import_module : bool -> Nametab.qualid located -> unit +val read_library : qualid located -> unit -val module_is_loaded : dir_path -> bool -val module_is_opened : dir_path -> bool +val read_library_from_file : System.physical_path -> unit -val loaded_modules : unit -> dir_path list -val opened_modules : unit -> dir_path list +val export_library : qualid located -> unit -val fmt_modules_state : unit -> Pp.std_ppcmds +val library_is_loaded : dir_path -> bool +val library_is_opened : dir_path -> bool -(*s Require. The command [require_module spec m file export] loads and opens - a module [m]. [file] specifies the filename, if not [None]. [spec] +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 module must be + ([false]), if not [None]. And [export] specifies if the library must be exported. *) -val require_module : - bool option -> Nametab.qualid located list -> bool -> unit +val require_library : + bool option -> qualid located list -> bool -> unit -val require_module_from_file : +val require_library_from_file : bool option -> identifier option -> string -> bool -> unit -(*s [save_module_to s f] saves the current environment as a module [s] +(*s [save_library_to s f] saves the current environment as a library [s] in the file [f]. *) -val save_module_to : dir_path -> string -> unit +val start_library : string -> dir_path * string +val save_library_to : dir_path -> string -> unit -(*s [module_segment m] returns the segment of the loaded module - [m]; if not given, the segment of the current module is returned +(*s [library_segment m] returns the segment of the loaded library + [m]; if not given, the segment of the current library is returned (which is then the same as [Lib.contents_after None]). - [module_full_filename] returns the full filename of a loaded module. *) +*) +(*val library_segment : dir_path option -> Lib.library_segment*) -val module_segment : dir_path option -> Lib.library_segment -val module_full_filename : dir_path -> string +(* [library_full_filename] returns the full filename of a loaded library. *) -(*s [fold_all_segments] and [iter_all_segments] iterate over all - segments, the modules' segments first and then the current - segment. Modules are presented in an arbitrary order. The given - function is applied to all leaves (together with their section - path). The boolean indicates if we must enter closed sections. *) +val library_full_filename : dir_path -> string -val fold_all_segments : bool -> ('a -> section_path -> obj -> 'a) -> 'a -> 'a -val iter_all_segments : bool -> (section_path -> obj -> unit) -> unit (*s Global load path *) type logical_path = dir_path @@ -82,16 +80,16 @@ exception LibNotFound type library_location = LibLoaded | LibInPath val locate_qualified_library : - Nametab.qualid -> library_location * dir_path * System.physical_path + qualid -> library_location * dir_path * System.physical_path -val check_required_module : string list -> unit -(*s Displays the memory use of a module. *) +val check_required_library : string list -> unit +(*s Displays the memory use of a library. *) val mem : dir_path -> Pp.std_ppcmds (* For discharge *) -type module_reference +type library_reference -val out_require : Libobject.obj -> module_reference -val reload_module : module_reference -> unit +val out_require : Libobject.obj -> library_reference +val reload_library : library_reference -> unit -- cgit v1.2.3