src/Tools/cache_io.ML
author wenzelm
Mon Mar 12 11:17:59 2018 +0100 (18 months ago)
changeset 67835 c8e4ee2b5482
parent 62549 9498623b27f0
permissions -rw-r--r--
tuned imports;
     1 (*  Title:      Tools/cache_io.ML
     2     Author:     Sascha Boehme, TU Muenchen
     3 
     4 Cache for output of external processes.
     5 *)
     6 
     7 signature CACHE_IO =
     8 sig
     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
    24 end
    25 
    26 structure Cache_IO : CACHE_IO =
    27 struct
    28 
    29 (* IO wrapper *)
    30 
    31 val cache_io_prefix = "cache-io-"
    32 
    33 type result = {
    34   output: string list,
    35   redirected_output: string list,
    36   return_code: int}
    37 
    38 fun 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 
    45 fun 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 
    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 
    60 fun 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 
    87 fun 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 
   105 fun 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 
   119 fun 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 
   124 end
   125 
   126 end