Declarations.mli: reorganization of modular structures

 The earlier type [struct_expr_body] was far too broad,
 leading to code with unclear invariants, many "assert false", etc etc.
 Its replacement [module_alg_expr] has only three constructors:
   * MEident
   * MEapply : note the module_path as 2nd arg, no more constraints here
   * MEwith : no more constant_body inside, constr is just fine
 But no more SEBfunctor or SEBstruct constructor here (see below).
 This way, this datatype corresponds to algebraic expressions,
 i.e. anything that can appear in non-interactive modules.
 In fact, it even coincides now with [Entries.module_struct_entry].

 - Functor constructors are now necessarily on top of other
   structures thanks to a generic [functorize] datatype.

 - Structures are now separated from algebraic expressions by design :
   the [mod_type] and [typ_expr] fields now only contain structures
   (or functorized structures), while [mod_type_alg] and [typ_expr_alg]
   are restricted to algebraic expressions only.

 - Only the implementation field [mod_expr] could be either algebraic
   or structural. We handle this via a specialized datatype
   [module_implementation] with four constructors:

    * Abstract : no implementation (cf. for instance Declare Module)
    * Algebraic(_) : for non-interactive modules, e.g. Module M := N.
    * Struct(_) : for interactive module, e.g. Module M : T. ... End M.
    * FullStruct : for interactive module with no type restriction.

   The [FullStruct] is a particular case of [Struct] where the implementation
   need not be stored at all, since it is exactly equal to its expanded
   type present in [mod_type]. This is less fragile than hoping as earlier
   that pointer equality between [mod_type] and [mod_expr] will be
   preserved...

 - We clearly emphasize that only [mod_type] and [typ_expr] are
   relevant for the kernel, while [mod_type_alg] and [typ_expr_alg]
   are there only for a nicer extraction and shorter module printing.
   [mod_expr] is also not accessed by the kernel, but it is important
   for Print Assumptions later.

 - A few implicit invariants remain, for instance "no MEwith in mod_expr",
   see the final comment in Declarations

 - Heavy refactoring of module-related files : modops, mod_typing,
   safe_typing, declaremods, extraction/extract_env.ml ...

 - Coqchk has been adapted accordingly. The code concerning MEwith
   in Mod_checking is now gone, since we cannot have any in mod_expr.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16712 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 183 insertions, 285 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index d5555c624..7794f19be 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -20,17 +20,13 @@ open Environ
 open Modops
 open Mod_subst
 
-exception Not_path
-
-let path_of_mexpr = function
-  | MSEident mp -> mp
-  | _ -> raise Not_path
+type 'alg translation =
+  module_signature * 'alg option * delta_resolver * Univ.constraints
 
 let rec mp_from_mexpr = function
-  | MSEident mp -> mp
-  | MSEapply (expr,_) -> mp_from_mexpr expr
-  | MSEfunctor (_,_,expr) -> mp_from_mexpr expr
-  | MSEwith (expr,_) -> mp_from_mexpr expr
+  | MEident mp -> mp
+  | MEapply (expr,_) -> mp_from_mexpr expr
+  | MEwith (expr,_) -> mp_from_mexpr expr
 
 let is_modular = function
   | SFBmodule _ | SFBmodtype _ -> true
@@ -39,7 +35,7 @@ let is_modular = function
 (** Split a [structure_body] at some label corresponding to
     a modular definition or not. *)
 
-let split_sign k m struc =
+let split_struc k m struc =
   let rec split rev_before = function
     | [] -> raise Not_found
     | (k',b)::after when Label.equal k k' && (is_modular b) == (m : bool) ->
@@ -48,8 +44,8 @@ let split_sign k m struc =
   in split [] struc
 
 let discr_resolver mtb = match mtb.typ_expr with
-  | SEBstruct _ -> mtb.typ_delta
-  | _ -> empty_delta_resolver (* when mp is a functor *)
+  | NoFunctor _ -> mtb.typ_delta
+  | MoreFunctor _ -> empty_delta_resolver
 
 let rec rebuild_mp mp l =
   match l with
@@ -58,19 +54,15 @@ let rec rebuild_mp mp l =
 
 let (+++) = Univ.union_constraints
 
-let rec check_with_def env sign (idl,c) mp equiv =
-  let sig_b = match sign with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> error_signature_expected sign
-  in
+let rec check_with_def env struc (idl,c) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
   in
   try
     let modular = not (List.is_empty idl) in
-    let before,spec,after = split_sign lab modular sig_b in
-    let env' = Modops.add_signature mp before equiv env in
+    let before,spec,after = split_struc lab modular struc in
+    let env' = Modops.add_structure mp before equiv env in
     if List.is_empty idl then
       (* Toplevel definition *)
       let cb = match spec with
@@ -80,27 +72,26 @@ let rec check_with_def env sign (idl,c) mp equiv =
       (* In the spirit of subtyping.check_constant, we accept
          any implementations of parameters and opaques terms,
 	 as long as they have the right type *)
-      let def,cst = match cb.const_body with
+      let c',cst = match cb.const_body with
 	| Undef _ | OpaqueDef _ ->
 	  let j,cst1 = Typeops.infer env' c in
 	  let typ = Typeops.type_of_constant_type env' cb.const_type in
 	  let cst2 = Reduction.conv_leq env' j.uj_type typ in
 	  let cst = Future.force cb.const_constraints +++ cst1 +++ cst2 in
-	  let def = Def (Lazyconstr.from_val j.uj_val) in
-	  def,cst
+	  j.uj_val,cst
 	| Def cs ->
 	  let cst1 = Reduction.conv env' c (Lazyconstr.force cs) in
 	  let cst = Future.force cb.const_constraints +++ cst1 in
-	  let def = Def (Lazyconstr.from_val c) in
-	  def,cst
+          c, cst
       in
+      let def = Def (Lazyconstr.from_val c') in
       let cb' =
 	{ cb with
 	  const_body = def;
 	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def);
 	  const_constraints = Future.from_val cst }
       in
-      SEBstruct(before@(lab,SFBconst(cb'))::after),cb',cst
+      before@(lab,SFBconst(cb'))::after, c', cst
     else
       (* Definition inside a sub-module *)
       let mb = match spec with
@@ -108,33 +99,30 @@ let rec check_with_def env sign (idl,c) mp equiv =
 	| _ -> error_not_a_module (Label.to_string lab)
       in
       begin match mb.mod_expr with
-      | Some _ -> error_generative_module_expected lab
-      | None ->
-	let sign,cb,cst =
-          check_with_def env' mb.mod_type (idl,c) (MPdot(mp,lab)) mb.mod_delta
+      | Abstract ->
+        let struc = Modops.destr_nofunctor mb.mod_type in
+        let struc',c',cst =
+          check_with_def env' struc (idl,c) (MPdot(mp,lab)) mb.mod_delta
         in
         let mb' = { mb with
-          mod_type = sign;
+          mod_type = NoFunctor struc';
 	  mod_type_alg = None }
         in
-	SEBstruct(before@(lab,SFBmodule mb')::after),cb,cst
+	before@(lab,SFBmodule mb')::after, c', cst
+      | _ -> error_generative_module_expected lab
       end
   with
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let rec check_with_mod env sign (idl,mp1) mp equiv =
-  let sig_b = match sign with
-    | SEBstruct(sig_b) -> sig_b
-    | _ -> error_signature_expected sign
-  in
+let rec check_with_mod env struc (idl,mp1) mp equiv =
   let lab,idl = match idl with
     | [] -> assert false
     | id::idl -> Label.of_id id, idl
   in
   try
-    let before,spec,after = split_sign lab true sig_b in
-    let env' = Modops.add_signature mp before equiv env in
+    let before,spec,after = split_struc lab true struc in
+    let env' = Modops.add_structure mp before equiv env in
     let old = match spec with
       | SFBmodule mb -> mb
       | _ -> error_not_a_module (Label.to_string lab)
@@ -142,33 +130,35 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
     if List.is_empty idl then
       (* Toplevel module definition *)
       let mb_mp1 = lookup_module mp1 env in
-      let mtb_mp1 = module_type_of_module None mb_mp1  in
+      let mtb_mp1 = module_type_of_module mb_mp1 in
       let cst = match old.mod_expr with
-	| None ->
+	| Abstract ->
 	  begin
             try
-              let mtb_old = module_type_of_module None old in
+              let mtb_old = module_type_of_module old in
               Subtyping.check_subtypes env' mtb_mp1 mtb_old
                 +++ old.mod_constraints
 	    with Failure _ -> error_incorrect_with_constraint lab
 	  end
-	| Some (SEBident(mp')) ->
+	| Algebraic (NoFunctor (MEident(mp'))) ->
 	  check_modpath_equiv env' mp1 mp';
 	  old.mod_constraints
-	| _ ->  error_generative_module_expected lab
+	| _ -> error_generative_module_expected lab
       in
       let mp' = MPdot (mp,lab) in
       let new_mb = strengthen_and_subst_mb mb_mp1 mp' false in
-      let new_mb' = {new_mb with
-        mod_mp = mp';
-        mod_expr = Some (SEBident mp1);
-        mod_constraints = cst }
+      let new_mb' =
+        { new_mb with
+          mod_mp = mp';
+          mod_expr = Algebraic (NoFunctor (MEident mp1));
+          mod_constraints = cst }
       in
+      let new_equiv = add_delta_resolver equiv new_mb.mod_delta in
       (* we propagate the new equality in the rest of the signature
 	 with the identity substitution accompagned by the new resolver*)
       let id_subst = map_mp mp' mp' new_mb.mod_delta in
-      SEBstruct(before@(lab,SFBmodule new_mb')::subst_signature id_subst after),
-      add_delta_resolver equiv new_mb.mod_delta,cst
+      let new_after = subst_structure id_subst after in
+      before@(lab,SFBmodule new_mb')::new_after, new_equiv, cst
     else
       (* Module definition of a sub-module *)
       let mp' = MPdot (mp,lab) in
@@ -177,255 +167,163 @@ let rec check_with_mod env sign (idl,mp1) mp equiv =
 	| _ -> error_not_a_module (Label.to_string lab)
       in
       begin match old.mod_expr with
-      | None ->
-	let sign,equiv',cst =
-	  check_with_mod env' old.mod_type (idl,mp1) mp' old.mod_delta in
+      | Abstract ->
+        let struc = destr_nofunctor old.mod_type in
+	let struc',equiv',cst =
+          check_with_mod env' struc (idl,mp1) mp' old.mod_delta
+        in
+	let new_mb =
+          { old with
+            mod_type = NoFunctor struc';
+            mod_type_alg = None;
+            mod_delta = equiv' }
+        in
 	let new_equiv = add_delta_resolver equiv equiv' in
-	let new_mb = { old with
-          mod_type = sign;
-          mod_type_alg = None;
-          mod_delta = equiv'}
-	in
 	let id_subst = map_mp mp' mp' equiv' in
-	SEBstruct(before@(lab,SFBmodule new_mb)::subst_signature id_subst after),
-	new_equiv,cst
-      | Some (SEBident mp0) ->
+        let new_after = subst_structure id_subst after in
+	before@(lab,SFBmodule new_mb)::new_after, new_equiv, cst
+      | Algebraic (NoFunctor (MEident mp0)) ->
 	let mpnew = rebuild_mp mp0 idl in
 	check_modpath_equiv env' mpnew mp;
-	SEBstruct(before@(lab,spec)::after),equiv,Univ.empty_constraint
+	before@(lab,spec)::after, equiv, Univ.empty_constraint
       | _ -> error_generative_module_expected lab
       end
   with
   | Not_found -> error_no_such_label lab
   | Reduction.NotConvertible -> error_incorrect_with_constraint lab
 
-let check_with env sign with_decl alg_sign mp equiv =
-  let sign,wd,equiv,cst= match with_decl with
-    | With_Definition (idl,c) ->
-	let sign,cb,cst = check_with_def env sign (idl,c) mp equiv in
-	sign,With_definition_body(idl,cb),equiv,cst
-    | With_Module (idl,mp1) ->
-	let sign,equiv,cst = check_with_mod env sign (idl,mp1) mp equiv in
-	sign,With_module_body(idl,mp1),equiv,cst
-  in
-  match alg_sign with
-  | None -> sign, None, equiv, cst
-  | Some s -> sign, Some (SEBwith(s, wd)), equiv, cst
-
-let rec translate_module env mp inl me =
-  match me.mod_entry_expr, me.mod_entry_type with
-    | None, None ->
-	Errors.anomaly ~label:"Mod_typing.translate_module"
-          (Pp.str "empty type and expr in module entry")
-    | None, Some mte ->
-	let mtb = translate_module_type env mp inl mte in
-	  { mod_mp = mp;
-	    mod_expr = None;
-	    mod_type = mtb.typ_expr;
-	    mod_type_alg = mtb.typ_expr_alg;
-	    mod_delta = mtb.typ_delta;
-	    mod_constraints = mtb.typ_constraints; 
-	    mod_retroknowledge = []}
-   | Some mexpr, _ ->
-	let sign,alg_implem,resolver,cst1 =
-	  translate_struct_module_entry env mp inl mexpr in
-	let sign,alg1,resolver,cst2 =
-	  match me.mod_entry_type with
-	    | None ->
-		sign,None,resolver,Univ.empty_constraint
-	    | Some mte ->
-		let mtb = translate_module_type env mp inl mte in
-                let cst = Subtyping.check_subtypes env
-		  {typ_mp = mp;
-		   typ_expr = sign;
-		   typ_expr_alg = None;
-		   typ_constraints = Univ.empty_constraint;
-		   typ_delta = resolver;}
-		  mtb
-		in
-		  mtb.typ_expr,mtb.typ_expr_alg,mtb.typ_delta,cst
-	in
-	  { mod_mp = mp;
-	    mod_type = sign;
-	    mod_expr = alg_implem;
-	    mod_type_alg = alg1;
-	    mod_constraints = cst1 +++ cst2;
-	    mod_delta = resolver;
-	    mod_retroknowledge = []} 
-	    (* spiwack: not so sure about that. It may
-	       cause a bug when closing nested modules.
-	       If it does, I don't really know how to
-	       fix the bug.*)
-
-and translate_apply env inl ftrans mexpr mkalg =
-  let sign,alg,resolver,cst1 = ftrans in
+let mk_alg_with alg wd = Option.map (fun a -> MEwith (a,wd)) alg
+
+let check_with env mp (sign,alg,reso,cst) = function
+  |WithDef(idl,c) ->
+    let struc = destr_nofunctor sign in
+    let struc',c',cst' = check_with_def env struc (idl,c) mp reso in
+    let alg' = mk_alg_with alg (WithDef (idl,c')) in
+    (NoFunctor struc'),alg',reso, cst+++cst'
+  |WithMod(idl,mp1) as wd ->
+    let struc = destr_nofunctor sign in
+    let struc',reso',cst' = check_with_mod env struc (idl,mp1) mp reso in
+    let alg' = mk_alg_with alg wd in
+    (NoFunctor struc'),alg',reso', cst+++cst'
+
+let mk_alg_app mpo alg arg = match mpo, alg with
+  | Some _, Some alg -> Some (MEapply (alg,arg))
+  | _ -> None
+
+(** Translation of a module struct entry :
+    - We translate to a module when a [module_path] is given,
+      otherwise to a module type.
+    - The first output is the expanded signature
+    - The second output is the algebraic expression, kept for the extraction.
+      It is never None when translating to a module, but for module type
+      it could not be contain [SEBapply] or [SEBfunctor].
+*)
+
+let rec translate_mse env mpo inl = function
+  |MEident mp1 ->
+    let sign,reso = match mpo with
+      |Some mp ->
+        let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp false in
+        mb.mod_type, mb.mod_delta
+      |None ->
+        let mtb = lookup_modtype mp1 env in
+        mtb.typ_expr, mtb.typ_delta
+    in
+    sign,Some (MEident mp1),reso,Univ.empty_constraint
+  |MEapply (fe,mp1) ->
+    translate_apply env inl (translate_mse env mpo inl fe) mp1 (mk_alg_app mpo)
+  |MEwith(me, with_decl) ->
+    assert (mpo == None); (* No 'with' syntax for modules *)
+    let mp = mp_from_mexpr me in
+    check_with env mp (translate_mse env None inl me) with_decl
+
+and translate_apply env inl (sign,alg,reso,cst1) mp1 mkalg =
   let farg_id, farg_b, fbody_b = destr_functor sign in
-  let mp1 =
-    try path_of_mexpr mexpr
-    with Not_path -> error_application_to_not_path mexpr
-  in
-  let mtb = module_type_of_module None (lookup_module mp1 env) in
+  let mtb = module_type_of_module (lookup_module mp1 env) in
   let cst2 = Subtyping.check_subtypes env mtb farg_b in
   let mp_delta = discr_resolver mtb in
   let mp_delta = inline_delta_resolver env inl mp1 farg_id farg_b mp_delta in
   let subst = map_mbid farg_id mp1 mp_delta in
-  subst_struct_expr subst fbody_b,
-  mkalg alg mp1 cst2,
-  subst_codom_delta_resolver subst resolver,
-  cst1 +++ cst2
-
-and translate_functor env inl arg_id arg_e trans mkalg =
-  let mtb = translate_module_type env (MPbound arg_id) inl arg_e in
-  let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-  let sign,alg,resolver,cst = trans env'
+  let body = subst_signature subst fbody_b in
+  let alg' = mkalg alg mp1 in
+  let reso' = subst_codom_delta_resolver subst reso in
+  body,alg',reso', cst1 +++ cst2
+
+let mk_alg_funct mpo mbid mtb alg = match mpo, alg with
+  | Some _, Some alg -> Some (MoreFunctor (mbid,mtb,alg))
+  | _ -> None
+
+let rec translate_mse_funct env mpo inl mse = function
+  |[] ->
+    let sign,alg,reso,cst = translate_mse env mpo inl mse in
+    sign, Option.map (fun a -> NoFunctor a) alg, reso, cst
+  |(mbid, ty) :: params ->
+    let mp_id = MPbound mbid in
+    let mtb = translate_modtype env mp_id inl ([],ty) in
+    let env' = add_module_type mp_id mtb env in
+    let sign,alg,reso,cst = translate_mse_funct env' mpo inl mse params in
+    let alg' = mk_alg_funct mpo mbid mtb alg in
+    MoreFunctor (mbid, mtb, sign), alg',reso, cst +++ mtb.typ_constraints
+
+and translate_modtype env mp inl (params,mte) =
+  let sign,alg,reso,cst = translate_mse_funct env None inl mte params in
+  let mtb =
+    { typ_mp = mp_from_mexpr mte;
+      typ_expr = sign;
+      typ_expr_alg = None;
+      typ_constraints = cst;
+      typ_delta = reso }
   in
-  SEBfunctor (arg_id, mtb, sign),
-  mkalg alg arg_id mtb,
-  resolver,
-  cst +++ mtb.typ_constraints
-
-and translate_struct_module_entry env mp inl = function
-  | MSEident mp1 ->
-      let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp false in
-      mb'.mod_type, Some (SEBident mp1), mb'.mod_delta,Univ.empty_constraint
-  | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let trans env' = translate_struct_module_entry env' mp inl body_expr in
-      let mkalg a id m = Option.map (fun a -> SEBfunctor (id,m,a)) a in
-      translate_functor env inl arg_id arg_e trans mkalg
-  | MSEapply (fexpr,mexpr) ->
-      let trans = translate_struct_module_entry env mp inl fexpr in
-      let mkalg a mp c = Option.map (fun a -> SEBapply(a,SEBident mp,c)) a in
-      translate_apply env inl trans mexpr mkalg
-  | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 =
-	translate_struct_module_entry env mp inl mte in
-      let sign,alg,resolve,cst2 =
-	check_with env sign with_decl alg mp resolve in
-      sign,alg,resolve, cst1 +++ cst2
-
-and translate_struct_type_entry env inl = function
-  | MSEident mp1 ->
-      let mtb = lookup_modtype mp1 env in
-      mtb.typ_expr,Some (SEBident mp1),mtb.typ_delta,Univ.empty_constraint
-  | MSEfunctor (arg_id, arg_e, body_expr) ->
-      let trans env' = translate_struct_type_entry env' inl body_expr in
-      translate_functor env inl arg_id arg_e trans (fun _ _ _ -> None)
-  | MSEapply (fexpr,mexpr) ->
-      let trans = translate_struct_type_entry env inl fexpr in
-      translate_apply env inl trans mexpr (fun _ _ _ -> None)
-  | MSEwith(mte, with_decl) ->
-      let sign,alg,resolve,cst1 = translate_struct_type_entry env inl mte in
-      let sign,alg,resolve,cst2 =
-	check_with env sign with_decl alg (mp_from_mexpr mte) resolve
-      in
-      sign,alg,resolve, cst1 +++ cst2
-
-and translate_module_type env mp inl mte =
-  let mp_from = mp_from_mexpr mte in
-  let sign,alg,resolve,cst = translate_struct_type_entry env inl mte in
-  let mtb = subst_modtype_and_resolver
-    {typ_mp = mp_from;
-     typ_expr = sign;
-     typ_expr_alg = None;
-     typ_constraints = cst;
-     typ_delta = resolve} mp
-  in {mtb with typ_expr_alg = alg}
-
-let rec translate_struct_include_module_entry env mp inl = function
-  | MSEident mp1 ->
-      let mb = lookup_module mp1 env in
-      let mb' = strengthen_and_subst_mb mb mp true in
-      let mb_typ = clean_bounded_mod_expr mb'.mod_type in
-      mb_typ,None,mb'.mod_delta,Univ.empty_constraint
-  | MSEapply (fexpr,mexpr) ->
-      let ftrans = translate_struct_include_module_entry env mp inl fexpr in
-      translate_apply env inl ftrans mexpr (fun _ _ _ -> None)
-  | _ -> Modops.error_higher_order_include ()
-
-let rec add_struct_expr_constraints env = function
-  | SEBident _ -> env
-
-  | SEBfunctor (_,mtb,meb) ->
-      add_struct_expr_constraints
-	(add_modtype_constraints env mtb) meb
-
-  | SEBstruct (structure_body) ->
-      List.fold_left
-        (fun env (_,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-      Environ.add_constraints cst
-        (add_struct_expr_constraints
-	  (add_struct_expr_constraints env meb1)
-	  meb2)
-  | SEBwith(meb,With_definition_body(_,cb))->
-      Environ.add_constraints (Future.force cb.const_constraints)
-	(add_struct_expr_constraints env meb)
-  | SEBwith(meb,With_module_body(_,_))->
-      add_struct_expr_constraints env meb
-		
-and add_struct_elem_constraints env = function 
-  | SFBconst cb -> 
-      Environ.add_constraints (Future.force cb.const_constraints) env
-  | SFBmind mib -> Environ.add_constraints mib.mind_constraints env
-  | SFBmodule mb -> add_module_constraints env mb
-  | SFBmodtype mtb -> add_modtype_constraints env mtb
-
-and add_module_constraints env mb =
-  let env = match mb.mod_expr with
-    | None -> env
-    | Some meb -> add_struct_expr_constraints env meb
-  in
-  let env =
-    add_struct_expr_constraints env mb.mod_type
-  in
-    Environ.add_constraints mb.mod_constraints env
-
-and add_modtype_constraints env mtb =
-  Environ.add_constraints mtb.typ_constraints
-    (add_struct_expr_constraints env mtb.typ_expr)
-
-
-let rec struct_expr_constraints cst = function
-  | SEBident _ -> cst
-
-  | SEBfunctor (_,mtb,meb) ->
-      struct_expr_constraints
-	(modtype_constraints cst mtb) meb
-
-  | SEBstruct (structure_body) ->
-      List.fold_left
-        (fun cst (_,item) -> struct_elem_constraints cst item)
-        cst
-        structure_body
-
-  | SEBapply (meb1,meb2,cst1) ->
-      struct_expr_constraints (struct_expr_constraints (cst1 +++ cst) meb1)
-        meb2
-  | SEBwith(meb,With_definition_body(_,cb))->
-      struct_expr_constraints ((Future.force cb.const_constraints) +++ cst) meb
-  | SEBwith(meb,With_module_body(_,_))->
-      struct_expr_constraints  cst meb
-
-and struct_elem_constraints cst = function
-  | SFBconst cb -> cst
-  | SFBmind mib -> cst
-  | SFBmodule mb -> module_constraints cst mb
-  | SFBmodtype mtb -> modtype_constraints cst mtb
-
-and module_constraints cst mb =
-  let cst = match mb.mod_expr with
-    | None -> cst
-    | Some meb -> struct_expr_constraints cst meb in
-  let cst = struct_expr_constraints cst mb.mod_type in
-  mb.mod_constraints +++ cst
-
-and modtype_constraints cst mtb =
-  struct_expr_constraints (mtb.typ_constraints +++ cst) mtb.typ_expr
-
-
-let struct_expr_constraints = struct_expr_constraints Univ.empty_constraint
-let module_constraints = module_constraints Univ.empty_constraint
+  let mtb' = subst_modtype_and_resolver mtb mp in
+  { mtb' with typ_expr_alg = alg }
+
+(** [finalize_module] :
+    from an already-translated (or interactive) implementation
+    and a signature entry, produce a final [module_expr] *)
+
+let finalize_module env mp (sign,alg,reso,cst) restype = match restype with
+  |None ->
+    let impl = match alg with Some e -> Algebraic e | None -> FullStruct in
+    { mod_mp = mp;
+      mod_expr = impl;
+      mod_type = sign;
+      mod_type_alg = None;
+      mod_constraints = cst;
+      mod_delta = reso;
+      mod_retroknowledge = [] }
+  |Some (params_mte,inl) ->
+    let res_mtb = translate_modtype env mp inl params_mte in
+    let auto_mtb = {
+      typ_mp = mp;
+      typ_expr = sign;
+      typ_expr_alg = None;
+      typ_constraints = Univ.empty_constraint;
+      typ_delta = reso } in
+    let cst' = Subtyping.check_subtypes env auto_mtb res_mtb in
+    let impl = match alg with Some e -> Algebraic e | None -> Struct sign in
+    { mod_mp = mp;
+      mod_expr = impl;
+      mod_type = res_mtb.typ_expr;
+      mod_type_alg = res_mtb.typ_expr_alg;
+      mod_constraints = cst +++ cst';
+      mod_delta = res_mtb.typ_delta;
+      mod_retroknowledge = [] }
+
+let translate_module env mp inl = function
+  |MType (params,ty) ->
+    let mtb = translate_modtype env mp inl (params,ty) in
+    module_body_of_type mp mtb
+  |MExpr (params,mse,oty) ->
+    let t = translate_mse_funct env (Some mp) inl mse params in
+    let restype = Option.map (fun ty -> ((params,ty),inl)) oty in
+    finalize_module env mp t restype
+
+let rec translate_mse_incl env mp inl = function
+  |MEident mp1 ->
+    let mb = strengthen_and_subst_mb (lookup_module mp1 env) mp true in
+    let sign = clean_bounded_mod_expr mb.mod_type in
+    sign,None,mb.mod_delta,Univ.empty_constraint
+  |MEapply (fe,arg) ->
+    let ftrans = translate_mse_incl env mp inl fe in
+    translate_apply env inl ftrans arg (fun _ _ -> None)
+  |_ -> Modops.error_higher_order_include ()