Variables are self-explanatory, they are changing, i.e. they are mutable. This means our implementations of new, deref, and set can be used to implement variables.
Variable Declaration
We can using a sequencing assignment (:=) to help declare and set variables. We can also use bind and new to create an identifier and location to store our value in.
(var x := t1 in t2) == (bind x = new t2 in t2)
This just makes x a location that contains the value we want to store.
Variable Dereference
Because all variables are just identifiers bound to locations we have to dereference them to get a useable value.
(x + 1) == ((deref x) + 1)
or in our interpreter (roughly)
eval e st (Var x) = (deref (lookup x e) st)
Variable Assignment
We can again use the walrus operator to force sequencing.
(x := t1) == (set x t1)
We have to evaluate t1 as locations only point to values. So the order of operations would go as such.
- Evaluate the right side of the walrus operator (
:=) to get a value - Store the value in x