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

2 files changed, 8 insertions, 6 deletions

diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 60e38d97f4..2008e5f01f 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 8a70e76260..366308bfa6 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 *)