src/Pure/Concurrent/lazy.ML
author wenzelm
Tue, 23 Aug 2011 15:48:41 +0200
changeset 44386 4048ca2658b7
parent 44298 b8f8488704e2
child 44387 0f0ba362ce50
permissions -rw-r--r--
some support for toplevel printing wrt. editor perspective (still inactive);
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
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    14
  val get_finished: 'a lazy -> 'a
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    15
  val lazy: (unit -> 'a) -> 'a lazy
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    16
  val value: 'a -> 'a lazy
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
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    20
  val future: Future.fork_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
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    35
fun peek (Lazy var) =
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
  (case Synchronized.value var 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
    37
    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
    38
  | Result res => Future.peek res);
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    39
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
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
    41
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
    42
44198
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    43
fun is_finished x = is_some (peek x);
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    44
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    45
fun get_finished x =
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    46
  (case peek x of
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    47
    SOME res => Exn.release res
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    48
  | NONE => raise Fail "Unfinished lazy evaluation");
a41ea419de68 explicit check of finished evaluation;
wenzelm
parents: 41701
diff changeset
    49
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    50
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    51
(* force result *)
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    52
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    53
fun force_result (Lazy var) =
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    54
  (case peek (Lazy var) of
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    55
    SOME res => res
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    56
  | NONE =>
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    57
      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
    58
        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
    59
          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
    60
            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
    61
              (fn Expr e =>
44298
b8f8488704e2 Future.promise: explicit abort operation (like uninterruptible future job);
wenzelm
parents: 44198
diff changeset
    62
                    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
    63
                    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
    64
                | 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
    65
        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
    66
          (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
    67
            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
    68
              let
41701
430493d65cd2 Lazy.force_result: more standard treatment of interruptibility, potentially addressing races of exceptions vs. interrupts;
wenzelm
parents: 40482
diff changeset
    69
                val res0 = Exn.capture (restore_attributes e) ();
40482
dc0d4d4a1aa1 Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
wenzelm
parents: 40389
diff changeset
    70
                val _ = Future.fulfill_result x res0;
dc0d4d4a1aa1 Laze.force_result: more robust treatment of interrupts stemming from peer group cancellation;
wenzelm
parents: 40389
diff changeset
    71
                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
    72
                (*semantic race: some other threads might see the same
40389
511e5263f5c6 tuned comments;
wenzelm
parents: 39232
diff changeset
    73
                  interrupt, until there is a fresh start*)
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
    74
                val _ =
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 37183
diff changeset
    75
                  if Exn.is_interrupt_exn res then
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 37183
diff changeset
    76
                    Synchronized.change var (fn _ => Expr e)
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 37183
diff changeset
    77
                  else ();
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
              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
    79
          | 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
    80
        end) ());
29422
fdf396a24a9f added force_result;
wenzelm
parents: 28971
diff changeset
    81
28673
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    82
d746a8c12c43 renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff changeset
    83
end;
44386
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    84
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    85
fun force r = Exn.release (force_result r);
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    86
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
    87
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
(* future evaluation *)
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    90
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    91
fun future params x =
4048ca2658b7 some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents: 44298
diff changeset
    92
  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
    93
  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
    94
32815
1a5e364584ae separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents: 32738
diff changeset
    95
end;
28971
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    96
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    97
type 'a lazy = 'a Lazy.lazy;
300ec36a19af renamed type Lazy.T to lazy;
wenzelm
parents: 28673
diff changeset
    98