Separating the module_type and module_body types by using a type parameter.

As explained in edf85b9, the original commit that merged the module_body
and module_type_body representations, this was delayed to a later time
assumedly due to OCaml lack of GADTs. Actually, the only thing that was
needed was polymorphic recursion, which has been around already for a
relatively long time (since 3.12).

5 files changed, 30 insertions, 20 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 59dd5bc4d..6724fa3f0 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -385,9 +385,9 @@ and module_implementation =
   | Struct of module_signature (** interactive body *)
   | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and module_body =
+and 'a generic_module_body =
   { mod_mp : module_path; (** absolute path of the module *)
-    mod_expr : module_implementation; (** implementation *)
+    mod_expr : 'a; (** implementation *)
     mod_type : module_signature; (** expanded type *)
     (** algebraic type, kept if it's relevant for extraction *)
     mod_type_alg : module_expression option;
@@ -397,11 +397,12 @@ and module_body =
     mod_delta : delta_resolver;
     mod_retroknowledge : action list }
 
+and module_body = module_implementation generic_module_body
+
 (** A [module_type_body] is just a [module_body] with no
-    implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge] *)
+    implementation and also an empty [mod_retroknowledge] *)
 
-and module_type_body = module_body
+and module_type_body = unit generic_module_body
 
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 093d999a3..884a1ef18 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -583,24 +583,30 @@ 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_module sub) (subst_expr sub) me
+  functor_map (subst_module_type sub) (subst_expr sub) me
 
 and subst_signature sub sign =
-  functor_map (subst_module sub) (subst_structure sub) sign
+  functor_map (subst_module_type 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_module sub mtb)
+    | SFBmodtype mtb -> SFBmodtype (subst_module_type sub mtb)
   in
   List.map (fun (l,b) -> (l,subst_body b)) struc
 
-and subst_module sub mb =
+and subst_body : 'a. (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun subst_impl sub mb ->
   { mb with
     mod_mp = subst_mp sub mb.mod_mp;
-    mod_expr =
-      implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
+    mod_expr = subst_impl sub mb.mod_expr;
     mod_type = subst_signature sub mb.mod_type;
     mod_type_alg = Option.smartmap (subst_expression sub) mb.mod_type_alg }
+
+and subst_module sub mb =
+  subst_body (fun sub e -> implem_map (subst_signature sub) (subst_expression sub) e) sub mb
+
+and subst_module_type sub mb =
+  subst_body (fun _ () -> ()) sub mb
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index b6816dd48..de568e636 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -70,7 +70,7 @@ let lookup_module mp env =
 
 let mk_mtb mp sign delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = Univ.ContextSet.empty;
diff --git a/checker/modops.ml b/checker/modops.ml
index 79cd5c29f..726988752 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -93,17 +93,19 @@ let strengthen_const mp_from l cb resolver =
 
 let rec strengthen_mod mp_from mp_to mb =
   if Declarations.mp_in_delta mb.mod_mp mb.mod_delta then mb
-  else strengthen_body true mp_from mp_to mb
+  else
+    let mk_expr mp_to = Algebraic (NoFunctor (MEident mp_to)) in
+    strengthen_body mk_expr mp_from mp_to mb
 
-and strengthen_body is_mod mp_from mp_to mb =
+and strengthen_body : 'a. (_ -> 'a) -> _ -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun mk_expr 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_expr = mk_expr mp_to;
       mod_type = NoFunctor sign_out;
       mod_delta = resolve_out }
 
@@ -130,7 +132,7 @@ and strengthen_sig mp_from sign mp_to resolver =
 	resolve_out,item::rest'
 
 let strengthen mtb mp =
-  strengthen_body false mtb.mod_mp mp mtb
+  strengthen_body ignore 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)
@@ -138,7 +140,7 @@ let subst_and_strengthen mb mp =
 let module_type_of_module mp mb =
   let mtb =
     { mb with
-      mod_expr = Abstract;
+      mod_expr = ();
       mod_type_alg = None;
       mod_retroknowledge = [] }
   in
diff --git a/checker/values.ml b/checker/values.ml
index c95c3f1b2..f1edabcfb 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 c802f941f368bedd96e931cda0559d67  checker/cic.mli
+MD5 6bfeaec4872c9636faed4967db1502a0 checker/cic.mli
 
 *)
 
@@ -54,6 +54,7 @@ let v_enum name n = Sum(name,n,[||])
 
 let v_pair v1 v2 = v_tuple "*" [|v1; v2|]
 let v_bool = v_enum "bool" 2
+let v_unit = v_enum "unit" 1
 let v_ref v = v_tuple "ref" [|v|]
 
 let v_set v =
@@ -311,7 +312,7 @@ and v_impl =
   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_noimpl = v_unit
 and v_module =
   Tuple ("module_body",
          [|v_mp;v_impl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])