src/Pure/Concurrent/lazy.ML
author wenzelm
Fri, 18 Mar 2016 16:26:35 +0100
changeset 62663 bea354f6ff21
parent 59348 8a6788917b32
child 62819 d3ff367a16a0
permissions -rw-r--r--
clarified modules; tuned signature;
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
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    12
  val lazy: (unit -> 'a) -> 'a lazy
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    13
  val value: 'a -> 'a lazy
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    14
  val peek: 'a lazy -> 'a Exn.result option
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    15
  val is_running: 'a lazy -> bool
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    16
  val is_finished: 'a lazy -> bool
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    17
  val force_result: 'a lazy -> 'a Exn.result
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    18
  val force: 'a lazy -> 'a
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    19
  val map: ('a -> 'b) -> 'a lazy -> 'b lazy
44427
c4a86d72a5cc tuned signature;
wenzelm
parents: 44387
diff changeset
    20
  val future: Future.params -> 'a lazy -> 'a future
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    21
end;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    22
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    23
structure Lazy: LAZY =
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    24
struct
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    25
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    26
(* datatype *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    27
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    28
datatype 'a expr =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    29
  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
    30
  Result of 'a future;
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    31
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
    32
abstype 'a lazy = Lazy of 'a expr Synchronized.var
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    33
with
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    34
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    35
fun lazy e = Lazy (Synchronized.var "lazy" (Expr e));
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    36
fun value a = Lazy (Synchronized.var "lazy" (Result (Future.value a)));
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    37
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    38
fun peek (Lazy var) =
59195
f8588372d70e back to full synchronization (cf. eb3e399f5b9f);
wenzelm
parents: 59193
diff changeset
    39
  (case Synchronized.value 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
    40
    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
    41
  | Result res => Future.peek res);
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    42
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    43
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    44
(* status *)
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    45
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    46
fun is_future pred (Lazy var) =
59191
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    47
  (case Synchronized.value var of
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    48
    Expr _ => false
59193
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    49
  | Result res => pred res);
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    50
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    51
fun is_running x = is_future (not o Future.is_finished) x;
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    52
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    53
fun is_finished x =
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    54
  is_future (fn res =>
59f1591a11cb eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
wenzelm
parents: 59191
diff changeset
    55
    Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res))) x;
59191
682aa538c5c0 more thorough Lazy.is_finished;
wenzelm
parents: 59147
diff changeset
    56
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    57
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    58
(* force result *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    59
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    60
fun force_result (Lazy var) =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    61
  (case peek (Lazy var) of
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    62
    SOME res => res
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    63
  | NONE =>
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    64
      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
    65
        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
    66
          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
    67
            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
    68
              (fn Expr e =>
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44198
diff changeset
    69
                    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
    70
                    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
    71
                | 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
    72
        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
    73
          (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
    74
            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
    75
              let
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    76
                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
    77
                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
    78
                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
    79
                (*semantic race: some other threads might see the same
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
    80
                  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
    81
                val _ =
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    82
                  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
    83
                    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
    84
                  else ();
b254fdaf1973 partial revert of 8a179a0493e3 -- expose failure status of result (potentially via group) instead of isolated interrupt;
wenzelm
parents: 47423
diff changeset
    85
              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
    86
          | 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
    87
        end) ());
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    88
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    89
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    90
end;
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    91
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    92
fun force r = Exn.release (force_result r);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    93
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
    94
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    95
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    96
(* future evaluation *)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    97
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    98
fun future params x =
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    99
  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
   100
  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
   101
62663
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   102
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   103
(* toplevel pretty printing *)
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   104
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   105
val _ =
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   106
  PolyML.addPrettyPrinter (fn depth => fn pretty => fn x =>
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   107
    (case peek x of
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   108
      NONE => PolyML.PrettyString "<lazy>"
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   109
    | SOME (Exn.Exn _) => PolyML.PrettyString "<failed>"
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   110
    | SOME (Exn.Res y) => pretty (y, depth)));
bea354f6ff21 clarified modules;
wenzelm
parents: 59348
diff changeset
   111
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
   112
end;
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
   113
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
   114
type 'a lazy = 'a Lazy.lazy;