Fix src/emit (phew!)

Convert type-grammars to use deltas for updates

This is very much analogous to what has been done for term grammars.

Fix EmitML in light of change to ParseDatatype API

Remove trailing whitespace in EmitML.sml

Get EmitML to compile again

pattern match support for emitML

this is a very first version. It still needs plenty of testing.

Get EmitML to handle polymorphic records correctly

Tests in src/emit/theory_tests.

Closes github issue #173

emit: improved whitespace in autogenerated ML code

Fix the breakage to records and EmitML caused by 6da728bc

Fix flow-on bugs in EmitML from changing EmitTeX.

Require failed emitML calls to cleanup (probably broken) ML files

Close #157 : failure to emit ML lets exn propagate all the way out

Attempt to address issue #109.

I don't know if this works because the report "sometimes fails" doesn't give me much to go on.

Put some syntax operations for bool$IN into boolSyntax.

Fix bug whereby IN was stored incorrectly in ConstMap.

Continued fallout from #52.

Now also emit valid Caml for MEM again.

Emit valid SML for MEM once more.

Make export message from EmitML more compact.

Fix bug whereby emitted theories would not load when Unicode is turned off.

Patch generation of Caml code, which hadn't been working for some time. Also
address some problems with WORDS_EMIT_RULE and avoid ML reserved word, e.g.
"op" now gets mapped to "op_".

Avoid warning messages when loading EmitML under Poly/ML.

Make the interface supported by Unicode slightly richer so that I can
make the Unicode not-equals not overlap entirely with <>, thereby
allowing <> to be used both for word_slice and for not-equals, without
it inheriting the \neq symbol when Unicode is on.

Ensure that the Unicode trace is off when calls to EmitML happen.

Last Substring.all --> Substring.full, I hope. Certainly this is
fairly late in the build sequence so I feel confident. I haven't done
any selftests or example checking however.

Changes to EmitML.

Implement ML code generation for large records.

Attempt to tidy up (fix) EmitML and finish off the transition that Scott
started. EmitML has been moved to the end of the build sequence. "Hooks"
have been eliminated and all EmitML related stuff has been removed from the
various theory directories. All code for generating ML/Caml is now
self-contained within src/emit. I've not tested the generated Caml code but
the SML seems to build fine.

The directories:

src/theoryML
src/theoryOcaml
src/emitScript

have been replaced by

src/emit/theories/ML
src/emit/theories/Caml
src/emit/theories

Suppress auto-emission ML definitions of
size functions for datatypes. This has not
been much used, I think, and was generating
the incorrect (i.e. not compilable in ML where strings
are a primitive type) size function for strings.
In the new world of string = char list,
the size of a string would be defined as
list_size char_size. But that doesn't typecheck.

Rework code here to allow more type-specific versions of constants to
map to different data. Thus, we can support APPEND mapping to
listML.APPEND everywhere except on char list -> char list -> char
list, where it can map to stringML.STRCAT.

Add integer operations to EmitML.

Added EmitML.emitCAML for exporting to Ocaml. This has required a fair
amount of hackery, none of which should effect emitML. In particular,
CAML constructors must start with an uppercase letter and other values
must not. Also, types can't start with a lowercase letter. Constructors
are added to the constants map with ConstMapML.insert_cons.

(I will eventually check-in the script for generating CAML versions of the
code emitted to src/theoryML.)

Moved EmitML code to a new directory src/emit.

Added a new structure EmitTeX. This allows HOL theories to be printed
as LaTeX source.

Added both of these structures to help/src/Keepers.sml