src/Pure/General/susp.ML
author wenzelm
Thu Jul 19 23:18:48 2007 +0200 (2007-07-19)
changeset 23863 8f3099589cfa
parent 20594 b80c4a5cd018
child 23922 707639e9497d
permissions -rw-r--r--
tuned signature;
haftmann@20594
     1
(*  Title:      Pure/General/susp.ML
haftmann@20594
     2
    ID:         $Id$
haftmann@20594
     3
    Author:     Sebastian Skalberg and Florian Haftmann, TU Muenchen
haftmann@20594
     4
haftmann@20594
     5
Delayed evaluation.
haftmann@20594
     6
*)
haftmann@20594
     7
haftmann@20594
     8
signature SUSP =
haftmann@20594
     9
sig
haftmann@20594
    10
  type 'a T
haftmann@20594
    11
  val value: 'a -> 'a T
haftmann@20594
    12
  val delay: (unit -> 'a) -> 'a T
haftmann@20594
    13
  val force: 'a T -> 'a
haftmann@20594
    14
  val peek: 'a T -> 'a option
haftmann@20594
    15
  val same: 'a T * 'a T -> bool
haftmann@20594
    16
end
haftmann@20594
    17
haftmann@20594
    18
structure Susp : SUSP =
haftmann@20594
    19
struct
haftmann@20594
    20
haftmann@20594
    21
datatype 'a susp =
haftmann@20594
    22
    Value of 'a
haftmann@20594
    23
  | Delay of unit -> 'a;
haftmann@20594
    24
haftmann@20594
    25
type 'a T = 'a susp ref;
haftmann@20594
    26
haftmann@20594
    27
fun value v = ref (Value v);
haftmann@20594
    28
haftmann@20594
    29
fun delay f = ref (Delay f);
haftmann@20594
    30
haftmann@20594
    31
fun force (ref (Value v)) = v
haftmann@20594
    32
  | force (r as ref (Delay f)) =
haftmann@20594
    33
      let
haftmann@20594
    34
        val v = f ()
haftmann@20594
    35
      in
haftmann@20594
    36
        r := Value v;
haftmann@20594
    37
        v
haftmann@20594
    38
      end;
haftmann@20594
    39
haftmann@20594
    40
fun peek (ref (Value v)) = SOME v
haftmann@20594
    41
  | peek (ref (Delay _)) = NONE;
haftmann@20594
    42
haftmann@20594
    43
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
haftmann@20594
    44
haftmann@20594
    45
end