rework compilation of modules, in particular exceptions

was not resetting to the beginning of the module in the case of an
exception. now we set up a new handler before starting the module, and
keep using that instead of the normal handler around each declaration.

at the end, we put all the module bindings into a tuple, pop the
exception, and pull them all out of the tuple again.

this is unverified: the proofs are broken. the tests still work.
WIP on updating compile_fake_exp_val for new definition of compiler

slowly going through the proof again, dealing with places where the
within-a-module version behaves slightly differently (namely, no
exception handlers wrapped around internal declarations).
more WIP on updating compile_fake_exp_val
more progress on compile_fake_exp_val

finished value case, up to exception case
complete rewrite of compiler interface

The treatment of modules before was slightly too broken in various
places.

The new version has simpler functions for compiling a single
declaration/list of declarations; in particular these functions don't
generate code for top-level exception handlers or printing.

There is a new wrapper function for compiling a list of declarations
(only) that does the exception-handler wrapping and optional printing of
values.

compile_top calls this wrapper for a module (without printing) then does
module output printing itself. For a non-module declaration, it also
calls the wrapper, with a singleton list and printing on, and does
constructor name printing itself if necessary.

For bootstrapping, I imagine we can use this wrapper too, and just live
with the unnecessary exception-handler and module-name-or-output
(printing is on iff there is no module name).

The rewritten implementation passes the compiler tests, but of course
the proofs are completely out of date and broken.
update compile_news_thm (new base case)
prove a theorem characterising compile_Cexp
most of a proof of a theorem about the new compile_fake_exp

not sure the statement is as useful as it needs to be yet, though
prove theorem about compile_fake_exp, with no cheats

but still unsure of statement.
also make a start on trying to state things about compile_dec.
reorganise file, and get decs_contab_thm proof working again
prove first case of a compile_dec_thm
more work on compile_dec_thm
add another invariant to env_rs

that "" is actually bound to tuple_cn
finish compile_dec_thm

require a tweak to the implementation - had forgotten about the
block_tag
wip on a lemma about compile_decs

should probably just go straight to trying to state the main theorem
aobut it though.
start on compile_decs_thm

but want to remove the optimisation for a single dec - the proof is more
uniform if the implementation unwraps the tuple, then immediately
re-wraps it to pop the exception, then unwraps it again. (in the general
case the wrap is of more stuff than just the tuple that was just
unwrapped.)

could prove as a bytecode optimisation that an unwrap followed by a wrap
is a no-op, then compile_decs wouldn't have to special-case. (or could
then define the optimised compile_decs and show it produces equivalent
bytecode.)
remove optimisation from compile_decs{,_wrap}
strengthen compile_dec_thm, and bit more of compile_decs_thm
more lemmas, and work on compile_decs_thm

also still strengthening compile_fake_exp_thm
prove error case of compile_decs_thm

the difficulty has been dealing with the changing contab and cenv, i.e.
figuring out what to put in the statement for which contab and cenv to
use for the exception case. not sure if it's good enough, but using the
final cenv (as if all declarations had gone through, and computed
separately) for this theorem statement. intuitively that matches the
semantics...