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, 64 insertions, 36 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index fd3351674..0b732e4b9 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -276,8 +276,30 @@ type mutual_inductive_body = {
     mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
   }
 
-(** {6 Modules: signature component specifications, module types, and
-  module declarations } *)
+(** {6 Module declarations } *)
+
+(** Functor expressions are forced to be on top of other expressions *)
+
+type ('ty,'a) functorize =
+  | NoFunctor of 'a
+  | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize
+
+(** The fully-algebraic module expressions : names, applications, 'with ...'.
+    They correspond to the user entries of non-interactive modules.
+    They will be later expanded into module structures in [Mod_typing],
+    and won't play any role into the kernel after that : they are kept
+    only for short module printing and for extraction. *)
+
+type with_declaration =
+  | WithMod of Id.t list * module_path
+  | WithDef of Id.t list * constr
+
+type module_alg_expr =
+  | MEident of module_path
+  | MEapply of module_alg_expr * module_path
+  | MEwith of module_alg_expr * with_declaration
+
+(** A component of a module structure *)
 
 type structure_field_body =
   | SFBconst of constant_body
@@ -285,45 +307,51 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
-and structure_body = (label * structure_field_body) list
+(** A module structure is a list of labeled components.
+
+    Note : we may encounter now (at most) twice the same label in
+    a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+    and once for an object ([SFBconst] or [SFBmind]) *)
+
+and structure_body = (Label.t * structure_field_body) list
+
+(** A module signature is a structure, with possibly functors on top of it *)
+
+and module_signature = (module_type_body,structure_body) functorize
+
+(** A module expression is an algebraic expression, possibly functorized. *)
+
+and module_expression = (module_type_body,module_alg_expr) functorize
 
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
+and module_implementation =
+  | Abstract (** no accessible implementation *)
+  | Algebraic of module_expression (** non-interactive algebraic expression *)
+  | Struct of module_signature (** interactive body *)
+  | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
 and module_body =
-    {  (** absolute path of the module *)
-      mod_mp : module_path;
-      (** Implementation *)
-      mod_expr : struct_expr_body option;
-      (** Signature *)
-      mod_type : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      mod_type_alg : struct_expr_body option;
-      (** set of all constraint in the module  *)
-      mod_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      mod_delta : delta_resolver;
-      mod_retroknowledge : action list}
+  { mod_mp : module_path; (** absolute path of the module *)
+    mod_expr : module_implementation; (** implementation *)
+    mod_type : module_signature; (** expanded type *)
+    (** algebraic type, kept if it's relevant for extraction *)
+    mod_type_alg : module_expression option;
+    (** set of all constraints in the module  *)
+    mod_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    mod_delta : delta_resolver;
+    mod_retroknowledge : action list }
+
+(** A [module_type_body] is similar to a [module_body], with
+    no implementation and retroknowledge fields *)
 
 and module_type_body =
-    {
-      (** Path of the module type *)
-      typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      typ_delta : delta_resolver}
+  { typ_mp : module_path; (** path of the module type *)
+    typ_expr : module_signature; (** expanded type *)
+    (** algebraic expression, kept if it's relevant for extraction  *)
+    typ_expr_alg : module_expression option;
+    typ_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    typ_delta : delta_resolver}
 
 
 (*************************************************************************)