# HG changeset patch
# User wenzelm
# Date 1262780068 -3600
# Node ID 228f274691396ae9dc8dd92cbed99ead72262c0d
# Parent  7325a5e3587fe4e8b27e6151926f7b114e081609
do not memoize interrupts;
actually memoize results in sequential version;
tuned;

diff -r 7325a5e3587f -r 228f27469139 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);
 
diff -r 7325a5e3587f -r 228f27469139 src/Pure/Concurrent/lazy_sequential.ML
--- a/src/Pure/Concurrent/lazy_sequential.ML	Tue Jan 05 23:38:10 2010 +0100
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Wed Jan 06 13:14:28 2010 +0100
@@ -1,7 +1,8 @@
 (*  Title:      Pure/Concurrent/lazy_sequential.ML
     Author:     Florian Haftmann and Makarius, TU Muenchen
 
-Lazy evaluation with memoing (sequential version).
+Lazy evaluation with memoing of results and regular exceptions
+(sequential version).
 *)
 
 structure Lazy: LAZY =
@@ -28,9 +29,16 @@
 (* force result *)
 
 fun force_result (Lazy r) =
-  (case ! r of
-    Expr e => Exn.capture e ()
-  | Result res => res);
+  let
+    val result =
+      (case ! r of
+        Expr e => Exn.capture e ()
+      | Result res => res);
+    val _ =
+      (case result of
+        Exn.Exn Exn.Interrupt => ()
+      | _ => r := result);
+  in result end;
 
 fun force r = Exn.release (force_result r);