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

1 files changed, 35 insertions, 7 deletions

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 =