1(* Title: Tools/cache_io.ML 2 Author: Sascha Boehme, TU Muenchen 3 4Cache for output of external processes. 5*) 6 7signature CACHE_IO = 8sig 9 (*IO wrapper*) 10 type result = { 11 output: string list, 12 redirected_output: string list, 13 return_code: int} 14 val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result 15 val run: (Path.T -> Path.T -> string) -> string -> result 16 17 (*cache*) 18 type cache 19 val unsynchronized_init: Path.T -> cache 20 val cache_path_of: cache -> Path.T 21 val lookup: cache -> string -> result option * string 22 val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result 23 val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result 24end 25 26structure Cache_IO : CACHE_IO = 27struct 28 29(* IO wrapper *) 30 31val cache_io_prefix = "cache-io-" 32 33type result = { 34 output: string list, 35 redirected_output: string list, 36 return_code: int} 37 38fun raw_run make_cmd str in_path out_path = 39 let 40 val _ = File.write in_path str 41 val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path) 42 val out1 = the_default [] (try (rev o File.fold_lines cons out_path) []) 43 in {output = split_lines out2, redirected_output = out1, return_code = rc} end 44 45fun run make_cmd str = 46 Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path => 47 Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path => 48 raw_run make_cmd str in_path out_path)) 49 50 51(* cache *) 52 53abstype cache = Cache of { 54 path: Path.T, 55 table: (int * (int * int * int) Symtab.table) Synchronized.var } 56with 57 58fun cache_path_of (Cache {path, ...}) = path 59 60fun unsynchronized_init cache_path = 61 let 62 val table = 63 if File.exists cache_path then 64 let 65 fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path) 66 67 fun int_of_string s = 68 (case read_int (raw_explode s) of 69 (i, []) => i 70 | _ => err ()) 71 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 ()) 76 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 86 87fun lookup (Cache {path = cache_path, table}) str = 88 let val key = SHA1.rep (SHA1.digest str) 89 in 90 Synchronized.change_result table (fn tab => 91 (case Symtab.lookup (snd tab) key of 92 NONE => ((NONE, key), tab) 93 | SOME (p, len1, len2) => 94 let 95 fun load line (i, xsp) = 96 if i < p then (i+1, xsp) 97 else if i < p + len1 then (i+1, apfst (cons line) xsp) 98 else if i < p + len2 then (i+1, apsnd (cons line) xsp) 99 else (i, xsp) 100 val (out, err) = 101 apply2 rev (snd (File.fold_lines load cache_path (1, ([], [])))) 102 in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end)) 103 end 104 105fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str = 106 let 107 val {output = err, redirected_output=out, return_code} = run make_cmd str 108 val (l1, l2) = apply2 length (out, err) 109 val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2 110 val lines = map (suffix "\n") (header :: out @ err) 111 112 val _ = Synchronized.change table (fn (p, tab) => 113 if Symtab.defined tab key then (p, tab) 114 else 115 let val _ = File.append_list cache_path lines 116 in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end) 117 in {output = err, redirected_output = out, return_code = return_code} end 118 119fun run_cached cache make_cmd str = 120 (case lookup cache str of 121 (NONE, key) => run_and_cache cache key make_cmd str 122 | (SOME output, _) => output) 123 124end 125 126end 127