src/Pure/Concurrent/lazy.ML
author wenzelm
Sun, 28 Dec 2014 12:18:01 +0100
changeset 59191 682aa538c5c0
parent 59147 eb3e399f5b9f
child 59193 59f1591a11cb
permissions -rw-r--r--
more thorough Lazy.is_finished;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
     1
(*  Title:      Pure/Concurrent/lazy.ML
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
     2
    Author:     Makarius
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     3
34278
228f27469139 do not memoize interrupts;
wenzelm
parents: 33023
diff changeset
     4
Lazy evaluation with memoing of results and regular exceptions.
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
     5
Parallel version based on (passive) futures, to avoid critical or
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
     6
multiple evaluation (unless interrupted).
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     7
*)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     8
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
     9
signature LAZY =
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    10
sig
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    11
  type 'a lazy
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    12
  val peek: 'a lazy -> 'a Exn.result option
44198
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    13
  val is_finished: 'a lazy -> bool
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    14
  val lazy: (unit -> 'a) -> 'a lazy
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    15
  val value: 'a -> 'a lazy
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    16
  val force_result: 'a lazy -> 'a Exn.result
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    17
  val force: 'a lazy -> 'a
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    18
  val map: ('a -> 'b) -> 'a lazy -> 'b lazy
44427
c4a86d72a5cc tuned signature;
wenzelm
parents: 44387
diff changeset
    19
  val future: Future.params -> 'a lazy -> 'a future
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    20
end;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    21
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    22
structure Lazy: LAZY =
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    23
struct
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    24
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    25
(* datatype *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    26
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    27
datatype 'a expr =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    28
  Expr of unit -> 'a |
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    29
  Result of 'a future;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    30
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    31
abstype 'a lazy = Lazy of 'a expr Synchronized.var
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    32
with
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    33
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    34
fun peek (Lazy var) =
59147
eb3e399f5b9f peek value without synchronization;
wenzelm
parents: 47430
diff changeset
    35
  (case Synchronized.peek var of
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    36
    Expr _ => NONE
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    37
  | Result res => Future.peek res);
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    38
59191
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    39
fun is_finished (Lazy var) =
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    40
  (case Synchronized.value var of
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    41
    Expr _ => false
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    42
  | Result res =>
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    43
      Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)));
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    44
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    45
fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    46
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    47
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    48
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    49
(* force result *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    50
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    51
fun force_result (Lazy var) =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    52
  (case peek (Lazy var) of
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    53
    SOME res => res
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    54
  | NONE =>
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    55
      uninterruptible (fn restore_attributes => fn () =>
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    56
        let
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    57
          val (expr, x) =
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    58
            Synchronized.change_result var
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    59
              (fn Expr e =>
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44198
diff changeset
    60
                    let val x = Future.promise I
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    61
                    in ((SOME e, x), Result x) end
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    62
                | Result x => ((NONE, x), Result x));
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    63
        in
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    64
          (case expr of
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    65
            SOME e =>
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    66
              let
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    67
                val res0 = Exn.capture (restore_attributes e) ();
47430
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    68
                val _ = Exn.capture (fn () => Future.fulfill_result x res0) ();
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    69
                val res = Future.join_result x;
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    70
                (*semantic race: some other threads might see the same
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
    71
                  interrupt, until there is a fresh start*)
47430
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    72
                val _ =
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    73
                  if Exn.is_interrupt_exn res then
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    74
                    Synchronized.change var (fn _ => Expr e)
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    75
                  else ();
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    76
              in res end
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    77
          | NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
37183
dae865999db5 force_result within the current execution context -- avoids overhead of potential thread context switch and robustifies Interrupt handling;
wenzelm
parents: 34278
diff changeset
    78
        end) ());
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    79
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    80
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    81
end;
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    82
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    83
fun force r = Exn.release (force_result r);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    84
fun map f x = lazy (fn () => f (force x));
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    85
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    86
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    87
(* future evaluation *)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    88
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    89
fun future params x =
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    90
  if is_finished x then Future.value_result (force_result x)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    91
  else (singleton o Future.forks) params (fn () => force x);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    92
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    93
end;
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    94
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    95
type 'a lazy = 'a Lazy.lazy;
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    96