src/Pure/General/susp.ML
author wenzelm
Thu Apr 03 18:42:36 2008 +0200 (2008-04-03)
changeset 26538 d65504ffb47d
parent 26063 b2862698dc79
child 28159 80823c582b9d
permissions -rw-r--r--
replaced ETX/EOT by ENQ/ACK, which are less likely to be interpreted by tty etc.;
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@26063
     5
Delayed evaluation.  Supposed to be value-oriented.
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
wenzelm@25317
    31
fun force (ref (Value v)) = v
wenzelm@25317
    32
  | force susp = NAMED_CRITICAL "susp" (fn () =>
wenzelm@25317
    33
      (case ! susp of
wenzelm@25317
    34
        Value v => v   (*race wrt. parallel force*)
haftmann@25310
    35
      | Delay f =>
haftmann@25310
    36
          let
haftmann@25310
    37
            val v = f ();
haftmann@25310
    38
            val _ = susp := Value v;
wenzelm@25317
    39
          in v end));
haftmann@20594
    40
wenzelm@23922
    41
fun peek susp =
wenzelm@23922
    42
  (case ! susp of
wenzelm@23922
    43
    Value v => SOME v
wenzelm@23922
    44
  | Delay _ => NONE);
haftmann@20594
    45
haftmann@20594
    46
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
haftmann@20594
    47
wenzelm@24299
    48
end;