src/Tools/cache_io.ML
author wenzelm
Thu Sep 02 00:48:07 2010 +0200 (2010-09-02)
changeset 38980 af73cf0dc31f
parent 37740 9bb4a74cff4e
child 40425 c9b5e0fcee31
permissions -rw-r--r--
turned show_question_marks into proper configuration option;
show_question_marks only affects regular type/term pretty printing, not raw Term.string_of_vname;
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   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
    12 
    13   type cache
    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
    21 end
    22 
    23 structure Cache_IO : CACHE_IO =
    24 struct
    25 
    26 val cache_io_prefix = "cache-io-"
    27 
    28 fun with_tmp_file name f =
    29   let
    30     val path = File.tmp_path (Path.explode (name ^ serial_string ()))
    31     val x = Exn.capture f path
    32     val _ = try File.rm path
    33   in Exn.release x end
    34 
    35 fun with_tmp_dir name f =
    36   let
    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
    41   in Exn.release x end
    42 
    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 =>
    46     let
    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))
    51 
    52 
    53 
    54 abstype cache = Cache of {
    55   path: Path.T,
    56   table: (int * (int * int * int) Symtab.table) Synchronized.var }
    57 with
    58 
    59 
    60 fun cache_path_of (Cache {path, ...}) = path
    61 
    62 
    63 fun load cache_path =
    64   let
    65     fun err () = error ("Cache IO: corrupted cache file: " ^
    66       File.shell_path cache_path)
    67 
    68     fun int_of_string s =
    69       (case read_int (explode s) of
    70         (i, []) => i
    71       | _ => err ())    
    72 
    73     fun split line =
    74       (case space_explode " " line of
    75         [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
    76       | _ => err ())
    77 
    78     fun parse line ((i, l), tab) =
    79       if i = l
    80       then
    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
    83       else ((i+1, l), tab)
    84   in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end 
    85 
    86 fun make path =
    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
    89 
    90 
    91 fun load_cached_result cache_path (p, len1, len2) =
    92   let
    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)
    97       else (i, xsp)
    98   in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
    99 
   100 
   101 fun lookup (Cache {path=cache_path, table}) str =
   102   let val key = SHA1.digest str
   103   in
   104     (case Symtab.lookup (snd (Synchronized.value table)) key of
   105       NONE => (NONE, key)
   106     | SOME pos => (SOME (load_cached_result cache_path pos), key))
   107   end
   108 
   109 
   110 fun run_and_cache (Cache {path=cache_path, table}) key make_cmd str =
   111   let
   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)
   116 
   117     val _ = Synchronized.change table (fn (p, tab) =>
   118       if Symtab.defined tab key then (p, tab)
   119       else
   120         let val _ = File.append_list cache_path lines
   121         in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
   122   in res end
   123 
   124 
   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)
   129 
   130 end
   131 end