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, 35 insertions, 19 deletions

diff --git a/kernel/modops.mli b/kernel/modops.mli
index e148f9628..6aed95988 100644
--- a/kernel/modops.mli
+++ b/kernel/modops.mli
@@ -16,30 +16,43 @@ open Mod_subst
 
 (** {6 Various operations on modules and module types } *)
 
-val module_body_of_type : module_path -> module_type_body  -> module_body
+(** Functors *)
 
-val module_type_of_module :
-  module_path option -> module_body -> module_type_body
+val is_functor : ('ty,'a) functorize -> bool
 
-val destr_functor :
-  struct_expr_body -> MBId.t * module_type_body * struct_expr_body
+val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
+
+val destr_nofunctor : ('ty,'a) functorize -> 'a
+
+(** Conversions between [module_body] and [module_type_body] *)
+
+val module_type_of_module : module_body -> module_type_body
+val module_body_of_type : module_path -> module_type_body -> module_body
 
 val check_modpath_equiv : env -> module_path -> module_path -> unit
 
-(** {6 Substitutions } *)
+val implem_smartmap :
+  (module_signature -> module_signature) ->
+  (module_expression -> module_expression) ->
+  (module_implementation -> module_implementation)
 
-val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
+(** {6 Substitutions } *)
 
-val subst_signature : substitution -> structure_body -> structure_body
+val subst_signature : substitution -> module_signature -> module_signature
+val subst_structure : substitution -> structure_body -> structure_body
 
 (** {6 Adding to an environment } *)
 
-val add_signature :
+val add_structure :
   module_path -> structure_body -> delta_resolver -> env -> env
 
 (** adds a module and its components, but not the constraints *)
 val add_module : module_body -> env -> env
 
+
+(** same, for a module type *)
+val add_module_type : module_path -> module_type_body -> env -> env
+
 (** {6 Strengthening } *)
 
 val strengthen : module_type_body -> module_path -> module_type_body
@@ -53,17 +66,22 @@ val strengthen_and_subst_mb : module_body -> module_path -> bool -> module_body
 val subst_modtype_and_resolver : module_type_body -> module_path ->
   module_type_body
 
-(** {6 Cleaning a bound module expression } *)
+(** {6 Cleaning a module expression from bounded parts }
 
-val clean_bounded_mod_expr : struct_expr_body -> struct_expr_body
+     For instance:
+       functor(X:T)->struct module M:=X end)
+     becomes:
+       functor(X:T)->struct module M:=<content of T> end)
+*)
+
+val clean_bounded_mod_expr : module_signature -> module_signature
 
 (** {6 Stm machinery : join and prune } *)
 
-val join_module_body : module_body -> unit
-val join_structure_body : structure_body -> unit
-val join_struct_expr_body : struct_expr_body -> unit
+val join_module : module_body -> unit
+val join_structure : structure_body -> unit
 
-val prune_structure_body : structure_body -> structure_body
+val prune_structure : structure_body -> structure_body
 
 (** {6 Errors } *)
 
@@ -91,12 +109,12 @@ type module_typing_error =
       Label.t * structure_field_body * signature_mismatch_error
   | LabelAlreadyDeclared of Label.t
   | ApplicationToNotPath of module_struct_entry
-  | NotAFunctor of struct_expr_body
+  | NotAFunctor
+  | IsAFunctor
   | IncompatibleModuleTypes of module_type_body * module_type_body
   | NotEqualModulePaths of module_path * module_path
   | NoSuchLabel of Label.t
   | IncompatibleLabels of Label.t * Label.t
-  | SignatureExpected of struct_expr_body
   | NotAModule of string
   | NotAModuleType of string
   | NotAConstant of Label.t
@@ -121,8 +139,6 @@ val error_incompatible_labels : Label.t -> Label.t -> 'a
 
 val error_no_such_label : Label.t -> 'a
 
-val error_signature_expected : struct_expr_body -> 'a
-
 val error_not_a_module : string -> 'a
 
 val error_not_a_constant : Label.t -> 'a