| author | wenzelm | 
| Thu, 30 Apr 2015 15:58:15 +0200 | |
| changeset 60159 | 879918f4ee0f | 
| 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; |