author | wenzelm |
Mon, 03 Dec 2012 15:23:36 +0100 | |
changeset 50316 | 7bdc53fb7282 |
parent 43850 | 7f2cbc713344 |
child 50317 | 4d1590544b91 |
permissions | -rw-r--r-- |
35942
667fd8553cd5
use internal SHA1 digest implementation for generating hash keys
boehmes
parents:
35941
diff
changeset
|
1 |
(* Title: Tools/cache_io.ML |
35151 | 2 |
Author: Sascha Boehme, TU Muenchen |
3 |
||
4 |
Cache for output of external processes. |
|
5 |
*) |
|
6 |
||
7 |
signature CACHE_IO = |
|
8 |
sig |
|
40425
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
9 |
(*IO wrapper*) |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
10 |
type result = { |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
11 |
output: string list, |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
12 |
redirected_output: string list, |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
13 |
return_code: int} |
50316 | 14 |
val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
15 |
val run: (Path.T -> Path.T -> string) -> string -> result |
35151 | 16 |
|
40425
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
17 |
(*cache*) |
35151 | 18 |
type cache |
19 |
val make: Path.T -> cache |
|
20 |
val cache_path_of: cache -> Path.T |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
21 |
val lookup: cache -> string -> result option * string |
50316 | 22 |
val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
23 |
val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result |
35151 | 24 |
end |
25 |
||
26 |
structure Cache_IO : CACHE_IO = |
|
27 |
struct |
|
28 |
||
40425
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
29 |
(* IO wrapper *) |
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
30 |
|
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
31 |
val cache_io_prefix = "cache-io-" |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
32 |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
33 |
type result = { |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
34 |
output: string list, |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
35 |
redirected_output: string list, |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
36 |
return_code: int} |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
37 |
|
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40538
diff
changeset
|
38 |
fun raw_run make_cmd str in_path out_path = |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40538
diff
changeset
|
39 |
let |
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40538
diff
changeset
|
40 |
val _ = File.write in_path str |
43850
7f2cbc713344
moved bash operations to Isabelle_System (cf. Scala version);
wenzelm
parents:
42127
diff
changeset
|
41 |
val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path) |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40538
diff
changeset
|
42 |
val out1 = the_default [] (try (rev o File.fold_lines cons out_path) []) |
50316 | 43 |
in {output = split_lines out2, redirected_output = out1, return_code = rc} end |
40578
2b098a549450
keep input and output files used to communicate with the SMT solver (for debugging purposes mainly)
boehmes
parents:
40538
diff
changeset
|
44 |
|
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
45 |
fun run make_cmd str = |
42127
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41954
diff
changeset
|
46 |
Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path => |
8223e7f4b0da
Isabelle_System.create_tmp_path/with_tmp_file: optional extension;
wenzelm
parents:
41954
diff
changeset
|
47 |
Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path => |
41307
bb8468ae414e
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
wenzelm
parents:
40743
diff
changeset
|
48 |
raw_run make_cmd str in_path out_path)) |
35151 | 49 |
|
50 |
||
40425
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
51 |
(* cache *) |
35151 | 52 |
|
53 |
abstype cache = Cache of { |
|
54 |
path: Path.T, |
|
55 |
table: (int * (int * int * int) Symtab.table) Synchronized.var } |
|
56 |
with |
|
57 |
||
58 |
fun cache_path_of (Cache {path, ...}) = path |
|
59 |
||
50316 | 60 |
fun make cache_path = |
35151 | 61 |
let |
50316 | 62 |
val table = |
63 |
if File.exists cache_path then |
|
64 |
let |
|
65 |
fun err () = error ("Cache IO: corrupted cache file: " ^ File.shell_path cache_path) |
|
35151 | 66 |
|
50316 | 67 |
fun int_of_string s = |
68 |
(case read_int (raw_explode s) of |
|
69 |
(i, []) => i |
|
70 |
| _ => err ()) |
|
35151 | 71 |
|
50316 | 72 |
fun split line = |
73 |
(case space_explode " " line of |
|
74 |
[key, len1, len2] => (key, int_of_string len1, int_of_string len2) |
|
75 |
| _ => err ()) |
|
35151 | 76 |
|
50316 | 77 |
fun parse line ((i, l), tab) = |
78 |
if i = l |
|
79 |
then |
|
80 |
let val (key, l1, l2) = split line |
|
81 |
in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end |
|
82 |
else ((i+1, l), tab) |
|
83 |
in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end |
|
84 |
else (1, Symtab.empty) |
|
85 |
in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end |
|
35151 | 86 |
|
87 |
fun load_cached_result cache_path (p, len1, len2) = |
|
88 |
let |
|
89 |
fun load line (i, xsp) = |
|
90 |
if i < p then (i+1, xsp) |
|
91 |
else if i < p + len1 then (i+1, apfst (cons line) xsp) |
|
92 |
else if i < p + len2 then (i+1, apsnd (cons line) xsp) |
|
93 |
else (i, xsp) |
|
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
94 |
val (out, err) = |
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
95 |
pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) |
50316 | 96 |
in {output = err, redirected_output = out, return_code = 0} end |
35151 | 97 |
|
50316 | 98 |
fun lookup (Cache {path = cache_path, table}) str = |
41954 | 99 |
let val key = SHA1.rep (SHA1.digest str) |
35151 | 100 |
in |
101 |
(case Symtab.lookup (snd (Synchronized.value table)) key of |
|
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
102 |
NONE => (NONE, key) |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
103 |
| SOME pos => (SOME (load_cached_result cache_path pos), key)) |
35151 | 104 |
end |
105 |
||
50316 | 106 |
fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = |
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
107 |
let |
50316 | 108 |
val {output = err, redirected_output=out, return_code} = run make_cmd str |
40538
b8482ff0bc92
check the return code of the SMT solver and raise an exception if the prover failed
boehmes
parents:
40425
diff
changeset
|
109 |
val (l1, l2) = pairself length (out, err) |
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
110 |
val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
111 |
val lines = map (suffix "\n") (header :: out @ err) |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
112 |
|
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
113 |
val _ = Synchronized.change table (fn (p, tab) => |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
114 |
if Symtab.defined tab key then (p, tab) |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
115 |
else |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
116 |
let val _ = File.append_list cache_path lines |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
117 |
in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end) |
50316 | 118 |
in {output = err, redirected_output = out, return_code = return_code} end |
36086
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
119 |
|
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
120 |
fun run_cached cache make_cmd str = |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
121 |
(case lookup cache str of |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
122 |
(NONE, key) => run_and_cache cache key make_cmd str |
8e5454761f26
simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents:
35942
diff
changeset
|
123 |
| (SOME output, _) => output) |
35151 | 124 |
|
125 |
end |
|
40425
c9b5e0fcee31
return the process return code along with the process outputs
boehmes
parents:
37740
diff
changeset
|
126 |
|
35151 | 127 |
end |