src/Pure/Concurrent/lazy.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.ML
     2     Author:     Makarius
     3 
     4 Lazy evaluation based on futures.
     5 *)
     6 
     7 signature LAZY =
     8 sig
     9   type 'a lazy
    10   val peek: 'a lazy -> 'a Exn.result option
    11   val lazy: (unit -> 'a) -> 'a lazy
    12   val value: 'a -> 'a lazy
    13   val force_result: 'a lazy -> 'a Exn.result
    14   val force: 'a lazy -> 'a
    15 end;
    16 
    17 structure Lazy: LAZY =
    18 struct
    19 
    20 (* datatype *)
    21 
    22 datatype 'a expr =
    23   Expr of unit -> 'a |
    24   Future of 'a future;
    25 
    26 abstype 'a lazy = Lazy of 'a expr Synchronized.var
    27 with
    28 
    29 fun peek (Lazy var) =
    30   (case Synchronized.value var of
    31     Expr _ => NONE
    32   | Future x => Future.peek x);
    33 
    34 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    35 fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a)));
    36 
    37 
    38 (* force result *)
    39 
    40 fun force_result (Lazy var) =
    41   (case peek (Lazy var) of
    42     SOME res => res
    43   | NONE =>
    44       Synchronized.guarded_access var
    45         (fn Expr e => let val x = Future.fork e in SOME (x, Future x) end
    46           | Future x => SOME (x, Future x))
    47       |> Future.join_result);
    48 
    49 fun force r = Exn.release (force_result r);
    50 
    51 end;
    52 end;
    53 
    54 type 'a lazy = 'a Lazy.lazy;
    55