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, 54 insertions, 60 deletions

diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index 99c1b8483..6cedb6ad2 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -319,10 +319,9 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 =
        check_conv error cst conv env ty1 ty2
 
 let rec check_modules cst env msb1 msb2 subst1 subst2 =
-  let mty1 = module_type_of_module None msb1 in
-  let mty2 =  module_type_of_module None msb2 in
-  let cst = check_modtypes cst env mty1 mty2 subst1 subst2 false in
-    cst
+  let mty1 = module_type_of_module msb1 in
+  let mty2 =  module_type_of_module msb2 in
+  check_modtypes cst env mty1 mty2 subst1 subst2 false
 
 and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2= 
   let map1 = make_labmap mp1 sig1 in
@@ -344,67 +343,62 @@ and check_signatures cst env mp1 sig1 mp2 sig2 subst1 subst2 reso1 reso2=
 	      | Modtype mtb -> mtb
 	      | _ -> error_signature_mismatch l spec2 ModuleTypeFieldExpected
 	    in
-	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
-	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
-	      check_modtypes cst env mtb1 mtb2 subst1 subst2 true
+	    let env =
+              add_module_type mtb2.typ_mp mtb2
+	        (add_module_type mtb1.typ_mp mtb1 env)
+            in
+	    check_modtypes cst env mtb1 mtb2 subst1 subst2 true
   in
     List.fold_left check_one_body cst sig2
 
-and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv = 
-  if mtb1==mtb2 then cst else 
-  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
-  let rec check_structure cst env str1 str2 equiv subst1 subst2 = 
-	match str1,str2 with
-	  | SEBstruct (list1), 
-	    SEBstruct (list2) -> 
-	      if equiv then
-		let subst2 = 
-		  add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
-		Univ.union_constraints 
-		  (check_signatures cst env
-		     mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
-		  mtb1.typ_delta mtb2.typ_delta) 
-		  (check_signatures cst env 
-		     mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
-		  mtb2.typ_delta  mtb1.typ_delta)
-	      else
-		check_signatures cst env
-		  mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
-		  mtb1.typ_delta  mtb2.typ_delta
-	  | SEBfunctor (arg_id1,arg_t1,body_t1),
-	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	      let subst1 = 
-		(join (map_mbid arg_id1 (MPbound arg_id2) arg_t2.typ_delta) subst1) in
-	      let cst = check_modtypes cst env 
-		arg_t2 arg_t1 subst2 subst1
-		equiv in 
-		(* contravariant *)
-	      let env = add_module 
-		(module_body_of_type (MPbound arg_id2) arg_t2) env 
-	      in
-	      let env = match body_t1 with
-		  SEBstruct str -> 
-		    add_module {mod_mp = mtb1.typ_mp;
-				mod_expr = None;
-				mod_type = subst_struct_expr subst1 body_t1;
-				mod_type_alg= None;
-				mod_constraints=mtb1.typ_constraints;
-				mod_retroknowledge = [];
-				mod_delta = mtb1.typ_delta} env
-		| _ -> env
-	      in
-		check_structure cst env body_t1 body_t2 equiv 
-		  subst1
-		  subst2
-	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
-      in
-     if mtb1'== mtb2' then cst
-     else check_structure cst env mtb1' mtb2' equiv subst1 subst2
+and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
+  if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then cst
+  else
+    let rec check_structure cst env str1 str2 equiv subst1 subst2 =
+      match str1,str2 with
+      |NoFunctor list1,
+       NoFunctor list2 ->
+	if equiv then
+	  let subst2 = add_mp mtb2.typ_mp mtb1.typ_mp mtb1.typ_delta subst2 in
+          let cst1 = check_signatures cst env
+	    mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+	    mtb1.typ_delta mtb2.typ_delta
+          in
+          let cst2 = check_signatures cst env
+	    mtb2.typ_mp list2 mtb1.typ_mp list1 subst2 subst1
+	    mtb2.typ_delta  mtb1.typ_delta
+	  in
+	  Univ.union_constraints cst1 cst2
+	else
+	  check_signatures cst env
+	    mtb1.typ_mp list1 mtb2.typ_mp list2 subst1 subst2
+	    mtb1.typ_delta  mtb2.typ_delta
+      |MoreFunctor (arg_id1,arg_t1,body_t1),
+       MoreFunctor (arg_id2,arg_t2,body_t2) ->
+        let mp2 = MPbound arg_id2 in
+	let subst1 = join (map_mbid arg_id1 mp2 arg_t2.typ_delta) subst1 in
+	let cst = check_modtypes cst env arg_t2 arg_t1 subst2 subst1 equiv in
+        (* contravariant *)
+	let env = add_module_type mp2 arg_t2 env in
+	let env =
+          if Modops.is_functor body_t1 then env
+          else add_module
+            {mod_mp = mtb1.typ_mp;
+	     mod_expr = Abstract;
+	     mod_type = subst_signature subst1 body_t1;
+	     mod_type_alg = None;
+	     mod_constraints = mtb1.typ_constraints;
+	     mod_retroknowledge = [];
+	     mod_delta = mtb1.typ_delta} env
+	in
+	check_structure cst env body_t1 body_t2 equiv subst1 subst2
+      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+    in
+    check_structure cst env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
 
 let check_subtypes env sup super =
-  let env = add_module 
-		(module_body_of_type sup.typ_mp sup) env in
-  check_modtypes empty_constraint env 
+  let env = add_module_type sup.typ_mp sup env in
+  check_modtypes empty_constraint env
     (strengthen sup sup.typ_mp) super empty_subst
     (map_mp super.typ_mp sup.typ_mp sup.typ_delta) false