Refactoring for the initial env.

Make the repl semantics parameterised over the initial enviroment, and
move everything about the initial env into the "initial" directory.
Ideally, the metatheory, inference, and compiler proofs won't depend at
all on the initial env. This now is true for everything but
compilerProofScript.
Some re-organisation
Some tweaks.

The plan is to have a series of initial programs. The first just defines
primitive types and exceptions that the compiler needs to know about,
the second will be the rest of the supported basis library, and
subsequent ones (if any) will include any other definitions that should
be in place before the user's program. For example, to support a REPL
with the HOL light kernel already loaded.

Each of the type inference, type soundness, and compiler correctness
proofs rely on an invariant about the various environments and other
inputs that they consume. We can construct these environments by EVALing
the inferencer and compiler on the first initial program, and then
manually proving that the result satisfies the invariant (the completely
empty environments that we will pass to the inferencer/compiler in the
EVAL won't satisfy the invariant). The subsequent initial programs can
be EVALed in the same way (starting from the previously built
initial env), but we can use the inferencer/compiler correctness proofs
to know that the new additions still satisfy the invariants.
fix the compile_prog theorems
Fixes
Define a type "environment".

A big record that should have everything that the semantics, type
system, inferencer and compiler needs. Define a function that takes a
program and runs the clocked interpreter, type inferencer, and compiler
on it and extends the environment.
Small progress
A complete-ish sketch of how the init env should work.
Merge remote-tracking branch 'origin/Word8Array' into init_env

Conflicts:
	compiler/conLang.lem
	compiler/conLangScript.sml
	compiler/proofs/compilerProofScript.sml
	compiler/proofs/conLangProofScript.sml
	compiler/proofs/modLangProofScript.sml
	explorer/pp/allPP.sml
	explorer/pp/astPP.sml
	inference/inferScript.sml
	initial/initialEnv.lem
	initial/initialProgramScript.sml
	metatheory/typeSoundScript.sml
	semantics/initialEnvScript.sml

The conflicts in the following files have not been fixed:

        explorer/pp/allPP.sml
        explorer/pp/astPP.sml
        compiler/proofs/compilerProofScript.sml
fix conflicts in compilerProofScript.sml
Merge remote-tracking branch 'origin/Word8Array' into init_env

Conflicts:
	explorer/pp/allPP.sml
	explorer/pp/astPP.sml
add special compile_initial_prog

for compiling a program that is known to succeed.
also prove half of its correctness theorem (cheat the part about
re-establishing the invariant; will prove later).
Start on refactoring the CakeML compset infrastructure

In each directory dirname, there should be a file compute_dirnameLib.sml
It should contain functions add_whatever_compset that adds theorems and
conversion relevant to the whatever to a given compset. It should also
contain a definition the_dirname_compset that creates a compset with
everything needed to run the various whatevers in dirname.

It doesn't work currently, because label removal in bytecode relies on
el_check which is defined in compiler, but the directories depend the
other way around.

The unify and label removal infrastructure had global state, I've
refactored so that the state is created locally to the add_..._compset
call.
remove dependence on el_check in compute_bytecodeLib.sml
add back definition of el_check to compilerLib.lem

not sure why it got deleted. doesn't appear to have been moved.
update typeSysProps for new location of check_dup_ctors_thm
update conLangProofScript.sml for new location of check_dup_ctors_thm
progress on the cheat in compile_initial_prog_thm

reduced to something about free vars and closed at the prog level
update initialEnv.lem for reorganised AST for App
Update the initial prog. with Word8Array

There is a problem with making primitive types usable in the program.
The type "Word8Array.array" should be there, but without type
abbreviations, there is no way to put it there and have it be the same
as the primitive type of arrays that all of the operations use. The
elaborator can be extended to handle this (just as it handles the
bindings for "int", "bool", etc), but that is less than ideal because
the initial environment doesn't exclusively come from the initial
program.