author | haftmann |
Wed, 03 May 2006 17:41:28 +0200 | |
changeset 19554 | bc0bef4a124e |
parent 17802 | f3b1ca16cebd |
permissions | -rw-r--r-- |
17802
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: HOL/Import/susp.ML |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
2 |
ID: $Id$ |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
3 |
Author: Sebastian Skalberg, TU Muenchen |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
4 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
5 |
Delayed evaluation. |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
6 |
*) |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
7 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
8 |
signature SUSP = |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
9 |
sig |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
10 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
11 |
type 'a susp |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
12 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
13 |
val force : 'a susp -> 'a |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
14 |
val delay : (unit -> 'a) -> 'a susp |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
15 |
val value : 'a -> 'a susp |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
16 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
17 |
end |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
18 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
19 |
structure Susp :> SUSP = |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
20 |
struct |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
21 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
22 |
datatype 'a suspVal |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
23 |
= Value of 'a |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
24 |
| Delay of unit -> 'a |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
25 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
26 |
type 'a susp = 'a suspVal ref |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
27 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
28 |
fun force (ref (Value v)) = v |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
29 |
| force (r as ref (Delay f)) = |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
30 |
let |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
31 |
val v = f () |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
32 |
in |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
33 |
r := Value v; |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
34 |
v |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
35 |
end |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
36 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
37 |
fun delay f = ref (Delay f) |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
38 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
39 |
fun value v = ref (Value v) |
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
40 |
|
f3b1ca16cebd
moved susp.ML, lazy_seq.ML, lazy_scan.ML to HOL/Import;
wenzelm
parents:
diff
changeset
|
41 |
end |