src/Pure/General/susp.ML
author wenzelm
Tue, 18 Sep 2007 18:05:34 +0200
changeset 24633 0a3a02066244
parent 24299 91d893799212
child 25310 2b928fb92f53
permissions -rw-r--r--
moved Tools/integer.ML to Pure/General/integer.ML;

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

Delayed evaluation. Supposed to be value oriented; may result in
multiple evaluations in a multi-threaded environment!
*)

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 susp =
  (case ! susp of
    Value v => v
  | Delay f =>
      let
        val v = f ();
        val _ = susp := Value v;
      in v end);

fun peek susp =
  (case ! susp of
    Value v => SOME v
  | Delay _ => NONE);

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

end;