| author | haftmann |
| Fri, 30 Oct 2009 13:59:51 +0100 | |
| changeset 33359 | 8b673ae1bf39 |
| parent 23510 | 4521fead5609 |
| child 39353 | 7f11d833d65b |
| permissions | -rw-r--r-- |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
1 |
(* ========================================================================= *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
2 |
(* SUPPORT FOR LAZY EVALUATION *) |
| 23510 | 3 |
(* Copyright (c) 2007 Joe Hurd, distributed under the BSD License *) |
|
23442
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
4 |
(* ========================================================================= *) |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
5 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
6 |
structure Lazy :> Lazy = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
7 |
struct |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
8 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
9 |
datatype 'a thunk = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
10 |
Value of 'a |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
11 |
| Thunk of unit -> 'a; |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
12 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
13 |
datatype 'a lazy = Lazy of 'a thunk ref; |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
14 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
15 |
fun delay f = Lazy (ref (Thunk f)); |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
16 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
17 |
fun force (Lazy (ref (Value v))) = v |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
18 |
| force (Lazy (s as ref (Thunk f))) = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
19 |
let |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
20 |
val v = f () |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
21 |
val () = s := Value v |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
22 |
in |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
23 |
v |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
24 |
end; |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
25 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
26 |
fun memoize f = |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
27 |
let |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
28 |
val t = delay f |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
29 |
in |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
30 |
fn () => force t |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
31 |
end; |
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
32 |
|
|
028e39e5e8f3
The Metis prover (slightly modified version from Larry);
wenzelm
parents:
diff
changeset
|
33 |
end |