author | wenzelm |
Mon, 23 Jul 2007 14:06:12 +0200 | |
changeset 23922 | 707639e9497d |
parent 20594 | b80c4a5cd018 |
child 24058 | 81aafd465662 |
permissions | -rw-r--r-- |
20594 | 1 |
(* Title: Pure/General/susp.ML |
2 |
ID: $Id$ |
|
3 |
Author: Sebastian Skalberg and Florian Haftmann, TU Muenchen |
|
4 |
||
5 |
Delayed evaluation. |
|
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 |
||
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
31 |
fun force susp = CRITICAL (fn () => |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
32 |
(case ! susp of |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
33 |
Value v => v |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
34 |
| Delay f => |
20594 | 35 |
let |
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
36 |
val v = f (); |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
37 |
val _ = susp := Value v; |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
38 |
in v end)); |
20594 | 39 |
|
23922
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
40 |
fun peek susp = |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
41 |
(case ! susp of |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
42 |
Value v => SOME v |
707639e9497d
marked some CRITICAL sections (for multithreading);
wenzelm
parents:
20594
diff
changeset
|
43 |
| Delay _ => NONE); |
20594 | 44 |
|
45 |
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*) |
|
46 |
||
47 |
end |