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