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

1 files changed, 12 insertions, 10 deletions

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