delete some commented out code

Mostly to get rid of the word "cheat" from compileCorrectnessScript.sml.
(There are still cheats in expToCexp since I haven't upgraded to the
semantics that does the closure check on equality, and in replScript
since there's basically nothing working in there...)
cleanup

move various theorems to where they might belong, remove some unused stuff.
WIP: new repl_exp_val theorem

things don't quite fit together, but the missing pieces so far seem not
too difficult.
more work towards repl_exp_val

need to say something about compile_code_env next.
more thoughts on repl_exp_val

figuring out how to deal with the previous code environment and its
relationship to the new part that needs to get added...
work towards thm about compile_code_env, but stuck

Because I want to induct on the code env as a list, but the notion of a
good code env just says the free labs of the bodies are anywhere in the
domain, rather than only in the previous part. I.e. I'm using a finite
map but maybe I care about the order. This would be equivalent to making
sure code envs are well founded. There may be a way around all this in
the proof, or otherwise maybe it is worthwhile going back and using a
list throughout... that will break a lot of stuff slightly...
more work on FOLDL_cce_aux_thm

attempting to get around the problem by asserting that every tail of the
code env is good (before it is converted to an fmap). now stuck on
proving which labels are supposed to be distinct/less than which state's
next_label field.
more attempt at cce_aux

probably better to stop trying to prove about code_env_code directly,
but instead prove something stronger that makes the induction work.
finish a proof about FOLDL cce_aux

hopefully it's sufficient...
theorem about compile_code_env
work on repl_exp_val

maybe almost done with it
more repl_exp_val

remaining subgoal is to show that the machine state (i.e. environment
and store) matches the semantic state after running the exp, and this is
almost in the assumptions except the store is (probably) syneq rather
than equal.
more repl_exp_val, and stuck wanting Cv_bv_syneq

I don't think it's true, but there may be a way around this, or else to
change the definition of Cv_bv so that it is true... perhaps it would be
helpful if syneq were reflexive...
change defn of Cv_bv, both compile_val and Cv_bv_syneq proved

one trick was using the reflexive closure of syneq
stuck on Cv_bv_c_SUBMAP

failing attempts to prove alternative versions of syneq_exp_c_SUBMAP.
might need to revisit the definition of syneq_defs yet again...
Initial work on removing the code env.

The idea is to store the closure data in the expression itself, as
opposed to storing labels in the expression that refer to a code
environment mapping labels to closure data. This way, we avoid all the
problems of the map's domain and the labels actually occurring in the
expression getting out of sync.

Have also removed the nz, ez, and ix components of closure data. nz and
ix are obvious from the context of where the thing appears in the
expression. not sure whether ez is actually necessary... will find
out... at least part of it is available from position in the expression
too...
fix minor issues with last commit

next need to define cce_aux, which now needs to traverse the expression
looking for closure data to compile. alternatively could collate them in
a list first... but the traversal needs to happen somewhere, may as well
be here. or label_closures could do it (as before)...

more radically, we could compile the closures on the fly as opposed to
in a separate phase beforehand...
get CompileTheory to build
make cce_aux properly recursive

have to go looking for bodies to compile inside the bodies as well.
prove termination of this definition.
fix mistake in defn of free_vars

tests now pass