Merge PR #931: Parametrize module body

6 files changed, 41 insertions, 26 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index 59dd5bc4d3..753fd0fc00 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;
@@ -395,13 +395,19 @@ and module_body =
     mod_constraints : Univ.ContextSet.t;
     (** quotiented set of equivalent constants and inductive names *)
     mod_delta : delta_resolver;
-    mod_retroknowledge : action list }
+    mod_retroknowledge : 'a module_retroknowledge; }
+
+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 = unit generic_module_body
 
-and module_type_body = module_body
+and _ module_retroknowledge =
+| ModBodyRK :
+  action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
 
 (*************************************************************************)
 (** {4 From safe_typing.ml} *)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 093d999a34..884a1ef18c 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 b6816dd484..3c9e1cac54 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -70,12 +70,12 @@ 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;
     mod_delta = delta;
-    mod_retroknowledge = []; }
+    mod_retroknowledge = ModTypeRK; }
 
 let rec check_module env mp mb =
   let (_:module_signature) =
diff --git a/checker/modops.ml b/checker/modops.ml
index 79cd5c29fd..f0abc39eac 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -49,7 +49,7 @@ let destr_functor = function
   | NoFunctor _ -> error_not_a_functor ()
 
 let module_body_of_type mp mtb =
-  { mtb with mod_mp = mp; mod_expr = Abstract }
+  { mtb with mod_mp = mp; mod_expr = Abstract; mod_retroknowledge = ModBodyRK [] }
 
 let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
@@ -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,9 +140,9 @@ 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 = [] }
+      mod_retroknowledge = ModTypeRK }
   in
   match mp with
   | Some mp -> strengthen {mtb with mod_mp = mp} mp
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 68a467bea2..98a9c8250d 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -393,7 +393,7 @@ and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
 			  mod_type = body_t1;
 			  mod_type_alg = None;
 			  mod_constraints = mtb1.mod_constraints;
-			  mod_retroknowledge = [];
+			  mod_retroknowledge = ModBodyRK [];
 			  mod_delta = mtb1.mod_delta} env
 	  in
 	  check_structure env body_t1 body_t2 equiv
diff --git a/checker/values.ml b/checker/values.ml
index c95c3f1b2b..afde84854c 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 62a4037e9e584d508909d631c5e8a759 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,13 +312,13 @@ 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|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;Any|])
+         [|v_mp;v_noimpl;v_sign;Opt v_mexpr;v_context_set;v_resolver;v_unit|])
 
 (** kernel/safe_typing *)