Updated as far as type_grammar.sml

Convert type-grammars to use deltas for updates

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

Polish type-grammar pretty-printing

Provide a hide_tyop function on type_grammars

The result of hide_tyop s is that the bare type-operator/abbrev name s
will no longer map to anything; the standard parser will stop parsing
when it sees such a name.

Unify handling of type abbrevs and type operators

This is analogous to what is done with terms, where the handling of
genuine constants passes through the overload map.

The main desirable effect should be that if multiple genuine type
operators with the same name are in the grammar, then only one will
print unqualified; all the others will print with theory-qualification.

Currently fails in src/datatype's selftest as ParseDatatype doesn't see
bare names that are existing types as possible occurrences of recursive
types.

Add preliminary, unused delta type for type grammars

Move type_grammar datatype decls into new _dtype struct

Implement theory namespaces for type abbreviations

Closes #168

Clean up type grammars to reflect reality of suffixes as tightest operators.

Also, fix a minor pretty-printing bug that was affecting types like

('a + 'b) [32]

and document this in src/n-bit/selftest.sml

Functions to list specific overloads/abbrevs, and to print without them

Add the following functions to Parse:
pp_overloads_on s
print the parsing and printing overloads associated with the token s

pp_abbrev s
print the type abbreviations associated with the token s

pp_term_without_overloads_on (ls : string list)
print a term without applying any overloads on the tokens in ls

pp_term_without_overloads (ls : (string * term) list)
same as above, but specify the overloads to remove more precisely

pp_type_without_abbrevs (ls : string list)
print a type without using any abbreviations on tokens in ls

Also add printing versions, with the prefix "pp_" replaced by "print_",
which don't need a ppstream and print to stdout. For the last three
functions, also add "print_backend_" versions.

Also add string versions of the last three functions, with the prefix
"pp_" removed and the suffix "_to_string" or "_to_backend_string" added,
which don't need a ppstream and return a string.

Apart from Parse.sig, also modify two other signatures:

Reveal the function structure_to_type in type_grammar, and

Add the function gen_remove_mapping to Overload, which removes an
arbitrary overload to a term, since remove_mapping can only handle
overloads to constants.

Move theory min's grammars into {type,term}_grammar (out of Parse).

Fix a bug that allowed type abbreviations to be applied to more type
arguments than expected. E.g.,

type_abbrev("foo", ``:bool``)

followed by

``:'a foo``

used to work. No more!

Removed trailing whitespace from all .sml and .sig files.

This affects over 900 files and was done using emacs's delete-trailing-whitespace
function in batch mode. Building the system with Poly/ML and Moscow ML seems to
work, so I'm hoping these changes don't break anything. Please complain if
they do!

Update to support ty1[ty2] syntax for array types. This means that a
32-bit word type now prints and parses as :bool[32]. I haven't quite
managed to rebuild all of the system (because I'm about to go to bed),
but I'm pretty confident the change won't break anything serious.
Where it might break things is in input such as

f:num list -> bool [3;4]

The above used to work, but is pretty unlikely. It will now break
because the type parser will grab the [ token that used to "belong"
only to the term level.

My change to type grammars (allowing for printing of abbreviations) silently
invalidated an assumption in EmitML about taking grammars apart and putting
them back together again. So, I add a new entry-point in type_grammars to
allow deletion of type operators by their infix names. This then allows
the EmitML behaviour to be recoded.
Also extend the type_grammar pretty-printer so that it shows which
abbreviations are not being printed.

Type abbreviations now print by default. Where this is "problematic",
as with the set and bag abbreviations, this printing can be turned off
by calling disable_tyabbrev_printing, which takes the abbreviation name
as an argument. (There is also a trace variable controlling tyabbrev
printing globally.)
Bag and set abbreviations are "problematic" because if left on they
do things like
- type_of ``(/\)``;
> val it = ``:bool -> bool set`` : hol_type
and
- type_of ``(+)``;
> val it = ``:num -> num multiset`` : hol_type
This code isn't done yet because it doesn't pick between multiple possibilities
in an intelligent way. The heuristic I want to implement will take the most
specific abbreviation first, and then the most recently asserted if two
are equally specific.

Adapting to new Basis (and SML/NJ).

New function to allow abbreviation removal.

Not sure what has been added here. Probably trivial.

Implementation of "parse only" type abbreviations. The main function to
use is type_abbrev : (string * hol_type) -> unit

If the hol_type has type variables in it, then these become parameters to
the string, making it an abbreviation for a type operator. E.g.,
type_abbrev("set", ``:'a -> bool``)
allows you to write ``:num set``.

No attempt to pretty-print types in accordance with stored abbreviations,
so the system will spit back ``:num -> bool`` in response to this. (Hey,
if it's good enough for Moscow ML, it's good enough for us.)

Also split off type_grammars into their own source module.