src/Pure/Concurrent/synchronized_sequential.ML
author haftmann
Thu Oct 22 13:48:06 2009 +0200 (2009-10-22)
changeset 33063 4d462963a7db
parent 32816 5db89f8d44f3
child 33060 e66b41782cb5
permissions -rw-r--r--
map_range (and map_index) combinator
wenzelm@32816
     1
(*  Title:      Pure/Concurrent/synchronized_sequential.ML
wenzelm@32736
     2
    Author:     Makarius
wenzelm@32736
     3
wenzelm@32816
     4
Sequential version of state variables -- plain refs.
wenzelm@32736
     5
*)
wenzelm@32736
     6
wenzelm@32736
     7
structure Synchronized: SYNCHRONIZED =
wenzelm@32736
     8
struct
wenzelm@32736
     9
wenzelm@32816
    10
abstype 'a var = Var of 'a Unsynchronized.ref
wenzelm@32816
    11
with
wenzelm@32736
    12
wenzelm@32738
    13
fun var _ x = Var (Unsynchronized.ref x);
wenzelm@32736
    14
fun value (Var var) = ! var;
wenzelm@32736
    15
wenzelm@32736
    16
fun timed_access (Var var) _ f =
wenzelm@32736
    17
  (case f (! var) of
wenzelm@32736
    18
    SOME (y, x') => (var := x'; SOME y)
wenzelm@32736
    19
  | NONE => Thread.unavailable ());
wenzelm@32736
    20
wenzelm@32736
    21
fun guarded_access var f = the (timed_access var (K NONE) f);
wenzelm@32736
    22
wenzelm@32736
    23
fun change_result var f = guarded_access var (SOME o f);
wenzelm@32736
    24
fun change var f = change_result var (fn x => ((), f x));
wenzelm@32736
    25
wenzelm@32736
    26
end;
wenzelm@32816
    27
end;