Just getting started with 2D arrays in PseudoC semantics.
Get PseudoC semantics to build with new handling of arrays.

The semantics gets a deal simpler, because AssignVar has disappeared,
and so too has the dexpr type. The only thing the latter loses us is
that index calculation for array assignments can't be interleaved with
data-reads. Instead, the address of an lvalue is calculated all at
once, when the RHS is ready to go.

Lots else does not build.
Progress with updating proofs to work with 2darrays
Separate memory accesses from expressions.

The two types are mutually recursive. This does cause dexprs to return
though because maccesses don't include values, and dexprs need to, as
that's what they evaluate when the reads are evaluated, as part of
interleaving evaluation.
Make Opns return Errors if any of their inputs are Array values.

Also define and use an isArray predicate in more places.
Progress with "Pseudo C properties" in light of multidimensional arrays
Complete revisions to Pseudo C "properties" theory.

The important lemma about writes ("actions") and expression evaluation
commuting has to pick up a new condition: the expression evaluation
can't involve any reads of whole arrays. As it happens, this is
guaranteed by the condition that the evaluation of the expression not
result in an error or an array value.
More strictness in evaluation of assignment rhses.

Error and Array values in dexprs will cause Aborts.
Progress with hierarchical DAGs and multidimensional arrays.

Straightforward so far, and I think it should stay that way.
Prove the graphOf construction works in multi-dim array world
Delete naive graph theory

Trying to get this old theory/approach to work in the multi-dim array
world isn't worth the effort
Remove trailing whitespace in fastwaveScript.sml
Get fastwave theory to build in light of multi-dim arrays.
Merge from master for fixes to evalpc.ML
Fix symbolic evaluator so that fastwave executes again.

Makes it to 100 steps, so it must be right.