diff options
author | 2012-01-12 16:08:29 +0100 | |
---|---|---|
committer | 2012-01-12 16:08:29 +0100 | |
commit | 23a6061a81ffa0c214d521287b6af0a31bfa22f0 (patch) | |
tree | f1ca9ba9240b98b8695a9f1870e56602734cf97c /library/declaremods.mli | |
parent | de109d8c0c68f569b907e6e24271f259ba28888e (diff) | |
parent | 39efc41237ec906226a3a53d7396d51173495204 (diff) |
Merge commit 'upstream/8.4_beta+dfsg' into experimental/master
Diffstat (limited to 'library/declaremods.mli')
-rw-r--r-- | library/declaremods.mli | 88 |
1 files changed, 60 insertions, 28 deletions
diff --git a/library/declaremods.mli b/library/declaremods.mli index 46b7f411..9d44ba97 100644 --- a/library/declaremods.mli +++ b/library/declaremods.mli @@ -1,14 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: declaremods.mli 14641 2011-11-06 11:59:10Z herbelin $ i*) - -(*i*) open Util open Names open Entries @@ -16,15 +13,41 @@ open Environ open Libnames open Libobject open Lib - (*i*) -(*s This modules provides official functions to declare modules and +(** This modules provides official functions to declare modules and module types *) +(** Rigid / flexible signature *) + +type 'a module_signature = + | Enforce of 'a (** ... : T *) + | Check of 'a list (** ... <: T1 <: T2, possibly empty *) + +(** Should we adapt a few scopes during functor application ? *) + +type scope_subst = (string * string) list + +val subst_scope : string -> string + +(** Which inline annotations should we honor, either None or the ones + whose level is less or equal to the given integer *) -(*s Modules *) +type inline = + | NoInline + | DefaultInline + | InlineAt of int -(* [declare_module interp_modtype interp_modexpr id fargs typ expr] +(** The type of annotations for functor applications *) + +type funct_app_annot = + { ann_inline : inline; + ann_scope_subst : scope_subst } + +type 'a annotated = ('a * funct_app_annot) + +(** {6 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 @@ -41,39 +64,44 @@ val declare_module : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> identifier -> - (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> - ('modast * bool) list -> module_path + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> + ('modast annotated) list -> module_path val start_module : (env -> 'modast -> module_struct_entry) -> - bool option -> identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) Topconstr.module_signature -> module_path + bool option -> identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) module_signature -> module_path val end_module : unit -> module_path -(*s Module types *) +(** {6 Module types } *) val declare_modtype : (env -> 'modast -> module_struct_entry) -> (env -> 'modast -> module_struct_entry * bool) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> ('modast * bool) list -> module_path + identifier -> + (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> + ('modast annotated) list -> + module_path val start_modtype : (env -> 'modast -> module_struct_entry) -> - identifier -> (identifier located list * ('modast * bool)) list -> - ('modast * bool) list -> module_path + identifier -> (identifier located list * ('modast annotated)) list -> + ('modast annotated) list -> module_path val end_modtype : unit -> module_path -(*s Objects of a module. They come in two lists: the substitutive ones +(** {6 ... } *) +(** 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 *) +(** {6 Libraries i.e. modules on disk } *) type library_name = dir_path @@ -88,27 +116,28 @@ val start_library : library_name -> unit val end_library : library_name -> Safe_typing.compiled_library * library_objects -(* set a function to be executed at end_library *) +(** set a function to be executed at end_library *) val set_end_library_hook : (unit -> unit) -> unit -(* [really_import_module mp] opens the module [mp] (in a Caml sense). +(** [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 +(** [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 -(* Include *) +(** Include *) val declare_include : (env -> 'struct_expr -> module_struct_entry * bool) -> - ('struct_expr * bool) list -> unit + ('struct_expr annotated) list -> unit -(*s [iter_all_segments] iterate over all segments, the modules' +(** {6 ... } *) +(** [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). *) @@ -120,7 +149,10 @@ val debug_print_modtab : unit -> Pp.std_ppcmds (*i val debug_print_modtypetab : unit -> Pp.std_ppcmds i*) -(* For translator *) +(** For translator *) val process_module_bindings : module_ident list -> - (mod_bound_id * (module_struct_entry * bool)) list -> unit + (mod_bound_id * (module_struct_entry annotated)) list -> unit +(** For Printer *) +val process_module_seb_binding : + mod_bound_id -> Declarations.struct_expr_body -> unit |