# 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; +