author | hoelzl |
Wed, 02 Apr 2014 18:35:01 +0200 | |
changeset 56369 | 2704ca85be98 |
parent 35014 | a725ff6ead26 |
permissions | -rw-r--r-- |
35014
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/Concurrent/single_assignment_sequential.ML |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
3 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
4 |
Single-assignment variables (sequential version). |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
5 |
*) |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
6 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
7 |
structure Single_Assignment: SINGLE_ASSIGNMENT = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
8 |
struct |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
9 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
10 |
abstype 'a var = Var of 'a SingleAssignment.saref |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
11 |
with |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
12 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
13 |
fun var _ = Var (SingleAssignment.saref ()); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
14 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
15 |
fun peek (Var var) = SingleAssignment.savalue var; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
16 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
17 |
fun await v = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
18 |
(case peek v of |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
19 |
SOME x => x |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
20 |
| NONE => Thread.unavailable ()); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
21 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
22 |
fun assign (v as Var var) x = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
23 |
(case peek v of |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
24 |
SOME _ => raise Fail "Duplicate assignment to variable" |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
25 |
| NONE => SingleAssignment.saset (var, x)); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
26 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
27 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
28 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
29 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
30 |