Up to hol.state0

Up to and boolTheory and slightly beyond

Now up to type pretty-printing

functions to print terms without using overloads

Remove -- as an alias for Term parser.

As per comment in release notes this has long been replaced as
appropriate style.

Add utility function to help with omitting subterms in p/printing

constant_string_printer "s" is a userprinter that emits s for all
possible input terms. Coupled with a call to {temp_,}add_user_printer
and a pattern that should be elided, it is then easy to have terms
print without uninteresting cruft included.

src/parse compiles but parser broken.

Completed change to remove LISTRULE form from grammar. Instead, all
list syntax is handled with embedded ListForms within normal rules.

WIP for change to list syntax handling.

Very broken at the moment

Use grammar-deltas for user-provided absyn post-processors

Preserve add_user_printer properly in grammar data

This requires a slightly involved process for storing references to
code in theory files.

Update the .doc file on add_user_printer (which was already incredibly
long), and add a test.

Closes #367

Fix one of the bugs in previous commit's test-case

This was done by simply removing the entry-points (uoverload_on, and
uset_fixity) that were causing problems. They have long been redundant
in terms of their desired effect, and introduced buggy behaviour with
the switch to explicit grammar deltas.

The uoverload_on function is still used internally.

Use grammar-delta merging to build theory grammars

Test-case illustrates this: as per the comment in the file, the old
method for merging grammars results in B's grammar having two rules for
"=", making it ambiguous and (because of the trace) causing any
subsequent parse to fail with an ambiguous grammar error.

The new method correctly merges grammar deltas, resulting in a grammar
with just one rule for =.

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.

Properly re-org grammar code, removing rule_fixity

Now there is just one fixity type. Also decide that set_fixity and
set_mapped_fixity shouldn't be in the grammar-delta type; instead the
"remove-termtok" and "add_rule" actions (which can be used to implement
the above) should be.

Refactor more grammar code

Ultimate is to switch to concrete "grammar-deltas" in theory files
rather than calls to the update_grms function. Start this process by
extending existing delta type with SET_MAPPED_FIXITY constructor. This
is not yet used.

Allow script files to specify their parent grammars

Demonstrate this in bagScript.sml, which doesn't need the patternMatches
and indexedLists grammars in its parsing context.

Refactor handling of ancestral grammars

The eventual aim is to make it easy for users to override the selection
of ancestral grammars. At the moment, you are forced to have the union
of the grammars from all the ancestral theories. This gets unreasonable
in the presence of heaps, which may include a whole bunch of theories
that you don't want to have messing up your parsing context.

Provide database of grammars keyed on theory names

This provides a mechanism to get at grammar values that doesn't rely on
the ML compiler. Instead of

listTheory.list_grammars

you can now write

valOf (Parse.grammarDB "list")

Refactor more parsing code

Aim is to move more specialised functions out of Parse and make clients
use TermParse. Here, the functions in question are those to do with
"parsing in context", where a context is a list of free variables to
treat as constants, and an optional type constraint.

In the change to BasicProvers, this allows a constraint that the
argument to "by" be boolean to be introduced.

Provide "typed" parsing-in-context entry-points

This allows

QTY_TAC ty tac q

to parse q in the context of the goal and also require the resulting
term to have the provided type. The resulting term is then passed to
tac, as per Q_TAC>

Get BasicProvers to compile

Make progress with functional pretype

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

Allow for user "preterm processors"

These are inserted into the process where the abstract syntax gets
turned into preterms, and can call back to the builtin processor if
necessary.

Something like this is necessary if you are going to mess with binding
structure and need to do so in a way that is itself aware of what the
context's free variables are. This technology is needed for
pattern-matching, and should allow us to move the handling of
set-comprehension out of src/parse as well.

Absyn post-processors now see the current grammar

Undo all pmatch changes to src/parse

I now want to make new-style pmatch parsing happen via the mechanism of
absyn post-processors (as is done with monad syntax). I don't think
that changing the "core" parser is necessary (and it's certainly not
desirable).

Provide user with API to change pmatch_use flag

Better overload-removal API in Parse

Previously, one could only remove mappings from strings to bare terms,
making it hard to remove overloadings to patterns. Now it is possible
to remove pattern overloadings too.

Illustrate new facility with example of fixing record field updates to
be less polymorphic.

Better overload-removal API in Parse

Previously, one could only remove mappings from strings to bare terms,
making it hard to remove overloadings to patterns. Now it is possible
to remove pattern overloadings too.

Illustrate new facility with example of fixing record field updates to
be less polymorphic.

Can now remove Absyn post-processors via Parse API

Only with a "temp_" variant for the moment

Implement/document/test thytype_abbrev

This function allows better control of type abbreviations in their
theory namespaces.

Implement theory namespaces for type abbreviations

Closes #168

Implement and document remove_type_abbrev.

Closes #148

Remove broken and unnecessary {temp_,}add_binder entry-points in Parse

Allow prefix-operators to be printed without parens in rand-position

This is a refinement to the decision in aeb0085a3d11, which insisted
that prefix operators (like if-then-else, binders, case-expressions
and others) should always get parentheses when printed as arguments to
functions.

Now you can tweak this by choosing the NotEvenIfRand parenthesis style
as an argument to add_rule. For particularly tight operators, ones
that may omit spaces before their arguments say, this may look better.
For example, you might define a "#" operator, when it might be nicer
to have

f #2 + g #n

print that way, rather than with extra parentheses. At the moment, our
standard number injection function & does print with parentheses, but
this case does feel like one where dispensing with the parentheses
might be a good idea.

informational function in Parse: print the term grammar rules

The existing term_grammar() returns the grammar which is pretty printed
by showing the rules, the known constants, and overloading info.
Sometimes this is too much information. So the new print_term_grammar()
just pretty prints the rules (and returns unit). This is useful
especially to see infix and precedence information.

Revise more of Parse's pretty-printing APIs.

In particular, remove a bunch of entry-points with names matching
*backend_string* and print_backend*.

The objective with these was to accompany things like
term_to_string (which printed to a raw_terminal backend) with a
printer that printed to the current backend. This is now easy enough
to do with

ppstring pp_term

and

print o ppstring pp_term

The flip of the current_backend reference so that it points at
"raw_terminal" can now also be done with the rawterm_pp function.

The other convenience entry-points that have gone, for the moment, are
those that did all of the above while also removing certain specified
overloads. Because pp_term_without_overloads_on is still present, you
have to make do with

print (ppstring (pp_term_without_overloads_on ["/\\"]) ``p /\ q``);

or

rawterm_pp (ppstring (pp_term_without_overloads_on ["/\\"]))
``p /\ q``;

Closes #13. I will open a fresh issue to do with making the last two
use-cases slightly easier to deal with.

Rework pp_overloads_on; remove a number of functions from Parse API.

The API was too big, and presented a bunch of functions that were just
variations on compositions of various existing entry-points.

Also, removed the type_abbrev version of pp_overloads_on entirely,
this information is easy to get from inspecting the output of
type_grammar()

This is progress (of a sort) with issue #13

Rename TruePrefix to Prefix; use fixity options with NONE for what was Prefix.

90+% of this work was done by Ramana Kumar. The following list are
the commits for a series of individual commits that have been squished
into one big change:
* remove mention of TruePrefix from the add_rule docfile
* first batch of changes removing TruePrefix from src/parse
* replace TruePrefix by Prefix in boolScript.sml
* remove TruePrefix from Rsyntax
is a fixity ever required for new_specification?
* some more Prefix -> NONE and TruePrefix -> Prefix in theories
* TruePrefix changes for datatype
* TruePrefix changes for res_quan
* TruePrefix->Prefix in a TeX selftest
* TruePrefix changes for quotient
* TruePrefix changes for integer and real
* fix quotient examples for TruePrefix removal
* more fixes for quotient examples
* fixes for lambda example for TruePrefix removal
* Reword description manual in light of removal of TruePrefix.
* Fix msgTheory quotient example; Poly 5.3 had problems with monotypes.
* Fixes for files in examples/lambda given removal of TruePrefix.
* Fix in examples/unification given removal of TruePrefix.
* Fix in examples/HolCheck given removal of TruePrefix.
* Fixes in examples/acl2 given removal of TruePrefix.

Addition of destructors and recognizers for datatypes.
So far, I've just got basic support put in.

Some other trivial mods as well.

Functions to list specific overloads/abbrevs, and to print without them

Add the following functions to Parse:
pp_overloads_on s
print the parsing and printing overloads associated with the token s

pp_abbrev s
print the type abbreviations associated with the token s

pp_term_without_overloads_on (ls : string list)
print a term without applying any overloads on the tokens in ls

pp_term_without_overloads (ls : (string * term) list)
same as above, but specify the overloads to remove more precisely

pp_type_without_abbrevs (ls : string list)
print a type without using any abbreviations on tokens in ls

Also add printing versions, with the prefix "pp_" replaced by "print_",
which don't need a ppstream and print to stdout. For the last three
functions, also add "print_backend_" versions.

Also add string versions of the last three functions, with the prefix
"pp_" removed and the suffix "_to_string" or "_to_backend_string" added,
which don't need a ppstream and return a string.

Apart from Parse.sig, also modify two other signatures:

Reveal the function structure_to_type in type_grammar, and

Add the function gen_remove_mapping to Overload, which removes an
arbitrary overload to a term, since remove_mapping can only handle
overloads to constants.

Add support for "inferior" overloads

Use Parse.inferior_overload_on(s,t) instead of Parse.overload_on(s,t) to
add the new resolution t of the token s at the lowest, instead of
highest, priority.

This allows the new resolution to be picked up when the types require
it, but, when the types aren't constraining enough, the new resolution
won't trump any existing resolutions.

Printing is also affected: terms matching t will be printed as before,
rather than using the overloaded string s. Caveat: if t is a more
specific pattern than any existing overload, it will be printed in terms
of s, since the printer won't realize that less specific overloads are
competing with t.

Also includes temp_inferior_overload_on, analogous to temp_overload_on.

Add new set_mapped_fixity function to Parse (some documentation included).

Rework grammar infrastructure, losing 'preference' for concrete syntax.

Instead, the most recent rule is the one the pretty-printer will prefer.
The clear_prefs function disappears, but the prefer_form function stays
because it can just adjust the timestamp on the desired form to be most
recent.

Reworked implementation of Unicode structure.

Unicode is now a sub-structure of Parse, with functionality provided
by a separate ProvideUnicode module. This organisation makes Parse
the primary module once again (previously Unicode built on top of
Parse).

Changes in src/bool result from

open Parse Unicode

not working. Instead the two opens must be in separate lines:

open Parse
open Unicode

Changes to make type-printing behave just like term or thm printing, i.e.:

- type_to_string and print_type now use the raw-terminal
- functions type_to_backend_string and print_backend_type added that use the current terminal

function add_style_to_string added in order to complement print_string_with_style

Add some functions to use PPBackends. There are
- term_to_backend_string
- thm_to_backend_string

These are used by
- print_backend_term
- print_backend_thm

The corresponding functions term_to_string, ... use always the raw_terminal. In contrast these functions use the currently set backend.

Moreover, there is a function
- print_with_style
now that allows printing strings in a specific style.

Make the interface supported by Unicode slightly richer so that I can
make the Unicode not-equals not overlap entirely with <>, thereby
allowing <> to be used both for word_slice and for not-equals, without
it inheriting the \neq symbol when Unicode is on.

Get interactive Poly/ML sessions to set the PPBackEnd appropriately.

Separate pretty-printing code into two halves, with a backend
component able to provide special treatment of the basic
pretty-printing functionality. The front-end can call a special
version of add_string in order to let the back-end know that a certain
piece of text has special properties. The handling of the given
annotations is up to the backend.

The raw_terminal backend ignores all annotations.

The emacs_terminal backend is the same as the raw_terminal backend for
the moment because I can't figure out how best to pass information
on.

The vt100_terminal backend colours free and bound variables blue and
green respectively using ANSI/vt100 escape codes. You should see this
if you start up HOL in an xterm (or gnome-terminal, or ...).

The current_backend reference variable in Parse can be set to alter
the backend being used for printing. For example, if you do

Parse.current_backend := PPBackEnd.vt100_terminal

while running in emacs, you will see your terms mangled with lots of
\^[ type junk.

I think a LaTeX backend should be possible, as might some sort of XML
or MathML thingy.

I suspect my token merging avoidance code will need updating.

Also, change std.prelude to set the interactive flag earlier, so that
Parse can see it (it will use raw_terminal if loaded non-interactively).

Handle the discrepancy in the behaviour between the way CHOOSE_THEN
and GEN_TAC choose variants by making them do the same thing (Konrad
earlier fixed GEN_TAC to use prim_variant, but CHOOSE_THEN was using
variant).

Decided that avoiding constant names in the current grammar was
probably a good idea, so open up the internal gen_variant function in
Term.sml, and feed it with the new predicate "is_constname" from
Parse. is_constname is true if a string is the name of a "constant"
as the parser sees things. In particular, if you do
overload_on ("foo", ``SUC``)
then "foo" (as well as "SUC") will be considered a const's name.

Hidden constants are not const names in this sense, so C doesn't get
primed in either of
STRIP_TAC ([], ``(?C. P C) ==> Q``)
or
STRIP_TAC ([], ``!C. P C ==> Q``)
even with combinTheory as an ancestor.

Modify the ability to add user-printers so that they're keyed off
term-matches (using first order term-matching). Also give the user's
function access to the relevant grammars, and to the "smart"
add_string and add_break functions that the system printer uses itself
to avoid symbol merging.

Get the absyn post-processors to actually be applied when a piece of
concrete syntax is turned into an Absyn value.

Provide a function (grammar_parse_in_context) to do a contextual parse
with respect to a particular grammar-pair.

Added:

Parse.send_to_back_overload : string -> {Name: string, Thy: string} -> unit
Parse.bring_to_front_overload : string -> {Name: string, Thy: string} -> unit
Parse.temp_send_to_back_overload : string -> {Name:string,Thy:string} -> unit
Parse.temp_bring_to_front_overload : string -> {Name:string,Thy:string} -> unit

These provide a more flexible way to control operator overloading.

For example:

- load "wordsTheory";
> val it = () : unit
- ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
<<HOL message: inventing new type variable names: 'a>>
> val it = ``(a :bool['a]) + (b :bool['a])``
- Parse.send_to_back_overload "+" {Name = "word_add", Thy = "words"};
> val it = () : unit
- ``a + b``;
<<HOL message: more than one resolution of overloading was possible>>
> val it = ``(a :num) + (b :num)`` : term
- ``a + b : word32``;
> val it = ``(a :bool[32]) + (b :bool[32])`` : term

Provide a way of looking at the pending grammar updates that are due
to be adjoined to the current theory when it is exported. Really only
for debugging.

Added support for recovering from grammar additions that later get
withdrawn.

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

Parse.post_process_term : (term -> term) ref

By default this does nothing.

Make symbol-merging be avoided by default. Also ensure that (* and *)
tokens are not created by separate calls to the printer. Remove the extra
"setting" and "getting" functions in Parse.sig that Peter introduced
because I think they are now unnecessary. (Feel free to put them back
if they are still needed for your application Peter.) There is now also
a flag that can be set to level 0 to get back the old behaviour of the
printer, though I can't imagine why anyone would ever want it.
This implementation does not attempt to create a new ppstream - instead
the "wrapping" happens above the PP calls that are made in term_pp. In
particular, add_string and add_break are masked by calls that share a
reference containing the last outputted character. The problem with
creating new ppstreams is that you end up with multiple copies of state
representing the "same" state of the output page, and this leads to
formatting errors.

----------------------------------------------------------------------

Committing in new ability to create and use safely printing ppstreams.

This provides a new term printer term_pp.pp_term_sep to enable better
separation of symbolic identifiers when printing terms.

However, to activate this, one must create and use a new ppstream which
has as its consumer function one which was wrapped by the function
term_pp.wrap_consumer_sep.

Example:

val normal_grammar_term_printer =
Parse.set_grammar_term_printer term_pp.pp_term_sep;

val linewidth = ref 75;

fun mk_sml_ppstream f =
PP.mk_ppstream {consumer = term_pp.wrap_consumer_sep (fn s => TextIO.output(f, s)),
linewidth = !linewidth,
flush = fn () => TextIO.flushOut f}

Then printing with mk_sml_ppstream should separate symbolic identifiers.

It's not a beautiful solution, but it works. Improvements are welcomed!

Modified Files:
Parse.sig Parse.sml term_pp.sig term_pp.sml
----------------------------------------------------------------------

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.

Extend the add_listform interface so that the user can specify a printing
"consistency" for the block of list elements. Previously, it was just
assumed that the user always wanted (INCONSISTENT,0). This is the value
now specified in the various places where add_listform is used.

Added "current_grammars()" entrypoint.

Adapting to new Basis (and SML/NJ).

Two changes.

1. Moved definition of ty_antiq to Parse so that it will
appear in the docs. Other changes arose.

2. "Fixed" HolCheck so that it builds. Is this a
difference between the std and expt kernels?
The change swaps type variables in arguments to
type operators so is probably not what Hasan had
in mind.

Modify the add_listform function in line with a suggestion of Lockwood
Morris's to provide slightly more flexibility in the way that list forms
are pretty-printed. Previously, the format was fixed as
<left-delimiter> el1 <sep> <a space> el2 <sep> <a space> ...
Now, the spacing is more directly under user-control.

I think I've done records to death. This latest (and hopefully
last) improvement speeds things up for a forty field record from 44
seconds to 27 seconds. It does this by eliminating update functions.
Instead, all updates are implemented with functional updates. (The new
documentation in DESCRIPTION explains this.) There are thus many fewer
theorems proved and stored, and initialisation of the stateful rewriter
should be that much faster too.

Gives users of the API another hook into the parsing process, for use when
doing "parses in context".

Modifications to make all pretty-printing routines pay attention to the
linewidth variable in Globals.

Simplified some proofs in MachineTransitionScript.

Reverted to Taupo-6 RW_TAC. This should make RW_TAC faster, and a little
less eager to case-split conditionals. Some proofs may break as a result.
In that case, use the drop-in replacement BasicProvers.NORM_TAC.

Term destructors now operate using same_const to check the operator
of the term being destructed. This may increase efficiency somewhat.
There were consequent changes to the xSyntax modules of the system.

Minor changes, mostly wi the change of DB.theorem to DB.fetch.
I've gone off this change, and will probably change it back in some fashion
after I've had a think.

ChhVS: ----------------------------------------------------------------------

Added simple function to print a term to standard out according to a pair
of grammars.

Removed gratuitous incompatibility with Taupo-6 in type of set_fixity;
its type is now string -> fixity -> unit, rather than
(string * fixity) -> unit.

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.

Modifications to implement parsing and printing of case expressions.

Made adding and removing user printers possible through the Parse
interface.

Added ability for users to add their own pretty-printers, tied to the type
of the term being printed out.

Cleaned up treatment of overloading and extended pretty-printer to
show types verbosely, when appropriate.

Fixed bug in temp_add_infix, which was calling remove_termtok instead
of temp_remove_termtok.

Fixed bug in Numeral.is_numeral.

Final changes (I hope) for Kananaskis-1 parser. Implement remove_ovl_mapping
for fine-tuning of overload maps.

More changes to Kananaskis parsing. System now doesn't allow for
possibility of overloading to different type instantiations of
polymorphic constants. Nor does it allow for printing of polymorphic
constants in any more than one way.
Treatment of number injection overloading is slightly simplified by
actually having a constant in arithmeticTheory with the magical property
that it can never be parsed as the LHS of an application.

Reinstated typedTerm function for benefit of TFL. Added some error-reporting
to update_grms, which is used when theories are loaded. Theories should
now load even though all of their grammars may not make it in. Fixed
a bug in overload_on_by_nametype, which printed something out to the
theory file that wasn't syntactically OK.

Changes to the way in which constant names are resolved. There is now
a much simpler map from names in the abstract syntax tree to actual
constant terms; everything now goes through the "overload" map.

Added a few more things that got missed out in the transfer from Konrad's
code.

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

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.

The function allow_for_overloading_on has been completely removed from
the system. The overload code now uses anti-unification of types to
figure out the least generalisation of all the types that an overloaded
operator needs to represent.

Implementation of move of hide/show information from Parse_support list
into grammars.

Relatively radical changes to get rid of the preterm type that lived
in parse_term and replace it with a cleaner Absyn type that Konrad
wrote for TFL.

Slight changes to accomodate parsing into parse_term.preterm ...
which is soon to be changed to "absyn" ...

Added print_from_grammars to Parse; now you can have a printing function
independent of the global grammar too if desired.

Added parse_in_context function to Parse; and fixed a couple of minor
bugs to do with printing and parsing record syntax.

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.

Implemented printing with the Global delimiters for terms and types.
So now Globals.{term,type}_pp_{pre,suf}fix are respected.

Added resolve_names function to allow parse_term.preterms to be turned
into Preterm.preterms. I think all stages in the parse process are now
visible to the external user.

The poorly named remove_term has been renamed to remove_rules_for_term.

Brought across remaining ParenStyle constructors from term_grammar.

Minor editing changes.

Fairly extensive changes, implementing a scheme whereby each theory keeps
track of its own personal grammar value, which can then be relied on by
other libraries. This is in contrast with the term_grammar() value. This
gets changed all the time, and library implementations can't really rely
on it being sensible.

For example, numLib quotes a term involving >. If this symbol was over-
ridden or messed with in some other way, before numLib was loaded, it
would try to parse that term and come a cropper. No more.

Changes in Preterm are more to do with trying to improve the error
reporting from the type-checking, particularly as with regards numerals.

Concrete syntax for records now very close to done. Thanks to Mark Staples
for suggesting that records with singleton updates could be done without
the brackets around the lists, thus: r with fld1 := 10.

Many changes, mainly to do with record syntax. Also implemented long IDs
as theory-name$id. All of HOL doesn't quite build because field selection
operator is ->, which is used in the real library. Will change this to be
just a simple "." Have also started on concrete syntax for updates.

Added export_theorems_as_docfiles and export_theory_as_docfiles to Parse.
These functions are used to generate .doc files containing the theorems
contained within a theory. These in turn can be used to generate nice
documentation listings of these theorems.

Many changes to allow numerals to be overloaded as well as operators.

Changes to get overloading to properly resolve types. I claimed yesterday
that if an overloaded constant didn't have its type determined by normal
type-checking, then it could be instantiated with any type in the candidate
list of types because if type-checking hadn't constrained it, then it
must be OK. This is rubbish though, because there may be constraints
implicit in other overloaded operators. For example, imagine that ~ is
overloaded to be both a boolean operator (not) and over integers
(negation).
Further, imagine that + is overloaded. Then consider the phrase
~x + 2
If we just guess the first type that comes to hand for x, then we may guess
bool, and this will be wrong, because the + has to go to num->num->num or
int->int->int. So, we need to do backtracking unifications through all
of the possibilities. Hence the use of seqs and seqmonad to implement
this.

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.

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.

Implementation of new pretty-printing support whereby grammar rules now
contain extra information on how various forms are to be printed, with
extra information specifying spacing, block structure and when things
should be parenthesised, even if not strictly necessary.

Changes necessary to make :: an infix operator representing CONS as well
as the restricted quantification operator. This change has required some
changes to the basic design of the parser; it's now not possible to have
more than one res. quan. operator.

Numerous changes allowing for printing and parsing of numerals and
treating them as members of different families depending on the contents
of the numeral_info part of the term_grammar. Tested inasmuch the
distribution builds correctly, and with integerTheory loaded.

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

Initial revision