Merge PR #931: Parametrize module body

7 files changed, 71 insertions, 39 deletions

diff --git a/kernel/declarations.ml b/kernel/declarations.ml
index 9697b0b8b2..e17fb1c38f 100644
--- a/kernel/declarations.ml
+++ b/kernel/declarations.ml
@@ -250,16 +250,16 @@ 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 *)
     mod_type_alg : module_expression option; (** algebraic type *)
     mod_constraints : Univ.ContextSet.t; (**
       set of all universes constraints in the module  *)
     mod_delta : Mod_subst.delta_resolver; (**
       quotiented set of equivalent constants and inductive names *)
-    mod_retroknowledge : Retroknowledge.action list }
+    mod_retroknowledge : 'a module_retroknowledge }
 
 (** For a module, there are five possible situations:
     - [Declare Module M : T] then [mod_expr = Abstract; mod_type_alg = Some T]
@@ -269,13 +269,19 @@ and module_body =
     - [Module M : T. ... End M] then [mod_expr = Struct; mod_type_alg = Some T]
     And of course, all these situations may be functors or not. *)
 
-(** A [module_type_body] is just a [module_body] with no
-    implementation ([mod_expr] always [Abstract]) and also
-    an empty [mod_retroknowledge]. Its [mod_type_alg] contains
+and module_body = module_implementation generic_module_body
+
+(** A [module_type_body] is just a [module_body] with no implementation and
+    also an empty [mod_retroknowledge]. Its [mod_type_alg] contains
     the algebraic definition of this module type, or [None]
     if it has been built interactively. *)
 
-and module_type_body = module_body
+and module_type_body = unit generic_module_body
+
+and _ module_retroknowledge =
+| ModBodyRK :
+  Retroknowledge.action list -> module_implementation module_retroknowledge
+| ModTypeRK : unit module_retroknowledge
 
 (** Extra invariants :
 
diff --git a/kernel/declareops.ml b/kernel/declareops.ml
index 85dd1e66db..66d66c7d09 100644
--- a/kernel/declareops.ml
+++ b/kernel/declareops.ml
@@ -318,7 +318,7 @@ let rec hcons_structure_field_body sb = match sb with
   let mb' = hcons_module_body mb in
   if mb == mb' then sb else SFBmodule mb'
 | SFBmodtype mb ->
-  let mb' = hcons_module_body mb in
+  let mb' = hcons_module_type mb in
   if mb == mb' then sb else SFBmodtype mb'
 
 and hcons_structure_body sb =
@@ -331,10 +331,10 @@ and hcons_structure_body sb =
   List.smartmap map sb
 
 and hcons_module_signature ms =
-  hcons_functorize hcons_module_body hcons_structure_body hcons_module_signature ms
+  hcons_functorize hcons_module_type hcons_structure_body hcons_module_signature ms
 
 and hcons_module_expression me =
-  hcons_functorize hcons_module_body hcons_module_alg_expr hcons_module_expression me
+  hcons_functorize hcons_module_type hcons_module_alg_expr hcons_module_expression me
 
 and hcons_module_implementation mip = match mip with
 | Abstract -> Abstract
@@ -346,9 +346,11 @@ and hcons_module_implementation mip = match mip with
   if ms == ms' then mip else Struct ms
 | FullStruct -> FullStruct
 
-and hcons_module_body mb =
+and hcons_generic_module_body :
+  'a. ('a -> 'a) -> 'a generic_module_body -> 'a generic_module_body =
+  fun hcons_impl mb ->
   let mp' = mb.mod_mp in
-  let expr' = hcons_module_implementation mb.mod_expr in
+  let expr' = hcons_impl mb.mod_expr in
   let type' = hcons_module_signature mb.mod_type in
   let type_alg' = mb.mod_type_alg in
   let constraints' = Univ.hcons_universe_context_set mb.mod_constraints in
@@ -373,3 +375,9 @@ and hcons_module_body mb =
     mod_delta = delta';
     mod_retroknowledge = retroknowledge';
   }
+
+and hcons_module_body mb =
+  hcons_generic_module_body hcons_module_implementation mb
+
+and hcons_module_type mb =
+  hcons_generic_module_body (fun () -> ()) mb
diff --git a/kernel/declareops.mli b/kernel/declareops.mli
index a8ba5fa392..b2d29759da 100644
--- a/kernel/declareops.mli
+++ b/kernel/declareops.mli
@@ -78,3 +78,4 @@ val safe_flags : typing_flags
 val hcons_const_body : constant_body -> constant_body
 val hcons_mind : mutual_inductive_body -> mutual_inductive_body
 val hcons_module_body : module_body -> module_body
+val hcons_module_type : module_type_body -> module_type_body
diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 0888ccc109..d2b41aae98 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -264,7 +264,9 @@ let rec translate_mse env mpo inl = function
   |MEident mp1 as me ->
     let mb = match mpo with
       |Some mp -> strengthen_and_subst_mb (lookup_module mp1 env) mp false
-      |None -> lookup_modtype mp1 env
+      |None ->
+        let mt = lookup_modtype mp1 env in
+        module_body_of_type mt.mod_mp mt
     in
     mb.mod_type, me, mb.mod_delta, Univ.ContextSet.empty
   |MEapply (fe,mp1) ->
@@ -281,9 +283,11 @@ let mk_mod mp e ty cst reso =
     mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = reso;
-    mod_retroknowledge = [] }
+    mod_retroknowledge = ModBodyRK []; }
 
-let mk_modtype mp ty cst reso = mk_mod mp Abstract ty cst reso
+let mk_modtype mp ty cst reso =
+  let mb = mk_mod mp Abstract ty cst reso in
+  { mb with mod_expr = (); mod_retroknowledge = ModTypeRK }
 
 let rec translate_mse_funct env mpo inl mse = function
   |[] ->
@@ -319,6 +323,7 @@ let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
     { res_mtb with
       mod_mp = mp;
       mod_expr = impl;
+      mod_retroknowledge = ModBodyRK [];
       (** cst from module body typing,
           cst' from subtyping,
           constraints from module type. *)
diff --git a/kernel/modops.ml b/kernel/modops.ml
index a079bc8931..76915e917a 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -143,11 +143,12 @@ let rec functor_iter fty f0 = function
 (** {6 Misc operations } *)
 
 let module_type_of_module mb =
-  { mb with mod_expr = Abstract; mod_type_alg = None }
+  { mb with mod_expr = (); mod_type_alg = None;
+    mod_retroknowledge = ModTypeRK; }
 
 let module_body_of_type mp mtb =
-  assert (mtb.mod_expr == Abstract);
-  { mtb with mod_mp = mp }
+  { mtb with mod_expr = Abstract; mod_mp = mp;
+      mod_retroknowledge = ModBodyRK []; }
 
 let check_modpath_equiv env mp1 mp2 =
   if ModPath.equal mp1 mp2 then ()
@@ -196,7 +197,8 @@ let rec subst_structure sub do_delta sign =
   in
   List.smartmap subst_body sign
 
-and subst_body is_mod sub do_delta mb =
+and subst_body : 'a. _ -> _ -> (_ -> 'a -> 'a) -> _ -> 'a generic_module_body -> 'a generic_module_body =
+  fun is_mod sub subst_impl do_delta mb ->
   let { mod_mp=mp; mod_expr=me; mod_type=ty; mod_type_alg=aty } = mb in
   let mp' = subst_mp sub mp in
   let sub =
@@ -205,10 +207,7 @@ and subst_body is_mod sub do_delta mb =
     else add_mp mp mp' empty_delta_resolver sub
   in
   let ty' = subst_signature sub do_delta ty in
-  let me' =
-    implem_smartmap
-      (subst_signature sub id_delta) (subst_expression sub id_delta) me
-  in
+  let me' = subst_impl sub me in
   let aty' = Option.smartmap (subst_expression sub id_delta) aty in
   let delta' = do_delta mb.mod_delta sub in
   if mp==mp' && me==me' && ty==ty' && aty==aty' && delta'==mb.mod_delta
@@ -221,9 +220,14 @@ and subst_body is_mod sub do_delta mb =
       mod_type_alg = aty';
       mod_delta = delta' }
 
-and subst_module sub do_delta mb = subst_body true sub do_delta mb
+and subst_module sub do_delta mb =
+  subst_body true sub subst_impl do_delta mb
+
+and subst_impl sub me =
+  implem_smartmap
+    (subst_signature sub id_delta) (subst_expression sub id_delta) me
 
-and subst_modtype sub do_delta mtb = subst_body false sub do_delta mtb
+and subst_modtype sub do_delta mtb = subst_body false sub (fun _ () -> ()) do_delta mtb
 
 and subst_expr sub do_delta seb = match seb with
   |MEident mp ->
@@ -268,7 +272,7 @@ let add_retroknowledge mp =
       CErrors.anomaly ~label:"Modops.add_retroknowledge"
         (Pp.str "had to import an unsupported kind of term.")
   in
-  fun lclrk env ->
+  fun (ModBodyRK lclrk) env ->
   (* The order of the declaration matters, for instance (and it's at the
      time this comment is being written, the only relevent instance) the
      int31 type registration absolutely needs int31 bits to be registered.
@@ -567,7 +571,7 @@ let rec is_bounded_expr l = function
       is_bounded_expr l (MEident mp) || is_bounded_expr l fexpr
   | _ -> false
 
-let rec clean_module l mb =
+let rec clean_module_body l mb =
   let impl, typ = mb.mod_expr, mb.mod_type in
   let typ' = clean_signature l typ in
   let impl' = match impl with
@@ -577,19 +581,25 @@ let rec clean_module l mb =
   if typ==typ' && impl==impl' then mb
   else { mb with mod_type=typ'; mod_expr=impl' }
 
+and clean_module_type l mb =
+  let (), typ = mb.mod_expr, mb.mod_type in
+  let typ' = clean_signature l typ in
+  if typ==typ' then mb
+  else { mb with mod_type=typ' }
+
 and clean_field l field = match field with
   |(lab,SFBmodule mb) ->
-    let mb' = clean_module l mb in
+    let mb' = clean_module_body l mb in
     if mb==mb' then field else (lab,SFBmodule mb')
   |_ -> field
 
 and clean_structure l = List.smartmap (clean_field l)
 
 and clean_signature l =
-  functor_smartmap (clean_module l) (clean_structure l)
+  functor_smartmap (clean_module_type l) (clean_structure l)
 
 and clean_expression l =
-  functor_smartmap (clean_module l) (fun me -> me)
+  functor_smartmap (clean_module_type l) (fun me -> me)
 
 let rec collect_mbid l sign =  match sign with
   |MoreFunctor (mbid,ty,m) ->
@@ -613,14 +623,16 @@ let join_constant_body except otab cb =
   | _ -> ()
 
 let join_structure except otab s =
-  let rec join_module mb =
-    implem_iter join_signature join_expression mb.mod_expr;
+  let rec join_module : 'a. 'a generic_module_body -> unit = fun mb ->
     Option.iter join_expression mb.mod_type_alg;
     join_signature mb.mod_type
   and join_field (l,body) = match body with
     |SFBconst sb -> join_constant_body except otab sb
     |SFBmind _ -> ()
-    |SFBmodule m |SFBmodtype m -> join_module m
+    |SFBmodule m ->
+      implem_iter join_signature join_expression m.mod_expr;
+      join_module m
+    |SFBmodtype m -> join_module m
   and join_structure struc = List.iter join_field struc
   and join_signature sign =
     functor_iter join_module join_structure sign
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 04051f2e23..ad622b07d8 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -574,7 +574,7 @@ let add_mind dir l mie senv =
 let add_modtype l params_mte inl senv =
   let mp = MPdot(senv.modpath, l) in
   let mtb = Mod_typing.translate_modtype senv.env mp inl params_mte  in
-  let mtb = Declareops.hcons_module_body mtb in
+  let mtb = Declareops.hcons_module_type mtb in
   let senv' = add_field (l,SFBmodtype mtb) MT senv in
   mp, senv'
 
@@ -677,7 +677,7 @@ let build_module_body params restype senv =
       (struc,None,senv.modresolver,senv.univ) restype'
   in
   let mb' = functorize_module params mb in
-  { mb' with mod_retroknowledge = senv.local_retroknowledge }
+  { mb' with mod_retroknowledge = ModBodyRK senv.local_retroknowledge }
 
 (** Returning back to the old pre-interactive-module environment,
     with one extra component and some updated fields
@@ -732,12 +732,12 @@ let end_module l restype senv =
 
 let build_mtb mp sign cst delta =
   { mod_mp = mp;
-    mod_expr = Abstract;
+    mod_expr = ();
     mod_type = sign;
     mod_type_alg = None;
     mod_constraints = cst;
     mod_delta = delta;
-    mod_retroknowledge = [] }
+    mod_retroknowledge = ModTypeRK }
 
 let end_modtype l senv =
   let mp = senv.modpath in
@@ -853,7 +853,7 @@ let export ?except senv dir =
       mod_type_alg = None;
       mod_constraints = senv.univ;
       mod_delta = senv.modresolver;
-      mod_retroknowledge = senv.local_retroknowledge
+      mod_retroknowledge = ModBodyRK senv.local_retroknowledge
     }
   in
   let ast, symbols =
diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml
index b311165f10..b564b2a8c1 100644
--- a/kernel/subtyping.ml
+++ b/kernel/subtyping.ml
@@ -416,7 +416,7 @@ and check_modtypes cst env mtb1 mtb2 subst1 subst2 equiv =
 	     mod_type = subst_signature subst1 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 cst env body_t1 body_t2 equiv subst1 subst2