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