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, 32 deletions

diff --git a/library/assumptions.ml b/library/assumptions.ml
index 2418f0648d..b1f133ac36 100644
--- a/library/assumptions.ml
+++ b/library/assumptions.ml
@@ -67,6 +67,23 @@ let rec search_cst_label lab = function
   | (l, SFBconst cb) :: _ when Label.equal l lab -> cb
   | _ :: fields -> search_cst_label lab fields
 
+(* TODO: using [empty_delta_resolver] below is probably slightly incorrect. But:
+    a) I don't see currently what should be used instead
+    b) this shouldn't be critical for Print Assumption. At worse some
+       constants will have a canonical name which is non-canonical,
+       leading to failures in [Global.lookup_constant], but our own
+       [lookup_constant] should work.
+*)
+
+let rec fields_of_functor f subs mp0 args = function
+  |NoFunctor a -> f subs mp0 args a
+  |MoreFunctor (mbid,_,e) ->
+    match args with
+    | [] -> assert false (* we should only encounter applied functors *)
+    | mpa :: args ->
+      let subs = add_mbid mbid mpa empty_delta_resolver (*TODO*) subs in
+      fields_of_functor f subs mp0 args e
+
 let rec lookup_module_in_impl mp =
   try Global.lookup_module mp
   with Not_found ->
@@ -93,43 +110,29 @@ and fields_of_mp mp =
     if mp_eq inner_mp mp then subs
     else add_mp inner_mp mp mb.mod_delta subs
   in
-  Modops.subst_signature subs fields
+  Modops.subst_structure subs fields
 
-and fields_of_mb subs mb args =
-  let seb = match mb.mod_expr with
-    | None -> mb.mod_type (* cf. Declare Module *)
-    | Some seb -> seb
-  in
-  fields_of_seb subs mb.mod_mp seb args
+and fields_of_mb subs mb args = match mb.mod_expr with
+  |Algebraic expr -> fields_of_expression subs mb.mod_mp args expr
+  |Struct sign -> fields_of_signature subs mb.mod_mp args sign
+  |Abstract|FullStruct -> fields_of_signature subs mb.mod_mp args mb.mod_type
 
-(* TODO: using [empty_delta_resolver] below in [fields_of_seb]
-   is probably slightly incorrect. But:
-    a) I don't see currently what should be used instead
-    b) this shouldn't be critical for Print Assumption. At worse some
-       constants will have a canonical name which is non-canonical,
-       leading to failures in [Global.lookup_constant], but our own
-       [lookup_constant] should work.
-*)
+(** The Abstract case above corresponds to [Declare Module] *)
 
-and fields_of_seb subs mp0 seb args = match seb with
-  | SEBstruct l ->
-    let () = assert (List.is_empty args) in
-    l, mp0, subs
-  | SEBident mp ->
+and fields_of_signature x =
+  fields_of_functor
+    (fun subs mp0 args struc ->
+      assert (List.is_empty args);
+      (struc, mp0, subs)) x
+
+and fields_of_expr subs mp0 args = function
+  |MEident mp ->
     let mb = lookup_module_in_impl (subst_mp subs mp) in
     fields_of_mb subs mb args
-  | SEBapply (seb1,seb2,_) ->
-    (match seb2 with
-      | SEBident mp2 -> fields_of_seb subs mp0 seb1 (mp2::args)
-      | _ -> assert false) (* only legal application is to module names *)
-  | SEBfunctor (mbid,mtb,seb) ->
-    (match args with
-      | [] -> assert false (* we should only encounter applied functors *)
-      | mpa :: args ->
-	let subs = add_mbid mbid mpa empty_delta_resolver subs in
-	fields_of_seb subs mp0 seb args)
-  | SEBwith _ -> assert false (* should not appear in a mod_expr
-				   or mod_type field *)
+  |MEapply (me1,mp2) -> fields_of_expr subs mp0 (mp2::args) me1
+  |MEwith _ -> assert false (* no 'with' in [mod_expr] *)
+
+and fields_of_expression x = fields_of_functor fields_of_expr x
 
 let lookup_constant_in_impl cst fallback =
   try