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
     1 (*  Title:      Pure/Concurrent/cache.ML
     2     Author:     Makarius
     3 
     4 Concurrently cached values, with minimal locking time and singleton
     5 evaluation due to lazy storage.
     6 *)
     7 
     8 signature CACHE =
     9 sig
    10   val create: 'table -> ('table -> 'key -> 'value lazy option) ->
    11     ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value
    12 end;
    13 
    14 structure Cache: CACHE =
    15 struct
    16 
    17 fun create empty lookup update f =
    18   let
    19     val cache = Synchronized.var "cache" empty;
    20     fun apply x =
    21       Synchronized.change_result cache
    22         (fn tab =>
    23           (case lookup tab x of
    24             SOME y => (y, tab)
    25           | NONE =>
    26               let val y = Lazy.lazy (fn () => f x)
    27               in (y, update (x, y) tab) end))
    28       |> Lazy.force;
    29   in apply end;
    30 
    31 end;
    32