Imported Upstream version 8.1~gammaupstream/8.1.gamma

1 files changed, 48 insertions, 29 deletions

diff --git a/kernel/modops.ml b/kernel/modops.ml
index b2f02a5f..5cc2a84d 100644
--- a/kernel/modops.ml
+++ b/kernel/modops.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: modops.ml 8879 2006-05-30 21:32:10Z letouzey $ i*)
+(*i $Id: modops.ml 9138 2006-09-14 15:20:45Z jforest $ i*)
 
 (*i*)
 open Util
@@ -170,34 +170,6 @@ and subst_module sub mb =
 let subst_signature_msid msid mp = 
   subst_signature (map_msid msid mp)
 
-let rec constants_of_specification env mp sign =
- let aux res (l,elem) =
-  match elem with
-   | SPBconst cb -> ((make_con mp empty_dirpath l),cb)::res
-   | SPBmind _ -> res
-   | SPBmodule mb ->
-      (constants_of_modtype env (MPdot (mp,l))
-        (module_body_of_spec mb).mod_type) @ res
-   | SPBmodtype mtb -> res (* ???? *)
- in
-  List.fold_left aux [] sign
-
-and constants_of_modtype env mp modtype =
- match scrape_modtype env modtype with
-    MTBident _ -> anomaly "scrape_modtype does not work!"
-  | MTBsig (msid,sign) ->
-     constants_of_specification env mp
-      (subst_signature_msid msid mp sign)
-  | MTBfunsig _ -> []
-
-(* returns a resolver for kn that maps mbid to mp *)
-(* Nota: Some delta-expansions used to happen here. 
-    Browse SVN if you want to know more. *)
-let resolver_of_environment mbid modtype mp env =
- let constants = constants_of_modtype env (MPbound mbid) modtype in
- let resolve = List.map (fun (con,_) -> con,None) constants in 
- Mod_subst.make_resolver resolve
-
 (* we assume that the substitution of "mp" into "msid" is already done
 (or unnecessary) *)
 let rec add_signature mp sign env = 
@@ -224,6 +196,53 @@ and add_module mp mb env =
       | MTBfunsig _ -> env
 
 
+let rec constants_of_specification env mp sign =
+ let aux (env,res) (l,elem) =
+  match elem with
+   | SPBconst cb -> env,((make_con mp empty_dirpath l),cb)::res
+   | SPBmind _ -> env,res
+   | SPBmodule mb ->
+       let new_env =  add_module (MPdot (mp,l)) (module_body_of_spec mb) env in 
+       new_env,(constants_of_modtype env (MPdot (mp,l))
+		  (module_body_of_spec mb).mod_type) @ res
+   | SPBmodtype mtb -> 
+       (* module type dans un module type. 
+	  Il faut au moins mettre mtb dans l'environnement (avec le bon 
+	  kn pour pouvoir continuer aller deplier les modules utilisant ce 
+	  mtb
+	  ex: 
+	  Module Type T1. 
+	  Module Type T2.
+	     ....
+    	    End T2.
+	  .....
+            Declare Module M : T2.
+         End T2 
+	  si on ne rajoute pas T2 dans l'environement de typage 
+	  on va exploser au moment du Declare Module
+       *)
+       let new_env = Environ.add_modtype (make_kn mp empty_dirpath l) mtb env in 
+       new_env, constants_of_modtype env (MPdot(mp,l)) mtb @ res
+ in
+ snd (List.fold_left aux (env,[]) sign)
+
+and constants_of_modtype env mp modtype =
+ match scrape_modtype env modtype with
+    MTBident _ -> anomaly "scrape_modtype does not work!"
+  | MTBsig (msid,sign) ->
+     constants_of_specification env mp
+      (subst_signature_msid msid mp sign)
+  | MTBfunsig _ -> []
+
+(* returns a resolver for kn that maps mbid to mp *)
+(* Nota: Some delta-expansions used to happen here. 
+    Browse SVN if you want to know more. *)
+let resolver_of_environment mbid modtype mp env =
+ let constants = constants_of_modtype env (MPbound mbid) modtype in
+ let resolve = List.map (fun (con,_) -> con,None) constants in 
+ Mod_subst.make_resolver resolve
+
+
 let strengthen_const env mp l cb = 
   match cb.const_opaque, cb.const_body with
   | false, Some _ -> cb