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

8 files changed, 305 insertions, 557 deletions

diff --git a/checker/cic.mli b/checker/cic.mli
index fd3351674..0b732e4b9 100644
--- a/checker/cic.mli
+++ b/checker/cic.mli
@@ -276,8 +276,30 @@ type mutual_inductive_body = {
     mind_native_name : native_name ref; (** status of the code (linked or not, and where) *)
   }
 
-(** {6 Modules: signature component specifications, module types, and
-  module declarations } *)
+(** {6 Module declarations } *)
+
+(** Functor expressions are forced to be on top of other expressions *)
+
+type ('ty,'a) functorize =
+  | NoFunctor of 'a
+  | MoreFunctor of MBId.t * 'ty * ('ty,'a) functorize
+
+(** The fully-algebraic module expressions : names, applications, 'with ...'.
+    They correspond to the user entries of non-interactive modules.
+    They will be later expanded into module structures in [Mod_typing],
+    and won't play any role into the kernel after that : they are kept
+    only for short module printing and for extraction. *)
+
+type with_declaration =
+  | WithMod of Id.t list * module_path
+  | WithDef of Id.t list * constr
+
+type module_alg_expr =
+  | MEident of module_path
+  | MEapply of module_alg_expr * module_path
+  | MEwith of module_alg_expr * with_declaration
+
+(** A component of a module structure *)
 
 type structure_field_body =
   | SFBconst of constant_body
@@ -285,45 +307,51 @@ type structure_field_body =
   | SFBmodule of module_body
   | SFBmodtype of module_type_body
 
-and structure_body = (label * structure_field_body) list
+(** A module structure is a list of labeled components.
+
+    Note : we may encounter now (at most) twice the same label in
+    a [structure_body], once for a module ([SFBmodule] or [SFBmodtype])
+    and once for an object ([SFBconst] or [SFBmind]) *)
+
+and structure_body = (Label.t * structure_field_body) list
+
+(** A module signature is a structure, with possibly functors on top of it *)
+
+and module_signature = (module_type_body,structure_body) functorize
+
+(** A module expression is an algebraic expression, possibly functorized. *)
+
+and module_expression = (module_type_body,module_alg_expr) functorize
 
-and struct_expr_body =
-  | SEBident of module_path
-  | SEBfunctor of MBId.t * module_type_body * struct_expr_body
-  | SEBapply of struct_expr_body * struct_expr_body * Univ.constraints
-  | SEBstruct of structure_body
-  | SEBwith of struct_expr_body * with_declaration_body
+and module_implementation =
+  | Abstract (** no accessible implementation *)
+  | Algebraic of module_expression (** non-interactive algebraic expression *)
+  | Struct of module_signature (** interactive body *)
+  | FullStruct (** special case of [Struct] : the body is exactly [mod_type] *)
 
-and with_declaration_body =
-    With_module_body of Id.t list * module_path
-  | With_definition_body of  Id.t list * constant_body
 and module_body =
-    {  (** absolute path of the module *)
-      mod_mp : module_path;
-      (** Implementation *)
-      mod_expr : struct_expr_body option;
-      (** Signature *)
-      mod_type : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      mod_type_alg : struct_expr_body option;
-      (** set of all constraint in the module  *)
-      mod_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      mod_delta : delta_resolver;
-      mod_retroknowledge : action list}
+  { mod_mp : module_path; (** absolute path of the module *)
+    mod_expr : module_implementation; (** implementation *)
+    mod_type : module_signature; (** expanded type *)
+    (** algebraic type, kept if it's relevant for extraction *)
+    mod_type_alg : module_expression option;
+    (** set of all constraints in the module  *)
+    mod_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    mod_delta : delta_resolver;
+    mod_retroknowledge : action list }
+
+(** A [module_type_body] is similar to a [module_body], with
+    no implementation and retroknowledge fields *)
 
 and module_type_body =
-    {
-      (** Path of the module type *)
-      typ_mp : module_path;
-      typ_expr : struct_expr_body;
-      (** algebraic structure expression is kept
-	 if it's relevant for extraction  *)
-      typ_expr_alg : struct_expr_body option ;
-      typ_constraints : Univ.constraints;
-      (** quotiented set of equivalent constant and inductive name  *)
-      typ_delta : delta_resolver}
+  { typ_mp : module_path; (** path of the module type *)
+    typ_expr : module_signature; (** expanded type *)
+    (** algebraic expression, kept if it's relevant for extraction  *)
+    typ_expr_alg : module_expression option;
+    typ_constraints : Univ.constraints;
+    (** quotiented set of equivalent constants and inductive names *)
+    typ_delta : delta_resolver}
 
 
 (*************************************************************************)
diff --git a/checker/declarations.ml b/checker/declarations.ml
index 0981cfd1a..eec76ba39 100644
--- a/checker/declarations.ml
+++ b/checker/declarations.ml
@@ -529,71 +529,50 @@ let subst_mind sub mib =
 
 (* Modules *)
 
-let rec subst_with_body sub = function
-  | With_module_body(id,mp) ->
-      With_module_body(id,subst_mp sub mp)
-  | With_definition_body(id,cb) ->
-      With_definition_body( id,subst_const_body sub cb)
+let rec functor_map fty f0 = function
+  | NoFunctor a -> NoFunctor (f0 a)
+  | MoreFunctor (mbid,ty,e) -> MoreFunctor(mbid,fty ty,functor_map fty f0 e)
+
+let implem_map fs fa = function
+  | Struct s -> Struct (fs s)
+  | Algebraic a -> Algebraic (fa a)
+  | impl -> impl
+
+let subst_with_body sub = function
+  | WithMod(id,mp) -> WithMod(id,subst_mp sub mp)
+  | WithDef(id,c) -> WithDef(id,subst_mps sub c)
+
+let rec subst_expr sub = function
+  | MEident mp -> MEident (subst_mp sub mp)
+  | MEapply (me1,mp2)-> MEapply (subst_expr sub me1, subst_mp sub mp2)
+  | MEwith (me,wd)-> MEwith (subst_expr sub me, subst_with_body sub wd)
+
+let rec subst_expression sub me =
+  functor_map (subst_modtype sub) (subst_expr sub) me
+
+and subst_signature sub sign =
+  functor_map (subst_modtype sub) (subst_structure sub) sign
 
 and subst_modtype sub mtb=
-  let typ_expr' = subst_struct_expr sub mtb.typ_expr in
-  let typ_alg' = 
-    Option.smartmap 
-      (subst_struct_expr sub) mtb.typ_expr_alg in
-  let mp = subst_mp sub mtb.typ_mp
-  in
-    if typ_expr'==mtb.typ_expr && 
-      typ_alg'==mtb.typ_expr_alg && mp==mtb.typ_mp then
-	mtb
-    else
-      {mtb with 
-	 typ_mp = mp;
-	 typ_expr = typ_expr';
-	 typ_expr_alg = typ_alg'}
+  { mtb with
+    typ_mp = subst_mp sub mtb.typ_mp;
+    typ_expr = subst_signature sub mtb.typ_expr;
+    typ_expr_alg = Option.smartmap (subst_expression sub) mtb.typ_expr_alg }
 
-and 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_modtype sub mtb)
+    | 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_modtype sub mtb)
   in
-    List.map (fun (l,b) -> (l,subst_body b)) sign
-
+  List.map (fun (l,b) -> (l,subst_body b)) struc
 
 and subst_module sub mb =
-  let mtb' = subst_struct_expr sub mb.mod_type in
-  let typ_alg' = Option.smartmap 
-    (subst_struct_expr sub ) mb.mod_type_alg in
-  let me' = Option.smartmap 
-    (subst_struct_expr sub) mb.mod_expr in
-  let mp = subst_mp sub mb.mod_mp in
-     if mtb'==mb.mod_type && mb.mod_expr == me' 
-       && mp == mb.mod_mp
-    then mb else
-      { mb with
-	  mod_mp = mp;
-	  mod_expr = me';
-	  mod_type_alg = typ_alg';
-	  mod_type=mtb'}
-
-and subst_struct_expr sub = function
-    | SEBident mp -> SEBident (subst_mp sub mp)
-    | SEBfunctor (mbid, mtb, meb') -> 
-	SEBfunctor(mbid,subst_modtype sub mtb
-		     ,subst_struct_expr sub meb')
-    | SEBstruct (str)->
-	SEBstruct( subst_structure sub  str)
-    | SEBapply (meb1,meb2,cst)->
-	SEBapply(subst_struct_expr sub meb1,
-		 subst_struct_expr sub meb2,
-		 cst)
-    | SEBwith (meb,wdb)-> 
-	SEBwith(subst_struct_expr sub meb,
-		subst_with_body sub wdb)
-
+  { mb with
+    mod_mp = subst_mp sub mb.mod_mp;
+    mod_expr =
+      implem_map (subst_signature sub) (subst_expression sub) mb.mod_expr;
+    mod_type = subst_signature sub mb.mod_type;
+    mod_type_alg = Option.map (subst_expression sub) mb.mod_type_alg }
 
diff --git a/checker/declarations.mli b/checker/declarations.mli
index 64234e8cd..ab74114d5 100644
--- a/checker/declarations.mli
+++ b/checker/declarations.mli
@@ -37,9 +37,7 @@ val mind_of_delta : delta_resolver -> mutual_inductive -> mutual_inductive
 
 val subst_const_body : constant_body subst_fun
 val subst_mind : mutual_inductive_body subst_fun
-val subst_modtype : substitution -> module_type_body -> module_type_body
-val subst_struct_expr :  substitution -> struct_expr_body -> struct_expr_body
-val subst_structure : substitution -> structure_body -> structure_body
+val subst_signature :  substitution -> module_signature -> module_signature
 val subst_module : substitution -> module_body -> module_body
 
 val join : substitution -> substitution -> substitution
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml
index 66f1194d3..b0f20da70 100644
--- a/checker/mod_checking.ml
+++ b/checker/mod_checking.ml
@@ -13,8 +13,7 @@ open Subtyping
 open Declarations
 open Environ
 
-(************************************************************************)
-(* Checking constants *)
+(** {6 Checking constants } *)
 
 let refresh_arity ar =
   let ctxt, hd = decompose_prod_assum ar in
@@ -43,339 +42,95 @@ let check_constant_declaration env kn cb =
         check_polymorphic_arity env ctxt par);
   add_constant kn cb env
 
-(************************************************************************)
-(* Checking modules *)
 
+(** {6 Checking modules } *)
 
-exception Not_path
-
-let path_of_mexpr = function
-  | SEBident mp -> mp
-  | _ -> raise Not_path
-
-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
-
-let check_definition_sub env cb1 cb2 =
-  let check_type env t1 t2 =
-
-    (* If the type of a constant is generated, it may mention
-       non-variable algebraic universes that the general conversion
-       algorithm is not ready to handle. Anyway, generated types of
-       constants are functions of the body of the constant. If the
-       bodies are the same in environments that are subtypes one of
-       the other, the types are subtypes too (i.e. if Gamma <= Gamma',
-       Gamma |- A |> T, Gamma |- A' |> T' and Gamma |- A=A' then T <= T').
-       Hence they don't have to be checked again *)
-
-    let t1,t2 =
-      if isArity t2 then
-        let (ctx2,s2) = destArity t2 in
-        match s2 with
-        | Type v when not (Univ.is_univ_variable v) ->
-          (* The type in the interface is inferred and is made of algebraic
-             universes *)
-          begin try
-            let (ctx1,s1) = dest_arity env t1 in
-            match s1 with
-            | Type u when not (Univ.is_univ_variable u) ->
-              (* Both types are inferred, no need to recheck them. We
-                 cheat and collapse the types to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Prop _ ->
-              (* The type in the interface is inferred, it may be the case
-                 that the type in the implementation is smaller because
-                 the body is more reduced. We safely collapse the upper
-                 type to Prop *)
-                mkArity (ctx1,Prop Null), mkArity (ctx2,Prop Null)
-            | Type _ ->
-              (* The type in the interface is inferred and the type in the
-                 implementation is not inferred or is inferred but from a
-                 more reduced body so that it is just a variable. Since
-                 constraints of the form "univ <= max(...)" are not
-                 expressible in the system of algebraic universes: we fail
-                 (the user has to use an explicit type in the interface *)
-                raise Reduction.NotConvertible
-          with UserError _ (* "not an arity" *) ->
-            raise Reduction.NotConvertible end
-        | _ -> t1,t2
-      else
-        (t1,t2) in
-    Reduction.conv_leq env t1 t2
-  in
-  (*Start by checking types*)
-  let typ1 = Typeops.type_of_constant_type env cb1.const_type in
-  let typ2 = Typeops.type_of_constant_type env cb2.const_type in
-  check_type env typ1 typ2;
-  (* In the spirit of subtyping.check_constant, we accept
-     any implementations of parameters and opaques terms,
-     as long as they have the right type *)
-  (match cb2.const_body with
-    | Undef _ | OpaqueDef _ -> ()
-    | Def lc2 ->
-	(match cb1.const_body with
-	  | Def lc1 ->
-	    let c1 = force_constr lc1 in
-            let c2 = force_constr lc2 in
-	    Reduction.conv env c1 c2
-	  (* Coq only places transparent cb in With_definition_body *)
-	  | _ -> assert false))
-
-let lookup_modtype mp env =
-  try Environ.lookup_modtype mp env
-  with Not_found ->
-    failwith ("Unknown module type: "^string_of_mp mp)
+(** We currently ignore the [mod_type_alg] and [typ_expr_alg] fields.
+    The only delicate part is when [mod_expr] is an algebraic expression :
+    we need to expand it before checking it is indeed a subtype of [mod_type].
+    Fortunately, [mod_expr] cannot contain any [MEwith]. *)
 
 let lookup_module mp env =
   try Environ.lookup_module mp env
   with Not_found ->
     failwith ("Unknown module: "^string_of_mp mp)
 
-let rec check_with env mtb with_decl mp=
-  match with_decl with
-    | With_definition_body (idl,c) ->
-	check_with_def env mtb (idl,c) mp;
-	mtb
-    | With_module_body (idl,mp1) ->
-	check_with_mod env mtb (idl,mp1) mp;
-	mtb
-
-and check_with_def env mtb (idl,c) mp =
-  let sig_b = match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb
+let rec check_module env mp mb =
+  let (_:module_signature) =
+    check_signature env mb.mod_type mb.mod_mp mb.mod_delta
   in
-  let id,idl = match idl with
-    | [] -> assert false
-    | id::idl -> id,idl
+  let optsign = match mb.mod_expr with
+    |Struct sign -> Some (check_signature env sign mb.mod_mp mb.mod_delta)
+    |Algebraic me -> Some (check_mexpression env me mb.mod_mp mb.mod_delta)
+    |Abstract|FullStruct -> None
   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 empty_delta_resolver env in
-      if idl = [] then
-	      let cb = match spec with
-		  SFBconst cb -> cb
-		| _ -> error_not_a_constant l
-	      in
-              check_definition_sub env' c cb
-      else
-	      let old = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-		begin
-		  match old.mod_expr with
-                    | None ->
-		        check_with_def env' old.mod_type (idl,c) (MPdot(mp,l))
-                    | Some msb ->
-			error_a_generative_module_expected l
-		end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
-
-and check_with_mod env mtb (idl,mp1) mp =
-  let sig_b =
-    match mtb with
-    | SEBstruct(sig_b) ->
-	sig_b
-    | _ -> error_signature_expected mtb 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,false) [] sig_b in
-      let before = List.rev rev_before in
-      let env' = Modops.add_signature mp before empty_delta_resolver env in
-      if idl = [] then
-	      let _ = match spec with
-		  SFBmodule msb -> msb
-		| _ -> error_not_a_module l
-	      in
-	      let (_:module_body) = (Environ.lookup_module mp1 env) in ()
-      else
-	    let old = match spec with
-		SFBmodule msb -> msb
-	      | _ -> error_not_a_module l
-	    in
-	      begin
-		match old.mod_expr with
-                    None ->
-		      check_with_mod env'
-			  old.mod_type (idl,mp1) (MPdot(mp,l))
-                  | Some msb ->
-                      error_a_generative_module_expected l
-              end
-    with
-	Not_found -> error_no_such_label l
-      | Reduction.NotConvertible -> error_with_incorrect l
+  match optsign with
+  |None -> ()
+  |Some sign ->
+    let mtb1 =
+      {typ_mp=mp;
+       typ_expr=sign;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    and mtb2 =
+      {typ_mp=mp;
+       typ_expr=mb.mod_type;
+       typ_expr_alg=None;
+       typ_constraints=Univ.empty_constraint;
+       typ_delta = mb.mod_delta;}
+    in
+    let env = add_module_type mp mtb1 env in
+    Subtyping.check_subtypes env mtb1 mtb2
 
 and check_module_type env mty =
-  let (_:struct_expr_body) =
-    check_modtype env mty.typ_expr mty.typ_mp mty.typ_delta in
+  let (_:module_signature) =
+    check_signature env mty.typ_expr mty.typ_mp mty.typ_delta in
   ()
 
-							 
-and check_module env mp mb =
-  match mb.mod_expr, mb.mod_type with
-    | None,mtb -> 
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, mtb when mtb==mexpr ->
-	let (_:struct_expr_body) =
-	  check_modtype env mtb mb.mod_mp mb.mod_delta in ()
-    | Some mexpr, _ ->
-	let sign = check_modexpr env mexpr mb.mod_mp mb.mod_delta in
-	let (_:struct_expr_body) =
-	  check_modtype env mb.mod_type mb.mod_mp mb.mod_delta in
-	let mtb1 =
-	  {typ_mp=mp;
-	   typ_expr=sign;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	and mtb2 =
-	  {typ_mp=mp;
-	   typ_expr=mb.mod_type;
-	   typ_expr_alg=None;
-	   typ_constraints=Univ.empty_constraint;
-	   typ_delta = mb.mod_delta;}
-	in
-	let env = add_module (module_body_of_type mp mtb1) env in
-	check_subtypes env mtb1 mtb2
-
 and check_structure_field env mp lab res = function
   | SFBconst cb ->
       let c = Constant.make2 mp lab in
-	check_constant_declaration env c cb
+      check_constant_declaration env c cb
   | SFBmind mib ->
       let kn = MutInd.make2 mp lab in
       let kn = mind_of_delta res kn in
-	Indtypes.check_inductive env kn mib
+      Indtypes.check_inductive env kn mib
   | SFBmodule msb ->
-      let (_:unit) = check_module env (MPdot(mp,lab)) msb in
-	Modops.add_module msb env
+      let () = check_module env (MPdot(mp,lab)) msb in
+      Modops.add_module msb env
   | SFBmodtype mty ->
       check_module_type env mty;
       add_modtype (MPdot(mp,lab)) mty env
-	
-and check_modexpr env mse mp_mse res = match mse with
-  | SEBident mp ->
+
+and check_mexpr env mse mp_mse res = match mse with
+  | MEident mp ->
       let mb = lookup_module mp env in
       (subst_and_strengthen mb mp_mse).mod_type
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb ;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let sign = check_modexpr env' body mp_mse res in
-	SEBfunctor (arg_id, mtb, sign)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modexpr env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
-      let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	(subst_struct_expr (map_mbid farg_id mp) fbody_b)
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modexpr env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in 
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-	SEBstruct(msb)
-	
-and check_modtype env mse mp_mse res = match mse with
-  | SEBident mp ->
-      let mtb = lookup_modtype mp env in
-	mtb.typ_expr
-  | SEBfunctor (arg_id, mtb, body) ->
-      check_module_type env mtb;
-      let env' = add_module (module_body_of_type (MPbound arg_id) mtb) env in
-      let body = check_modtype env' body mp_mse res in
-	SEBfunctor(arg_id,mtb,body)
-  | SEBapply (f,m,cst) ->
-      let sign = check_modtype env f mp_mse res in
-      let farg_id, farg_b, fbody_b = destr_functor env sign in
-      let mp =
-	try (path_of_mexpr m)
-	with Not_path -> error_application_to_not_path m
-	  (* place for nondep_supertype *) in
+  | MEapply (f,mp) ->
+      let sign = check_mexpr env f mp_mse res in
+      let farg_id, farg_b, fbody_b = destr_functor sign in
       let mtb = module_type_of_module (Some mp) (lookup_module mp env) in
-	check_subtypes env mtb farg_b;
-	subst_struct_expr (map_mbid farg_id mp) fbody_b
-  | SEBwith(mte, with_decl) ->
-      let sign = check_modtype env mte mp_mse res in
-      let sign = check_with env sign with_decl mp_mse in
-	sign
-  | SEBstruct(msb) ->
-      let (_:env) = List.fold_left (fun env (lab,mb) ->
-		   check_structure_field env mp_mse lab res mb) env msb in
-      SEBstruct(msb)
-	
-(*
-  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 (l,item) -> add_struct_elem_constraints env item)
-        env
-        structure_body
-
-  | SEBapply (meb1,meb2,cst) ->
-(*  let g = Univ.merge_constraints cst Univ.initial_universes in
-msgnl(str"ADDING FUNCTOR APPLICATION CONSTRAINTS:"++fnl()++
-      Univ.pr_universes g++str"============="++fnl());
-*)
-      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(_,_,cst))->
-      Environ.add_constraints cst
-	(add_struct_expr_constraints env meb)
+      check_subtypes env mtb farg_b;
+      subst_signature (map_mbid farg_id mp) fbody_b
+  | MEwith _ -> error_with_module ()
 
-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
-  | SFBalias (mp,Some cst) -> Environ.add_constraints cst env
-  | SFBalias (mp,None) -> env
-  | 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 = match mb.mod_type with
-    | None -> env
-    | Some mtb ->
-	add_struct_expr_constraints env mtb
-  in
-    Environ.add_constraints mb.mod_constraints env
+and check_mexpression env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_mexpression env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor me -> check_mexpr env me mp_mse res
 
-and add_modtype_constraints env mtb =
-  add_struct_expr_constraints env mtb.typ_expr
-*)
+and check_signature env sign mp_mse res = match sign with
+  | MoreFunctor (arg_id, mtb, body) ->
+      check_module_type env mtb;
+      let env' = add_module_type (MPbound arg_id) mtb env in
+      let body = check_signature env' body mp_mse res in
+      MoreFunctor(arg_id,mtb,body)
+  | NoFunctor struc ->
+      let (_:env) = List.fold_left (fun env (lab,mb) ->
+	check_structure_field env mp_mse lab res mb) env struc
+      in
+      NoFunctor struc
diff --git a/checker/modops.ml b/checker/modops.ml
index 20f330812..89ffcb50b 100644
--- a/checker/modops.ml
+++ b/checker/modops.ml
@@ -19,7 +19,7 @@ open Declarations
 let error_not_a_constant l =
   error ("\""^(Label.to_string l)^"\" is not a constant")
 
-let error_not_a_functor _ = error "Application of not a functor"
+let error_not_a_functor () = error "Application of not a functor"
 
 let error_incompatible_modtypes _ _ = error "Incompatible module types"
 
@@ -38,61 +38,52 @@ let error_not_a_module_loc loc s =
 
 let error_not_a_module s = error_not_a_module_loc Loc.ghost s
 
-let error_with_incorrect l =
-  error ("Incorrect constraint for label \""^(Label.to_string l)^"\"")
+let error_with_module () =
+  error "Unsupported 'with' constraint in module implementation"
 
-let error_a_generative_module_expected l =
-  error ("The module " ^ Label.to_string l ^ " is not generative. Only " ^
-         "component of generative modules can be changed using the \"with\" " ^
-         "construct.")
+let is_functor = function
+  | MoreFunctor _ -> true
+  | NoFunctor _ -> false
 
-let error_signature_expected mtb =
-  error "Signature expected"
+let destr_functor = function
+  | MoreFunctor (arg_id,arg_t,body_t) -> (arg_id,arg_t,body_t)
+  | NoFunctor _ -> error_not_a_functor ()
 
-let error_application_to_not_path _ = error "Application to not path"
-
-let destr_functor env mtb =
-  match mtb with
-  | SEBfunctor (arg_id,arg_t,body_t) ->
-      	    (arg_id,arg_t,body_t)
-  | _ -> error_not_a_functor mtb
-
-let module_body_of_type mp mtb = 
+let module_body_of_type mp mtb =
   { mod_mp = mp;
     mod_type = mtb.typ_expr;
     mod_type_alg = mtb.typ_expr_alg;
-    mod_expr = None;
+    mod_expr = Abstract;
     mod_constraints = mtb.typ_constraints;
     mod_delta = mtb.typ_delta;
     mod_retroknowledge = []}
 
-let rec add_signature mp sign resolver env = 
+let rec add_structure mp sign resolver env =
   let add_one env (l,elem) =
     let kn = KerName.make2 mp l in
     let con = Constant.make1 kn in
     let mind = mind_of_delta resolver (MutInd.make1 kn) in
       match elem with
-	| SFBconst cb -> 
+	| SFBconst cb ->
 	   (* let con =  constant_of_delta resolver con in*)
 	      Environ.add_constant con cb env
-	| SFBmind mib -> 
+	| SFBmind mib ->
 	   (* let mind =  mind_of_delta resolver mind in*)
 	    Environ.add_mind mind mib env
 	| SFBmodule mb -> add_module mb env
 	      (* adds components as well *)
 	| SFBmodtype mtb -> Environ.add_modtype mtb.typ_mp mtb env
   in
-    List.fold_left add_one env sign
+  List.fold_left add_one env sign
 
-and add_module mb env = 
+and add_module mb env =
   let mp = mb.mod_mp in
   let env = Environ.shallow_add_module mp mb env in
-    match mb.mod_type with
-      | SEBstruct (sign) -> 
-	    add_signature mp sign mb.mod_delta env
-      | SEBfunctor _ -> env
-      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+  match mb.mod_type with
+  | NoFunctor struc -> add_structure mp struc mb.mod_delta env
+  | MoreFunctor _ -> env
 
+let add_module_type mp mtb env = add_module (module_body_of_type mp mtb) env
 
 let strengthen_const mp_from l cb resolver =
   match cb.const_body with
@@ -107,20 +98,20 @@ let rec strengthen_mod mp_from mp_to mb =
     mb
   else
     match mb.mod_type with
-     | SEBstruct (sign) -> 
-	 let resolve_out,sign_out = 
-	   strengthen_sig mp_from sign mp_to mb.mod_delta in
-	   { mb with
-	       mod_expr = Some (SEBident mp_to);
-	       mod_type = SEBstruct(sign_out);
-	       mod_type_alg = mb.mod_type_alg;
-	       mod_constraints = mb.mod_constraints;
-	       mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to 
-	       (add_delta_resolver mb.mod_delta resolve_out)*);
-	       mod_retroknowledge = mb.mod_retroknowledge}
-     | SEBfunctor _ -> mb
-     | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
-	 
+     | NoFunctor (sign) ->
+	 let resolve_out,sign_out =
+	   strengthen_sig mp_from sign mp_to mb.mod_delta
+         in
+	 { mb with
+	   mod_expr = Algebraic (NoFunctor (MEident mp_to));
+	   mod_type = NoFunctor sign_out;
+	   mod_type_alg = mb.mod_type_alg;
+	   mod_constraints = mb.mod_constraints;
+	   mod_delta = resolve_out(*add_mp_delta_resolver mp_from mp_to
+	   (add_delta_resolver mb.mod_delta resolve_out)*);
+	   mod_retroknowledge = mb.mod_retroknowledge}
+     | MoreFunctor _ -> mb
+
 and strengthen_sig mp_from sign mp_to resolver =
   match sign with
     | [] -> empty_delta_resolver,[]
@@ -139,21 +130,20 @@ and strengthen_sig mp_from sign mp_to resolver =
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out (*add_delta_resolver resolve_out mb.mod_delta*),
 	item':: rest'
-    | (l,SFBmodtype mty as item) :: rest -> 
+    | (l,SFBmodtype mty as item) :: rest ->
 	let resolve_out,rest' = strengthen_sig mp_from rest mp_to resolver in
 	resolve_out,item::rest'
 
-let strengthen mtb mp =
-    match mtb.typ_expr with
-      | SEBstruct (sign) -> 
-	  let resolve_out,sign_out =
-	    strengthen_sig mtb.typ_mp sign mp mtb.typ_delta in
-	    {mtb with
-	       typ_expr = SEBstruct(sign_out);
-	       typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
-		(add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
-      | SEBfunctor _ -> mtb
-      | _ -> anomaly ~label:"Modops" (Pp.str "the evaluation of the structure failed ")
+let strengthen mtb mp = match mtb.typ_expr with
+  | NoFunctor sign ->
+    let resolve_out,sign_out =
+      strengthen_sig mtb.typ_mp sign mp mtb.typ_delta
+    in
+    { mtb with
+      typ_expr = NoFunctor sign_out;
+      typ_delta = resolve_out(*add_delta_resolver mtb.typ_delta
+      (add_mp_delta_resolver mtb.typ_mp mp resolve_out)*)}
+  | MoreFunctor _ -> mtb
 
 let subst_and_strengthen mb mp =
   strengthen_mod mb.mod_mp mp (subst_module (map_mp mb.mod_mp mp) mb)
@@ -161,17 +151,16 @@ let subst_and_strengthen mb mp =
 
 let module_type_of_module mp mb =
   match mp with
-      Some mp ->
-	strengthen {
-	  typ_mp = mp;
-	  typ_expr = mb.mod_type;
-	  typ_expr_alg = None;
-	  typ_constraints = mb.mod_constraints;
-	  typ_delta = mb.mod_delta} mp
-	  
-    | None ->
-	{typ_mp = mb.mod_mp;
-	 typ_expr = mb.mod_type;
-	 typ_expr_alg = None;
-	 typ_constraints = mb.mod_constraints;
-	 typ_delta = mb.mod_delta}
+  | Some mp ->
+    strengthen {
+      typ_mp = mp;
+      typ_expr = mb.mod_type;
+      typ_expr_alg = None;
+      typ_constraints = mb.mod_constraints;
+      typ_delta = mb.mod_delta} mp
+  | None ->
+    { typ_mp = mb.mod_mp;
+      typ_expr = mb.mod_type;
+      typ_expr_alg = None;
+      typ_constraints = mb.mod_constraints;
+      typ_delta = mb.mod_delta}
diff --git a/checker/modops.mli b/checker/modops.mli
index 0b94edb54..396eb8e7c 100644
--- a/checker/modops.mli
+++ b/checker/modops.mli
@@ -15,20 +15,18 @@ open Environ
 
 (* Various operations on modules and module types *)
 
-(* make the envirconment entry out of type *)
-val module_body_of_type : module_path -> module_type_body -> module_body
+val module_type_of_module :
+  module_path option -> module_body -> module_type_body
 
-val module_type_of_module : module_path option -> module_body ->
-  module_type_body
+val is_functor : ('ty,'a) functorize -> bool
 
-val destr_functor :
-  env -> struct_expr_body -> MBId.t * module_type_body * struct_expr_body
-
-val add_signature : module_path -> structure_body -> delta_resolver -> env -> env
+val destr_functor : ('ty,'a) functorize -> MBId.t * 'ty * ('ty,'a) functorize
 
 (* adds a module and its components, but not the constraints *)
 val add_module : module_body ->  env -> env
 
+val add_module_type : module_path -> module_type_body -> env -> env
+
 val strengthen : module_type_body -> module_path -> module_type_body
 
 val subst_and_strengthen : module_body -> module_path -> module_body
@@ -38,19 +36,13 @@ val error_incompatible_modtypes :
 
 val error_not_match : label -> structure_field_body -> 'a
 
-val error_with_incorrect : label -> 'a
+val error_with_module : unit -> 'a
 
 val error_no_such_label : label -> 'a
 
 val error_no_such_label_sub :
   label -> module_path -> 'a
 
-val error_signature_expected : struct_expr_body -> 'a
-
 val error_not_a_constant : label -> 'a
 
 val error_not_a_module : label -> 'a
-
-val error_a_generative_module_expected : label -> 'a
-
-val error_application_to_not_path : struct_expr_body -> 'a
diff --git a/checker/subtyping.ml b/checker/subtyping.ml
index 150e99bc9..7903c33c5 100644
--- a/checker/subtyping.ml
+++ b/checker/subtyping.ml
@@ -320,55 +320,52 @@ and check_signatures env mp1 sig1 sig2 subst1 subst2 =
 		| Modtype mtb -> mtb
 		| _ -> error_not_match l spec2
 	    in
-	    let env = add_module (module_body_of_type mtb2.typ_mp mtb2)
-	      (add_module (module_body_of_type mtb1.typ_mp mtb1) env) in
-	      check_modtypes  env mtb1 mtb2 subst1 subst2 true
+	    let env =
+              add_module_type mtb2.typ_mp mtb2
+	        (add_module_type mtb1.typ_mp mtb1 env)
+            in
+	    check_modtypes env mtb1 mtb2 subst1 subst2 true
   in
-    List.iter check_one_body sig2
+  List.iter check_one_body sig2
 
-and check_modtypes  env mtb1 mtb2 subst1 subst2 equiv = 
-  if mtb1==mtb2 then () else 
-  let mtb1',mtb2'=mtb1.typ_expr,mtb2.typ_expr in
-  let rec check_structure  env str1 str2 equiv subst1 subst2 = 
-	match str1,str2 with
-	  | SEBstruct (list1), 
-	    SEBstruct (list2) -> 
-	       check_signatures env
-		mtb1.typ_mp list1 list2 subst1 subst2;
-		if equiv then
-		  check_signatures  env 
-		     mtb2.typ_mp list2 list1 subst1 subst2
-		else
-		  ()
-	  | SEBfunctor (arg_id1,arg_t1,body_t1),
-	      SEBfunctor (arg_id2,arg_t2,body_t2) ->
-	       check_modtypes env 
-		arg_t2 arg_t1
-		(map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
-		equiv ;
-		(* contravariant *)
-	      let env = add_module 
-		(module_body_of_type (MPbound arg_id2) arg_t2) env 
-	      in
-	      let env = match body_t1 with
-		  SEBstruct str ->
-		    let env = shallow_remove_module mtb1.typ_mp env in
-		    add_module {mod_mp = mtb1.typ_mp;
-				mod_expr = None;
-				mod_type = body_t1;
-				mod_type_alg= None;
-				mod_constraints=mtb1.typ_constraints;
-				mod_retroknowledge = [];
-				mod_delta = mtb1.typ_delta} env
-		| _ -> env
-	      in
-		check_structure env body_t1 body_t2 equiv 
-		  (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
-		  subst2
-	  | _ , _ -> error_incompatible_modtypes mtb1 mtb2
-      in
-     if mtb1'== mtb2' then ()
-     else check_structure  env mtb1' mtb2' equiv subst1 subst2
+and check_modtypes env mtb1 mtb2 subst1 subst2 equiv =
+  if mtb1==mtb2 || mtb1.typ_expr == mtb2.typ_expr then ()
+  else
+    let rec check_structure  env str1 str2 equiv subst1 subst2 =
+      match str1,str2 with
+      | NoFunctor (list1),
+        NoFunctor (list2) ->
+	  check_signatures env mtb1.typ_mp list1 list2 subst1 subst2;
+	  if equiv then
+	    check_signatures env mtb2.typ_mp list2 list1 subst1 subst2
+	  else
+	    ()
+      | MoreFunctor (arg_id1,arg_t1,body_t1),
+	MoreFunctor (arg_id2,arg_t2,body_t2) ->
+	  check_modtypes env
+	    arg_t2 arg_t1
+	    (map_mp arg_t1.typ_mp arg_t2.typ_mp) subst2
+	    equiv;
+	  (* contravariant *)
+	  let env = add_module_type (MPbound arg_id2) arg_t2 env in
+	  let env =
+            if is_functor body_t1 then env
+            else
+	      let env = shallow_remove_module mtb1.typ_mp env in
+	      add_module {mod_mp = mtb1.typ_mp;
+			  mod_expr = Abstract;
+			  mod_type = body_t1;
+			  mod_type_alg = None;
+			  mod_constraints = mtb1.typ_constraints;
+			  mod_retroknowledge = [];
+			  mod_delta = mtb1.typ_delta} env
+	  in
+	  check_structure env body_t1 body_t2 equiv
+	    (join (map_mbid arg_id1 (MPbound arg_id2)) subst1)
+	    subst2
+      | _ , _ -> error_incompatible_modtypes mtb1 mtb2
+    in
+    check_structure env mtb1.typ_expr mtb2.typ_expr equiv subst1 subst2
 
 let check_subtypes env sup super =
   check_modtypes env (strengthen sup sup.typ_mp) super empty_subst
diff --git a/checker/values.ml b/checker/values.ml
index 974d3431e..b39d90548 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 43e0b61e2a549058ae0a59bbadbb9d61 checker/cic.mli
+MD5 09a4e5d657809e040f50837a78fe6dfe checker/cic.mli
 
 *)
 
@@ -248,6 +248,18 @@ let v_ind_pack = v_tuple "mutual_inductive_body"
     v_cstrs;
     Any|]
 
+let v_with =
+  Sum ("with_declaration_body",0,
+       [|[|List v_id;v_mp|];
+         [|List v_id;v_constr|]|])
+
+let rec v_mae =
+  Sum ("module_alg_expr",0,
+  [|[|v_mp|];         (* SEBident *)
+    [|v_mae;v_mp|];   (* SEBapply *)
+    [|v_mae;v_with|]  (* SEBwith *)
+  |])
+
 let rec v_sfb =
   Sum ("struct_field_body",0,
   [|[|v_cb|];       (* SFBconst *)
@@ -255,27 +267,25 @@ let rec v_sfb =
     [|v_module|];   (* SFBmodule *)
     [|v_modtype|]   (* SFBmodtype *)
   |])
-and v_sb = List (Tuple ("label*sfb",[|v_id;v_sfb|]))
-and v_seb =
-  Sum ("struct_expr_body",0,
-  [|[|v_mp|];                  (* SEBident *)
-    [|v_uid;v_modtype;v_seb|]; (* SEBfunctor *)
-    [|v_seb;v_seb;v_cstrs|];   (* SEBapply *)
-    [|v_sb|];                  (* SEBstruct *)
-    [|v_seb;v_with|]           (* SEBwith *)
-  |])
-and v_with =
-  Sum ("with_declaration_body",0,
-       [|[|List v_id;v_mp|];
-         [|List v_id;v_cb|]|])
+and v_struc = List (Tuple ("label*sfb",[|v_id;v_sfb|]))
+and v_sign =
+  Sum ("module_sign",0,
+  [|[|v_struc|];                   (* NoFunctor *)
+    [|v_uid;v_modtype;v_sign|]|])  (* MoreFunctor *)
+and v_mexpr =
+  Sum ("module_expr",0,
+  [|[|v_mae|];                     (* NoFunctor *)
+    [|v_uid;v_modtype;v_mexpr|]|]) (* MoreFunctor *)
+and v_impl =
+  Sum ("module_impl",2,
+  [|[|v_mexpr|];  (* Algebraic *)
+    [|v_sign|]|])  (* Struct *)
 and v_module =
   Tuple ("module_body",
-         [|v_mp;Opt v_seb;v_seb;
-           Opt v_seb;v_cstrs;v_resolver;Any|])
+         [|v_mp;v_impl;v_sign;Opt v_mexpr;v_cstrs;v_resolver;Any|])
 and v_modtype =
   Tuple ("module_type_body",
-         [|v_mp;v_seb;Opt v_seb;v_cstrs;v_resolver|])
-
+         [|v_mp;v_sign;Opt v_mexpr;v_cstrs;v_resolver|])
 
 (** kernel/safe_typing *)