add Locations to the observable values

Assuming printing will be done in the context of an actual store, I am
leaving the "observable value" as a location containing an address.
Also, assuming that the addresses are the same between languages
(source, intermediate, bytecode).

Alternative approaches:
  - make conversion to observable values take a store argument and do
    lookups (but then how to deal with cycles?)
  - (if necessary) provide a translation between addresses in different
    languages as an argument (just as we currently translate from
    numeric tags to constructor names)
start work on updating compileCorrectnessTheory

leaving the new expression constructors out of the language subset, but
need to account for the store everywhere, and also many theorems are on
the unrestricted language anyway.
make compiled code push a unit after ref update

Make prim2_to_bc return a list of bytecode instructions rather than a
single one. This is probably better than making the bytecode Update
instruction generate the unit value, because sometimes I might not want
it (e.g. when manipulating internal references used for closures).
split CUpd off as a separate expression constructor

This leaves Cprim2 in its simpler original form, for pure operations
only. On balance, having another Cexp constructor is slightly less bad
than the baggage of lists and the store in CevalPrim2, and new proofs
now don't have to be done inside a case split of old proofs.