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