author | bulwahn |
Thu, 07 Jul 2011 23:33:14 +0200 | |
changeset 43704 | 47b0be18ccbe |
parent 40449 | 9c390868d255 |
child 43727 | a0c3de0573d4 |
permissions | -rw-r--r-- |
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32738
diff
changeset
|
1 |
(* Title: Pure/Concurrent/synchronized_sequential.ML |
32736
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
3 |
|
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32738
diff
changeset
|
4 |
Sequential version of state variables -- plain refs. |
32736
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
5 |
*) |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
6 |
|
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
7 |
structure Synchronized: SYNCHRONIZED = |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
8 |
struct |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
9 |
|
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32738
diff
changeset
|
10 |
abstype 'a var = Var of 'a Unsynchronized.ref |
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32738
diff
changeset
|
11 |
with |
32736
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
12 |
|
32738 | 13 |
fun var _ x = Var (Unsynchronized.ref x); |
32736
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
14 |
fun value (Var var) = ! var; |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
15 |
|
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
16 |
fun timed_access (Var var) _ f = |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
17 |
(case f (! var) of |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
18 |
SOME (y, x') => (var := x'; SOME y) |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
19 |
| NONE => Thread.unavailable ()); |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
20 |
|
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
21 |
fun guarded_access var f = the (timed_access var (K NONE) f); |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
22 |
|
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
23 |
fun change_result var f = guarded_access var (SOME o f); |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
24 |
fun change var f = change_result var (fn x => ((), f x)); |
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
25 |
|
f126e68d003d
Dummy version of state variables -- plain refs for sequential access.
wenzelm
parents:
diff
changeset
|
26 |
end; |
40449 | 27 |
|
28 |
fun counter () = |
|
29 |
let |
|
30 |
val counter = var "counter" 0; |
|
31 |
fun next () = |
|
32 |
change_result counter |
|
33 |
(fn i => |
|
34 |
let val j = i + 1 |
|
35 |
in (j, j) end); |
|
36 |
in next end; |
|
37 |
||
32816
5db89f8d44f3
more official status of sequential implementations;
wenzelm
parents:
32738
diff
changeset
|
38 |
end; |