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