Started sketching inference completeness

There is a statement of a theorem, but I think that the invariants are
not right, yet.
remove %K memory reports

since they seem to always return a useless 0. the %M measure doesn't
look particularly plausible either, but it's probably measuring
something.
fix compiler proofs for changed location of convert_t_def
more opening of the new inferPropsTheory
save calculation of length of ml_repl_module_decls
add missing op datatypes to compiler compset

don't know why they weren't in there before. found out because
compile_call_repl_step_eq wasn't being evaluated fully (but it's
not used anywhere yet... would be used for the machine-code repl
theorems...)
add back old (swapped) version of zHEAP_EL

just for use as a macro in other instructions. the real El(2)
instruction still gets the new version.
(cherry picked from commit 9bbf49635188866c463594553cc60247e878b636)
added support for vector to translator
fix build of BottomUpMergeSortTheory

by changing the state of the parser
delete some now unused commented out broken theorems
move various theorems back into more appropriate places
fix bootstrap_lemmasScript.sml for moved theorems
Start a medium-sized refactoring of the semantics

Instead of a custom env type in the lib.lem, use finite maps where
possible and alists and ALOOKUP where not.
Fix semantics/proofs

Except for 2 lemmas about bootstrapping in evalPropsScript
Some more progress.

Mostly un-finite mapping things. A surprising amount depends on being
able to access various shadowed bindings.
Slow progress fixing the type soundness proof
Progress on type soundness repairs.
add targets dir to the build sequence
Metatheory repaired
Mostly fix translator

Commented out

DeclAssumCons_SNOC_Dtype
DeclAssumCons_cons_lookup

because of the change of type of the constructor environments from lists
to finite maps. Correspondingly, DeclAssumCons lost an ALL_DISTINCT
assumption. I don't know why it was there, unless it was an artifact
from the past when duplicate constructors causes the evaluation to type
error.