Declarations.mli refactoring: module_type_body = module_body

 After this commit, module_type_body is a particular case of module_type.
 For a [module_type_body], the implementation field [mod_expr] is
 supposed to be always [Abstract]. This is verified by coqchk, even
 if this isn't so crucial, since [mod_expr] is never read in the case
 of a module type.

 Concretely, this amounts to the following rewrite on field names
 for module_type_body:
  - typ_expr --> mod_type
  - typ_expr_alg --> mod_type_alg
  - typ_* --> mod_*
 and adding two new fields to mtb:
  - mod_expr (always containing Abstract)
  - mod_retroknowledge (always containing [])

 This refactoring should be completely transparent for the user.

 Pros: code sharing, for instance subst_modtype = subst_module.
 Cons: a runtime invariant (mod_expr = Abstract) which isn't
 enforced by typing. I tried a polymorphic typing of mod_expr,
 to share field names while not having mtb = mb, but the OCaml
 typechecker isn't clever enough with polymorphic mutual fixpoints,
 and reject code sharing (e.g. between subst_modtype and subst_module).
 In the future (with ocaml>=4), some GADT could maybe help here,
 but for now the current solution seems good enough.

1 files changed, 26 insertions, 49 deletions

diff --git a/checker/modops.ml b/checker/modops.ml
index c27c5d598..1e5cd4347 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,13 +49,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mod_mp = mp;
-    mod_type = mtb.typ_expr;
-    mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = Abstract;
-    mod_constraints = mtb.typ_constraints;
-    mod_delta = mtb.typ_delta;
-    mod_retroknowledge = []}
+  { mtb with mod_mp = mp; mod_expr = Abstract }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -71,7 +65,7 @@ let rec add_structure mp sign resolver env =
 	    Environ.add_mind mind mib env
 	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
-	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
+	| SFBmodtype mtb -> Environ.add_modtype mtb.mod_mp mtb env
   in
   List.fold_left add_one env sign
 
@@ -97,23 +91,20 @@ let strengthen_const mp_from l cb resolver =
       { cb with const_body = Def (Declarations.from_val (Const (con,u))) }
 
 let rec strengthen_mod mp_from mp_to mb =
-  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then
-    mb
-  else
-    match mb.mod_type with
-     | NoFunctor (sign) ->
-	 let resolve_out,sign_out =
-	   strengthen_sig mp_from sign mp_to mb.mod_delta
-         in
-	 { mb with
-	   mod_expr = Algebraic (NoFunctor (MEident mp_to));
-	   mod_type = NoFunctor sign_out;
-	   mod_type_alg = mb.mod_type_alg;
-	   mod_constraints = mb.mod_constraints;
-	   mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to
-	   (add_delta_resolver mb.mod_delta resolve_out)*);
-	   mod_retroknowledge = mb.mod_retroknowledge}
-     | MoreFunctor _ -> mb
+  if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
+  else strengthen_body true mp_from mp_to mb
+
+and strengthen_body is_mod mp_from mp_to mb =
+  match mb.mod_type with
+  | MoreFunctor _ -> mb
+  | NoFunctor sign ->
+    let resolve_out,sign_out = strengthen_sig mp_from sign mp_to mb.mod_delta
+    in
+    { mb with
+      mod_expr =
+        (if is_mod then Algebraic (NoFunctor (MEident mp_to)) else Abstract);
+      mod_type = NoFunctor sign_out;
+      mod_delta = resolve_out }
 
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
@@ -137,33 +128,19 @@ and strengthen_sig mp_from sign mp_to resolver =
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out,item::rest'
 
-let strengthen mtb mp = match mtb.typ_expr with
-  | NoFunctor sign ->
-    let resolve_out,sign_out =
-      strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
-    in
-    { mtb with
-      typ_expr = NoFunctor sign_out;
-      typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
-      (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
-  | MoreFunctor _ -> mtb
+let strengthen mtb mp =
+  strengthen_body false mtb.mod_mp mp mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
 
-
 let module_type_of_module mp mb =
+  let mtb =
+    { mb with
+      mod_expr = Abstract;
+      mod_type_alg = None;
+      mod_retroknowledge = [] }
+  in
   match mp with
-  | Some mp ->
-    strengthen {
-      typ_mp = mp;
-      typ_expr = mb.mod_type;
-      typ_expr_alg = None;
-      typ_constraints = mb.mod_constraints;
-      typ_delta = mb.mod_delta} mp
-  | None ->
-    { typ_mp = mb.mod_mp;
-      typ_expr = mb.mod_type;
-      typ_expr_alg = None;
-      typ_constraints = mb.mod_constraints;
-      typ_delta = mb.mod_delta}
+  | Some mp -> strengthen {mtb with mod_mp = mp} mp
+  | None -> mtb