src/Pure/General/susp.ML
author wenzelm
Sun, 07 Sep 2008 22:20:08 +0200
changeset 28159 80823c582b9d
parent 26063 b2862698dc79
child 28349 46a0dc9b51bb
permissions -rw-r--r--
opaque signature constraint abstracts local type abbrev;
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
26063
b2862698dc79 tuned whitespace
haftmann
parents: 25317
diff changeset
     5
Delayed evaluation.  Supposed to be value-oriented.
20594
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
28159
80823c582b9d opaque signature constraint abstracts local type abbrev;
wenzelm
parents: 26063
diff changeset
    18
structure Susp :> SUSP =
20594
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
25317
8b38b394fa8e fixed spelling;
wenzelm
parents: 25310
diff changeset
    31
fun force (ref (Value v)) = v
8b38b394fa8e fixed spelling;
wenzelm
parents: 25310
diff changeset
    32
  | force susp = NAMED_CRITICAL "susp" (fn () =>
8b38b394fa8e fixed spelling;
wenzelm
parents: 25310
diff changeset
    33
      (case ! susp of
8b38b394fa8e fixed spelling;
wenzelm
parents: 25310
diff changeset
    34
        Value v => v   (*race wrt. parallel force*)
25310
2b928fb92f53 CRITICAL force
haftmann
parents: 24299
diff changeset
    35
      | Delay f =>
2b928fb92f53 CRITICAL force
haftmann
parents: 24299
diff changeset
    36
          let
2b928fb92f53 CRITICAL force
haftmann
parents: 24299
diff changeset
    37
            val v = f ();
2b928fb92f53 CRITICAL force
haftmann
parents: 24299
diff changeset
    38
            val _ = susp := Value v;
25317
8b38b394fa8e fixed spelling;
wenzelm
parents: 25310
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;