src/Pure/General/lazy.ML
author wenzelm
Tue Sep 29 11:49:22 2009 +0200 (2009-09-29)
changeset 32738 15bb09ca0378
parent 29422 fdf396a24a9f
permissions -rw-r--r--
explicit indication of Unsynchronized.ref;
     1 (*  Title:      Pure/General/lazy.ML
     2     Author:     Florian Haftmann and Makarius, TU Muenchen
     3 
     4 Lazy evaluation with memoing.  Concurrency may lead to multiple
     5 attempts of evaluation -- the first result persists.
     6 *)
     7 
     8 signature LAZY =
     9 sig
    10   type 'a lazy
    11   val same: 'a lazy * 'a lazy -> bool
    12   val lazy: (unit -> 'a) -> 'a lazy
    13   val value: 'a -> 'a lazy
    14   val peek: 'a lazy -> 'a Exn.result option
    15   val force_result: 'a lazy -> 'a Exn.result
    16   val force: 'a lazy -> 'a
    17   val map_force: ('a -> 'a) -> 'a lazy -> 'a lazy
    18 end
    19 
    20 structure Lazy :> LAZY =
    21 struct
    22 
    23 (* datatype *)
    24 
    25 datatype 'a T =
    26   Lazy of unit -> 'a |
    27   Result of 'a Exn.result;
    28 
    29 type 'a lazy = 'a T Unsynchronized.ref;
    30 
    31 fun same (r1: 'a lazy, r2) = r1 = r2;
    32 
    33 fun lazy e = Unsynchronized.ref (Lazy e);
    34 fun value x = Unsynchronized.ref (Result (Exn.Result x));
    35 
    36 fun peek r =
    37   (case ! r of
    38     Lazy _ => NONE
    39   | Result res => SOME res);
    40 
    41 
    42 (* force result *)
    43 
    44 fun force_result r =
    45   let
    46     (*potentially concurrent evaluation*)
    47     val res =
    48       (case ! r of
    49         Lazy e => Exn.capture e ()
    50       | Result res => res);
    51     (*assign result -- first one persists*)
    52     val res' = NAMED_CRITICAL "lazy" (fn () =>
    53       (case ! r of
    54         Lazy _ => (r := Result res; res)
    55       | Result res' => res'));
    56   in res' end;
    57 
    58 fun force r = Exn.release (force_result r);
    59 
    60 fun map_force f = value o f o force;
    61 
    62 end;
    63 
    64 type 'a lazy = 'a Lazy.lazy;
    65