author | wenzelm |
Wed, 06 Jan 2010 13:14:28 +0100 | |
changeset 34278 | 228f27469139 |
parent 33023 | 207c21697a48 |
child 37183 | dae865999db5 |
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. |
5 |
Parallel version based on futures -- avoids critical or multiple |
|
6 |
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 |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
12 |
val peek: 'a lazy -> 'a Exn.result option |
28971 | 13 |
val lazy: (unit -> 'a) -> 'a lazy |
14 |
val value: 'a -> 'a lazy |
|
29422 | 15 |
val force_result: 'a lazy -> 'a Exn.result |
28971 | 16 |
val force: 'a lazy -> 'a |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
17 |
end; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
18 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
19 |
structure Lazy: LAZY = |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
20 |
struct |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
21 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
22 |
(* datatype *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
23 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
24 |
datatype 'a expr = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
25 |
Expr of unit -> 'a | |
34278 | 26 |
Result of 'a; |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
27 |
|
34278 | 28 |
abstype 'a lazy = Lazy of 'a expr future Synchronized.var |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
29 |
with |
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
30 |
|
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
31 |
fun peek (Lazy var) = |
34278 | 32 |
(case Future.peek (Synchronized.value var) of |
33 |
NONE => NONE |
|
34 |
| SOME (Exn.Result (Expr _)) => NONE |
|
35 |
| SOME (Exn.Result (Result x)) => SOME (Exn.Result x) |
|
36 |
| SOME (Exn.Exn exn) => SOME (Exn.Exn exn)); |
|
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
37 |
|
34278 | 38 |
fun lazy e = Lazy (Synchronized.var "lazy" (Future.value (Expr e))); |
39 |
fun value a = Lazy (Synchronized.var "lazy" (Future.value (Result a))); |
|
28673
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
40 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
41 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
42 |
(* force result *) |
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
43 |
|
34278 | 44 |
fun fork e = |
45 |
let val x = Future.fork (fn () => Result (e ()) handle Exn.Interrupt => Expr e) |
|
46 |
in (x, x) end; |
|
47 |
||
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
48 |
fun force_result (Lazy var) = |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
49 |
(case peek (Lazy var) of |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
50 |
SOME res => res |
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
51 |
| NONE => |
34278 | 52 |
let |
53 |
val result = |
|
54 |
Synchronized.change_result var |
|
55 |
(fn x => |
|
56 |
(case Future.peek x of |
|
57 |
SOME (Exn.Result (Expr e)) => fork e |
|
58 |
| _ => (x, x))) |
|
59 |
|> Future.join_result; |
|
60 |
in |
|
61 |
case result of |
|
62 |
Exn.Result (Expr _) => Exn.Exn Exn.Interrupt |
|
63 |
| Exn.Result (Result x) => Exn.Result x |
|
64 |
| Exn.Exn exn => Exn.Exn exn |
|
65 |
end); |
|
29422 | 66 |
|
67 |
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
|
68 |
|
d746a8c12c43
renamed structure Susp to Lazy, and Susp.delay to Lazy.lazy;
wenzelm
parents:
diff
changeset
|
69 |
end; |
32815
1a5e364584ae
separate concurrent/sequential versions of lazy evaluation;
wenzelm
parents:
32738
diff
changeset
|
70 |
end; |
28971 | 71 |
|
72 |
type 'a lazy = 'a Lazy.lazy; |
|
73 |