Move Preterm datatype definition to separate file.

As was done with Absyn in 019a332d49, this reduces redundancy and helps
with Poly/ML's pretty-printing

Add entry-points to let parsing to return >1 parse

This is possible in the presence of overloading.

Also some minor tidy-ups in the body of Preterm.sml (more still to be
done in this vein).

Get Defn to compile; also report ambiguous overloads

Set comprehensions will be the next task

Get BasicProvers to compile

Switch type-checking to errormonad everywhere

The optionmonad doesn't hold any advantage, and flipping back and forth
between them was just annoying.

Get basic kernel working

Interactive behaviour in terms of error messages and the like may still
be broken.

Make progress with functional pretype

The change to pretty-printing raises an exception, but parsing simple
cases seems to work.

Get Preterm to compile

extra semicolons removed from (some) .sig files

Make Preterm’s public API a bit richer.

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!

Modifications to support overloading to a pattern. For example, one
can now do
overload_on ("<>", ``\x y. ~(x = y)``)
The parser does the right thing. The pretty-printer remains
blissfully ignorant for the moment. I don't think Unicode aliasing
will work quite yet either. Backwards compatible in that all the
functions in Parse behave the same if given inputs that were
previously acceptable.

"The parser does the right thing" means the following

- set_fixity "<>" (Infix(NONASSOC, 100));
> val it = () : unit

- ``$<>``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``\x y. ~(x = y)`` : term

- ``$<> p``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``\y. ~(p = y)`` : term

- ``p <> q``;
<<HOL message: inventing new type variable names: 'a>>
> val it = ``~(p = q)`` : term

When the pretty-printer is working correctly, the output will probably
be

``\x y. x <> y``

``\y. p <> y``

``p <> q``

In the first two cases, fixing what would appear to the user to be an
odd eta-expansion may be too difficult.

* Remove use of Raise from Parse.sml, as most sub-modules are printing
messages anyway, and if they're not, they should (at least under the
control of a trace variable)
* Also add location information to the 'last error' information in Preterm.

Put the reporting of type-checking errors under the control of a trace
variable, put the message into the exception raised, and also record
the cause of the error in a special reference. This should allow
better programmatic handling of the parser when it might fail.

Added a hook for a "post processing" phase to the term parser.

Parse.post_process_term : (term -> term) ref

By default this does nothing.

Adapting to new Basis (and SML/NJ).

Add a Locn field to each constructor of Preterm.preterm, in
preparation for located type error messages etc.

* Thanks to Joe Hurd for helping locate a bug in an earlier version:
Preterm, while still an equality type, is no longer safe to compare
for equality. Instead, Preterm.eq must be used; this ignores the
locations. (The symptom was a parse_in_context failing to notice
that the binder variables were the same as the bound occurrences,
leading to weird failure in Q.PAT_ASSUM).

* Constrained and Antiq now take records, to accommodate the Locn field.

* Lots of small changes, mainly adding ",...", to code using preterms.

* Pass locations down into the preterm constructor functions.

Fixed a bug reported by Anthony. Gist of it was that the parse in
context function (used extensively by the Q library) wasn't calling the
special code to deal with case expressions.

Modifications to implement parsing and printing of case expressions.

Case expressions now parse and convert appropriately. Still to print them.

Interface by which TypeBase can augment preterm conversion with case
information.

Support for new representation of strings.Minor changes.

Changes to bring about Kananaskis parser. Known bug exists in
treatment of qualified identifiers.

Reorganised the interface to Preterm; with sensible names for functions,
and all of the useful ones exported.

Big raft of changes allowing a simple form of overloading to be supported.

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.

Change to antiquote processing. Now free variables in the antiquotation
will affect type inference in the surrounding term. This is the
way it was done in HOL88, but not HOL90.

Also, some now outdated code has been removed.

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

Initial revision