Ajout des alias de module dans le noyau.

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

2 files changed, 85 insertions, 5 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index dabea0f3c9..445a26c729 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -35,7 +35,7 @@ let toplevel_env () =
 	  | "INDUCTIVE" -> SFBmind (Global.lookup_mind kn) 
 	  | "MODULE" -> SFBmodule (Global.lookup_module (MPdot (mp,l)))
 	  | "MODULE TYPE" -> 
-	      SFBmodtype (fst (Global.lookup_modtype (MPdot (mp,l))))
+	      SFBmodtype (Global.lookup_modtype (MPdot (mp,l)))
 	  | _ -> failwith "caught"
 	in l,seb
     | _ -> failwith "caught"
@@ -164,10 +164,18 @@ let rec extract_sfb_spec env mp = function
       (l,Smodule spec) :: specs
   | (l,SFBmodtype mtb) :: msig -> 
       let specs = extract_sfb_spec env mp msig in
-      (l,Smodtype (extract_seb_spec env true(*?*) mtb)) :: specs
+      (l,Smodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: specs
+  | (l,SFBalias(mp1,_))::msig -> 
+      extract_sfb_spec env mp 
+	((l,SFBmodule {mod_expr = Some (SEBident mp1);
+		      mod_type = None;
+		      mod_constraints = Univ.Constraint.empty;
+		      mod_alias = Mod_subst.empty_subst;
+		      mod_retroknowledge = []})::msig)
 
 (* From [struct_expr_body] to specifications *)
 
+
 and extract_seb_spec env truetype = function
   | SEBident kn when truetype -> Visit.add_mp kn; MTident kn 
   | SEBwith(mtb',With_definition_body(idl,cb))->
@@ -182,7 +190,7 @@ and extract_seb_spec env truetype = function
   | SEBfunctor (mbid, mtb, mtb') -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in
-	MTfunsig (mbid, extract_seb_spec env true mtb, 
+	MTfunsig (mbid, extract_seb_spec env true mtb.typ_expr, 
 		  extract_seb_spec env' truetype mtb')
   | SEBstruct (msid, msig) -> 
       let mp = MPself msid in 
@@ -240,7 +248,18 @@ let rec extract_sfb env mp all = function
       let ms = extract_sfb env mp all msb in
       let mp = MPdot (mp,l) in
        if all || Visit.needed_mp mp then 
-	(l,SEmodtype (extract_seb_spec env true(*?*) mtb)) :: ms
+	(l,SEmodtype (extract_seb_spec env true(*?*) mtb.typ_expr)) :: ms
+      else ms
+  | (l,SFBalias (mp1,cst)) :: msb -> 
+      let ms = extract_sfb env mp all msb in
+      let mp = MPdot (mp,l) in 
+      if all || Visit.needed_mp mp then 
+	(l,SEmodule (extract_module env mp true 
+		       {mod_expr = Some (SEBident mp1);
+			mod_type = None;
+		        mod_constraints= Univ.Constraint.empty;
+			mod_alias = empty_subst;
+			mod_retroknowledge = []})) :: ms
       else ms
 
 (* From [struct_expr_body] to implementations *)
@@ -255,7 +274,7 @@ and extract_seb env mpo all = function
   | SEBfunctor (mbid, mtb, meb) -> 
       let mp = MPbound mbid in 
       let env' = Modops.add_module mp (Modops.module_body_of_type mtb) env in 
-      MEfunctor (mbid, extract_seb_spec env true mtb, 
+      MEfunctor (mbid, extract_seb_spec env true mtb.typ_expr, 
 		 extract_seb env' None true meb)
   | SEBstruct (msid, msb) -> 
       let mp,msb = match mpo with 
diff --git a/contrib/extraction/modutil.ml b/contrib/extraction/modutil.ml
index dca56efaed..87f9187348 100644
--- a/contrib/extraction/modutil.ml
+++ b/contrib/extraction/modutil.ml
@@ -20,6 +20,67 @@ open Mod_subst
 
 (*S Functions upon modules missing in [Modops]. *) 
 
+(*<<<<<<< .mine
+(*s Add _all_ direct subobjects of a module, not only those exported. 
+   Build on the [Modops.add_signature] model. *)
+
+let add_structure mp msb env = 
+  let add_one env (l,elem) = 
+    let kn = make_kn mp empty_dirpath l in 
+    let con = make_con mp empty_dirpath l in 
+    match elem with 
+      | SFBconst cb -> Environ.add_constant con cb env 
+      | SFBmind mib -> Environ.add_mind kn mib env 
+      | SFBmodule mb -> Modops.add_module (MPdot (mp,l)) mb env 
+      | SFBmodtype mtb -> Environ.add_modtype (MPdot (mp,l)) mtb env
+      | SFBalias (mp1,_) -> Environ.register_alias (MPdot (mp,l)) mp1 env
+  in List.fold_left add_one env msb
+
+(*s Apply a module path substitution on a module.
+   Build on the [Modops.subst_modtype] model. *)
+
+let rec subst_module sub mb =
+  let mtb' = Option.smartmap (Modops.subst_struct_expr sub) mb.mod_type
+  and meb' = Option.smartmap (subst_meb sub) mb.mod_expr in
+  if (mtb'==mb.mod_type) && (meb'==mb.mod_expr) 
+  then mb
+  else { mod_expr= meb'; 
+	 mod_type=mtb'; 
+	 mod_constraints=mb.mod_constraints;
+	 mod_alias = mb.mod_alias;
+         mod_retroknowledge=[] } (* spiwack: since I'm lazy and it's unused at 
+				    this point. I forget about retroknowledge, 
+				    this may need a change later *) 
+
+and subst_meb sub = function 
+  | SEBident mp -> SEBident (subst_mp sub mp) 
+  | SEBfunctor (mbid, mtb, meb) -> 
+      assert (not (occur_mbid mbid sub)); 
+      SEBfunctor (mbid, Modops.subst_modtype sub mtb, subst_meb sub meb)
+  | SEBstruct (msid, msb) -> 
+      assert (not (occur_msid msid sub));
+      SEBstruct (msid, subst_msb sub msb)
+  | SEBapply (meb, meb', c) -> 
+      SEBapply (subst_meb sub meb, subst_meb sub meb', c)
+  | SEBwith (meb,With_module_body(id,mp,cst))->
+	SEBwith(subst_meb sub meb,
+		With_module_body(id,Mod_subst.subst_mp sub mp,cst))
+  | SEBwith (meb,With_definition_body(id,cb))->
+      SEBwith(subst_meb sub meb,
+	      With_definition_body(id,Declarations.subst_const_body sub cb))
+
+
+and subst_msb sub msb = 
+  let subst_body = function
+    | SFBconst cb -> SFBconst (subst_const_body sub cb)
+    | SFBmind mib -> SFBmind (subst_mind sub mib)
+    | SFBmodule mb -> SFBmodule (subst_module sub mb)
+    | SFBmodtype mtb -> SFBmodtype (Modops.subst_modtype sub mtb)
+    | SFBalias (mp,cst) -> SFBalias(subst_mp sub mp,cst)
+  in List.map (fun (l,b) -> (l,subst_body b)) msb
+
+=======
+>>>>>>> .r10624 *)
 (*s Change a msid in a module type, to follow a module expr. 
   Because of the "with" construct, the module type of a module can be a 
   [MTBsig] with a msid different from the one of the module. *)