Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 28 insertions, 28 deletions

diff --git a/kernel/mod_typing.mli b/kernel/mod_typing.mli
index 0990e36c1..21171705d 100644
--- a/kernel/mod_typing.mli
+++ b/kernel/mod_typing.mli
@@ -12,40 +12,40 @@ open Entries
 open Mod_subst
 open Names
 
+(** Main functions for translating module entries
+
+    Note : [module_body] and [module_type_body] obtained this way
+    won't have any [MEstruct] in their algebraic fields.
+*)
 
 val translate_module :
   env -> module_path -> inline -> module_entry -> module_body
 
-val translate_module_type :
-  env -> module_path -> inline -> module_struct_entry -> module_type_body
+val translate_modtype :
+  env -> module_path -> inline -> module_type_entry -> module_type_body
 
-val translate_struct_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body (* Signature *)
-  * struct_expr_body option  (* Algebraic expr, in fact never None *)
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_type_entry :
-  env -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option
-  * delta_resolver
-  * Univ.constraints
-
-val translate_struct_include_module_entry :
-  env -> module_path -> inline -> module_struct_entry ->
-  struct_expr_body
-  * struct_expr_body option (* Algebraic expr, always None *)
-  * delta_resolver
-  * Univ.constraints
+(** Low-level function for translating a module struct entry :
+    - We translate to a module when a [module_path] is given,
+      otherwise to a module type.
+    - The first output is the expanded signature
+    - The second output is the algebraic expression, kept for the extraction.
+      It is never None when translating to a module, but for module type
+      it could not be contain applications or functors.
+      Moreover algebraic expressions obtained here cannot contain [MEstruct].
+*)
 
-val add_modtype_constraints : env -> module_type_body -> env
+type 'alg translation =
+  module_signature * 'alg option * delta_resolver * Univ.constraints
 
-val add_module_constraints : env -> module_body -> env
+val translate_mse :
+  env -> module_path option -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val add_struct_expr_constraints : env -> struct_expr_body -> env
-
-val struct_expr_constraints : struct_expr_body -> Univ.constraints
+val translate_mse_incl :
+  env -> module_path -> inline -> module_struct_entry ->
+    module_alg_expr translation
 
-val module_constraints : module_body -> Univ.constraints
+val finalize_module :
+  env -> module_path -> module_expression translation ->
+  (module_type_entry * inline) option ->
+  module_body