buffered output (faster than direct output)

--- a/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_solver.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -106,22 +106,6 @@
 
 local
 
-fun invoke ctxt output f problem_path =
-  let
-    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
-      (map Pretty.str ls))
-
-    val x = File.open_output output problem_path
-    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines o File.read)
-      problem_path
-
-    val (res, err) = with_timeout ctxt f problem_path
-    val _ = trace_msg ctxt (pretty "SMT solver:") err
-
-    val ls = rev (dropwhile (equal "") (rev res))
-    val _ = trace_msg ctxt (pretty "SMT result:") ls
-  in (x, ls) end
-
 fun choose {env_var, remote_name} =
   let
     val local_solver = getenv env_var
@@ -144,29 +128,40 @@
   map File.shell_quote (solver @ args) @
   [File.shell_path problem_path, "2>&1", ">", File.shell_path proof_path])
 
-fun no_cmd _ _ = error ("Bad certificates cache: missing certificate")
-
-fun run ctxt cmd args problem_path =
-  let val certs = Certificates.get (Context.Proof ctxt)
-  in
-    if is_none certs 
-    then Cache_IO.run' (make_cmd (choose cmd) args) problem_path
-    else if Config.get ctxt fixed_certificates
-    then Cache_IO.cached' (the certs) (make_cmd (choose cmd) args) problem_path
-    else
-     (tracing ("Using cached certificate from " ^
-        File.shell_path (Cache_IO.cache_path_of (the certs)) ^ " ...");
-      Cache_IO.cached' (the certs) no_cmd problem_path)
-  end
+fun run ctxt cmd args input =
+  (case Certificates.get (Context.Proof ctxt) of
+    NONE => Cache_IO.run (make_cmd (choose cmd) args) input
+  | SOME certs =>
+      (case Cache_IO.lookup certs input of
+        (NONE, key) =>
+          if Config.get ctxt fixed_certificates
+          then error ("Bad certificates cache: missing certificate")
+          else Cache_IO.run_and_cache certs key (make_cmd (choose cmd) args)
+            input
+      | (SOME output, _) =>
+         (tracing ("Using cached certificate from " ^
+            File.shell_path (Cache_IO.cache_path_of certs) ^ " ...");
+          output)))
 
 in
 
-fun run_solver ctxt cmd args output =
-  Cache_IO.with_tmp_file "smt-" (invoke ctxt output (run ctxt cmd args))
+fun run_solver ctxt cmd args input =
+  let
+    fun pretty tag ls = Pretty.string_of (Pretty.big_list tag
+      (map Pretty.str ls))
+
+    val _ = trace_msg ctxt (pretty "SMT problem:" o split_lines) input
+
+    val (res, err) = with_timeout ctxt (run ctxt cmd args) input
+    val _ = trace_msg ctxt (pretty "SMT solver:") err
+
+    val ls = rev (dropwhile (equal "") (rev res))
+    val _ = trace_msg ctxt (pretty "SMT result:") ls
+  in ls end
 
 end
 
-fun make_proof_data ctxt ((recon, thms), ls) =
+fun make_proof_data ctxt (ls, (recon, thms)) =
   {context=ctxt, output=ls, recon=recon, assms=SOME thms}
 
 fun gen_solver name solver ctxt prems =
@@ -179,7 +174,8 @@
     val thy = ProofContext.theory_of ctxt
   in
     SMT_Normalize.normalize ctxt prems
-    ||> run_solver ctxt command arguments o SMT_Translate.translate tc thy
+    ||> SMT_Translate.translate tc thy
+    ||> apfst (run_solver ctxt command arguments)
     ||> reconstruct o make_proof_data ctxt
     |-> fold SMT_Normalize.discharge_definition
   end

--- a/src/HOL/SMT/Tools/smt_translate.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smt_translate.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -55,11 +55,10 @@
     prefixes: prefixes,
     markers: markers,
     builtins: builtins,
-    serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+    serialize: sign -> (string, string) sterm list -> string}
   type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
-  val translate: config -> theory -> thm list -> TextIO.outstream ->
-    recon * thm list
+  val translate: config -> theory -> thm list -> string * (recon * thm list)
 
   val dest_binT: typ -> int
   val dest_funT: int -> typ -> typ list * typ
@@ -180,7 +179,7 @@
   prefixes: prefixes,
   markers: markers,
   builtins: builtins,
-  serialize: sign -> (string, string) sterm list -> TextIO.outstream -> unit}
+  serialize: sign -> (string, string) sterm list -> string}
 type recon = {typs: typ Symtab.table, terms: term Symtab.table}
 
 
@@ -527,7 +526,7 @@
 
 (* Combination of all translation functions and invocation of serialization. *)
 
-fun translate config thy thms stream =
+fun translate config thy thms =
   let val {strict, prefixes, markers, builtins, serialize} = config
   in
     map Thm.prop_of thms
@@ -535,8 +534,8 @@
     |> intermediate
     |> (if strict then separate thy else pair [])
     ||>> signature_of prefixes markers builtins thy
-    ||> (fn (sgn, ts) => serialize sgn ts stream)
-    |> (fn ((thms', rtab), _) => (rtab, thms' @ thms))
+    ||> (fn (sgn, ts) => serialize sgn ts)
+    |> (fn ((thms', rtab), str) => (str, (rtab, thms' @ thms)))
   end
 
 end

--- a/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
+++ b/src/HOL/SMT/Tools/smtlib_interface.ML	Wed Apr 07 20:40:42 2010 +0200
@@ -61,7 +61,7 @@
 
 (* serialization *)
 
-fun wr s stream = (TextIO.output (stream, s); stream)
+val wr = Buffer.add
 fun wr_line f = f #> wr "\n"
 
 fun sep f = wr " " #> f
@@ -118,11 +118,10 @@
           | wr_pat (T.SNoPat ts) = wrp "nopat" ts
       in par (wr_quant q #> fold wr_var vs #> wre b #> fold wr_pat ps) end)
 
-fun serialize attributes comments ({typs, funs, preds} : T.sign) ts stream =
-  let
-    fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
+fun serialize attributes comments ({typs, funs, preds} : T.sign) ts =
+  let fun wr_decl (n, Ts) = wr_line (sep (par (wr n #> fold wr1 Ts)))
   in
-    stream
+    Buffer.empty
     |> wr_line (wr "(benchmark Isabelle")
     |> wr_line (wr ":status unknown")
     |> fold (wr_line o wr) attributes
@@ -140,7 +139,7 @@
     |> wr_line (wr ":formula true")
     |> wr_line (wr ")")
     |> fold (fn comment => wr_line (wr ("; " ^ comment))) comments
-    |> K ()
+    |> Buffer.content
   end