progress on compiler correctness proof

Start a lemma about the semantics of intermediate language: Can
remove/add unnecessary variables from/to the environment.  This is not
currently true because junk variables get stored in closure
environments, however I plan to restrict closure environments to
occurring variables for the intermediate language semantics. (They are
already canonicalised to some extent by being sorted.)

Prove a lemma about how Cpmatch is equivalent to a match in the empty
environment followed by merging with the original environment (i.e. its
argument is an accumulator).

Improve definition of Cpmatch: it now fails more often (in the case of
type errors).

Various improvements to definition of Cevaluate along the same lines.
Eventually Cevaluate may need to look more like evaluate (and take a
constructor environment).
canonicalise closure environments in intermediate language

I think because of the changes to v_to_Cv, whereby we restrict
environments to only mention variables free in the body, it's no longer
necessary to sort the environments, because we go through alist_to_fmap
and fmap_to_alist... but I'm keeping the sorting as well for now anyway.
(I was surprised by a subgoal now being solved without any mention of
sorting.)
slow progress on compiler correctness

mainly trying to prove that adding/removing junk from environments is
allowed by the semantics of the intermediate language. this is
significantly complicated by closures, and relies on the intermediate
language semantics forcing canonical environments for its closures.

defined, programmatically, EVERY_Cexp and EVERY_Cv for mapping over
those types with a predicate. a little complicated because of the mutual
recursion between them.
more slow progress on compiler correctness

Made force_dom take a default value so that we can still know something
good about the values in the environments stored in closures in badly
typed terms.

Tried fixing EVERY_Cexp to be more (mutually) recursive, but termination
proofs become impossible. Instead, made it easy to automatically define
instances of EVERY_Cexp P from the interesting equations for P (i.e.
automatically fill out the recursion).

Fixed semantics of Cevaluate for calling recursive closures: was putting
the index rather than the name as the last component of the CRecClos
generated for the environment in which to evaluate the body. Also need
to canonicalise the environment for those CRecClos's. But now thinking
perhaps it would be better to simply check closures have good
environments everywhere in Cevaluate, and also force good environments
for anything it produces... i.e. move the proof of that fact into the
definition.
make int.lang. semantics canonicalise all values recursively

this should make proving that it generates canonical values trivial. a
canonical value is one where all closures have canonical environments,
recursively throughout the value.

proved that the function for making a value canonical generates
something for which the predicate for testing canonicity holds.
proved that int.lang. semantics always generates canonical values

although the proof doesn't look completely trivial, this result is
basically baked into the new definition of the semantics.
progress on Cevaluate_any_env
compiler correctness progress: finish Cevaluate_any_env

i.e. that you can add and remove junk to environments in the
intermediate language semantics.

make doPrim2 return an option so it becomes totally specified

experimentation with THEN1 instead of TRY in the proofscript, and
abstracting out some common bits of tactic. the proof still probably
takes longer than it should to replay.