simplified Cache_IO interface (input is just a string and not already stored in a file)
--- a/src/Tools/cache_io.ML Wed Apr 07 20:40:42 2010 +0200
+++ b/src/Tools/cache_io.ML Wed Apr 07 20:40:42 2010 +0200
@@ -7,20 +7,23 @@
signature CACHE_IO =
sig
val with_tmp_file: string -> (Path.T -> 'a) -> 'a
- val run: (Path.T -> string) -> Path.T -> string list
- val run': (Path.T -> Path.T -> string) -> Path.T -> string list * string list
+ val run: (Path.T -> Path.T -> string) -> string -> string list * string list
type cache
val make: Path.T -> cache
val cache_path_of: cache -> Path.T
- val cached: cache -> (Path.T -> string) -> Path.T -> string list
- val cached': cache -> (Path.T -> Path.T -> string) -> Path.T ->
+ val lookup: cache -> string -> (string list * string list) option * string
+ val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
+ string -> string list * string list
+ val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
string list * string list
end
structure Cache_IO : CACHE_IO =
struct
+val cache_io_prefix = "cache-io-"
+
fun with_tmp_file name f =
let
val path = File.tmp_path (Path.explode (name ^ serial_string ()))
@@ -28,14 +31,14 @@
val _ = try File.rm path
in Exn.release x end
-fun run' make_cmd in_path =
- with_tmp_file "cache-io-" (fn out_path =>
+fun run make_cmd str =
+ with_tmp_file cache_io_prefix (fn in_path =>
+ with_tmp_file cache_io_prefix (fn out_path =>
let
+ val _ = File.write in_path str
val (out2, _) = bash_output (make_cmd in_path out_path)
val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
- in (out1, split_lines out2) end)
-
-fun run make_cmd = snd o run' (fn in_path => fn _ => make_cmd in_path)
+ in (out1, split_lines out2) end))
@@ -85,28 +88,35 @@
else (i, xsp)
in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
-fun cached' (Cache {path=cache_path, table}) make_cmd in_path =
- let val key = SHA1.digest (File.read in_path)
+
+fun lookup (Cache {path=cache_path, table}) str =
+ let val key = SHA1.digest str
in
(case Symtab.lookup (snd (Synchronized.value table)) key of
- SOME pos => load_cached_result cache_path pos
- | NONE =>
- let
- val res as (out, err) = run' make_cmd in_path
- val (l1, l2) = pairself length res
- val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
- val lines = map (suffix "\n") (header :: out @ err)
-
- val _ = Synchronized.change table (fn (p, tab) =>
- if Symtab.defined tab key then (p, tab)
- else
- let val _ = File.append_list cache_path lines
- in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
- in res end)
+ NONE => (NONE, key)
+ | SOME pos => (SOME (load_cached_result cache_path pos), key))
end
-fun cached cache make_cmd =
- snd o cached' cache (fn in_path => fn _ => make_cmd in_path)
+
+fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
+ let
+ val res as (out, err) = run make_cmd str
+ val (l1, l2) = pairself length res
+ val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
+ val lines = map (suffix "\n") (header :: out @ err)
+
+ val _ = Synchronized.change table (fn (p, tab) =>
+ if Symtab.defined tab key then (p, tab)
+ else
+ let val _ = File.append_list cache_path lines
+ in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
+ in res end
+
+
+fun run_cached cache make_cmd str =
+ (case lookup cache str of
+ (NONE, key) => run_and_cache cache key make_cmd str
+ | (SOME output, _) => output)
end
end