author | wenzelm |
Mon, 11 Jul 2011 22:55:47 +0200 | |
changeset 43761 | e72ba84ae58f |
parent 39232 | 69c6d3e87660 |
child 44198 | a41ea419de68 |
permissions | -rw-r--r-- |
32817 | 1 |
(* Title: Pure/Concurrent/lazy_sequential.ML |
2 |
Author: Florian Haftmann and Makarius, TU Muenchen |
|
3 |
||
34278 | 4 |
Lazy evaluation with memoing of results and regular exceptions |
5 |
(sequential version). |
|
32817 | 6 |
*) |
7 |
||
8 |
structure Lazy: LAZY = |
|
9 |
struct |
|
10 |
||
11 |
(* datatype *) |
|
12 |
||
13 |
datatype 'a expr = |
|
14 |
Expr of unit -> 'a | |
|
15 |
Result of 'a Exn.result; |
|
16 |
||
17 |
abstype 'a lazy = Lazy of 'a expr Unsynchronized.ref |
|
18 |
with |
|
19 |
||
20 |
fun peek (Lazy r) = |
|
21 |
(case ! r of |
|
22 |
Expr _ => NONE |
|
32844 | 23 |
| Result res => SOME res); |
32817 | 24 |
|
25 |
fun lazy e = Lazy (Unsynchronized.ref (Expr e)); |
|
43761
e72ba84ae58f
tuned signature -- corresponding to Scala version;
wenzelm
parents:
39232
diff
changeset
|
26 |
fun value a = Lazy (Unsynchronized.ref (Result (Exn.Res a))); |
32817 | 27 |
|
28 |
||
29 |
(* force result *) |
|
30 |
||
31 |
fun force_result (Lazy r) = |
|
34278 | 32 |
let |
33 |
val result = |
|
34 |
(case ! r of |
|
35 |
Expr e => Exn.capture e () |
|
36 |
| Result res => res); |
|
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
34293
diff
changeset
|
37 |
val _ = if Exn.is_interrupt_exn result then () else r := Result result; |
34278 | 38 |
in result end; |
32817 | 39 |
|
40 |
fun force r = Exn.release (force_result r); |
|
41 |
||
42 |
end; |
|
43 |
end; |
|
44 |
||
45 |
type 'a lazy = 'a Lazy.lazy; |
|
46 |