Add string and character stuff to the basis

Committing to a branch, because it breaks the build. The necessary
theorem that the basis evaluates to SOME rather than NONE no longer
proves.

Ideally, this theorem could be proved by evaluation, but you run into
the following problem.

Suppose that we have

val f x = 1;
val g x = 1;
val h x = 1;

Then after f, the environment is

(f|->Closure [])

after g, it's

(g|->Closure [(f|->Closure [])]),
(f|->Closure [])

and after h it's

(h|->Closure [(g|->Closure [(f|->Closure [])]),(f|->Closure [])]),
(g|->Closure [(f|->Closure [])]),
(f|->Closure [])

As you can see it grows exponentially, although there is the possibility
of sharing since each Closure simply duplicates the environment as it
stands. Possible fixes:

1) Alter the semantics so that there is a heap for environment frames to
go in. Then the semantics itself can express the sharing. This would
probably complicate the translator and any future reasoning about CakeML
programs.

2) Make a super smart EVAL that keeps let bindings at the top of the
term to capture the sharing. So when you're about to put (f|->Closure
[]) into g's closure, you go to
let frame1 = (f|->Closure []) in (g|->Closure [frame1]),frame1
This is the shallowly embedded version of 1. It seems hard, but might
be of general use.

3) Make another interpreter for CakeML that does 1, but then have a
custom conversion that maps the heap-threaded environments onto normal
environments using the let technique of 2 to maintain all of the
sharing. I worry that this is more work than it's worth.
fix proof of basis_sem_env_SOME

just using abbreviations within the tactic proof, c.f. issue #6
Merge remote-tracking branch 'origin/master' into string_basis