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 --- contrib/extraction/scheme.ml | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) (limited to 'contrib/extraction/scheme.ml') diff --git a/contrib/extraction/scheme.ml b/contrib/extraction/scheme.ml index 5048002d0..b6724f584 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; -- cgit v1.2.3