restore lex_until_toplevel_semicolon

We will enforce semicolons after declarations, so don't need to be smart
about figuring out when the next declaration starts.

(It would be easy to treat end-of-input as an implicit semicolon too,
but I'm not doing that here.)
make repl_funExamplesTheory print the test cases as it builds
update parser and grammar for single-declarations-followed-by-semicolons

I've left the old REPLPhrase and parse functions intact (to not break
tests, and since they may be independently interesting).

Here I extend the grammar with a REPLTop that takes a single declaration
(or expression). The repl_fun implementation uses parse_top instead of
parse.
make PushExc and PopExc bump the pc
add Stop instruction to bytecode

this is a dummy instruction. when it is reached, that means the code
generated for a decelaration has finished executing (whether it succeeds
or fails).
make compile_dec deal properly with the possibility of an exception

following the scheme that if the generated code raises an exception, we
reset the stack and put a 1 on top (above the exception), otherwise we
update the stack with the new bindings and put a 0 on top.

compiler (emitml) tests and repl_fun (eval) tests still work.
compiler proofs broken.
fix bytecodeExtraTheory for changes to Push/PopExc
fix compileLabelsTheory for changes to Push/PopExc
move some theorems out of compilerProofs into misc and intLangExtra
work towards fixing compile_fake_exp_val

now that it does the extra work of setting up the default exception
handler
update top-level README
Remove uses of HD, replacing with case expressions where possible.
Allow for “validating” parser by adding a flag to mmlParseREPLTop.

This function is called from within parse_def, which doesn’t expose
the flag. I did it this way so that the validation/not decision
wouldn’t contaminate higher-level clients, but changing it does
require a big recompilation. Whoever has the lock on REPL
implementation is welcome to make the flag appear in a higher-level
API.
get proof of compile_fake_exp_val working again
improved support for induction on mutrec functions
bug fix
work towards compile_dec_val, Dlet case

might need to tweak compile_fake_exp_val's statement
make the initial compiler state contain the mapping for the tuple constructor

this saves adding it on every time a declaration is compiled, and also
should make the proofs more uniform.
prove Dlet case of compile_dec_val
finish Dletrec case of compile_dec_val

Dtype case remains.

(Also there's the cheat about equivalent environments in the proof of
compile_fake_exp_val, and the cheats for exceptions in compile_val.)