src/Pure/Concurrent/lazy.ML

--- a/src/Pure/Concurrent/lazy.ML	Tue Jan 05 23:38:10 2010 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Wed Jan 06 13:14:28 2010 +0100
@@ -1,7 +1,9 @@
 (*  Title:      Pure/Concurrent/lazy.ML
     Author:     Makarius
 
-Lazy evaluation based on futures.
+Lazy evaluation with memoing of results and regular exceptions.
+Parallel version based on futures -- avoids critical or multiple
+evaluation, unless interrupted.
 *)
 
 signature LAZY =
@@ -21,30 +23,46 @@
 
 datatype 'a expr =
   Expr of unit -> 'a |
-  Future of 'a future;
+  Result of 'a;
 
-abstype 'a lazy = Lazy of 'a expr Synchronized.var
+abstype 'a lazy = Lazy of 'a expr future Synchronized.var
 with
 
 fun peek (Lazy var) =
-  (case Synchronized.value var of
-    Expr _ => NONE
-  | Future x => Future.peek x);
+  (case Future.peek (Synchronized.value var) of
+    NONE => NONE
+  | SOME (Exn.Result (Expr _)) => NONE
+  | SOME (Exn.Result (Result x)) => SOME (Exn.Result x)
+  | SOME (Exn.Exn exn) => SOME (Exn.Exn exn));
 
-fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
-fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
+fun lazy e = Lazy (Synchronized.var "lazy" (Future.value (Expr e)));
+fun value a = Lazy (Synchronized.var "lazy" (Future.value (Result a)));
 
 
 (* force result *)
 
+fun fork e =
+  let val x = Future.fork (fn () => Result (e ()) handle Exn.Interrupt => Expr e)
+  in (x, x) end;
+
 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);
+      let
+        val result =
+          Synchronized.change_result var
+            (fn x =>
+              (case Future.peek x of
+                SOME (Exn.Result (Expr e)) => fork e
+              | _ => (x, x)))
+          |> Future.join_result;
+      in
+        case result of
+          Exn.Result (Expr _) => Exn.Exn Exn.Interrupt
+        | Exn.Result (Result x) => Exn.Result x
+        | Exn.Exn exn => Exn.Exn exn
+      end);
 
 fun force r = Exn.release (force_result r);