src/Pure/General/susp.ML

added is_reflexive;

(*  Title:      Pure/General/susp.ML
    ID:         $Id$
    Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen

Delayed evaluation.
*)

signature SUSP =
sig
  type 'a T
  val value: 'a -> 'a T
  val delay: (unit -> 'a) -> 'a T
  val force: 'a T -> 'a
  val peek: 'a T -> 'a option
  val same: 'a T * 'a T -> bool
end

structure Susp : SUSP =
struct

datatype 'a susp =
    Value of 'a
  | Delay of unit -> 'a;

type 'a T = 'a susp ref;

fun value v = ref (Value v);

fun delay f = ref (Delay f);

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

fun peek (ref (Value v)) = SOME v
  | peek (ref (Delay _)) = NONE;

fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)

end