author | haftmann |
Sat, 20 Aug 2011 01:21:22 +0200 | |
changeset 44323 | 4b5b430eb00e |
parent 44198 | a41ea419de68 |
child 44386 | 4048ca2658b7 |
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 |
|
44198 | 28 |
fun is_finished x = is_some (peek x); |
29 |
||
30 |
fun get_finished x = |
|
31 |
(case peek x of |
|
32 |
SOME res => Exn.release res |
|
33 |
| NONE => raise Fail "Unfinished lazy evaluation"); |
|
34 |
||
32817 | 35 |
|
36 |
(* force result *) |
|
37 |
||
38 |
fun force_result (Lazy r) = |
|
34278 | 39 |
let |
40 |
val result = |
|
41 |
(case ! r of |
|
42 |
Expr e => Exn.capture e () |
|
43 |
| 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
|
44 |
val _ = if Exn.is_interrupt_exn result then () else r := Result result; |
34278 | 45 |
in result end; |
32817 | 46 |
|
47 |
fun force r = Exn.release (force_result r); |
|
48 |
||
49 |
end; |
|
50 |
end; |
|
51 |
||
52 |
type 'a lazy = 'a Lazy.lazy; |
|
53 |