Add a more generic version of word_preludeScript.sml

This translates various word functions (as in the original
word_preludeScript.sml, which is still under other-examples) according
to a word size argument.

It's not ideal because:
  - The translator doesn't let you specify names of constants, so you
    end up with word_add, word_add_1, word_add_2, where word4_add,
    word8_add, word16_add would be more informative.
  - One could probably instead translate some generic functions that
    take the word size argument in CakeML (rather than during
    translation-time).
translate word_1comp
tweaks to word_prelude
move parts of compileReplDecsScript into repl_compute

not sure that all of this makes sense: some of the stuff is
bootstrap-specific. but the idea is to make it reusable for other times
we might want to evaluate the compiler in the logic.
better error message when translator encounters a non-datatype

make it show what type it was trying to translate
start work on verified MIPS simulator

As mentioned in the comments in the file, our translation of words into
CakeML probably needs to be changed, although exactly how needs to be
discussed. At the moment, it makes this kind of translation cumbersome
since I have to specify the type of each use of all the polymorphic word
constants. (This could be ameliorated somewhat by more automation.)
A draft bytecode interpreter in C.

This in untested so far, but I hope to be able to use it in benchmarking
to get a coarse understanding of how much of performance relies on the
ML->bytecode compiler and how much on the bytecode->x86 compiler.
Merge remote-tracking branch 'origin/master' into exn
Repair some of the _closed lemmas in replCorrect.

The script now progresses up to some broken theorems about printing.