From 68dfbbc355bdcab7f7880bacc4be6fe337afa800 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Mon, 16 Nov 2009 13:46:22 +0000
Subject: 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
---
 kernel/safe_typing.ml  | 32 ++++++++++++++++++++++++++++----
 kernel/safe_typing.mli |  4 +++-
 2 files changed, 31 insertions(+), 5 deletions(-)

(limited to 'kernel')

diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index b0dc6dd8a0..ef2ea800cf 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 f011d42b7f..169fd158d8 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
   
-- 
cgit v1.2.3