src/Pure/Concurrent/lazy_sequential.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 33023 207c21697a48
child 34278 228f27469139
permissions -rw-r--r--
map_range (and map_index) combinator
     1 (*  Title:      Pure/Concurrent/lazy_sequential.ML
     2     Author:     Florian Haftmann and Makarius, TU Muenchen
     3 
     4 Lazy evaluation with memoing (sequential version).
     5 *)
     6 
     7 structure Lazy: LAZY =
     8 struct
     9 
    10 (* datatype *)
    11 
    12 datatype 'a expr =
    13   Expr of unit -> 'a |
    14   Result of 'a Exn.result;
    15 
    16 abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref
    17 with
    18 
    19 fun peek (Lazy r) =
    20   (case ! r of
    21     Expr _ => NONE
    22   | Result res => SOME res);
    23 
    24 fun lazy e = Lazy (Unsynchronized.ref (Expr e));
    25 fun value a = Lazy (Unsynchronized.ref (Result (Exn.Result a)));
    26 
    27 
    28 (* force result *)
    29 
    30 fun force_result (Lazy r) =
    31   (case ! r of
    32     Expr e => Exn.capture e ()
    33   | Result res => res);
    34 
    35 fun force r = Exn.release (force_result r);
    36 
    37 end;
    38 end;
    39 
    40 type 'a lazy = 'a Lazy.lazy;
    41