src/Pure/Concurrent/lazy.ML
author wenzelm
Thu Sep 09 17:20:27 2010 +0200 (2010-09-09 ago)
changeset 39232 69c6d3e87660
parent 37183 dae865999db5
child 40389 511e5263f5c6
permissions -rw-r--r--
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
     1 (*  Title:      Pure/Concurrent/lazy.ML
     2     Author:     Makarius
     3 
     4 Lazy evaluation with memoing of results and regular exceptions.
     5 Parallel version based on futures -- avoids critical or multiple
     6 evaluation, unless interrupted.
     7 *)
     8 
     9 signature LAZY =
    10 sig
    11   type 'a lazy
    12   val peek: 'a lazy -> 'a Exn.result option
    13   val lazy: (unit -> 'a) -> 'a lazy
    14   val value: 'a -> 'a lazy
    15   val force_result: 'a lazy -> 'a Exn.result
    16   val force: 'a lazy -> 'a
    17 end;
    18 
    19 structure Lazy: LAZY =
    20 struct
    21 
    22 (* datatype *)
    23 
    24 datatype 'a expr =
    25   Expr of unit -> 'a |
    26   Result of 'a future;
    27 
    28 abstype 'a lazy = Lazy of 'a expr Synchronized.var
    29 with
    30 
    31 fun peek (Lazy var) =
    32   (case Synchronized.value var of
    33     Expr _ => NONE
    34   | Result res => Future.peek res);
    35 
    36 fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
    37 fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
    38 
    39 
    40 (* force result *)
    41 
    42 fun force_result (Lazy var) =
    43   (case peek (Lazy var) of
    44     SOME res => res
    45   | NONE =>
    46       uninterruptible (fn restore_interrupts => fn () =>
    47         let
    48           val (expr, x) =
    49             Synchronized.change_result var
    50               (fn Expr e =>
    51                     let val x = Future.promise ()
    52                     in ((SOME e, x), Result x) end
    53                 | Result x => ((NONE, x), Result x));
    54         in
    55           (case expr of
    56             SOME e =>
    57               let
    58                 val res = restore_interrupts (fn () => Exn.capture e ()) ();
    59                 val _ = Future.fulfill_result x res;
    60                 (*semantic race: some other threads might see the same
    61                   Interrupt, until there is a fresh start*)
    62                 val _ =
    63                   if Exn.is_interrupt_exn res then
    64                     Synchronized.change var (fn _ => Expr e)
    65                   else ();
    66               in res end
    67           | NONE => restore_interrupts (fn () => Future.join_result x) ())
    68         end) ());
    69 
    70 fun force r = Exn.release (force_result r);
    71 
    72 end;
    73 end;
    74 
    75 type 'a lazy = 'a Lazy.lazy;
    76