# HG changeset patch
# User wenzelm
# Date 1254414246 -7200
# Node ID 4ed308181f7fb44bfa2273859ffffc7c2a652f40
# Parent  5db89f8d44f3875c48399b74f09347bbeb0b60db
Lazy evaluation with memoing (sequential version).

diff -r 5db89f8d44f3 -r 4ed308181f7f src/Pure/Concurrent/lazy_sequential.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/lazy_sequential.ML	Thu Oct 01 18:24:06 2009 +0200
@@ -0,0 +1,43 @@
+(*  Title:      Pure/Concurrent/lazy_sequential.ML
+    Author:     Florian Haftmann and Makarius, TU Muenchen
+
+Lazy evaluation with memoing (sequential version).
+*)
+
+structure Lazy: LAZY =
+struct
+
+(* datatype *)
+
+datatype 'a expr =
+  Expr of unit -> 'a |
+  Result of 'a Exn.result;
+
+abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
+with
+
+fun peek (Lazy r) =
+  (case ! r of
+    Expr _ => NONE
+  | Result x => SOME x);
+
+fun lazy e = Lazy (Unsynchronized.ref (Expr e));
+fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
+
+
+(* force result *)
+
+fun force_result (Lazy r) =
+  (case ! r of
+    Expr e => Exn.capture e ()
+  | Result res => res);
+
+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;
+