src/Pure/General/susp.ML
author wenzelm
Thu, 02 Jun 2005 09:11:32 +0200
changeset 16179 fa7e70be26b0
parent 14278 ae499452700a
permissions -rw-r--r--
header;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
16179
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     1
(*  Title:      Pure/General/susp.ML
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     2
    ID:         $Id$
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     3
    Author:     Sebastian Skalberg, TU Muenchen
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     4
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     5
Delayed evaluation.
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     6
*)
fa7e70be26b0 header;
wenzelm
parents: 14278
diff changeset
     7
14278
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     8
signature SUSP =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
     9
sig
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    10
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    11
type 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    12
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    13
val force : 'a susp -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    14
val delay : (unit -> 'a) -> 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    15
val value : 'a -> 'a susp
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    16
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    17
end
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
structure Susp :> SUSP =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    20
struct
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    21
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    22
datatype 'a suspVal
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    23
  = Value of 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    24
  | Delay of unit -> 'a
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    25
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    26
type 'a susp = 'a suspVal ref
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    27
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    28
fun force (ref (Value v)) = v
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    29
  | force (r as ref (Delay f)) =
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    30
    let
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    31
	val v = f ()
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    32
    in
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    33
	r := Value v;
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    34
	v
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    35
    end
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    36
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    37
fun delay f = ref (Delay f)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    38
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    39
fun value v = ref (Value v)
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    40
ae499452700a Added lazy sequences and parser combinators for same.
skalberg
parents:
diff changeset
    41
end