32840
|
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 |
|