author | wenzelm |
Tue, 20 Oct 2009 19:28:01 +0200 | |
changeset 33023 | 207c21697a48 |
parent 32815 | 1a5e364584ae |
child 34278 | 228f27469139 |
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 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
4 |
Lazy evaluation based on futures. |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
5 |
*) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
6 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
7 |
signature LAZY = |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
8 |
sig |
28971 | 9 |
type 'a lazy |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
10 |
val peek: 'a lazy -> 'a Exn.result option |
28971 | 11 |
val lazy: (unit -> 'a) -> 'a lazy |
12 |
val value: 'a -> 'a lazy |
|
29422 | 13 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 14 |
val force: 'a lazy -> 'a |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
15 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
16 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
17 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
18 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
19 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
20 |
(* datatype *) |
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 |
datatype 'a expr = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
23 |
Expr of unit -> 'a | |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
24 |
Future of 'a future; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
25 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
26 |
abstype 'a lazy = Lazy of 'a expr Synchronized.var |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
27 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
28 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
29 |
fun peek (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
30 |
(case Synchronized.value var of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
31 |
Expr _ => NONE |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
32 |
| Future x => Future.peek x); |
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 lazy e = Lazy (Synchronized.var "lazy" (Expr e)); |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
35 |
fun value a = Lazy (Synchronized.var "lazy" (Future (Future.value a))); |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
36 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
37 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
38 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
39 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
40 |
fun force_result (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
41 |
(case peek (Lazy var) of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
42 |
SOME res => res |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
43 |
| NONE => |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
44 |
Synchronized.guarded_access var |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
45 |
(fn Expr e => let val x = Future.fork e in SOME (x, Future x) end |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
46 |
| Future x => SOME (x, Future x)) |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
47 |
|> Future.join_result); |
29422 | 48 |
|
49 |
fun force r = Exn.release (force_result r); |
|
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 |
end; |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
52 |
end; |
28971 | 53 |
|
54 |
type 'a lazy = 'a Lazy.lazy; |
|
55 |