rework compiler toplevel, towards handling Tmod

Got the tests working with the new definitions of
compile_dec/compile_top, but the proof about compile_dec will be broken.

Tmod case of definition of compile_top still missing.
use new compile_top instead of compile_dec for compile_primitives
start on updating compilerProofs for new compile_dec

probably best to define the Tmod case first, though, since the
definition will probably need to change again a few times...
rework toplevel again, define compile_top for modules

current tests pass, proofs broken.
no tests of modules yet.
a couple of elementary module compilation tests
update proof about compile_fake_exp

simpler now because it either just goes to the end of the code (success)
leaving a new stack satisfying env_rs, or jumps to address 0 with the
old stack plus an exception on top.
start on updating compile_dec theorem

removing the mn = NONE hypothesis makes some subgoals in the case for a
type declaration harder - cheating for now.

will also need theorems about compile_decs and compile_top.
prove cheats in compile_dec_val
Merge branch 'modules'

Although I haven't proved anything about compile_decs or compile_top,
the modules branch is now in as good a state as master was before it
started (i.e. there is a theorem about compile_dec). Also, I want to get
the latest semantics from master, so may as well merge back.
get replCorrect building again

and thoughts on type system part of initial_invariant
add clock field to initial_bc_state