author | blanchet |
Tue, 02 Oct 2012 01:00:18 +0200 | |
changeset 49681 | aa66ea552357 |
parent 35014 | a725ff6ead26 |
permissions | -rw-r--r-- |
35014
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
1 |
(* Title: Pure/ML-Systems/single_assignment_polyml.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 |
References with single assignment. Unsynchronized! Emulates |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
5 |
structure SingleAssignment from Poly/ML 5.4. |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
6 |
*) |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
7 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
8 |
signature SINGLE_ASSIGNMENT = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
9 |
sig |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
10 |
type 'a saref |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
11 |
exception Locked |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
12 |
val saref: unit -> 'a saref |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
13 |
val savalue: 'a saref -> 'a option |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
14 |
val saset: 'a saref * 'a -> unit |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
15 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
16 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
17 |
structure SingleAssignment: SINGLE_ASSIGNMENT = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
18 |
struct |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
19 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
20 |
exception Locked; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
21 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
22 |
abstype 'a saref = SARef of 'a option ref |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
23 |
with |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
24 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
25 |
fun saref () = SARef (ref NONE); |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
26 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
27 |
fun savalue (SARef r) = ! r; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
28 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
29 |
fun saset (SARef (r as ref NONE), x) = |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
30 |
(r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r) |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
31 |
| saset _ = raise Locked; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
32 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
33 |
end; |
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
34 |
|
a725ff6ead26
explicit representation of single-assignment variables;
wenzelm
parents:
diff
changeset
|
35 |
end; |