diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-17 23:29:08 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2007-10-17 23:29:08 +0000 |
| commit | e82372fe9b5c1a9c56a605c582d4365e6bfcd593 (patch) | |
| tree | e90a8d1ff76d5349dc01fbe683bd1d999feb85fb /lib | |
| parent | 350398eaea679b2bf66c93e9ac5e0308349bc959 (diff) | |
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
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/util.ml | 7 | ||||
| -rw-r--r-- | lib/util.mli | 3 |
2 files changed, 10 insertions, 0 deletions
diff --git a/lib/util.ml b/lib/util.ml index fa21cd83e..3b5c90b02 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 6d6d9c2a8..5e89788b9 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 |