1 (* Title: Tools/cache_io.ML
2 Author: Sascha Boehme, TU Muenchen
4 Cache for output of external processes.
9 val with_tmp_file: string -> (Path.T -> 'a) -> 'a
10 val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
11 val run: (Path.T -> Path.T -> string) -> string -> string list * string list
14 val make: Path.T -> cache
15 val cache_path_of: cache -> Path.T
16 val lookup: cache -> string -> (string list * string list) option * string
17 val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
18 string -> string list * string list
19 val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
20 string list * string list
23 structure Cache_IO : CACHE_IO =
26 val cache_io_prefix = "cache-io-"
28 fun with_tmp_file name f =
30 val path = File.tmp_path (Path.explode (name ^ serial_string ()))
31 val x = Exn.capture f path
32 val _ = try File.rm path
35 fun with_tmp_dir name f =
37 val path = File.tmp_path (Path.explode (name ^ serial_string ()))
38 val _ = File.mkdir path
39 val x = Exn.capture f path
40 val _ = try File.rm_tree path
43 fun run make_cmd str =
44 with_tmp_file cache_io_prefix (fn in_path =>
45 with_tmp_file cache_io_prefix (fn out_path =>
47 val _ = File.write in_path str
48 val (out2, _) = bash_output (make_cmd in_path out_path)
49 val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
50 in (out1, split_lines out2) end))
54 abstype cache = Cache of {
56 table: (int * (int * int * int) Symtab.table) Synchronized.var }
60 fun cache_path_of (Cache {path, ...}) = path
65 fun err () = error ("Cache IO: corrupted cache file: " ^
66 File.shell_path cache_path)
69 (case read_int (explode s) of
74 (case space_explode " " line of
75 [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
78 fun parse line ((i, l), tab) =
81 let val (key, l1, l2) = split line
82 in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
84 in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
87 let val table = if File.exists path then load path else (1, Symtab.empty)
88 in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
91 fun load_cached_result cache_path (p, len1, len2) =
93 fun load line (i, xsp) =
94 if i < p then (i+1, xsp)
95 else if i < p + len1 then (i+1, apfst (cons line) xsp)
96 else if i < p + len2 then (i+1, apsnd (cons line) xsp)
98 in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
101 fun lookup (Cache {path=cache_path, table}) str =
102 let val key = SHA1.digest str
104 (case Symtab.lookup (snd (Synchronized.value table)) key of
106 | SOME pos => (SOME (load_cached_result cache_path pos), key))
110 fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
112 val res as (out, err) = run make_cmd str
113 val (l1, l2) = pairself length res
114 val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
115 val lines = map (suffix "\n") (header :: out @ err)
117 val _ = Synchronized.change table (fn (p, tab) =>
118 if Symtab.defined tab key then (p, tab)
120 let val _ = File.append_list cache_path lines
121 in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
125 fun run_cached cache make_cmd str =
126 (case lookup cache str of
127 (NONE, key) => run_and_cache cache key make_cmd str
128 | (SOME output, _) => output)