affichage module et module type

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

4 files changed, 78 insertions, 47 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 7208774591..b304e0aab5 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -117,26 +117,13 @@ let contents_first_level mp =
 	  mib.mind_packets
     | _ -> ()
   in
-  try 
-    let m = Environ.lookup_module mp !cur_env in 
-    match m.mod_expr with 
-      | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s)
-      | _ -> mp,!s
-  with Not_found -> mp,!s
+  match (Environ.lookup_module mp !cur_env).mod_expr with 
+    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; (mp,!s)
+    | _ -> mp,!s
 
-let modules_first_level mp = 
-  let s = ref Stringset.empty in 
-  let add id = s := Stringset.add (rename_module id) !s in 
-  let contents_seb = function 
-    | (l, (SEBmodule _ | SEBmodtype _)) -> add (id_of_label l) 
-    | _ -> ()
-  in
-  try 
-    let m = Environ.lookup_module mp !cur_env in
-    match m.mod_expr with 
-      | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
-      | _ -> !s
-  with Not_found -> !s
+(* The previous functions might fail if [mp] isn't a directly visible module. *)
+(* Ex: [MPself] under functor, [MPbound], etc ... *)
+(* Exception [Not_found] is catched in [pp_global]. *) 
 
 let contents_first_level = 
   let cache = ref MPmap.empty in 
@@ -147,6 +134,17 @@ let contents_first_level =
       cache := MPmap.add mp res !cache; 
       res
 
+let modules_first_level mp = 
+  let s = ref Stringset.empty in 
+  let add id = s := Stringset.add (rename_module id) !s in 
+  let contents_seb = function 
+    | (l, (SEBmodule _ | SEBmodtype _)) -> add (id_of_label l) 
+    | _ -> ()
+  in
+  match (Environ.lookup_module mp !cur_env).mod_expr with 
+    | Some (MEBstruct (_,msb)) -> List.iter contents_seb msb; !s
+    | _ -> !s
+
 let rec clash_in_contents mp0 s = function  
   | [] -> false
   | (mp,_) :: _ when mp = mp0 -> false
@@ -231,7 +229,7 @@ let create_mono_renamings struc =
 module ToplevelParams = struct
   let globals () = Idset.empty
   let pp_global _ r = pr_global r
-  let pp_long_module mp = str (string_of_mp mp)
+  let pp_long_module _ mp = str (string_of_mp mp)
   let pp_short_module id = pr_id id
 end
 
@@ -268,21 +266,29 @@ module StdParams = struct
       if (Refset.mem r !must_qualify) || (lang () = Haskell)
       then str (string_of_ren l s)
       else 
-	if clash_in_contents mp s (decreasing_contents cur_mp) 
-	then str (string_of_ren l s)
-	else str s
+	try 
+	  if clash_in_contents mp s (decreasing_contents cur_mp) 
+	  then str (string_of_ren l s)
+	  else str s
+	with Not_found -> str (string_of_ren l s) 
     else 
       let nl = List.length l in 
       if n = nl && nl < List.length cur_l then (* strict prefix *)
-	if clash_in_contents mp s (decreasing_contents cur_mp) 
-	then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
-	else str s
+	try 
+	  if clash_in_contents mp s (decreasing_contents cur_mp) 
+	  then error_unqualified_name (string_of_ren l s) (string_of_modlist cur_l)
+	  else str s
+	with Not_found -> str (string_of_ren l s)
       else (* [cur_mp] and [mp] are orthogonal *)
 	let l = remove_common cur_l l 
 	in str (string_of_ren l s)
 	     
-  let pp_long_module mp = 
-    str (string_of_modlist (if !modular then mp_to_list mp else mp_to_list' mp))
+  let pp_long_module cur_mp mp = 
+    let cur_mp = long_mp cur_mp in 
+    let cur_l = if !modular then mp_to_list cur_mp else mp_to_list' cur_mp in 
+    let mp = long_mp mp in 
+    let l = if !modular then mp_to_list mp else mp_to_list' mp in 
+    str (string_of_modlist (remove_common cur_l l))
 
   let pp_short_module id = str (rename_module id)
 end
diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index ab798eebfc..325e2c8c5e 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -424,7 +424,29 @@ let extraction_module m =
 	let v = { kn = KNset.empty; mp = MPset.singleton (MPfile dir_m) } in 
 	let l = environment_until (Some dir_m) in 
 	init_env l;
-	let mp,meb = list_last l in 
+(* TEMPORARY: make Extraction Module look like Recursive Extraction Module *)
+	let struc = 
+	  let select l (mp,meb) = 
+	    if in_mp v mp then (mp, unpack (extract_meb v true meb)) :: l else l
+	  in List.fold_left select [] (List.rev l)
+	in 
+	let dummy_prm = {modular=true; mod_name=m; to_appear=[]} in
+	let struc = optimize_struct dummy_prm None struc in 
+	let rec print = function 
+	  | [] -> () 
+	  | (MPfile dir, _) :: l when dir <> dir_m -> print l 
+	  | (MPfile dir, sel) as e :: l -> 
+	      let short_m = snd (split_dirpath dir) in
+	      let f = module_file_name short_m in 
+	      let prm = {modular=true;mod_name=short_m;to_appear=[]} in
+	      print_structure_to_file (Some f) prm [e]; 
+	      print l 
+	  | _ -> assert false
+	in print struc; 
+	reset_tables ()
+
+
+(*i	let mp,meb = list_last l in 
 	let struc = [mp, unpack (extract_meb v true meb)] in 
 	let extern_decls = 
 	  let filter kn l = 
@@ -435,6 +457,8 @@ let extraction_module m =
 	let struc = optimize_struct prm (Some extern_decls) struc in 
 	print_structure_to_file (Some (module_file_name m)) prm struc; 
 	reset_tables ()
+i*)
+
 	  
 (*s Recursive Extraction of all the modules [M] depends on. 
   The vernacular command is \verb!Recursive Extraction Module! [M]. *) 
diff --git a/contrib/extraction/miniml.mli b/contrib/extraction/miniml.mli
index 235847f323..3b255a4404 100644
--- a/contrib/extraction/miniml.mli
+++ b/contrib/extraction/miniml.mli
@@ -141,7 +141,7 @@ type ml_signature = (module_path * ml_module_sig) list
 module type Mlpp_param = sig
   val globals : unit -> Idset.t
   val pp_global : module_path -> global_reference -> std_ppcmds
-  val pp_long_module : module_path -> std_ppcmds
+  val pp_long_module : module_path -> module_path -> std_ppcmds
   val pp_short_module : identifier -> std_ppcmds
 end
 
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index f11ac89d51..1892d6e952 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -515,46 +515,47 @@ let rec pp_structure_elem mp = function
 	(str "module " ++ P.pp_short_module (id_of_label l) ++ 
 	 (match m.ml_mod_equiv with 
 	    | None -> 
-		str ":" ++ fnl () ++ 
-		pp_module_type m.ml_mod_type ++ fnl () ++
+		str " :" ++ fnl () ++ 
+		pp_module_type mp m.ml_mod_type ++ fnl () ++
 		str "= " ++ fnl () ++ 
 		(match m.ml_mod_expr with 
 		   | None -> assert false (* see Jacek *)
-		   | Some me -> pp_module_expr me)
-	    | Some mp -> 
-		str " = " ++ P.pp_long_module mp))
+		   | Some me -> pp_module_expr mp me)
+	    | Some mp' -> 
+		str " = " ++ P.pp_long_module mp mp'))
   | (l,SEmodtype m) -> 
       hov 1 
 	(str "module type " ++ P.pp_short_module (id_of_label l) ++
-	 str " = " ++ fnl () ++ pp_module_type m)
+	 str " = " ++ fnl () ++ pp_module_type mp m)
 
-and pp_module_expr = function 
-  | MEident mp -> P.pp_long_module (long_mp mp)
+and pp_module_expr mp = function 
+  | MEident mp' -> P.pp_long_module mp mp'
   | MEfunctor (mbid, mt, me) -> 
       str "functor (" ++ 
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
-      pp_module_type mt ++
+      pp_module_type mp mt ++
       str ") ->" ++ fnl () ++
-      pp_module_expr me
+      pp_module_expr mp me
   | MEapply (me, me') -> 
-      str "(" ++ pp_module_expr me ++ spc () ++ pp_module_expr me' ++ str ")"
+      str "(" ++ pp_module_expr mp me ++ spc () ++ pp_module_expr mp me' ++ 
+      str ")"
   | MEstruct (msid, sel) -> 
       let l = map_succeed (pp_structure_elem (MPself msid)) sel in 
       str "struct " ++ fnl () ++
       v 1 (str " " ++ prlist_with_sep fnl2 identity l) ++ 
       fnl () ++ str "end" 
 
-and pp_module_type = function 
+and pp_module_type mp = function 
   | MTident kn -> 
-      let mp,_,l = repr_kn kn in P.pp_long_module (MPdot (long_mp mp,l)) 
+      let mp',_,l = repr_kn kn in P.pp_long_module mp (MPdot (mp,l)) 
   | MTfunsig (mbid, mt, mt') -> 
       str "functor (" ++ 
       P.pp_short_module (id_of_mbid mbid) ++
       str ":" ++
-      pp_module_type mt ++
+      pp_module_type mp mt ++
       str ") ->" ++ fnl () ++
-      pp_module_type mt'
+      pp_module_type mp mt'
   | MTsig (msid, sign) -> 
       let l = map_succeed (pp_specif (MPself msid)) sign in 
       str "sig " ++ fnl () ++ 
@@ -567,12 +568,12 @@ and pp_specif mp = function
       hov 1 
 	(str "module " ++ 
 	 P.pp_short_module (id_of_label l) ++
-	 str " : " ++ fnl () ++ pp_module_type mt)
+	 str " : " ++ fnl () ++ pp_module_type mp mt)
   | (l,Smodtype mt) -> 
       hov 1
 	(str "module type " ++
 	 P.pp_short_module (id_of_label l) ++
-	 str " : " ++ fnl () ++ pp_module_type mt)
+	 str " = " ++ fnl () ++ pp_module_type mp mt)
 
 let pp_struct s =
   let l mp sel = map_succeed (pp_structure_elem mp) sel in