| author | wenzelm | 
| Thu, 18 Aug 2011 15:37:01 +0200 | |
| changeset 44265 | b94951f06e48 | 
| 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.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!  | 
| 
 
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  | 
signature SINGLE_ASSIGNMENT =  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
8  | 
sig  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
9  | 
type 'a saref  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
10  | 
exception Locked  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
11  | 
val saref: unit -> 'a saref  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
12  | 
val savalue: 'a saref -> 'a option  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
13  | 
val saset: 'a saref * 'a -> unit  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
14  | 
end;  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
15  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
16  | 
structure SingleAssignment: SINGLE_ASSIGNMENT =  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
17  | 
struct  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
18  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
19  | 
exception Locked;  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
20  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
21  | 
abstype 'a saref = SARef of 'a option ref  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
22  | 
with  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
23  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
24  | 
fun saref () = SARef (ref NONE);  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
25  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
26  | 
fun savalue (SARef r) = ! r;  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
27  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
28  | 
fun saset (SARef (r as ref NONE), x) = r := SOME x  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
29  | 
| saset _ = raise Locked;  | 
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
30  | 
|
| 
 
a725ff6ead26
explicit representation of single-assignment variables;
 
wenzelm 
parents:  
diff
changeset
 | 
31  | 
end;  | 
| 
 
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;  |