Repair Haskell/Scheme extraction in the new extraction backend design:

Unlike prlist_xxxx and prvect, the function prlist is acting lazily,
which is bad for extraction (synchronization with tables).  We add and
use a prlist_strict function.

Additionaly: 
 - cleanup of the preamble printing
 - no need for 2-pass printing (/dev/null trick) when the language 
   isn't ocaml



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

6 files changed, 51 insertions, 58 deletions

diff --git a/contrib/extraction/extract_env.ml b/contrib/extraction/extract_env.ml
index 953e4930bf..b8d964b854 100644
--- a/contrib/extraction/extract_env.ml
+++ b/contrib/extraction/extract_env.ml
@@ -321,11 +321,14 @@ let print_structure_to_file (fn,si,mo) struc =
   let ft = match cout with 
     | None -> !Pp_control.std_ft
     | Some cout -> Pp_control.with_output_to cout in 
-  let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in 
   begin try 
     msg_with ft (d.preamble mo used_modules unsafe_needs);
-    msg_with devnull (d.pp_struct struc); (* for computing objects to duplicate *)
-    reset_renaming_tables OnlyLocal; 
+    if lang () = Ocaml then begin 
+      (* for computing objects to duplicate *)
+      let devnull = Format.make_formatter (fun _ _ _ -> ()) (fun _ -> ()) in
+      msg_with devnull (d.pp_struct struc);
+      reset_renaming_tables OnlyLocal; 
+    end; 
     msg_with ft (d.pp_struct struc);
     option_iter close_out cout; 
   with e -> 
diff --git a/contrib/extraction/haskell.ml b/contrib/extraction/haskell.ml
index f55bc6feb8..e8ba789039 100644
--- a/contrib/extraction/haskell.ml
+++ b/contrib/extraction/haskell.ml
@@ -31,20 +31,17 @@ let keywords =
   Idset.empty
 
 let preamble mod_name used_modules usf =
-  let pp_mp = function 
-    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
-    | _ -> assert false 
-  in  
+  let pp_import mp = str ("import qualified "^ string_of_modfile mp ^"\n")
+  in 
   (if not usf.magic then mt () 
    else
      str "{-# OPTIONS_GHC -cpp -fglasgow-exts #-}\n" ++
      str "{- For Hugs, use the option -F\"cpp -P -traditional\" -}\n\n")
   ++
-  str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl () 
-  ++ fnl() ++ 
-  str "import qualified Prelude" ++ fnl() ++
-  prlist (fun mp -> str "import qualified " ++ pp_mp mp ++ fnl ()) used_modules
-  ++ fnl () ++
+  str "module " ++ pr_upper_id mod_name ++ str " where" ++ fnl2 () ++
+  str "import qualified Prelude" ++ fnl () ++
+  prlist pp_import used_modules ++ fnl () ++ 
+  (if used_modules = [] then mt () else fnl ()) ++
   (if not usf.magic then mt () 
    else str "\
 #ifdef __GLASGOW_HASKELL__
@@ -54,14 +51,10 @@ unsafeCoerce = GHC.Base.unsafeCoerce#
 -- HUGS
 import qualified IOExts
 unsafeCoerce = IOExts.unsafeCoerce
-#endif")
-  ++
-  fnl() ++ fnl() 
+#endif" ++ fnl2 ())
   ++
   (if not usf.mldummy then mt () 
-   else
-     str "__ = Prelude.error \"Logical or arity value used\"" 
-     ++ fnl () ++ fnl())
+   else str "__ = Prelude.error \"Logical or arity value used\"" ++ fnl2 ())
 
 let pp_abst = function
   | [] -> (mt ())
@@ -320,9 +313,11 @@ let pp_structure_elem = function
 
 let pp_struct = 
   let pp_sel (mp,sel) = 
-    push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+    push_visible mp; 
+    let p = prlist_strict pp_structure_elem sel in 
+    pop_visible (); p
   in 
-  prlist pp_sel 
+  prlist_strict pp_sel 
 
 
 let haskell_descr = {
diff --git a/contrib/extraction/ocaml.ml b/contrib/extraction/ocaml.ml
index 7548c14874..3326544a1c 100644
--- a/contrib/extraction/ocaml.ml
+++ b/contrib/extraction/ocaml.ml
@@ -69,34 +69,21 @@ let keywords =
     "land"; "lor"; "lxor"; "lsl"; "lsr"; "asr" ; "unit" ; "_" ; "__" ] 
   Idset.empty
 
+let pp_open mp = str ("open "^ string_of_modfile mp ^"\n")
+
 let preamble _ used_modules usf = 
-  let pp_mp = function 
-    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
-    | _ -> assert false 
-  in 
-  prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules
-  ++ 
-  (if used_modules = [] then mt () else fnl ())
-  ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() else mt())
-  ++
+  prlist pp_open used_modules ++
+  (if used_modules = [] then mt () else fnl ()) ++
+  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n" else mt()) ++
   (if usf.mldummy then 
-     str "let __ = let rec f _ = Obj.repr f in Obj.repr f" ++ fnl ()
-   else mt ()) 
-  ++ 
+     str "let __ = let rec f _ = Obj.repr f in Obj.repr f\n"
+   else mt ()) ++
   (if usf.tdummy || usf.tunknown || usf.mldummy then fnl () else mt ())
 
 let sig_preamble _ used_modules usf =
-  let pp_mp = function 
-    | MPfile d -> pr_upper_id (List.hd (repr_dirpath d))
-    | _ -> assert false 
-  in 
-  prlist (fun mp -> str "open " ++ pp_mp mp ++ fnl ()) used_modules
-  ++ 
-  (if used_modules = [] then mt () else fnl ())
-  ++
-  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t" ++ fnl() ++ fnl () 
-   else mt()) 
+  prlist pp_open used_modules ++
+  (if used_modules = [] then mt () else fnl ()) ++
+  (if usf.tdummy || usf.tunknown then str "type __ = Obj.t\n\n" else mt())
 
 (*s The pretty-printer for Ocaml syntax*)
 
@@ -648,7 +635,8 @@ let pp_struct s =
     let p = pp_structure_elem s ++ fnl2 () in 
     pop_visible (); p
   in
-  prlist (fun (mp,sel) -> prlist identity (map_succeed (pp mp) sel)) s
+  prlist_strict 
+    (fun (mp,sel) -> prlist_strict identity (map_succeed (pp mp) sel)) s
 
 let pp_signature s = 
   let pp mp s = 
@@ -656,7 +644,8 @@ let pp_signature s =
     let p = pp_specif s ++ fnl2 () in 
     pop_visible (); p
   in 
-  prlist (fun (mp,sign) -> prlist identity (map_succeed (pp mp) sign)) s
+  prlist_strict
+    (fun (mp,sign) -> prlist_strict identity (map_succeed (pp mp) sign)) s
 
 let pp_decl d = 
   try pp_decl d with Failure "empty phrase" -> mt ()
diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml
index 5048002d07..b6724f584d 100644
--- a/contrib/extraction/scheme.ml
+++ b/contrib/extraction/scheme.ml
@@ -30,16 +30,10 @@ let keywords =
     Idset.empty
 
 let preamble _ _ usf = 
-  str ";; This extracted scheme code relies on some additional macros" ++ 
-  fnl () ++
-  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme" ++
-  fnl () ++
-  str "(load \"macros_extr.scm\")" ++
-  fnl () ++ fnl () ++
-  (if usf.mldummy then 
-     str "(define __ (lambda (_) __))" 
-     ++ fnl () ++ fnl()
-   else mt ())
+  str ";; This extracted scheme code relies on some additional macros\n" ++ 
+  str ";; available at http://www.pps.jussieu.fr/~letouzey/scheme\n" ++
+  str "(load \"macros_extr.scm\")\n\n" ++
+  (if usf.mldummy then str "(define __ (lambda (_) __))\n\n" else mt ())
 
 let pr_id id = 
   let s = string_of_id id in
@@ -60,7 +54,7 @@ let pp_apply st _ = function
   | [] -> st 
   | [a] -> hov 2 (paren (st ++ spc () ++ a))
   | args -> hov 2 (paren (str "@ " ++ st ++ 
-			  (prlist (fun x -> spc () ++ x) args))) 
+			  (prlist_strict (fun x -> spc () ++ x) args)))
 
 (*s The pretty-printer for Scheme syntax *)
 
@@ -189,9 +183,11 @@ let pp_structure_elem = function
 
 let pp_struct = 
   let pp_sel (mp,sel) = 
-    push_visible mp; let p = prlist pp_structure_elem sel in pop_visible (); p
+    push_visible mp; 
+    let p = prlist_strict pp_structure_elem sel in 
+    pop_visible (); p
   in
-  prlist pp_sel
+  prlist_strict pp_sel
 
 let scheme_descr = {
   keywords = keywords;  
diff --git a/lib/util.ml b/lib/util.ml
index fa21cd83ed..3b5c90b020 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -857,6 +857,13 @@ let rec prlist elem l = match l with
   | []   -> mt ()
   | h::t -> Stream.lapp (fun () -> elem h) (prlist elem t)
 
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+
+let rec prlist_strict elem l = match l with 
+  | []   -> mt ()
+  | h::t -> (elem h)++(prlist_strict elem t)
+
 let rec prlist_with_sep sep elem l = match l with
   | []   -> mt ()
   | [h]  -> elem h
diff --git a/lib/util.mli b/lib/util.mli
index 6d6d9c2a85..5e89788b9b 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -255,6 +255,9 @@ val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 val nth : int -> std_ppcmds
 
 val prlist : ('a -> std_ppcmds) -> 'a list -> std_ppcmds
+(* unlike all other functions below, [prlist] works lazily.
+   if a strict behavior is needed, use [prlist_strict] instead. *)
+val prlist_strict :  ('a -> std_ppcmds) -> 'a list -> std_ppcmds
 val prlist_with_sep :
    (unit -> std_ppcmds) -> ('b -> std_ppcmds) -> 'b list -> std_ppcmds
 val prvect : ('a -> std_ppcmds) -> 'a array -> std_ppcmds