Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: intprover.ML Sprache: SML

Original von: Isabelle^©

(*  Title:      Tools/cache_io.ML
    Author:     Sascha Boehme, TU Muenchen

Cache for output of external processes.
*)

signature CACHE_IO =
sig
  (*IO wrapper*)
  type result = {
    output: string list,
    redirected_output: string list,
    return_code: int}
  val raw_run: (Path.T -> Path.T -> string) -> string -> Path.T -> Path.T -> result
  val run: (Path.T -> Path.T -> string) -> string -> result

  (*cache*)
  type cache
  val unsynchronized_init: Path.T -> cache
  val cache_path_of: cache -> Path.T
  val lookup: cache -> string -> result option * string
  val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
  val run_cached: cache -> (Path.T -> Path.T -> string) -> string -> result
end

structure Cache_IO : CACHE_IO =
struct

(* IO wrapper *)

val cache_io_prefix = "cache-io-"

type result = {
  output: string list,
  redirected_output: string list,
  return_code: int}

fun raw_run make_cmd str in_path out_path =
  let
    val _ = File.write in_path str
    val (out2, rc) = Isabelle_System.bash_output (make_cmd in_path out_path)
    val out1 = the_default [] (try (rev o File.fold_lines cons out_path) [])
  in {output = split_lines out2, redirected_output = out1, return_code = rc} end

fun run make_cmd str =
  Isabelle_System.with_tmp_file cache_io_prefix "" (fn in_path =>
    Isabelle_System.with_tmp_file cache_io_prefix "" (fn out_path =>
      raw_run make_cmd str in_path out_path))

(* cache *)

abstype cache = Cache of {
  path: Path.T,
  table: (int * (int * int * int) Symtab.table) Synchronized.var }
with

fun cache_path_of (Cache {path, ...}) = path

fun unsynchronized_init cache_path =
  let
    val table =
      if File.exists cache_path then
        let
          fun err () = error ("Cache IO: corrupted cache file: " ^ File.bash_path cache_path)

          fun int_of_string s =
            (case read_int (raw_explode s) of
              (i, []) => i
            | _ => err ())

          fun split line =
            (case space_explode " " line of
              [key, len1, len2] => (key, int_of_string len1, int_of_string len2)
            | _ => err ())

          fun parse line ((i, l), tab) =
            if i = l
            then
              let val (key, l1, l2) = split line
              in ((i+1, l+l1+l2+1), Symtab.update (key, (i+1, l1, l2)) tab) end
            else ((i+1, l), tab)
        in apfst fst (File.fold_lines parse cache_path ((1, 1), Symtab.empty)) end
      else (1, Symtab.empty)
  in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end

fun lookup (Cache {path = cache_path, table}) str =
  let val key = SHA1.rep (SHA1.digest str)
  in
    Synchronized.change_result table (fn tab =>
      (case Symtab.lookup (snd tab) key of
        NONE => ((NONE, key), tab)
      | SOME (p, len1, len2) =>
          let
            fun load line (i, xsp) =
              if i < p then (i+1, xsp)
              else if i < p + len1 then (i+1, apfst (cons line) xsp)
              else if i < p + len2 then (i+1, apsnd (cons line) xsp)
              else (i, xsp)
            val (out, err) =
              apply2 rev (snd (File.fold_lines load cache_path (1, ([], []))))
          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
  end

fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =
  let
    val {output = err, redirected_output=out, return_code} = run make_cmd str
    val (l1, l2) = apply2 length (out, err)
    val header = key ^ " " ^ string_of_int l1 ^ " " ^ string_of_int l2
    val lines = map (suffix "\n") (header :: out @ err)

    val _ = Synchronized.change table (fn (p, tab) =>
      if Symtab.defined tab key then (p, tab)
      else
        let val _ = File.append_list cache_path lines
        in (p+l1+l2+1, Symtab.update (key, (p+1, l1, l2)) tab) end)
  in {output = err, redirected_output = out, return_code = return_code} end

fun run_cached cache make_cmd str =
  (case lookup cache str of
    (NONE, key) => run_and_cache cache key make_cmd str
  | (SOME output, _) => output)

end

end

¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.