src/HOL/Import/susp.ML
author haftmann
Wed, 03 May 2006 17:41:28 +0200
changeset 19554 bc0bef4a124e
parent 17802 f3b1ca16cebd
permissions -rw-r--r--
added world map
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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