Extraction: better support of modules

 - For Haskell, modules abbreviations and applied functors are expanded.
   The only remaining sitation that isn't supported is extracting functors
   and applying them after extraction.

 - Add a module extraction for Scheme with the same capabilities as for
   Haskell (with no Extraction Library, though).

 - Nicer extracted module types (use of the mb.mod_type_alg if present)

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

4 files changed, 28 insertions, 19 deletions

diff --git a/plugins/extraction/common.ml b/plugins/extraction/common.ml
index afa674e9d..0941ed50f 100644
--- a/plugins/extraction/common.ml
+++ b/plugins/extraction/common.ml
@@ -304,7 +304,7 @@ and mp_renaming =
 let ref_renaming_fun (k,r) =
   let mp = modpath_of_r r in
   let l = mp_renaming mp in
-  let l = if lang () = Haskell && not (modular ()) then [""] else l in
+  let l = if lang () <> Ocaml && not (modular ()) then [""] else l in
   let s =
     if l = [""] (* this happens only at toplevel of the monolithic case *)
     then
diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index a426b2274..2fca8016c 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -137,17 +137,8 @@ let factor_fix env l cb msb =
     labels, recd, msb''
   end
 
-let build_mb mp expr typ_opt =
-  { mod_mp = mp;
-    mod_expr = Some expr;
-    mod_type = typ_opt;
-    mod_type_alg = None;
-    mod_constraints = Univ.Constraint.empty;
-    mod_delta = Mod_subst.empty_delta_resolver;
-    mod_retroknowledge = [] }
-
 let my_type_of_mb env mb =
-   mb.mod_type
+  match mb.mod_type_alg with Some m -> m | None -> mb.mod_type
 
 (** Ad-hoc update of environment, inspired by [Mod_type.check_with_aux_def].
     To check with Elie. *)
@@ -282,6 +273,17 @@ let rec extract_sfb env mp all = function
 (* From [struct_expr_body] to implementations *)
 
 and extract_seb env mp all = function
+  | (SEBident _ | SEBapply _) as seb when lang () <> Ocaml ->
+      (* in Haskell/Scheme, we expanse everything *)
+      let rec seb2mse = function
+	| SEBident mp -> Entries.MSEident mp
+	| SEBapply (s,s',_) -> Entries.MSEapply(seb2mse s, seb2mse s')
+	| _ -> assert false
+      in
+      let seb,_,_,_ =
+	Mod_typing.translate_struct_module_entry env mp true (seb2mse seb)
+      in
+      extract_seb env mp all seb
   | SEBident mp ->
       if is_modfile mp && not (modular ()) then error_MPfile_as_mod mp false;
       Visit.add_mp mp; MEident mp
diff --git a/plugins/extraction/haskell.ml b/plugins/extraction/haskell.ml
index 333bdcddd..ce9fab735 100644
--- a/plugins/extraction/haskell.ml
+++ b/plugins/extraction/haskell.ml
@@ -319,9 +319,10 @@ let rec pp_structure_elem = function
 
 and pp_module_expr = function
   | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel
-  | MEident _ -> failwith "Not Implemented: Module Ident"
-  | MEfunctor _ -> failwith "Not Implemented: Module Functor"
-  | MEapply _ -> failwith "Not Implemented: Module Application"
+  | MEfunctor _ -> mt ()
+      (* for the moment we simply discard unapplied functors *)
+  | MEident _ | MEapply _ -> assert false
+      (* should be expansed in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =
diff --git a/plugins/extraction/scheme.ml b/plugins/extraction/scheme.ml
index 097df6a61..9c600760f 100644
--- a/plugins/extraction/scheme.ml
+++ b/plugins/extraction/scheme.ml
@@ -180,12 +180,18 @@ let pp_decl = function
 	  hov 2 (paren (str "define " ++ pp_global Term r ++ spc () ++
 			  pp_expr (empty_env ()) [] a)) ++ fnl () ++ fnl ()
 
-let pp_structure_elem = function
+let rec pp_structure_elem = function
   | (l,SEdecl d) -> pp_decl d
-  | (l,SEmodule m) ->
-      failwith "TODO: Scheme extraction of modules not implemented yet"
-  | (l,SEmodtype m) ->
-      failwith "TODO: Scheme extraction of modules not implemented yet"
+  | (l,SEmodule m) -> pp_module_expr m.ml_mod_expr
+  | (l,SEmodtype m) -> mt ()
+      (* for the moment we simply discard module type *)
+
+and pp_module_expr = function
+  | MEstruct (mp,sel) -> prlist_strict pp_structure_elem sel
+  | MEfunctor _ -> mt ()
+      (* for the moment we simply discard unapplied functors *)
+  | MEident _ | MEapply _ -> assert false
+      (* should be expansed in extract_env *)
 
 let pp_struct =
   let pp_sel (mp,sel) =