src/Pure/Concurrent/cache.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/cache.ML	Thu Oct 01 22:39:06 2009 +0200
@@ -0,0 +1,32 @@
+(*  Title:      Pure/Concurrent/cache.ML
+    Author:     Makarius
+
+Concurrently cached values, with minimal locking time and singleton
+evaluation due to lazy storage.
+*)
+
+signature CACHE =
+sig
+  val create: 'table -> ('table -> 'key -> 'value lazy option) ->
+    ('key * 'value lazy -> 'table -> 'table) -> ('key -> 'value) -> 'key -> 'value
+end;
+
+structure Cache: CACHE =
+struct
+
+fun create empty lookup update f =
+  let
+    val cache = Synchronized.var "cache" empty;
+    fun apply x =
+      Synchronized.change_result cache
+        (fn tab =>
+          (case lookup tab x of
+            SOME y => (y, tab)
+          | NONE =>
+              let val y = Lazy.lazy (fn () => f x)
+              in (y, update (x, y) tab) end))
+      |> Lazy.force;
+  in apply end;
+
+end;
+