src/Pure/General/susp.ML
author wenzelm
Thu, 16 Aug 2007 21:52:08 +0200
changeset 24299 91d893799212
parent 24058 81aafd465662
child 25310 2b928fb92f53
permissions -rw-r--r--
force: non-critical, but also non-thread-safe (potentially multiple evaluations);
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
24299
91d893799212 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents: 24058
diff changeset
     5
Delayed evaluation. Supposed to be value oriented; may result in
91d893799212 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents: 24058
diff changeset
     6
multiple evaluations in a multi-threaded environment!
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
     7
*)
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
     8
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
     9
signature SUSP =
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    10
sig
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    11
  type 'a T
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    12
  val value: 'a -> 'a T
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    13
  val delay: (unit -> 'a) -> 'a T
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    14
  val force: 'a T -> 'a
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    15
  val peek: 'a T -> 'a option
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    16
  val same: 'a T * 'a T -> bool
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    17
end
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    18
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    19
structure Susp : SUSP =
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    20
struct
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    21
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    22
datatype 'a susp =
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    23
    Value of 'a
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    24
  | Delay of unit -> 'a;
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    25
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    26
type 'a T = 'a susp ref;
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    27
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    28
fun value v = ref (Value v);
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    29
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    30
fun delay f = ref (Delay f);
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    31
24299
91d893799212 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents: 24058
diff changeset
    32
fun force susp =
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    33
  (case ! susp of
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    34
    Value v => v
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    35
  | Delay f =>
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    36
      let
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    37
        val v = f ();
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    38
        val _ = susp := Value v;
24299
91d893799212 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents: 24058
diff changeset
    39
      in v end);
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    40
23922
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    41
fun peek susp =
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    42
  (case ! susp of
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    43
    Value v => SOME v
707639e9497d marked some CRITICAL sections (for multithreading);
wenzelm
parents: 20594
diff changeset
    44
  | Delay _ => NONE);
20594
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    45
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    46
fun same (r1 : 'a T, r2) = (r1 = r2); (*equality on references*)
b80c4a5cd018 added suspensions in Pure
haftmann
parents:
diff changeset
    47
24299
91d893799212 force: non-critical, but also non-thread-safe (potentially multiple evaluations);
wenzelm
parents: 24058
diff changeset
    48
end;