author | wenzelm |
Sat, 01 Sep 2018 14:25:03 +0200 | |
changeset 68867 | a8728e3f9822 |
parent 68698 | 6ee53660a911 |
child 68868 | 5f44ad150ed8 |
permissions | -rw-r--r-- |
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 | 4 |
Lazy evaluation with memoing of results and regular exceptions. |
40389 | 5 |
Parallel version based on (passive) futures, to avoid critical or |
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 | 11 |
type 'a lazy |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
12 |
val value: 'a -> 'a lazy |
66167 | 13 |
val lazy_name: string -> (unit -> 'a) -> 'a lazy |
28971 | 14 |
val lazy: (unit -> '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
|
15 |
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
|
16 |
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
|
17 |
val is_finished: 'a lazy -> bool |
68867
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
18 |
val finished_result: 'a lazy -> 'a Exn.result |
29422 | 19 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 20 |
val force: 'a lazy -> 'a |
67661 | 21 |
val force_value: 'a lazy -> 'a lazy |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
22 |
val map: ('a -> 'b) -> 'a lazy -> 'b lazy |
67661 | 23 |
val map_finished: ('a -> 'b) -> 'a lazy -> 'b lazy |
67668 | 24 |
val consolidate: 'a lazy list -> 'a lazy list |
44427 | 25 |
val future: Future.params -> 'a lazy -> 'a future |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
26 |
end; |
28673
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 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
29 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
30 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
31 |
(* datatype *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
32 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
33 |
datatype 'a expr = |
66167 | 34 |
Expr of string * (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
|
35 |
Result of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
36 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
37 |
abstype 'a lazy = Value of 'a | Lazy of 'a expr Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
38 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
39 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
40 |
fun value a = Value a; |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
41 |
|
66167 | 42 |
fun lazy_name name e = Lazy (Synchronized.var "lazy" (Expr (name, e))); |
43 |
fun lazy e = lazy_name "lazy" e; |
|
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
|
44 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
45 |
fun peek (Value a) = SOME (Exn.Res a) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
46 |
| peek (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
47 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
48 |
Expr _ => NONE |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
49 |
| Result res => Future.peek res); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
50 |
|
67661 | 51 |
|
52 |
(* status *) |
|
66168 | 53 |
|
67657 | 54 |
fun is_value (Value _) = true |
55 |
| is_value (Lazy _) = false; |
|
66168 | 56 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
57 |
fun is_running (Value _) = false |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
58 |
| is_running (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
59 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
60 |
Expr _ => false |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
61 |
| Result res => not (Future.is_finished res)); |
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
|
62 |
|
68867
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
63 |
fun is_finished_future res = |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
64 |
Future.is_finished res andalso not (Exn.is_interrupt_exn (Future.join_result res)); |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
65 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
66 |
fun is_finished (Value _) = true |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
67 |
| is_finished (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
68 |
(case Synchronized.value var of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
69 |
Expr _ => false |
68867
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
70 |
| Result res => is_finished_future res); |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
71 |
|
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
72 |
fun finished_result (Value a) = Exn.Res a |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
73 |
| finished_result (Lazy var) = |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
74 |
let fun fail () = Exn.Exn (Fail "Unfinished lazy") in |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
75 |
(case Synchronized.value var of |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
76 |
Expr _ => fail () |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
77 |
| Result res => if is_finished_future res then Future.join_result res else fail ()) |
a8728e3f9822
more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
wenzelm
parents:
68698
diff
changeset
|
78 |
end; |
59191 | 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 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
82 |
|
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
83 |
fun force_result (Value a) = Exn.Res a |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
84 |
| force_result (Lazy var) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
85 |
(case peek (Lazy var) of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
86 |
SOME res => res |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
87 |
| NONE => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
88 |
Thread_Attributes.uninterruptible (fn restore_attributes => fn () => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
89 |
let |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
90 |
val (expr, x) = |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
91 |
Synchronized.change_result var |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
92 |
(fn Expr (name, e) => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
93 |
let val x = Future.promise_name name I |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
94 |
in ((SOME (name, e), x), Result x) end |
68597
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
95 |
| Result x => ((NONE, x), Result x)) |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
96 |
handle exn as Fail _ => |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
97 |
(case Synchronized.value var of |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
98 |
Expr _ => Exn.reraise exn |
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
99 |
| Result x => (NONE, x)); |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
100 |
in |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
101 |
(case expr of |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
102 |
SOME (name, e) => |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
103 |
let |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
104 |
val res0 = Exn.capture (restore_attributes e) (); |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
105 |
val _ = Exn.capture (fn () => Future.fulfill_result x res0) (); |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
106 |
val res = Future.join_result x; |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
107 |
(*semantic race: some other threads might see the same |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
108 |
interrupt, until there is a fresh start*) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
109 |
val _ = |
68590
f3c3c1e6133a
store immutable result: fewer refs, mutexes, condvars;
wenzelm
parents:
68130
diff
changeset
|
110 |
if Exn.is_interrupt_exn res |
f3c3c1e6133a
store immutable result: fewer refs, mutexes, condvars;
wenzelm
parents:
68130
diff
changeset
|
111 |
then Synchronized.change var (fn _ => Expr (name, e)) |
68597
afa7c5a239e6
more frugal assignment of lazy value: fewer mutexes, condvars;
wenzelm
parents:
68590
diff
changeset
|
112 |
else Synchronized.assign var (Result (Future.value_result res)); |
66904
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
113 |
in res end |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
114 |
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ()) |
d9783ea1160c
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
wenzelm
parents:
66168
diff
changeset
|
115 |
end) ()); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
116 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
117 |
end; |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
118 |
|
66168 | 119 |
fun force x = Exn.release (force_result x); |
120 |
||
67661 | 121 |
fun force_value x = if is_value x then x else value (force x); |
122 |
||
123 |
||
124 |
(* map *) |
|
67657 | 125 |
|
66167 | 126 |
fun map f x = lazy_name "Lazy.map" (fn () => f (force x)); |
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
127 |
|
67661 | 128 |
fun map_finished f x = if is_finished x then value (f (force x)) else map f x; |
129 |
||
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
130 |
|
67668 | 131 |
(* consolidate in parallel *) |
132 |
||
133 |
fun consolidate xs = |
|
134 |
let |
|
68698
6ee53660a911
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
wenzelm
parents:
68697
diff
changeset
|
135 |
val unfinished = |
6ee53660a911
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
wenzelm
parents:
68697
diff
changeset
|
136 |
xs |> map_filter (fn x => if is_finished x then NONE else SOME (fn () => force_result x)); |
67668 | 137 |
val _ = |
68698
6ee53660a911
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
wenzelm
parents:
68697
diff
changeset
|
138 |
if Future.relevant unfinished then |
6ee53660a911
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
wenzelm
parents:
68697
diff
changeset
|
139 |
ignore (Future.forked_results {name = "Lazy.consolidate", deps = []} unfinished) |
6ee53660a911
eliminated non-monotomnic Lazy.is_pending: Result may return to Expr due to Interrupt;
wenzelm
parents:
68697
diff
changeset
|
140 |
else List.app (fn e => ignore (e ())) unfinished; |
67668 | 141 |
in xs end; |
142 |
||
143 |
||
44386
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
144 |
(* future evaluation *) |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
145 |
|
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
146 |
fun future params x = |
4048ca2658b7
some support for toplevel printing wrt. editor perspective (still inactive);
wenzelm
parents:
44298
diff
changeset
|
147 |
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
|
148 |
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
|
149 |
|
62663 | 150 |
|
151 |
(* toplevel pretty printing *) |
|
152 |
||
153 |
val _ = |
|
62819
d3ff367a16a0
careful export of type-dependent functions, without losing their special status;
wenzelm
parents:
62663
diff
changeset
|
154 |
ML_system_pp (fn depth => fn pretty => fn x => |
62663 | 155 |
(case peek x of |
62823 | 156 |
NONE => PolyML_Pretty.PrettyString "<lazy>" |
157 |
| SOME (Exn.Exn _) => PolyML_Pretty.PrettyString "<failed>" |
|
62663 | 158 |
| SOME (Exn.Res y) => pretty (y, depth))); |
159 |
||
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
160 |
end; |
28971 | 161 |
|
162 |
type 'a lazy = 'a Lazy.lazy; |