Updated as far as Pretype.sml

Still no use of smpp tech.

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

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.

Move the pretty-printing facilities around a bit so that both SML
implementations use our own version of the PP structure. This
implementation is called HOLPP in src/portableML. After the kernel's
Overlay.sml is loaded, it is also available under the name PP. This
retains fairly good backwards incompatibility. The one deliberate
incompatibility is to make references to General.ppstream invalid.
This makes us better conform with Basis 2002.

The advantage of this manoeuvre is to allow me to better control what
our pretty-printers do at a low level.

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.

Added a few newlines at end of files to suppress warnings from my
Mosml -> MLton preprocessor.

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