equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/single_assignment_polyml.ML |
|
2 Author: Makarius |
|
3 |
|
4 References with single assignment. Unsynchronized! Emulates |
|
5 structure SingleAssignment from Poly/ML 5.4. |
|
6 *) |
|
7 |
|
8 signature SINGLE_ASSIGNMENT = |
|
9 sig |
|
10 type 'a saref |
|
11 exception Locked |
|
12 val saref: unit -> 'a saref |
|
13 val savalue: 'a saref -> 'a option |
|
14 val saset: 'a saref * 'a -> unit |
|
15 end; |
|
16 |
|
17 structure SingleAssignment: SINGLE_ASSIGNMENT = |
|
18 struct |
|
19 |
|
20 exception Locked; |
|
21 |
|
22 abstype 'a saref = SARef of 'a option ref |
|
23 with |
|
24 |
|
25 fun saref () = SARef (ref NONE); |
|
26 |
|
27 fun savalue (SARef r) = ! r; |
|
28 |
|
29 fun saset (SARef (r as ref NONE), x) = |
|
30 (r := SOME x; RunCall.run_call1 RuntimeCalls.POLY_SYS_lockseg r) |
|
31 | saset _ = raise Locked; |
|
32 |
|
33 end; |
|
34 |
|
35 end; |
|