src/Pure/Concurrent/cache.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32840 75dff0bd4d5d
child 65046 18f3d341f8c0
permissions -rw-r--r--
map_range (and map_index) combinator
wenzelm@32840
     1
(*  Title:      Pure/Concurrent/cache.ML
wenzelm@32840
     2
    Author:     Makarius
wenzelm@32840
     3
wenzelm@32840
     4
Concurrently cached values, with minimal locking time and singleton
wenzelm@32840
     5
evaluation due to lazy storage.
wenzelm@32840
     6
*)
wenzelm@32840
     7
wenzelm@32840
     8
signature CACHE =
wenzelm@32840
     9
sig
wenzelm@32840
    10
  val create: 'table -> ('table -> 'key -> 'value lazy option) ->
wenzelm@32840
    11
    ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value
wenzelm@32840
    12
end;
wenzelm@32840
    13
wenzelm@32840
    14
structure Cache: CACHE =
wenzelm@32840
    15
struct
wenzelm@32840
    16
wenzelm@32840
    17
fun create empty lookup update f =
wenzelm@32840
    18
  let
wenzelm@32840
    19
    val cache = Synchronized.var "cache" empty;
wenzelm@32840
    20
    fun apply x =
wenzelm@32840
    21
      Synchronized.change_result cache
wenzelm@32840
    22
        (fn tab =>
wenzelm@32840
    23
          (case lookup tab x of
wenzelm@32840
    24
            SOME y => (y, tab)
wenzelm@32840
    25
          | NONE =>
wenzelm@32840
    26
              let val y = Lazy.lazy (fn () => f x)
wenzelm@32840
    27
              in (y, update (x, y) tab) end))
wenzelm@32840
    28
      |> Lazy.force;
wenzelm@32840
    29
  in apply end;
wenzelm@32840
    30
wenzelm@32840
    31
end;
wenzelm@32840
    32