diff options
author | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
---|---|---|
committer | Samuel Mimram <samuel.mimram@ens-lyon.org> | 2004-07-28 21:54:47 +0000 |
commit | 6b649aba925b6f7462da07599fe67ebb12a3460e (patch) | |
tree | 43656bcaa51164548f3fa14e5b10de5ef1088574 /library/declaremods.mli |
Imported Upstream version 8.0pl1upstream/8.0pl1
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r-- | library/declaremods.mli | 116 |
1 files changed, 116 insertions, 0 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli new file mode 100644 index 00000000..f229da1e --- /dev/null +++ b/library/declaremods.mli @@ -0,0 +1,116 @@ +(************************************************************************) +(* 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 *) +(************************************************************************) + +(*i $Id: declaremods.mli,v 1.8.2.1 2004/07/16 19:30:35 herbelin Exp $ i*) + +(*i*) +open Util +open Names +open Entries +open Environ +open Libnames +open Libobject +open Lib + (*i*) + +(*s This modules provides official functions to declare modules and + module types *) + + +(*s Modules *) + +(* [declare_module interp_modtype interp_modexpr id fargs typ expr] + declares module [id], with type constructed by [interp_modtype] + from functor arguments [fargs] and [typ] and with module body + constructed by [interp_modtype] from functor arguments [fargs] and + by [interp_modexpr] from [expr]. At least one of [typ], [expr] must + be non-empty. + + The [bool] in [typ] tells if the module must be abstracted [true] + with respect to the module type or merely matched without any + restriction [false]. +*) + +val declare_module : + (env -> 'modtype -> module_type_entry) -> (env -> 'modexpr -> module_expr) -> + identifier -> + (identifier located list * 'modtype) list -> ('modtype * bool) option -> + 'modexpr option -> unit + +val start_module : (env -> 'modtype -> module_type_entry) -> + identifier -> + (identifier located list * 'modtype) list -> ('modtype * bool) option -> + unit + +val end_module : identifier -> unit + + + +(*s Module types *) + +val declare_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier located list * 'modtype) list -> 'modtype -> unit + +val start_modtype : (env -> 'modtype -> module_type_entry) -> + identifier -> (identifier located list * 'modtype) list -> unit + +val end_modtype : identifier -> unit + + +(*s Objects of a module. They come in two lists: the substitutive ones + and the other *) + +val module_objects : module_path -> library_segment + + +(*s Libraries i.e. modules on disk *) + +type library_name = dir_path + +type library_objects + +val register_library : + library_name -> + Safe_typing.compiled_library -> library_objects -> Digest.t -> unit + +val start_library : library_name -> unit + +val end_library : + library_name -> Safe_typing.compiled_library * library_objects + + +(* [really_import_module mp] opens the module [mp] (in a Caml sense). + It modifies Nametab and performs the "open_object" function for + every object of the module. *) + +val really_import_module : module_path -> unit + +(* [import_module export mp] is a synchronous version of + [really_import_module]. If [export] is [true], the module is also + opened every time the module containing it is. *) + +val import_module : bool -> module_path -> unit + + +(*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 fold_all_segments : bool -> ('a -> object_name -> obj -> 'a) -> 'a -> 'a +val iter_all_segments : bool -> (object_name -> obj -> unit) -> unit + + +val debug_print_modtab : unit -> Pp.std_ppcmds + +(*val debug_print_modtypetab : unit -> Pp.std_ppcmds*) + +(* For translator *) +val process_module_bindings : module_ident list -> + (mod_bound_id * module_type_entry) list -> unit |