src/Pure/Concurrent/lazy.ML
changeset 32815 1a5e364584ae
parent 32738 15bb09ca0378
child 33023 207c21697a48
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy.ML	Thu Oct 01 18:10:41 2009 +0200
@@ -0,0 +1,58 @@
+(*  Title:      Pure/Concurrent/lazy.ML
+    Author:     Makarius
+
+Lazy evaluation based on futures.
+*)
+
+signature LAZY =
+sig
+  type 'a lazy
+  val peek: 'a lazy -> 'a Exn.result option
+  val lazy: (unit -> 'a) -> 'a lazy
+  val value: 'a -> 'a lazy
+  val force_result: 'a lazy -> 'a Exn.result
+  val force: 'a lazy -> 'a
+  val map_force: ('a -> 'b) -> 'a lazy -> 'b lazy
+end;
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Future of 'a future;
+
+abstype 'a lazy = Lazy of 'a expr Synchronized.var
+with
+
+fun peek (Lazy var) =
+  (case Synchronized.value var of
+    Expr _ => NONE
+  | Future x => Future.peek x);
+
+fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
+fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
+
+
+(* force result *)
+
+fun force_result (Lazy var) =
+  (case peek (Lazy var) of
+    SOME res => res
+  | NONE =>
+      Synchronized.guarded_access var
+        (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
+          | Future x => SOME (x, Future x))
+      |> Future.join_result);
+
+fun force r = Exn.release (force_result r);
+
+fun map_force f = value o f o force;
+
+end;
+end;
+
+type 'a lazy = 'a Lazy.lazy;
+