src/HOL/Import/susp.ML
changeset 17802 f3b1ca16cebd
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Import/susp.ML	Sat Oct 08 22:39:40 2005 +0200
     1.3 @@ -0,0 +1,41 @@
     1.4 +(*  Title:      HOL/Import/susp.ML
     1.5 +    ID:         $Id$
     1.6 +    Author:     Sebastian Skalberg, TU Muenchen
     1.7 +
     1.8 +Delayed evaluation.
     1.9 +*)
    1.10 +
    1.11 +signature SUSP =
    1.12 +sig
    1.13 +
    1.14 +type 'a susp
    1.15 +
    1.16 +val force : 'a susp -> 'a
    1.17 +val delay : (unit -> 'a) -> 'a susp
    1.18 +val value : 'a -> 'a susp
    1.19 +
    1.20 +end
    1.21 +
    1.22 +structure Susp :> SUSP =
    1.23 +struct
    1.24 +
    1.25 +datatype 'a suspVal
    1.26 +  = Value of 'a
    1.27 +  | Delay of unit -> 'a
    1.28 +
    1.29 +type 'a susp = 'a suspVal ref
    1.30 +
    1.31 +fun force (ref (Value v)) = v
    1.32 +  | force (r as ref (Delay f)) =
    1.33 +    let
    1.34 +	val v = f ()
    1.35 +    in
    1.36 +	r := Value v;
    1.37 +	v
    1.38 +    end
    1.39 +
    1.40 +fun delay f = ref (Delay f)
    1.41 +
    1.42 +fun value v = ref (Value v)
    1.43 +
    1.44 +end