do not memoize interrupts;
actually memoize results in sequential version;
tuned;
--- 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);
--- 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);