Imported Upstream version 8.5~beta1+dfsg

1 files changed, 290 insertions, 409 deletions

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index 55fdf1ab..97c1d1fd 100644
--- a/kernel/mod_typing.ml
+++ b/kernel/mod_typing.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -14,432 +14,313 @@
 
 open Util
 open Names
-open Univ
 open Declarations
 open Entries
 open Environ
-open Term_typing
 open Modops
-open Subtyping
 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
   | SFBconst _ | SFBmind _ -> false
 
-let rec list_split_assoc ((k,m) as km) rev_before = function
-  | [] -> raise Not_found
-  | (k',b)::after when k=k' && is_modular b = m -> rev_before,b,after
-  | h::tail -> list_split_assoc km (h::rev_before) tail
+(** Split a [structure_body] at some label corresponding to
+    a modular definition or not. *)
 
-let discr_resolver env mtb =
-     match mtb.typ_expr with
-	SEBstruct _ -> 
-	  mtb.typ_delta
-      | _ -> (*case mp is a functor *)
-	  empty_delta_resolver
-	
-let rec rebuild_mp mp l =
-  match l with
-      []-> mp
-    | i::r -> rebuild_mp (MPdot(mp,i)) r 
-	
-let rec 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
-    if alg_sign = None then
-      sign,None,equiv,cst
-    else
-      sign,Some (SEBwith(Option.get(alg_sign),wd)),equiv,cst
-	    
-and 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 id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
-  in
-  let l = label_of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,(idl<>[])) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before equiv env in
-      if idl = [] then
-	      (* Toplevel definition *)
-	      let cb = match spec with
-		| SFBconst cb -> cb
-		| _ -> error_not_a_constant l
-	      in
-	      (* 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
-		| 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 =
-		      union_constraints
-			(union_constraints cb.const_constraints cst1)
-			cst2
-		    in
-		    let def = Def (Declarations.from_val j.uj_val) in
-		    def,cst
-		| Def cs ->
-		    let cst1 = Reduction.conv env' c (Declarations.force cs) in
-		    let cst = union_constraints cb.const_constraints cst1 in
-		    let def = Def (Declarations.from_val c) in
-		    def,cst
-	      in
-	      let cb' =
-		{ cb with
-		  const_body = def;
-		  const_body_code =
-		    Cemitcodes.from_val (compile_constant_body env' def);
-		  const_constraints = cst }
-	      in
-	      SEBstruct(before@(l,SFBconst(cb'))::after),cb',cst
-      else
-	      (* Definition inside a sub-module *)
-	      let old = match spec with
-		| SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
-	      in
-		begin
-		  match old.mod_expr with
-                    | None ->
-			let sign,cb,cst = 
-			  check_with_def env' old.mod_type (idl,c)
-			    (MPdot(mp,l)) old.mod_delta in
-			let new_spec = SFBmodule({old with
-						    mod_type = sign;
-						    mod_type_alg = None}) in
-			  SEBstruct(before@(l,new_spec)::after),cb,cst
-                    | Some msb ->
-			error_generative_module_expected l
-		end
-    with
-      | Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_incorrect_with_constraint l
+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) ->
+      List.rev rev_before,b,after
+    | h::tail -> split (h::rev_before) tail
+  in split [] struc
 
-and 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 id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
-  in
-  let l = label_of_id id in
-    try
-      let rev_before,spec,after = list_split_assoc (l,true) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before equiv env in
-      if idl = [] then
-	      (* Toplevel module definition *)
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
-	      in
-	      let mb_mp1 = (lookup_module mp1 env) in
-	      let mtb_mp1 = 
-		module_type_of_module None mb_mp1  in
-	      let cst =
-		match old.mod_expr with
-		    None ->
-		      begin
-			try union_constraints
-			  (check_subtypes env' mtb_mp1 
-			     (module_type_of_module None old))
-			  old.mod_constraints
-			with Failure _ -> error_incorrect_with_constraint (label_of_id id)
-		      end
-		  | Some (SEBident(mp')) ->
-		      check_modpath_equiv env' mp1 mp';
-		      old.mod_constraints
-		  | _ ->  error_generative_module_expected l
-	      in
-	      let new_mb = strengthen_and_subst_mb mb_mp1 (MPdot(mp,l)) false
-	      in
-	      let new_spec = SFBmodule {new_mb with 
-					  mod_mp = MPdot(mp,l);
-					  mod_expr = Some (SEBident mp1);
-					  mod_constraints = cst} 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 (MPdot(mp,l)) (MPdot(mp,l)) new_mb.mod_delta in
-		SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
-	      add_delta_resolver equiv new_mb.mod_delta,cst
-      else
-	      (* Module definition of a sub-module *)
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module (string_of_label l)
-	      in
-	      begin
-		match old.mod_expr with
-		    None ->
-		      let sign,equiv',cst =
-			check_with_mod env'
-			  old.mod_type (idl,mp1) (MPdot(mp,l)) old.mod_delta in
-		      let new_equiv = add_delta_resolver equiv equiv' in
-		      let new_spec = SFBmodule {old with 
-						  mod_type = sign;
-						  mod_type_alg = None;
-						  mod_delta = equiv'}
-		      in
-		      let id_subst = map_mp (MPdot(mp,l)) (MPdot(mp,l)) equiv' in
-			SEBstruct(before@(l,new_spec)::subst_signature id_subst after),
-		      new_equiv,cst
-		  | Some (SEBident(mp')) ->
-		      let mpnew = rebuild_mp mp' (List.map label_of_id idl) in
-			check_modpath_equiv env' mpnew mp;
-			  SEBstruct(before@(l,spec)::after)
-			    ,equiv,empty_constraint
-		  | _ ->
-		      error_generative_module_expected l
-              end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_incorrect_with_constraint l
+let discr_resolver mtb = match mtb.mod_type with
+  | NoFunctor _ -> mtb.mod_delta
+  | MoreFunctor _ -> empty_delta_resolver
 
-and translate_module env mp inl me =
-  match me.mod_entry_expr, me.mod_entry_type with
-    | None, None ->
-	anomaly "Mod_typing.translate_module: 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,empty_constraint
-	    | Some mte ->
-		let mtb = translate_module_type env mp inl mte in
-                let cst = check_subtypes env
-		  {typ_mp = mp;
-		   typ_expr = sign;
-		   typ_expr_alg = None;
-		   typ_constraints = 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 = Univ.union_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.*)
+let rec rebuild_mp mp l =
+  match l with
+  | []-> mp
+  | i::r -> rebuild_mp (MPdot(mp,Label.of_id i)) r
 
-and translate_apply env inl ftrans mexpr mkalg =
-  let sign,alg,resolver,cst1 = ftrans in
-  let farg_id, farg_b, fbody_b = destr_functor env 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 cst2 = check_subtypes env mtb farg_b in
-  let mp_delta = discr_resolver env 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,
-  Univ.union_constraints cst1 cst2
+let (+++) = Univ.Constraint.union
 
-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 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
-  SEBfunctor (arg_id, mtb, sign),
-  mkalg alg arg_id mtb,
-  resolver,
-  Univ.union_constraints 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,Univ.union_constraints 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
+  try
+    let modular = not (List.is_empty idl) 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
+	| SFBconst cb -> cb
+	| _ -> error_not_a_constant lab
       in
-      sign,alg,resolve,Univ.union_constraints 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)
-  | _ -> error ("You cannot Include a high-order structure.")
-
-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 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 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 the spirit of subtyping.check_constant, we accept
+         any implementations of parameters and opaques terms,
+	 as long as they have the right type *)
+      let ccst = Declareops.constraints_of_constant (opaque_tables env) cb in
+      let env' = Environ.add_constraints ccst env' in
+      let c',cst = match cb.const_body with
+	| Undef _ | OpaqueDef _ ->
+	  let j = Typeops.infer env' c in
+	  let typ = Typeops.type_of_constant_type env' cb.const_type in
+	  let cst = Reduction.infer_conv_leq env' (Environ.universes env')
+	    j.uj_type typ in
+	  j.uj_val,cst
+	| Def cs ->
+	  let cst = Reduction.infer_conv env' (Environ.universes env') c
+	    (Mod_subst.force_constr cs) in
+	  let cst = (*FIXME MS: what to check here? subtyping of polymorphic constants... *)
+	    if cb.const_polymorphic then cst
+	    else ccst +++ cst 
+	  in
+            c, cst
+      in
+      let def = Def (Mod_subst.from_val c') in
+      let cb' =
+	{ cb with
+	  const_body = def;
+	  const_body_code = Cemitcodes.from_val (compile_constant_body env' def) }
+	  (* const_universes = Future.from_val cst } *)
+      in
+      before@(lab,SFBconst(cb'))::after, c', cst
+    else
+      (* Definition inside a sub-module *)
+      let mb = match spec with
+	| SFBmodule mb -> mb
+	| _ -> error_not_a_module (Label.to_string lab)
+      in
+      begin match mb.mod_expr with
+      | 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 = NoFunctor struc';
+	  mod_type_alg = None }
+        in
+	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 struc (idl,mp1) mp equiv =
+  let lab,idl = match idl with
+    | [] -> assert false
+    | id::idl -> Label.of_id id, idl
   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 (Univ.union_constraints cst1 cst) meb1)
-	meb2
-  | SEBwith(meb,With_definition_body(_,cb))->
-      struct_expr_constraints
-        (Univ.union_constraints 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
-  Univ.union_constraints mb.mod_constraints cst
-
-and modtype_constraints cst mtb =
-  struct_expr_constraints  (Univ.union_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
+  try
+    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)
+    in
+    if List.is_empty idl then
+      (* Toplevel module definition *)
+      let mb_mp1 = lookup_module mp1 env in
+      let mtb_mp1 = module_type_of_module mb_mp1 in
+      let cst = match old.mod_expr with
+	| Abstract ->
+	  begin
+            try
+              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
+	| Algebraic (NoFunctor (MEident(mp'))) ->
+	  check_modpath_equiv env' mp1 mp';
+	  old.mod_constraints
+	| _ -> 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 = 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
+      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
+      let old = match spec with
+        | SFBmodule msb -> msb
+	| _ -> error_not_a_module (Label.to_string lab)
+      in
+      begin match old.mod_expr with
+      | 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 id_subst = map_mp mp' mp' equiv' in
+        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;
+	before@(lab,spec)::after, equiv, Univ.Constraint.empty
+      | _ -> error_generative_module_expected lab
+      end
+  with
+  | Not_found -> error_no_such_label lab
+  | Reduction.NotConvertible -> error_incorrect_with_constraint lab
+
+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.mod_type, mtb.mod_delta
+    in
+    sign,Some (MEident mp1),reso,Univ.Constraint.empty
+  |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 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
+  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 mk_mod mp e ty ty' cst reso =
+  { mod_mp = mp;
+    mod_expr = e;
+    mod_type = ty;
+    mod_type_alg = ty';
+    mod_constraints = cst;
+    mod_delta = reso;
+    mod_retroknowledge = [] }
+
+let mk_modtype mp ty cst reso = mk_mod mp Abstract ty None cst reso
+
+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.mod_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 = mk_modtype (mp_from_mexpr mte) sign cst reso in
+  let mtb' = subst_modtype_and_resolver mtb mp in
+  { mtb' with mod_type_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
+    mk_mod mp impl sign None cst reso
+  |Some (params_mte,inl) ->
+    let res_mtb = translate_modtype env mp inl params_mte in
+    let auto_mtb = mk_modtype mp sign Univ.Constraint.empty 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
+    { res_mtb with
+      mod_mp = mp;
+      mod_expr = impl;
+      mod_constraints = cst +++ cst' }
+
+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.Constraint.empty
+  |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 ()