compiler correctness attempts

Tried to prove that if Cevaluate produces a result then the free
variables of the expression were all in the environment, but that is not
true because of lazy evaluation (of things like pattern-matching and if
statements). Of course in reality the whole expression would have been
type-checked first...

Tried to make progress on exp_to_Cexp_thm1, but the statement may need
to change to either force the environment in the conclusion to have the
free variables of the expression, or to make use of the fact that
evaluate succeeded (i.e. no type error)...
progress on proving revised statement of exp_to_Cexp_thm1

the new statement makes the Cevaluate happen in an environment whose
domain is forced to be the free variables of the expression.

it looks like will need to make exp_to_Cexp mutually recursive with
v_to_Cv (currently it's just undefined on non-literal values; I guess
alternatively could litter proofs with preconditions on the expression)
make exp_to_Cexp and v_to_Cv mutually recursive

also, try to fix everything that breaks because of that, but
in trying to prove v_to_Cv_canonical (or rather exp_to_Cexp_canonical)
it is becoming obvious that the mechanism for dealing with declaration
variables is too complicated and possibly buggy. will need to rethink
the implementation.
tests that might show up problems with declaration variables

I haven't run these tests yet because the testing infrastructure hasn't
kept up with changes to the compiler: currently it can't be emitted, and
I'm rethinking how many of those changes I actually want in the running
compiler and how many can be moved exclusively to the proofs.
get compile testing infrastructure working again

by omitting the equations defining v_to_Cv from the mutually recursive
equations for exp_to_Cexp. (eventually we could define a new version of
exp_to_Cexp that doesn't have those equations and prove it equivalent on
source expressions to the one about which the theorems are proved.)

also tweaked underscore rule, because RENAME_VARS_CONV primes variables
as necessary. but we don't want underscores to be primed. so just rename
them all to "usn" for some number n.

surprisingly, the new tests succeed, so the treatment of declaration
variables may be correct. but it's still too complicated.
another compiler test for variable scoping
major changes to miniml compiler intermediate lang and wrapper

mostly trying to simplify treatement of declarations.

added a dedicated expression to the intermediate language to sit at the
bottom of a declaration, and reference all the declaration variables.

exp_to_Cexp no longer modifies the state, and no longer has its own
state type but just uses the repl state. it doesn't need to modify the
state because pat_to_Cpat and repl_dec take care of updating the map
with new declaration variables. (any other variable mappings made during
descent of the expression can be thrown away because they're local.)
remove number_pat_vars and extend_rs; abstract out two cases in
exp_to_Cexp for reuse in repl_dec.

compiling the new declaration expression toggles a flag in the compiler
state, which compile_bindings reads on return to determine whether to
pop stack variables or not. the compiler state no longer explicitly
tracks whether it was called on a declaration or not.

none of this is tested. (this commit is just a checkpoint.)
more changes to compiler and fix tests

issues were with how compile_bindings, compilation of a CDecl, and
branching expressions interact. the method now is: compilation of CDecl
saves the environment and stack size for the next repl invocation in a
separate slot, and otherwise looks like an expression that returned one
argument onto the stack. therefore things like CIf don't get messed up
by it being on one of the branches. compile_bindings doesn't pop the new
bindings if the body ends in a CDecl, because we leave it up to CDecl to
rearrange the stack completely (this behavior is as before the major
changes).