src/Tools/cache_io.ML
author wenzelm
Mon Dec 20 14:44:00 2010 +0100 (2010-12-20)
changeset 41307 bb8468ae414e
parent 40743 b07a0dbc8a38
child 41945 8e32c3992cb3
permissions -rw-r--r--
slightly more standard Isabelle_System.with_tmp_file/with_tmp_dir (cf. Scala version);
more robust rm_tree -- somewhat dangerous and not exported;
tuned;
     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 ->
    15     result
    16   val run: (Path.T -> Path.T -> string) -> string -> result
    17 
    18   (*cache*)
    19   type cache
    20   val make: Path.T -> cache
    21   val cache_path_of: cache -> Path.T
    22   val lookup: cache -> string -> result option * string
    23   val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
    24     string -> result
    25   val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
    26 end
    27 
    28 structure Cache_IO : CACHE_IO =
    29 struct
    30 
    31 (* IO wrapper *)
    32 
    33 val cache_io_prefix = "cache-io-"
    34 
    35 type result = {
    36   output: string list,
    37   redirected_output: string list,
    38   return_code: int}
    39 
    40 fun raw_run make_cmd str in_path out_path =
    41   let
    42     val _ = File.write in_path str
    43     val (out2, rc) = bash_output (make_cmd in_path out_path)
    44     val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
    45   in {output=split_lines out2, redirected_output=out1, return_code=rc} end
    46 
    47 fun run make_cmd str =
    48   Isabelle_System.with_tmp_file cache_io_prefix (fn in_path =>
    49     Isabelle_System.with_tmp_file cache_io_prefix (fn out_path =>
    50       raw_run make_cmd str in_path out_path))
    51 
    52 
    53 (* cache *)
    54 
    55 abstype cache = Cache of {
    56   path: Path.T,
    57   table: (int * (int * int * int) Symtab.table) Synchronized.var }
    58 with
    59 
    60 fun cache_path_of (Cache {path, ...}) = path
    61 
    62 fun load cache_path =
    63   let
    64     fun err () = error ("Cache IO: corrupted cache file: " ^
    65       File.shell_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 
    85 fun make path =
    86   let val table = if File.exists path then load path else (1, Symtab.empty)
    87   in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
    88 
    89 fun load_cached_result cache_path (p, len1, len2) =
    90   let
    91     fun load line (i, xsp) =
    92       if i < p then (i+1, xsp)
    93       else if i < p + len1 then (i+1, apfst (cons line) xsp)
    94       else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    95       else (i, xsp)
    96     val (out, err) =
    97       pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
    98   in {output=err, redirected_output=out, return_code=0} end
    99 
   100 fun lookup (Cache {path=cache_path, table}) str =
   101   let val key = SHA1.digest str
   102   in
   103     (case Symtab.lookup (snd (Synchronized.value table)) key of
   104       NONE => (NONE, key)
   105     | SOME pos => (SOME (load_cached_result cache_path pos), key))
   106   end
   107 
   108 fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
   109   let
   110     val {output=err, redirected_output=out, return_code} = run make_cmd str
   111     val (l1, l2) = pairself length (out, err)
   112     val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
   113     val lines = map (suffix "\n") (header :: out @ err)
   114 
   115     val _ = Synchronized.change table (fn (p, tab) =>
   116       if Symtab.defined tab key then (p, tab)
   117       else
   118         let val _ = File.append_list cache_path lines
   119         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   120   in {output=err, redirected_output=out, return_code=return_code} end
   121 
   122 fun run_cached cache make_cmd str =
   123   (case lookup cache str of
   124     (NONE, key) => run_and_cache cache key make_cmd str
   125   | (SOME output, _) => output)
   126 
   127 end
   128 
   129 end