Start to put cenv and menv in closures in eval'
Started to put envC & envM in closures in the main semantics.

This is a bit of an experiment, but it should work like this:

- The main semantics has the module and closure environments in the
  closures.

- This should make like easy for the translator, and it shouldn't be too
  hard for the type soundness proof or the big/small step equivalence
  proof.

- The current semantics will be renamed to evaluate', and moved into the
  compiler correctness proof directory.

- The current evaluate' semantics will be dropped.

- The compiler proof will get an extra first step that says if a program
  does not raise an exception (in the new extended closure semantics),
  then it has the same result in evaluate'. The IL generation phase
  should be able to run from there without change (except for some
  renaming).

Thus, we get a nice semantics, don't have to alter the compiler proofs,
and get the removal of closure and module environments from the closures
as an optimisation phase (with the identity optimisation function, since
the source code isn't actually changes). In the future, we might be able
to remove other things from the closures here, too.
Massive and tedious refactoring started.

With the menv end cenv in the closures now, it makes no sense for them
to be separate arguments to all of the functions.
Refactor all metatheory except type soundness
Some work on type soundness.

This will require more plumbing than I initially thought, since the cenv
and menv can now change from step to step.
Merge remote-tracking branch 'origin/master' into cenv_close
New invariants for type soundness. Proofs broken.
Work in progress on the type soundness.

Putting the module environment in closures complicates thing more than I
anticipated, because the typing relation for values now has to be in mutual
recursion with the typing relation for modules.
Grinding through type soundness again

At least I think the invariant is correct now.
Further tweak the semantics.
More type soundness progress.

But the system is still not quite right for non-global cenvs.
Good progress on type soundness.
Get the type soundness working for expressions.

Next step, declarations.
Type soundness proves again
Meta-theory builds again
Some work on the translator.
Work on the translator.

Proved the theorems in ml_translateScript.sml up until they start
obviously dealing with the cenv. I guess these are likely to change
significantly, or be obsolete, now.
Abstracted some types to allow a little bit of reuse
Minor fixes
Update for Conv change

Constructor values now record the type that is constructed, and the
printer needed to be updated for that.