src/Pure/Concurrent/cache.ML
author hoelzl
Wed, 02 Apr 2014 18:35:01 +0200
changeset 56369 2704ca85be98
parent 32840 75dff0bd4d5d
child 65046 18f3d341f8c0
permissions -rw-r--r--
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32840
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/Concurrent/cache.ML
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     3
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     4
Concurrently cached values, with minimal locking time and singleton
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     5
evaluation due to lazy storage.
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     6
*)
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     7
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     8
signature CACHE =
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
     9
sig
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    10
  val create: 'table -> ('table -> 'key -> 'value lazy option) ->
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    11
    ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    12
end;
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    13
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    14
structure Cache: CACHE =
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    15
struct
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    16
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    17
fun create empty lookup update f =
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    18
  let
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    19
    val cache = Synchronized.var "cache" empty;
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    20
    fun apply x =
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    21
      Synchronized.change_result cache
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    22
        (fn tab =>
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    23
          (case lookup tab x of
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    24
            SOME y => (y, tab)
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    25
          | NONE =>
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    26
              let val y = Lazy.lazy (fn () => f x)
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    27
              in (y, update (x, y) tab) end))
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    28
      |> Lazy.force;
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    29
  in apply end;
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    30
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    31
end;
75dff0bd4d5d Concurrently cached values.
wenzelm
parents:
diff changeset
    32