src/Pure/General/susp.ML
author skalberg
Sun, 13 Feb 2005 17:15:14 +0100
changeset 15531 08c8dad8e399
parent 14278 ae499452700a
child 16179 fa7e70be26b0
permissions -rw-r--r--
Deleted Library.option type.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     1
signature SUSP =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     2
sig
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     3
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     4
type 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     5
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     6
val force : 'a susp -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     7
val delay : (unit -> 'a) -> 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     8
val value : 'a -> 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     9
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    10
end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    11
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    12
structure Susp :> SUSP =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    13
struct
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    14
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    15
datatype 'a suspVal
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    16
  = Value of 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    17
  | Delay of unit -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    18
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    19
type 'a susp = 'a suspVal ref
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    20
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    21
fun force (ref (Value v)) = v
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    22
  | force (r as ref (Delay f)) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    23
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    24
	val v = f ()
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    25
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    26
	r := Value v;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    27
	v
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    28
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    29
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    30
fun delay f = ref (Delay f)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    31
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    32
fun value v = ref (Value v)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    33
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    34
end