src/Pure/General/susp.ML
author wenzelm
Mon, 23 Jul 2007 14:06:12 +0200
changeset 23922 707639e9497d
parent 20594 b80c4a5cd018
child 24058 81aafd465662
permissions -rw-r--r--
marked some CRITICAL sections (for multithreading);
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
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    31
fun force susp = CRITICAL (fn () =>
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    32
  (case ! susp of
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    33
    Value v => v
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    34
  | Delay f =>
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    35
      let
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    36
        val v = f ();
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    37
        val _ = susp := Value v;
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    38
      in v end));
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    39
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    40
fun peek susp =
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    41
  (case ! susp of
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    42
    Value v => SOME v
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    43
  | Delay _ => NONE);
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    44
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    45
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    46
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    47
end