src/HOL/Import/susp.ML

note_thmss, read/cert_vars etc.: natural argument order;
added string_of_thm;
tuned;

(*  Title:      HOL/Import/susp.ML
    ID:         $Id$
    Author:     Sebastian Skalberg, TU Muenchen

Delayed evaluation.
*)

signature SUSP =
sig

type 'a susp

val force : 'a susp -> 'a
val delay : (unit -> 'a) -> 'a susp
val value : 'a -> 'a susp

end

structure Susp :> SUSP =
struct

datatype 'a suspVal
  = Value of 'a
  | Delay of unit -> 'a

type 'a susp = 'a suspVal ref

fun force (ref (Value v)) = v
  | force (r as ref (Delay f)) =
    let
	val v = f ()
    in
	r := Value v;
	v
    end

fun delay f = ref (Delay f)

fun value v = ref (Value v)

end