Imported Upstream version 8.0pl1upstream/8.0pl1

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