Fix ParseDatatype bug when parsing Datatype syntax

One test case would be

foo = Con1 bool; bar = Con2 foo (bool -> bool);

which didn't cope with the first semicolon, which is next to the bool
argument without an intervening space.

The previous handling of the "feature" whereby atomic types don't need
to be separated from other arguments involved a recursive call to the
type parser on a specially constructed sub-buffer. This was
disgusting and broken. Now the code just calls a parse_atom function
made visible from inside the type parser.

Add some illustrative test-cases.

Thanks to Oskar Abrahamsson for the bug report.

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.

make type parser honour qualified abbreviations

arguably should have been done for #168

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

Fix bug concerning interaction of arrays and other suffixes.

In the process, make it clear that suffixes really do have to be the
tightest operators in the grammar.

Also, add a type-parsing test for array types to
src/n-bit/selftest.sml.

Thanks to Anthony for the report.

Move type antiquotation stuff from term_pp to parse_type.

Name a complicated record type used in parse_type.

More rampant Unicodification.
* the Unicode trace is now *on* by default. You can turn this off by
doing
set_trace "Unicode" 0
In the emacs mode, you can also type M-h C-u. No script file should
need changing as a result of this.

* Type variables can now be printed as Greek lower-case letters. This
is controlled by a trace "Greek tyvars", that is a slave to the
Unicode trace. (This means that if you turn Unicode on, Greek
tyvars is turned on too; and if you turn Unicode off, Greek tyvars
is turned off as well. However, you can adjust the trace directly using
set_trace as well, if you wish.)

The effect of "Greek tyvars" is too allow lower-case Greek letters
alpha to omega to act as aliases for 'a, 'b ... forms. This
aliasing is done with both parsing and printing. The lambda is
*not* adjusted in this way. It'd be surprising if anyone ever
wanted more than about alpha, beta, gamma and delta of course.

This is purely a presentational matter. You may see a Greek alpha
on your screen, but to the kernel, it's still mk_vartype "'a".

* There is one possible backwards incompatibility that I can think
of. The quotation filter had to be adjusted to push it into type
parsing when it saw

``:

followed by a lowercase greek letter. Previously, it saw such a
thing as the start of a term 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.

Types can now be numerals. Numeral types have as many elements in
them as the number provided. This is thanks to the fact that they
encode into type-operators provided by fcpTheory (bit0 and bit1), and
the unit type. The plan is to have these types used for the indexes
of finite cartesian products, and to further support :elem[num] as the
notation for these "array" types. 32 bit words will thus be
:bool[32]. If people want to save two characters, they can still
abbreviate :bool[32] to :word32 of course. This is not dependent
typing, so writing things like :bool[n] will be an error.

Specific type abbreviations are no longer required because it is all
special-cased in the type parser/printer combination.

Note that :0 is not allowed!

Adapting to new Basis (and SML/NJ).

Propagate locations through parse_type, so parse errors in type
expressions are now located as well.

This commit contains the initial version of the error-location
reporting code I have been working on over the last couple of weeks.

Basically, error messages will now report the source location they
relate to, enabling users to locate bugs more easily within large
definitions.

So far, errors are reported by the lexer, the term parser, and the
datatype parser. Type parser errors will follow, and (hopefully)
typecheck errors.

src/0/locn is a small location-handling library. locn.locn is the
type of locations, and 'a locn.located is a synonym for 'a *
locn.locn. There is a location, Loc_None, for compiler-generated
text, and another, Loc_Unknown, for text of unknown location.

src/0/Feedback now includes some functions for generating located errors.

The lexer now returns located tokens, term_token and type_token
maintain the locations, and parse_term maintains them *internally* on
each terminal and nonterminal. When the system is complete, locations
will persist into absyn and preterm (if I understand the code
correctly!) to enable the typechecker to yield located errors.

I would appreciate any feedback:

* Is the performance impact significant?
* Are any error messages incorrect? (there's a lot of
location-manipulation code in parse_term, some of which I don't
fully understand, and surely some bugs)
* Have I broken anything for anyone, or am I likely to?

The actual output format of the location information is provisional
only, and I intend to generate absolute file positions (rather than
fragment offsets) shortly.

--KW 8-)

NB: tags pre-locn-change and post-locn-change cover this commit.

A complete re-implementation of lexing. Speeds things up considerably
through the use of mosmllex. (The example at the bottom of term_tokens.sml
goes through four to five times faster than it used to.) The basic
design is now more stateful than it used to be. There is a new type,
called the qbuf, which provides buffered access to a quotation. The
implementation of parse_type changes completely because it can no longer
do the monadic-parsing trick of backing up over failed parses. The
implementation of the term parser doesn't really change at all.

Fix for bug #584933.

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.

Added a pretty-printer for type grammars and extended the term grammar
to note the existence of user pretty-printers.

Changes to make the type parser handle thy$tyname syntax. This syntax
can only be used as suffixes. Thus: (bool,bool) min$fun, for example.

Support for new representation of strings.Minor changes.

Slew of changes to get rid of local open in end in signature files, and
one or two other fixes to make source mosml2.00 compatible. Also added
ability to set and get term_printer function, as per request by Peter
Homeier.

Changes to support the proper construction and export of theory grammar
values. Theory export now takes an extra parameter, which is a string
that will be pre-pended to the Theory.sml file. This allows me to
remove code in TheoryPP that was rather specific to what was being
done in Parse. Now, this code can remain ignorant of that level of the
system, as should be the case.

Implementation of type checking is now entirely above the level of the
kernel. New TCPretype module (type-checking pretype) implements much
of the required functionality, including type unification.
Parse_type generalised to target any type providing the appropriate
constructor functions.

A number of changes, doing away with the old Pretype and Strm modules.
These changes support the new implementation of the ParseDatatype
module, which now refers to the type parser provided in this directory,
meaning that ParseDatatype can see new user-defined type infixes as and
when they become available.

Fixed to bring it up to date with Taupo release 0.
(Changes have come across from parse_branch development.)