author | wenzelm |
Fri, 23 May 2008 21:18:47 +0200 | |
changeset 26977 | e736139b553d |
parent 26063 | b2862698dc79 |
child 28159 | 80823c582b9d |
permissions | -rw-r--r-- |
20594 | 1 |
(* Title: Pure/General/susp.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sebastian Skalberg and Florian Haftmann, TU Muenchen |
|
4 |
||
26063 | 5 |
Delayed evaluation. Supposed to be value-oriented. |
20594 | 6 |
*) |
7 |
||
8 |
signature SUSP = |
|
9 |
sig |
|
10 |
type 'a T |
|
11 |
val value: 'a -> 'a T |
|
12 |
val delay: (unit -> 'a) -> 'a T |
|
13 |
val force: 'a T -> 'a |
|
14 |
val peek: 'a T -> 'a option |
|
15 |
val same: 'a T * 'a T -> bool |
|
16 |
end |
|
17 |
||
18 |
structure Susp : SUSP = |
|
19 |
struct |
|
20 |
||
21 |
datatype 'a susp = |
|
22 |
Value of 'a |
|
23 |
| Delay of unit -> 'a; |
|
24 |
||
25 |
type 'a T = 'a susp ref; |
|
26 |
||
27 |
fun value v = ref (Value v); |
|
28 |
||
29 |
fun delay f = ref (Delay f); |
|
30 |
||
25317 | 31 |
fun force (ref (Value v)) = v |
32 |
| force susp = NAMED_CRITICAL "susp" (fn () => |
|
33 |
(case ! susp of |
|
34 |
Value v => v (*race wrt. parallel force*) |
|
25310 | 35 |
| Delay f => |
36 |
let |
|
37 |
val v = f (); |
|
38 |
val _ = susp := Value v; |
|
25317 | 39 |
in v end)); |
20594 | 40 |
|
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
41 |
fun peek susp = |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
42 |
(case ! susp of |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
43 |
Value v => SOME v |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
44 |
| Delay _ => NONE); |
20594 | 45 |
|
46 |
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*) |
|
47 |
||
24299
91d893799212
force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents:
24058
diff
changeset
|
48 |
end; |