Updated as far as Pretype.sml

Still no use of smpp tech.

Fix basic unification bug (add derived test-case)

Switch type-checking to errormonad everywhere

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

Give Pretype environment slightly richer API

Get basic kernel working

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

Tweak optmonad.addState to return updated extra state

Change error monads to wrap the state & result

So, the state-error monad (called optmonad here) changes from

'state -> ('state * 'a option)

to

'state -> ('state * 'a) option

No doubt there is some precise monad-transformer jargon I could use to
describe this change.

The advantage of the latter is that it makes for an easy lift into the
seqmonad (which replaces option above with seq).

Begin to make pretypes purely functional

I want to do without the references that are used in the unification
algorithm.

Add has_unbound_uvar and mk_fun_ty to Pretype API.

Also document some entrypoints there in the .sig suffix.

Add changes to Pretype required to make TermParse module compile.

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!

Minor prettification of the pretty-printing of pretypes.

Debugging Preterm.sml made me write a pretty-printer for pretype
values (and I was almost annoyed enough to write one for Preterms
too). I use Moscow ML compiler magic to get numbers for references,
and have written to the Poly/ML mailing list to ask how to do the same
in poly.

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.

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.

Latest mods for making everything paired.

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

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.

Initial revision