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.

6 files changed, 65 insertions, 103 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index c8b7c9e66..75ce98e90 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -365,7 +365,7 @@ and module_signature = (module_type_body,structure_body) functorize
 and module_expression = (module_type_body,module_alg_expr) functorize
 
 and module_implementation =
-  | Abstract (** no accessible implementation *)
+  | Abstract (** no accessible implementation (keep this constructor first!) *)
   | 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] *)
@@ -382,18 +382,11 @@ and module_body =
     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 =
-  { 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}
+(** A [module_type_body] is just a [module_body] with no
+    implementation ([mod_expr] always [Abstract]) and also
+    an empty [mod_retroknowledge] *)
 
+and module_type_body = module_body
 
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index d38df793f..c6709a785 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -591,23 +591,17 @@ let rec subst_expr sub = function
   | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
 
 let rec subst_expression sub me =
-  functor_map (subst_modtype sub) (subst_expr sub) me
+  functor_map (subst_module sub) (subst_expr sub) me
 
 and subst_signature sub sign =
-  functor_map (subst_modtype sub) (subst_structure sub) sign
-
-and subst_modtype sub mtb=
-  { mtb with
-    typ_mp = subst_mp sub mtb.typ_mp;
-    typ_expr = subst_signature sub mtb.typ_expr;
-    typ_expr_alg = Option.smartmap (subst_expression sub) mtb.typ_expr_alg }
+  functor_map (subst_module sub) (subst_structure sub) sign
 
 and subst_structure sub struc =
   let subst_body = function
     | SFBconst cb -> SFBconst (subst_const_body sub cb)
     | SFBmind mib -> SFBmind (subst_mind sub mib)
-    | SFBmodule mb -> SFBmodule (subst_module sub  mb)
-    | SFBmodtype mtb -> SFBmodtype (subst_modtype sub mtb)
+    | SFBmodule mb -> SFBmodule (subst_module sub mb)
+    | SFBmodtype mtb -> SFBmodtype (subst_module sub mtb)
   in
   List.map (fun (l,b) -> (l,subst_body b)) struc
 
@@ -617,5 +611,4 @@ and subst_module sub mb =
     mod_expr =
       implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
-    mod_type_alg = Option.map (subst_expression sub) mb.mod_type_alg }
-
+    mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 9e61d3491..998e23c6e 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -64,6 +64,15 @@ let lookup_module mp env =
   with Not_found ->
     failwith ("Unknown module: "^string_of_mp mp)
 
+let mk_mtb mp sign delta =
+  { mod_mp = mp;
+    mod_expr = Abstract;
+    mod_type = sign;
+    mod_type_alg = None;
+    mod_constraints = Univ.Constraint.empty;
+    mod_delta = delta;
+    mod_retroknowledge = []; }
+
 let rec check_module env mp mb =
   let (_:module_signature) =
     check_signature env mb.mod_type mb.mod_mp mb.mod_delta
@@ -76,25 +85,14 @@ let rec check_module env mp mb =
   match optsign with
   |None -> ()
   |Some sign ->
-    let mtb1 =
-      {typ_mp=mp;
-       typ_expr=sign;
-       typ_expr_alg=None;
-       typ_constraints=Univ.Constraint.empty;
-       typ_delta = mb.mod_delta;}
-    and mtb2 =
-      {typ_mp=mp;
-       typ_expr=mb.mod_type;
-       typ_expr_alg=None;
-       typ_constraints=Univ.Constraint.empty;
-       typ_delta = mb.mod_delta;}
-    in
+    let mtb1 = mk_mtb mp sign mb.mod_delta
+    and mtb2 = mk_mtb mp mb.mod_type mb.mod_delta in
     let env = add_module_type mp mtb1 env in
     Subtyping.check_subtypes env mtb1 mtb2
 
 and check_module_type env mty =
   let (_:module_signature) =
-    check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in
+    check_signature env mty.mod_type mty.mod_mp mty.mod_delta in
   ()
 
 and check_structure_field env mp lab res = function
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
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 0144580bc..fe88a5071 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -354,52 +354,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
 		| _ -> error_not_match l spec2
 	    in
 	    let env =
-              add_module_type mtb2.typ_mp mtb2
-	        (add_module_type mtb1.typ_mp mtb1 env)
+              add_module_type mtb2.mod_mp mtb2
+	        (add_module_type mtb1.mod_mp mtb1 env)
             in
 	    check_modtypes env mtb1 mtb2 subst1 subst2 true
   in
   List.iter check_one_body sig2
 
 and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
-  if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then ()
+  if mtb1==mtb2 || mtb1.mod_type == mtb2.mod_type then ()
   else
     let rec check_structure  env str1 str2 equiv subst1 subst2 =
       match str1,str2 with
       | NoFunctor (list1),
         NoFunctor (list2) ->
-	  check_signatures env mtb1.typ_mp list1 list2 subst1 subst2;
+	  check_signatures env mtb1.mod_mp list1 list2 subst1 subst2;
 	  if equiv then
-	    check_signatures env mtb2.typ_mp list2 list1 subst1 subst2
+	    check_signatures env mtb2.mod_mp list2 list1 subst1 subst2
 	  else
 	    ()
       | MoreFunctor (arg_id1,arg_t1,body_t1),
 	MoreFunctor (arg_id2,arg_t2,body_t2) ->
 	  check_modtypes env
 	    arg_t2 arg_t1
-	    (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+	    (map_mp arg_t1.mod_mp arg_t2.mod_mp) subst2
 	    equiv;
 	  (* contravariant *)
 	  let env = add_module_type (MPbound arg_id2) arg_t2 env in
 	  let env =
             if is_functor body_t1 then env
             else
-	      let env = shallow_remove_module mtb1.typ_mp env in
-	      add_module {mod_mp = mtb1.typ_mp;
+	      let env = shallow_remove_module mtb1.mod_mp env in
+	      add_module {mod_mp = mtb1.mod_mp;
 			  mod_expr = Abstract;
 			  mod_type = body_t1;
 			  mod_type_alg = None;
-			  mod_constraints = mtb1.typ_constraints;
+			  mod_constraints = mtb1.mod_constraints;
 			  mod_retroknowledge = [];
-			  mod_delta = mtb1.typ_delta} env
+			  mod_delta = mtb1.mod_delta} env
 	  in
 	  check_structure env body_t1 body_t2 equiv
 	    (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
 	    subst2
       | _ , _ -> error_incompatible_modtypes mtb1 mtb2
     in
-    check_structure env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
+    check_structure env mtb1.mod_type mtb2.mod_type equiv subst1 subst2
 
 let check_subtypes env sup super =
-  check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
-      (map_mp super.typ_mp sup.typ_mp) false
+  check_modtypes env (strengthen sup sup.mod_mp) super empty_subst
+      (map_mp super.mod_mp sup.mod_mp) false
diff --git a/checker/values.ml b/checker/values.ml
index 0ac8bf78c..5c4876e59 100644
--- a/checker/values.ml
+++ b/checker/values.ml
@@ -13,7 +13,7 @@
 To ensure this file is up-to-date, 'make' now compares the md5 of cic.mli
 with a copy we maintain here:
 
-MD5 27f35ee65fef280d5a7a80bb11b31837 checker/cic.mli
+MD5 f4d390282966a3fbd22a9e384046d231 checker/cic.mli
 
 *)
 
@@ -296,15 +296,16 @@ and v_mexpr =
   [|[|v_mae|];                     (* NoFunctor *)
     [|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *)
 and v_impl =
-  Sum ("module_impl",2,
+  Sum ("module_impl",2, (* Abstract, FullStruct *)
   [|[|v_mexpr|];  (* Algebraic *)
     [|v_sign|]|])  (* Struct *)
+and v_noimpl = v_enum "no_impl" 1 (* Abstract is mandatory for mtb *)
 and v_module =
   Tuple ("module_body",
          [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_sign;Opt v_mexpr;v_cstrs;v_resolver|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
 
 (** kernel/safe_typing *)