modifs des preambules d'extraction modulaire

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

5 files changed, 53 insertions, 45 deletions

diff --git a/contrib/extraction/common.ml b/contrib/extraction/common.ml
index 4b95ba410..7dba81ff2 100644
--- a/contrib/extraction/common.ml
+++ b/contrib/extraction/common.ml
@@ -232,40 +232,29 @@ module HaskellModularPp = Haskell.Make(ModularParams)
 
 (*s Extraction to a file. *)
 
-let init_global_ids lang = 
-  Hashtbl.clear renamings;
-  keywords := 
-  (match lang with 
-     | Ocaml -> Ocaml.keywords
-     | Haskell -> Haskell.keywords);
-  global_ids := !keywords
-
 let extract_to_file f prm decls =
-  cons_cofix := Refset.empty;
-  current_module := prm.mod_name;
-  init_global_ids prm.lang;
+  let preamble,keyw = match prm.lang with 
+    | Ocaml -> Ocaml.preamble,Ocaml.keywords
+    | Haskell -> Haskell.preamble,Haskell.keywords
+  in 
   let pp_decl = match prm.lang,prm.modular with 
     | Ocaml, false -> OcamlMonoPp.pp_decl
     | Ocaml, _ -> OcamlModularPp.pp_decl
-    | Haskell, false -> HaskellMonoPp.pp_decl
+    | Haskell, false -> HaskellMonoPp.pp_decl    
     | Haskell, _ -> HaskellModularPp.pp_decl
   in
-  let preamble,prop_decl,open_str = match prm.lang with 
-    | Ocaml -> Ocaml.preamble, Ocaml.prop_decl, "open "
-    | Haskell -> Haskell.preamble, Haskell.prop_decl, "import qualified "
-  in
   let used_modules = if prm.modular then 
     Idset.remove prm.mod_name (decl_get_modules decls)
   else Idset.empty
   in 
+  cons_cofix := Refset.empty;
+  current_module := prm.mod_name;
+  Hashtbl.clear renamings;
+  keywords := keyw;
+  global_ids := keyw; 
   let cout = open_out f in
   let ft = Pp_control.with_output_to cout in
-  pp_with ft (preamble prm);
-  Idset.iter 
-    (fun m -> msgnl_with ft (str open_str ++ pr_id (uppercase_id m))) 
-    used_modules; 
-  if (decl_print_prop decls) then msgnl_with ft prop_decl
-  else msgnl_with ft (mt()); 
+  pp_with ft (preamble prm used_modules (decl_print_prop decls));
   begin 
     try
       List.iter (fun d -> msgnl_with ft (pp_decl d)) decls
@@ -273,4 +262,17 @@ let extract_to_file f prm decls =
       pp_flush_with ft (); close_out cout; raise e
   end;
   pp_flush_with ft ();
-  close_out cout  
+  close_out cout;  
+
+(*i 
+  (* names resolution *)
+  let cout = open_out (f^".ren") in 
+  let ft = Pp_control.with_output_to cout in
+  Hashtbl.iter 
+    (fun r id -> 
+       if short_module r = !current_module then 
+	 msgnl_with ft (pr_id id ++ str " " ++ pr_sp (sp_of_r r)))
+    renamings;
+  pp_flush_with ft ();
+  close_out cout;
+i*)    
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index 4970a0791..7abccdf5d 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -31,17 +31,23 @@ let keywords =
     "as"; "qualified"; "hiding" ; "prop" ; "arity" ]
   Idset.empty
 
-let preamble prm =
+let preamble prm used_modules used_prop =
   let m = String.capitalize (string_of_id prm.mod_name)   in 
   str "module " ++ str m ++ str " where" ++ fnl () ++ fnl() ++ 
-  str "import qualified Prelude" ++ fnl()
+  str "import qualified Prelude" ++ fnl() ++
+  Idset.fold 
+    (fun m s -> 
+       s ++ str "import qualified " ++ pr_id (uppercase_id m) ++ fnl())
+    used_modules (mt ())
+  ++ 
+  (if used_prop then 
+     str "import qualified Unit" ++ fnl () ++ fnl () ++
+     str "type Prop = Unit.Unit" ++ fnl () ++
+     str "prop = Unit.unit" ++ fnl () ++ fnl () ++
+     str "data Arity = Unit.Unit" ++ fnl () ++
+     str "arity = Unit.unit" ++ fnl () ++ fnl () 
+   else fnl ())
 
-let prop_decl = 
-  str "import qualified Unit" ++ fnl () ++ fnl () ++
-  str "type Prop = Unit.Unit" ++ fnl () ++
-  str "prop = Unit.unit" ++ fnl () ++ fnl () ++
-  str "data Arity = Unit.Unit" ++ fnl () ++
-  str "arity = Unit.unit" ++ fnl ()
 
 let pp_abst = function
   | [] -> (mt ())
diff --git a/contrib/extraction/haskell.mli b/contrib/extraction/haskell.mli
index 73e9e974a..5d744be2a 100644
--- a/contrib/extraction/haskell.mli
+++ b/contrib/extraction/haskell.mli
@@ -15,8 +15,6 @@ open Miniml
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> std_ppcmds
-
-val prop_decl : std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
 
 module Make : functor(P : Mlpp_param) -> Mlpp
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 42b7cbf9c..5dcbc4667 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -117,14 +117,18 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "prop" ; "arity" ] 
   Idset.empty
 
-let preamble _ = mt()
-
-let prop_decl = 
-  fnl () ++
-  str "type prop = unit" ++ fnl () ++
-  str "let prop = ()" ++ fnl () ++ fnl () ++
-  str "type arity = unit" ++ fnl () ++
-  str "let arity = ()" ++ fnl ()
+let preamble _ used_modules used_prop = 
+  (if used_prop then 
+    str "type prop = unit" ++ fnl () ++
+    str "let prop = ()" ++ fnl () ++ fnl () ++
+    str "type arity = unit" ++ fnl () ++
+    str "let arity = ()" ++ fnl () ++ fnl ()
+  else mt ())
+  ++
+  Idset.fold (fun m s -> s ++ str "open " ++ pr_id (uppercase_id m) ++ fnl())
+    used_modules (mt ())
+  ++ 
+  (if Idset.is_empty used_modules  then mt () else fnl ()) 
 
 (*s The pretty-printing functor. *)
 
diff --git a/contrib/extraction/ocaml.mli b/contrib/extraction/ocaml.mli
index 7c5855d13..0e4d79a7c 100644
--- a/contrib/extraction/ocaml.mli
+++ b/contrib/extraction/ocaml.mli
@@ -42,9 +42,7 @@ val get_db_name : int -> env -> identifier
 
 val keywords : Idset.t
 
-val preamble : extraction_params -> std_ppcmds
-
-val prop_decl : std_ppcmds
+val preamble : extraction_params -> Idset.t -> bool -> std_ppcmds
 
 (*s Production of Ocaml syntax. We export both a functor to be used for 
     extraction in the Coq toplevel and a function to extract some