Fix type-grammar becoming unprintable because of a stale tyop

In particular, if a tyop name is reused but picks up a different
arity, a grammar's type abbreviation information might think that
an abbreviation using that tyop is still valid.

Clean up handling of type_grammar deltas and interaction with Thyops

Need a slightly better interface for querying the kernel name
signature information for types, and also alter term functions to not
return constants that don't have up-to-date types.

Now deleting a type doesn't result in broken theories.

With a regression test.

Closes #179

Implement "input only type abbreviations"

Closes #599

Fix type-grammar pretty-printing; include regression test

Updated as far as Pretype.sml

Still no use of smpp tech.

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.

Move type_grammar datatype decls into new _dtype struct

Fixes and tests arising from namespacing tyabbrevs

Document how to remove/disable-printing-for all type abbreviations of a
given name, or a specific abbreviation from a given theory.

Tests for this. Final cleanup for #168 I hope.

Implement theory namespaces for type abbreviations

Closes #168

Replace old with new type abbreviations properly

Closes #294

type_grammar.sml now uses record type internally

This is a prelude to changing behaviours and fixing bugs. I didn't like
the look of an anonymous 4-tuple when I came to start working on this
file.

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

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

Tidy up the pretty-printing of type grammars. In particular, make it
cope with types there that have become outdated (as will happen after
a complicated Hol_datatype call). Thanks to Ramana Kumar for the bug
report.

Fix for the bug caused by allowing
type_abbrev("foo", ``:'a``)
Fix is to forbid this.

Replace some occurrences of Binaryset with HOLset in type_grammar.sml.

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.

When printing the RHSs of type abbreviations, it makes sense to turn
type-abbreviation printing off. Otherwise you get lots of instances of
ty = ty

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.

The situation I originally thought wasn't likely (and warranted an error)
can actually occur quite reasonably: if the user asserts two abbreviations
for the same pattern (as we do in bagTheory, with bag and multiset).
So, now the attempt to remove a printing just silently does nothing.

*** empty log message ***

When multiple type abbreviations apply, a sensible choice is made as to
which should be used. Example:
- type_abbrev ("foo", ``:'a -> 'b``);
> val it = () : unit

- ``:bool -> bool``;
> val it = ``:(bool, bool) foo`` : hol_type

- ``:bool -> bool -> bool``;
> val it = ``:(bool, (bool, bool) foo) foo`` : hol_type

- type_abbrev ("set", ``:'a -> bool``);
> val it = () : unit

- ``:bool -> bool -> bool``;
> val it = ``:(bool, bool set) foo`` : hol_type

- ``:'b -> bool``;
> val it = ``:'b set`` : hol_type

- type_abbrev ("tes", ``:bool -> 'a``);
> val it = () : unit

- ``:bool -> 'b``;
> val it = ``:'b tes`` : hol_type

- ``:bool -> bool``;
> val it = ``:bool tes`` : hol_type

- ``:'a -> bool``;
> val it = ``:'a set`` : hol_type

- ``:'a -> 'b``;
> val it = ``:('a, 'b) foo`` : hol_type

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.

Fix for bug #579696.

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.