From e82372fe9b5c1a9c56a605c582d4365e6bfcd593 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Wed, 17 Oct 2007 23:29:08 +0000
Subject: 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
---
 lib/util.ml  | 7 +++++++
 lib/util.mli | 3 +++
 2 files changed, 10 insertions(+)

(limited to 'lib')

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
-- 
cgit v1.2.3