src/Tools/cache_io.ML
author boehmes
Mon, 08 Nov 2010 12:13:51 +0100
changeset 40425 c9b5e0fcee31
parent 37740 9bb4a74cff4e
child 40538 b8482ff0bc92
permissions -rw-r--r--
return the process return code along with the process outputs
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
35942
667fd8553cd5 use internal SHA1 digest implementation for generating hash keys
boehmes
parents: 35941
diff changeset
     1
(*  Title:      Tools/cache_io.ML
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     2
    Author:     Sascha Boehme, TU Muenchen
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     3
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     4
Cache for output of external processes.
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     5
*)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     6
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     7
signature CACHE_IO =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
     8
sig
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
     9
  (*IO wrapper*)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    10
  val with_tmp_file: string -> (Path.T -> 'a) -> 'a
37740
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    11
  val with_tmp_dir: string -> (Path.T -> 'a) -> 'a
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    12
  val run: (Path.T -> Path.T -> string) -> string ->
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    13
    {output: string list, redirected_output: string list, return_code: int}
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    14
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    15
  (*cache*)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    16
  type cache
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    17
  val make: Path.T -> cache
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    18
  val cache_path_of: cache -> Path.T
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    19
  val lookup: cache -> string -> (string list * string list) option * string
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    20
  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) ->
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    21
    string -> string list * string list
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    22
  val run_cached: cache -> (Path.T -> Path.T -> string) -> string ->
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    23
    string list * string list
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    24
end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    25
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    26
structure Cache_IO : CACHE_IO =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    27
struct
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    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
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    33
fun with_tmp_file name f =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    34
  let
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    35
    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    36
    val x = Exn.capture f path
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    37
    val _ = try File.rm path
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    38
  in Exn.release x end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    39
37740
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    40
fun with_tmp_dir name f =
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    41
  let
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    42
    val path = File.tmp_path (Path.explode (name ^ serial_string ()))
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    43
    val _ = File.mkdir path
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    44
    val x = Exn.capture f path
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    45
    val _ = try File.rm_tree path
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    46
  in Exn.release x end
9bb4a74cff4e combinator with_tmp_dir
haftmann
parents: 36086
diff changeset
    47
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    48
fun run 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
    49
  with_tmp_file cache_io_prefix (fn in_path =>
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    50
  with_tmp_file cache_io_prefix (fn out_path =>
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    51
    let
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
    52
      val _ = File.write in_path str
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    53
      val (out2, rc) = bash_output (make_cmd in_path out_path)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    54
      val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    55
    in {output=split_lines out2, redirected_output=out1, return_code=rc} end))
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    56
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    57
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
    58
(* cache *)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    59
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    60
abstype cache = Cache of {
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    61
  path: Path.T,
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    62
  table: (int * (int * int * int) Symtab.table) Synchronized.var }
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    63
with
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    64
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    65
fun cache_path_of (Cache {path, ...}) = path
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    66
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    67
fun load cache_path =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    68
  let
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    69
    fun err () = error ("Cache IO: corrupted cache file: " ^
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    70
      File.shell_path cache_path)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    71
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    72
    fun int_of_string s =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    73
      (case read_int (explode s) of
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    74
        (i, []) => i
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    75
      | _ => err ())    
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    76
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    77
    fun split line =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    78
      (case space_explode " " line of
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    79
        [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    80
      | _ => err ())
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    81
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    82
    fun parse line ((i, l), tab) =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    83
      if i = l
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    84
      then
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    85
        let val (key, l1, l2) = split line
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    86
        in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    87
      else ((i+1, l), tab)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    88
  in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end 
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    89
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    90
fun make path =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    91
  let val table = if File.exists path then load path else (1, Symtab.empty)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    92
  in Cache {path=path, table=Synchronized.var (Path.implode path) table} end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    93
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    94
fun load_cached_result cache_path (p, len1, len2) =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    95
  let
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    96
    fun load line (i, xsp) =
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    97
      if i < p then (i+1, xsp)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    98
      else if i < p + len1 then (i+1, apfst (cons line) xsp)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
    99
      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   100
      else (i, xsp)
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   101
  in pairself rev (snd (File.fold_lines load cache_path (1, ([], [])))) end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   102
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   103
fun lookup (Cache {path=cache_path, table}) str =
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   104
  let val key = SHA1.digest str
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   105
  in
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   106
    (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
   107
      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
   108
    | SOME pos => (SOME (load_cached_result cache_path pos), key))
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   109
  end
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   110
36086
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   111
fun run_and_cache (Cache {path=cache_path, table}) 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
   112
  let
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
   113
    val {output=err, redirected_output=out, ...} = run make_cmd str
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
   114
    val res = (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
   115
    val (l1, l2) = pairself length res
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   116
    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
   117
    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
   118
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   119
    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
   120
      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
   121
      else
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   122
        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
   123
        in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   124
  in res end
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   125
8e5454761f26 simplified Cache_IO interface (input is just a string and not already stored in a file)
boehmes
parents: 35942
diff changeset
   126
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
   127
  (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
   128
    (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
   129
  | (SOME output, _) => output)
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   130
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   131
end
40425
c9b5e0fcee31 return the process return code along with the process outputs
boehmes
parents: 37740
diff changeset
   132
35151
117247018b54 added Cache_IO: cache for output of external tools,
boehmes
parents:
diff changeset
   133
end