First stab sketching out semantics of word8 arrays.

Only looked at the AST and big step semantics so far. Looks to be a much
more far-reaching change than I had imagined. The type of the store has
to change. The organisation of the AST probably needs some careful
consideration to avoid complexity.
make Aalloc an op by reworking do_app

do_app is now split into do_opapp and do_app. The former returns a new
environment and expression whereas the latter returns a result. Both
become simplified by this division.
fix up the small step semantics definition

and minor tweak to bigStep to make it build
get replTheory to build

just change a type annotation
make explicit op <> Opapp in one of the app cases

this is implicitly true because of do_app's definition, but this way the
determinism proof doesn't need to expand that definition.
fix up evalPropsTheory
add missing case to big step

when opapp fails
fix up bigClockTheory
fix up interpTheory
Begin some refactoring.

Fix the word8Array primitives to raise Size exceptions on bad indices.
Add the word8Array primitives to the type system.  Refactor the
semantics to have 1 do_app for primitives of any number of arguments
(instead of do_app for 2 arg prims, and do_uapp for 1 arg). This will be
more flexible as we start to add more primitives, e.g. array update with
3 args.
Fix semantics/proofs
Tweak the small-step semantics

To support 0-ary application as in the big step
Get the big/small equivalence building

But with lots of cheats in
Fix some proofs
More progress on type soundness

The type of a store updated to take into affouct the new difference
between Refv and W8arrays that can be in the store.
Make metatheory build

There are significant cheats dealing with the new application form and
new primitives in bigSmallEquiv and typeSoundness
Some progress on fixing the translator
More translator fixes
Merge remote-tracking branch 'origin/master' into Word8Array
Finish type soundness proof (again)