Include Self (Type) Foo: applying a (Type) Functor to the current context

 If you have some Module Type F (X:Sig), and you are in a Module Type
 containing everything required to satisfy Sig (typically thanks to
 some earlier Include), then you can say Include Self Type F, and voila,
 objects of F are now added in your context, instantiated by local objects.
 Same behavior (hopefully) for modules and functors when using Include Self F.

 This experimental new command allows to easily produce static signatures
 out of functorial ones:

 Module Type F_static. Include Sig. Include Self F. End F_static.

 ... is similar to ...

 Module Type F_static. Declare Module X:Sig. Include F X. End F_static.

 ... but without the pollution of this artificial inner module X.

 This allow to split things in many othogonal components, and then mix them.
 It is a lightweight way to tackle the "diamond problem" of modular
 developpements without things like "overlapping" Include's (planned, but
 not yet there). See next commit for an example of use.

 Thanks to Elie for the debugging of my first ugly prototype...

 NB: According to Yann R.G., this is related with Scala's Traits.

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

10 files changed, 92 insertions, 28 deletions

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b0dc6dd8a..ef2ea800c 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -431,13 +431,29 @@ let end_module l restype senv =
        let mtb = 
 	 translate_module_type senv.env 
 	   senv.modinfo.modpath me in
-	 mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
+       mtb.typ_expr,mtb.typ_constraints,mtb.typ_delta
    in
    let senv = add_constraints cst senv in
    let mp_sup = senv.modinfo.modpath in
+     (* Include Self support  *)
+   let rec compute_sign sign mb senv = 
+     match sign with
+     | SEBfunctor(mbid,mtb,str) ->
+	 let cst_sub = check_subtypes senv.env mb mtb in
+	 let senv = add_constraints cst_sub senv in
+	 let mpsup_delta = complete_inline_delta_resolver senv.env mp_sup 
+	   mbid mtb mb.typ_delta in
+	   (compute_sign 
+	     (subst_struct_expr (map_mbid mbid mp_sup mpsup_delta) str) mb senv)
+     | str -> str,senv
+   in
+   let sign,senv = compute_sign sign {typ_mp = mp_sup;
+				      typ_expr = SEBstruct (List.rev senv.revstruct);
+				      typ_expr_alg = None;
+				      typ_constraints = Constraint.empty;
+				      typ_delta = senv.modinfo.resolver} senv in
    let str = match sign with
-     | SEBstruct(str_l) ->
-	 str_l
+     | SEBstruct(str_l) -> str_l
      | _ -> error ("You cannot Include a high-order structure.")
    in
    let senv =
@@ -683,7 +699,15 @@ let start_library dir senv =
 	loads = [];
         local_retroknowledge = [] }
 
-
+let pack_module senv =
+  {mod_mp=senv.modinfo.modpath;
+   mod_expr=None;
+   mod_type= SEBstruct (List.rev senv.revstruct);
+   mod_type_alg=None;
+   mod_constraints=Constraint.empty;
+   mod_delta=senv.modinfo.resolver;
+   mod_retroknowledge=[];
+  }
 
 let export senv dir =
   let modinfo = senv.modinfo in
diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli
index f011d42b7..169fd158d 100644
--- a/kernel/safe_typing.mli
+++ b/kernel/safe_typing.mli
@@ -89,8 +89,10 @@ val end_modtype :
   label -> safe_environment -> module_path * safe_environment
 
 val add_include :
-  module_struct_entry -> bool -> safe_environment -> delta_resolver * safe_environment
+  module_struct_entry -> bool -> safe_environment ->
+   delta_resolver * safe_environment
 
+val pack_module : safe_environment -> module_body
 val current_modpath : safe_environment -> module_path
 val delta_of_senv : safe_environment -> delta_resolver*delta_resolver
   
diff --git a/library/declaremods.ml b/library/declaremods.ml
index 68ce86b3a..c40e94c51 100644
--- a/library/declaremods.ml
+++ b/library/declaremods.ml
@@ -750,8 +750,6 @@ let rec get_module_substobjs env mp_from = function
   | MSEwith (mty, With_Definition _) -> get_module_substobjs env mp_from mty
   | MSEwith (mty, With_Module (idl,mp)) -> assert false
 
-
-
 (* Include *)
 
 let rec subst_inc_expr subst me =
@@ -769,7 +767,8 @@ let rec subst_inc_expr subst me =
     | MSEapply (me1,me2) ->
 	MSEapply (subst_inc_expr subst me1,
 		  subst_inc_expr subst me2)
-    | _ -> anomaly "You cannot Include a high-order structure"
+    | MSEfunctor(mbid,me1,me2) ->
+        MSEfunctor (mbid, subst_inc_expr subst me1, subst_inc_expr subst me2)
 
 let lift_oname (sp,kn) =
   let mp,_,_ = Names.repr_kn kn in
@@ -893,19 +892,49 @@ let declare_module interp_modtype interp_modexpr id args mty_o mexpr_o =
     Summary.unfreeze_summaries fs; raise e
 
 
-let declare_include interp_struct me_ast is_mod =
+let declare_include interp_struct me_ast is_mod is_self =
 
   let fs = Summary.freeze_summaries () in
 
     try
       let env = Global.env() in
-      let me = interp_struct env me_ast in 
+      let me = interp_struct env me_ast in
       let mp1,_ = current_prefix () in
-      let (mbids,mp,objs)= 	
+      let compute_objs objs = function
+	| MSEident mp -> 
+	    let mb_mp = if is_mod then 
+	     Environ.lookup_module mp env else  
+	       Modops.module_body_of_type mp (Environ.lookup_modtype mp env) in
+	      (match objs with
+		 |([],_,_) -> objs	  
+		 |(mbids,mp_self,objects) -> 
+		    let mb = Global.pack_module() in
+		    let rec compute_subst mbids sign  =
+		      match mbids with
+			  [] -> empty_subst
+			| mbid::mbids ->
+			    let farg_id, farg_b, fbody_b = 
+			      Modops.destr_functor env sign in
+			    let subst=compute_subst mbids fbody_b in
+			    let mp_delta = 
+			      Modops.complete_inline_delta_resolver env mb.mod_mp 
+				farg_id farg_b mb.mod_delta in
+			      join (map_mbid mbid mb.mod_mp mp_delta) subst
+		    in
+		    let subst = compute_subst mbids mb_mp.mod_type in
+		      ([],mp_self,subst_objects subst objects)
+		 
+	    )
+	| _ -> objs
+      in
+   
+      let (mbids,mp,objs)=
 	if is_mod then
 	  get_module_substobjs env mp1 me
 	else
 	  get_modtype_substobjs env mp1 me in
+      let (mbids,mp,objs) = if is_self 
+      then compute_objs (mbids,mp,objs) me else (mbids,mp,objs) in
       let id = current_mod_id() in
       let resolver =  Global.add_include me is_mod in
       let substobjs = (mbids,mp1,
@@ -916,7 +945,6 @@ let declare_include interp_struct me_ast is_mod =
       (* Something wrong: undo the whole process *)
       Summary.unfreeze_summaries fs; raise e
 
-
 (*s Iterators. *)
 
 let iter_all_segments f =
diff --git a/library/declaremods.mli b/library/declaremods.mli
index 5cda0d28d..4a037b005 100644
--- a/library/declaremods.mli
+++ b/library/declaremods.mli
@@ -100,7 +100,7 @@ val import_module : bool -> module_path -> unit
 (* Include  *)
 
 val declare_include : (env -> 'struct_expr -> module_struct_entry) ->
-  'struct_expr -> bool -> unit
+  'struct_expr -> bool -> bool -> unit
 
 (*s [iter_all_segments] iterate over all segments, the modules'
     segments first and then the current segment. Modules are presented
diff --git a/library/global.ml b/library/global.ml
index 6d7942ec0..3129c1caf 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -108,6 +108,8 @@ let end_modtype fs id =
     global_env := newenv;
     kn
 
+let pack_module () = 
+  pack_module !global_env
 
 
 
diff --git a/library/global.mli b/library/global.mli
index 30bd04150..b7e788912 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -52,7 +52,8 @@ val add_mind        :
 
 val add_module      : identifier -> module_entry -> module_path * delta_resolver
 val add_modtype     : identifier -> module_struct_entry -> module_path
-val add_include : module_struct_entry -> bool -> delta_resolver
+val add_include :
+ module_struct_entry -> bool -> delta_resolver
 
 val add_constraints : constraints -> unit
 
@@ -74,7 +75,7 @@ val add_module_parameter : mod_bound_id -> module_struct_entry -> delta_resolver
 
 val start_modtype : identifier -> module_path
 val end_modtype : Summary.frozen -> identifier -> module_path
-
+val pack_module : unit -> module_body
 
 
 (* Queries *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 3bc27965a..3a99b2473 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -413,8 +413,13 @@ GEXTEND Gram
 	  VernacRequireFrom (export, None, filename)
       | IDENT "Import"; qidl = LIST1 global -> VernacImport (false,qidl)
       | IDENT "Export"; qidl = LIST1 global -> VernacImport (true,qidl)
-      | IDENT "Include"; expr = module_expr -> VernacInclude(CIME(expr))
-      | IDENT "Include"; "Type"; expr = module_type -> VernacInclude(CIMTE(expr)) ] ]
+      | IDENT "Include"; expr = module_expr -> VernacInclude(false,CIME(expr))
+      | IDENT "Include"; "Type"; expr = module_type ->
+          VernacInclude(false,CIMTE(expr))
+      | IDENT "Include"; "Self"; expr = module_expr ->
+          VernacInclude(true,CIME(expr))
+      | IDENT "Include"; "Self"; "Type"; expr = module_type ->
+          VernacInclude(true,CIMTE(expr)) ] ]
   ;
   export_token:
     [ [ IDENT "Import" -> Some false
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 9e7bd10e7..52ef1875f 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -761,15 +761,15 @@ let rec pr_vernac = function
       let b = pr_module_binders_list bl pr_lconstr in
 	hov 2 (str"Module Type " ++ pr_lident id ++ b ++
 		 pr_opt (fun mt -> str ":= " ++ pr_module_type pr_lconstr mt) m)
-  | VernacInclude (in_ast) ->
+  | VernacInclude (b,in_ast) ->
       begin
 	match in_ast with
 	  | CIMTE mty ->
-	      hov 2 (str"Include" ++
-		       (fun mt -> str " " ++ pr_module_type pr_lconstr mt) mty)
+	      hov 2 (str"Include " ++ str (if b then "Self " else "") ++
+		     pr_module_type pr_lconstr mty)
 	  | CIME mexpr ->
-	      hov 2 (str"Include" ++
-		       (fun me -> str " " ++ pr_module_expr me) mexpr)
+	      hov 2 (str"Include " ++ str (if b then "Self " else "") ++
+		     pr_module_expr mexpr)
       end
   (* Solving *)
   | VernacSolve (i,tac,deftac) ->
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 60e38d97f..2008e5f01 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -555,11 +555,13 @@ let vernac_end_modtype (loc,id) =
   Dumpglob.dump_modref loc mp "modtype";
   if_verbose message ("Module Type "^ string_of_id id ^" is defined")
 
-let vernac_include = function
+let vernac_include is_self = function
   | CIMTE mty_ast ->
-      Declaremods.declare_include Modintern.interp_modtype mty_ast false
+      Declaremods.declare_include
+	Modintern.interp_modtype mty_ast false is_self
   | CIME mexpr_ast ->
-      Declaremods.declare_include Modintern.interp_modexpr mexpr_ast true
+      Declaremods.declare_include
+	Modintern.interp_modexpr mexpr_ast true is_self
 
 (**********************)
 (* Gallina extensions *)
@@ -1331,8 +1333,8 @@ let interp c = match c with
       vernac_define_module export lid bl mtyo mexpro
   | VernacDeclareModuleType (lid,bl,mtyo) ->
       vernac_declare_module_type lid bl mtyo
-  | VernacInclude (in_ast) ->
-      vernac_include in_ast
+  | VernacInclude (is_self,in_ast) ->
+      vernac_include is_self in_ast
   (* Gallina extensions *)
   | VernacBeginSection lid -> vernac_begin_section lid
 
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 8a70e7626..366308bfa 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -264,7 +264,7 @@ type vernac_expr =
       module_binder list * (module_type_ast * bool) option * module_ast option
   | VernacDeclareModuleType of lident *
       module_binder list * module_type_ast option
-  | VernacInclude of include_ast
+  | VernacInclude of bool * include_ast
 
   (* Solving *)