| author | kleing | 
| Thu, 03 Nov 2011 18:10:13 +1100 | |
| changeset 45323 | df7554ebe024 | 
| 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; |