Test and fix for bug caused by not checking reference in right order

Move smpp to Portable - get everything up to arithmeticScript working

Handle prefixes (quotes and turnstiles) for terms, types and thms

Fix theorem pretty-printing

Up to and boolTheory and slightly beyond

Progress through Parse.sml

Delete some trailing whitespace

functions to print terms without using overloads

Use the Unicode turnstile (user-customizable) when printing theorems

When the trace “Unicode” is changed to 1 or 0 the theorem prefix is set to “⊢”
or the ASCII approximation “|-”, respectively. The prefix and suffix (empty by
default) can be customized via Globals.{thm_pp_prefix,thm_pp_suffix}.

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.

Delete some unused code in Parse.sml

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

Remove complicated behaviour behind Unicode trace/flag

Now the Unicode trace is just an inverted handle on the behaviour behind
the PP.avoid_unicode trace. I couldn't use the alias machinery for
this because of the inversion, but they can still alias to the same
underlying SML reference.

While the ProvideUnicode structure still exists it is dramatically
simpler (I decided I didn't want to cut and paste it into the already-
quite-long-enough Parse.sml).

Closes #363

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

Use cache Absyn to speed up QTY_TAC

Addressing github issue #383

Improve efficiency of grammar ancestry calculation

Fix unicode_version to record grammar-deltas

This should ensure that exported grammars pick up all unicode-related
deltas.

The API in ProvideUnicode has changed a bit, but I don't care because
the whole module is going to die in the short-to-medium term anyway.

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.

Ensure Unicode lambda is in grammars from min onwards

Fixes bug identified in 7cfe487

Handle clear_overloads_on with user-deltas

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 =.

Change set_fixity to remove all rules involving token

Previously, only rules which mapped the token to a name that was the
same string got removed. So, if one had

set_mapped_fixity
{term_name = "foo", tok = "<*>", fixity = Infixl 500}

followed by

set_fixity "<*>" (Infixl 600)

the resulting grammar would include two rules for <*>: one at 500
mapping <*> to "foo", and one at 600 mapping <*> to "<*>".

Now, the grammar contains just the latter rule.

Convert type-grammars to use deltas for updates

This is very much analogous to what has been done for term grammars.

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.

Handle add_numeral_form et al with user-deltas

Also take the opportunity to remove redundant add_actual_overloading
entrypoint in Overload module.

Stop temp consts from being added to grammar

This means that they can't be named directly, and can only be accessed
with the $ notation.

Also make the "_tupled" constants used internally by tfl be temporary
constants of this form so they don't get added either.

Add deltas for moving overload operations

Sadly, making an inferior overload is not *quite* the same as making a
normal one, then then moving it "to the back", so I've left both
operations in the user_delta type for the moment.

Handle gen_remove_ovl_mapping

This gets tests as far as string_numTheory

Make more progress with new parsing architecture

monofldB test in datatype/theory_tests fails

Ensure non-temp unicode-ish overloads are recorded

Previously, this was ensured because theory files actually included
calls to the temp_overload_on function, which did the magic
ProvideUnicode stuff itself.

Get tracked user_deltas to build grammars in Theory files

Begin process to use GrammarDeltas inside theories

This doesn't work yet (just attempting to load boolTheory leads to an
exception), but it's close to working, at least for some situations. I'm
generating new constructors for the user_delta type more or less as the
errors prompt me to.

The new constructors in this commit are IOVERLOAD_ON for "add inferior
overload on" (it's not really clear that this is used enough to warrant
inclusion, but hey); ASSOC_RESTR for "associate restriction", which is
used in boolTheory and probably nowhere else ever, and RMOVMAP for
"remove overload mapping", which is used to remove overloadings to
constants.

General pattern in Parse is to generate the user_delta values, and to
then feed these to the term_grammar.add_delta function to make the
grammar updates. This makes Parse simpler on the whole, which is
definitely an improvement.

Record overload_on calls in GrammarDeltas

Record grammar deltas in Parse

These are not used for any other purpose just yet, and the set of
possible grammar deltas is not yet big enough. (Next addition:
overload_on).

Remove BRULE constructor from user_delta type

It is redundant, though the GRULE representation of a grammar's binder
rule contains information that is never used.

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.

Store theories' grammars with Unicode details

When you refer to something like boolTheory.bool_grammars, it makes
sense to see the Unicode-features of the term grammar.

Includes a test-case that would have failed under the old
behaviour (because the ⇔ symbol wouldn't have mapped to boolean
equality without the Unicode symbols being included).

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.

Start to refactor parsing-in-context code

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

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.

Fix bug caused by intro of new entry-points to Portable

Now that Portable includes a bunch of things that used to be in U, some
forms of type abbreviation would result in an unloadable theory.

Test-case demonstrates the problem.

Provide p/printer for rules part of a term grammar

Closes #249

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.

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

Fix errors in b3de5020; add fupd for pmatch_on

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

Fix another record pretty-printing problem

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

Fix thm_to_string to use raw backend properly.

The term_to_string and type_to_string functions do this already.

Implement and document remove_type_abbrev.

Closes #148

Set max_print_depth to -1 before printing terms to theory files

Closes #234.

Handle Unicode on Windows better with new PP.avoid_unicode trace

If the trace variable is true, then the pretty-printer strives to not
print Unicode characters. If it's false, then it obeys the grammar
(which encodes various printing preferences as well). The trace
is initialised to true on Windows systems.

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.

Make the Unicode trace variable 0 by default on Windows.

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

Fix printing of unnecessary guff on theory load with Unicode off.

More theory signature events now reported to hooks.

In particular, {new,remove}{typeOp,constant} events are reported.

Use this to do away with some of the cruftiness in boolLib whereby the
entry-points there had to mask the primitive principles in order to
update the grammar. Now the parser installs hooks to watch for things
being deleted or added and adjusts the grammar as it goes.

The disadvantage is that it's impossible to bypass these changes to
the grammar.

Rework various Theory hooks into one general framework.

The basis for the framework is the TheoryDelta type. Client code can
ask to be notified of theory changes, and will have their provided
call-back function called at appropriate times.

This commit hasn't adjusted the theory functions for
{add,del}{const/typeOp} yet; it has just unified the existing
functionality (register_onload, after_new_theory and
register_onexport).

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.

Bug-fix: exported xTheory.sig files could contain spurious 'comments'.

In particular, if a comment-string (i.e., (* or *)) appeared as part
of a string literal in an exported theorem, this caused the resulting
Theory.sig file to be malformed SML. The fix was to create a trace
variable allowing string-literal printing to become more 'paranoid'
when done in the TheoryPP code. In that context, occurrences of the
bad strings have their asterisks replaced by \042, which is correct
SML/HOL notation for ASCII character 42, which is the asterisk.

Note that this problem doesn't arise in normal interactive use: the
HOL lexer doesn't get confused by comment strings in string literals,
and the SML level thinks all of the content in a quotation is inside
one of its own string literals.

Include a comment in the Description manual about not using tokens
that include comment strings or whitespace.

Thanks to Magnus for the bug report.

Fix bug in Parse.add_user_printer

fix print_with_style

Minor rephrasing to avoid a "Pattern is not exhaustive" compiler warning.

Make more use of abstracted functions in Parse

make_to_string, make_to_backend_string, make_print, and
print_with_newline in particular

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.

Fix for bug identified in r8267.

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.

Bugfix: unsetting Unicode trace wasn't correctly removing all Unicode rules.

Stop repeat calls to set_trace "Unicode" 1 repeatedly adding rules to grammar.

Calls to overload_on put changes into 'Unicode land' if string is Unicodeish.

Realised I was recording Unicode-add_rules and set_fixities twice.

Make standard add_rule and set_fixity entry-points Unicode-aware.

In particular, if you give these entry-points things that include
Unicode characters (code > 127), then they will be handled by the
Unicode-specific facilities. This means that with the Unicode trace
off, these additions will "disappear", only to again be seen if the
trace is turned back on again.

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

Move theory min's grammars into {type,term}_grammar (out of Parse).

Change Parse to use new TermParse facilities.

Move type antiquotation stuff from term_pp to parse_type.

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

Get parse errors from the Absyn stage into exceptions more accurately.

(I noticed that the error message printed out from something like /\ p)
was not the same as the text inside the accompanying HOL_ERR.)

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.

Fix a bug reported by Anthony whereby theories exported with Unicode
on couldn't be loaded with Unicode off. Also set up a new trace that
allows generation of annotations for PPBackEnd to be turned off.
Having it off, which is its state when not running interactively,
speeds up the pretty-printing done to the Theory.sig file when a
theory is exported.

Link the type pretty-printer to the PPBackEnd infrastructure. In
Emacs, types are printed in italics, with tooltips indicating the real
nature of the underlying thing (type abbreviations supported).

Make some minor changes to the HOL/emacs link in response to issues
identified by Thomas (who is using an older version of emacs than I
am). Along the way, allow people not using the hol-mode, but still
using hol within emacs, to continue doing so straightforwardly.

Make the term_to_string and thm_to_string functions use the raw_terminal.

Fix the automatic detection of appropriate terminal types so that it
works on MacOS X. (There the standard terminal sets up TERM to be
"xterm-color", not just "xterm".) Note how I assume the whole world
has colour xterms these days.

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).

More corrections required to our sources when I do the migration to
Basis 97 properly.

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.

Variables in the patterns of case expressions are now properly
'fresh'. They bind expressions on the other side of the case-arrow,
but do not affect variables outside the case expression or in other
branches. This revealed a bug in DecodeScript, where a theorem about
encoding sums ended up being about sums of type 'a + 'a only because
case pattern variables that should have been independent weren't.

Fairly dramatic change, supporting the use of "syntactic patterns".
It is now possible to overload a name to term (typically a
lambda-abstraction) in order to create syntax-only definitions. For
example, there is a definition of not-equals now in the system:
val _ = overload_on ("<>", ``\x y. ~(x = y)``)
val _ = set_fixity "<>" (Infix(NONASSOC, 450))
This definition is parsed and pretty-printed.

Two other annoying changes. The interface for adding unicode variants
has changed, and I have made precedence level 450 of the parser
non-associative. This latter change has caused most of the (minor)
adjustments to the files below. The regression test doesn't go
through yet. (Currently there is a failure in
quotient/examples/sigma that I don't understand.)

More code for pretty-printing patterns. The interface in Parse stays
the same, but you can now overload to type specific instances of
constants. This is exploited in the ParseExtras structure, which is
loaded with boolLib. This implements the <=> "constant" for
if-and-only-if. This is just equality, but presented with a new face
when applied to boolean arguments.

The other obvious application of this is to make :string and alias for
:char list, and to make the appropriate string constants overloads of
the corresponding list constants. Code that relies on things like
``STRCAT`` mapping to {Thy = "string", Name = "STRCAT", Ty = ...}
would fail. Otherwise, life should remain the same.

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.

Update the handling of binders so that different concrete syntax forms
can map to the same abstract syntax form. This makes binders more
similar to other forms. For example, the if-then-else and =>-|
concrete forms might both map to the underlying name "COND". Now,
with Unicode enabled, the Unicode universal quantifier as well as "!"
can both map to the name "!". (Internally, there is a preferred flag
set, so that the pretty-printer knows which should be printed when it
comes to the term "!".)

This couldn't be done before, so for example the Unicode universal
quantifier mapped to itself, and this name was then overloaded to be
an alias for "!". This use of the overloading level for Unicode led
to some problems, and was inconsistent with the approach taken for the
other symbols.

There are some other tidy-ups now that binders are more like other
forms.

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.

Get the new version of parse_in_context to work properly (two stupid
errors fixed), and also document the potential incompatibility in the
release notes. (Also remove talk of Define using conjunction and
disjunction congruence rules.)

Change parse_in_context so that it forces free variables in the term
that are also in the context to have the context's types. Previously,
this function allowed variables whose types were completely determined
by the parse to override the context. The change can be seen in
parse_in_context [``x:bool``] `x T = T`;
This now raises a type error exception; it used to accept the string
and return the corresponding term, ignoring the context.

Couple of parse message fixes:
* when doing a parse-in-context, don't automatically "say" errors.
Now only do it if the "report type errors" trace allows.
* The set_goal command in the emacs mode doesn't need to Raise any
exceptions (doing so causes type error messages to be printed
twice).

* 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.

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

Fix for the bug caused by allowing
type_abbrev("foo", ``:'a``)
Fix is to forbid this.

Another fix to the way Unicode-overloading works. It now checks to
see if the term you are overloading to has an ASCII concrete syntax.
(For example, integer$int_le has an ASCII concrete syntax of <= as an
infix.) If so, it will set up the Unicode symbol as an alias for that
concrete syntax. This means that subsequent overloads on the same
ASCII symbol will also pick up the Unicode symbol.

Graphically, we have something like



x <= y +----- arithmetic$<=
\ |
>---> COMB(COMB(<=,x),y) >---+----- integer$int_le
/ |
x ≤ y +----- words$word_le
|
... etc

where the middle column is the result of Absyn applied to the given
quotation.

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.

Make the revised code in these directories use the common interface in
Theory.sig rather than stuff that only appears in the
experimental-kernel.

Make the datatype package remove the intermediate cruft that it
generates in the process of setting up a new algebraic datatype. This
knocks the ladder away once the summit is reached, but definitions as
a conservative extension mean this is sound, as well as healthier for
our bloated theory files.
The change to abstraction.sml comes about because it was making the
mistake of thinking the the definitions and theorems functions
necessarily returned up-to-date theorems.
The change to Parse.sml stops it from emitting theory-instructions
that refer to out-of-date constants.

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
----------------------------------------------------------------------

Fix bugs:
* a call to overload_on was being made in boolSyntax.sml, which prompted
the code in Parse.sml to complain about updates being thrown away. The
call in boolSyntax.sml should have been to temp_overload_on if anything.
But better still to put the call to overload_on in a theory file...
* Modified Parse.sml to report the throwing away updates error more verbosely.
* Putting the call to overload_on in boolScript caused an exception. This
happened because the pretty-printer was raising an exception when trying
to print literal_case_THM, featuring the term ``literal_case f x``.
(This was happening because the call to overload_on was making the
pretty-printer think that it should be treating such terms as case
expressions.) Fix this by removing the redundant code in term_pp.sml that
was attempting to do the printing and raising the wrong sort of exception
in the process. (Also add an exception handler to the call-out to the
provided case-expression destructor in the other branch, just to be
paranoid.)

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.

Implement and document a new, unambiguous set comprehension syntax.
Only fixes required are to ieeeScript where old style =>-| if-then-else
syntax was nested to extraordinary degree without any parentheses.
Adding parentheses was the only thing required to fix the problem.

Revised exportML so that it takes a path parameter, which tells
where the ML corresponding to a theory is to be written.

This has been propagated to all the theories that already export
ML, and the mkword.exe tool has been upgraded to also take a
path where it should write the generated ML. This is useful,
because doing an exportML to the same directory as the theory
files will end up confusing Holmake.

Changes to make it easier to dispense with the let-and concrete syntax
and put something else there instead. Even without throwing them away
it is now possible to write ``$let`` and have this just be a variable of
type alpha, rather than a parse error. So that's an improvement.
If you wanted to define a constant "and", allowing this would be as
simple as chucking the rule for "and", by using
remove_termtok {term = GrammarSpecials.and_special, tok = "and"}
and then defining the new constant "and" with Define, and possibly
giving it fixities etc, as you might with any other constant. Similarly
for let.

Starting to remove redundant (and potentially error-introducing) infix
declarations.

Adapting to new Basis (and SML/NJ).

Cause EmitML.exportML and Parse.export_theorems_as_docfiles to "fail"
with warnings and to do nothing, rather than fail with exceptions that
will cause builds to fail themselves.

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.

* Use export_theory_as_docfiles to generate the .doc files.
Had to modify this function to accept absolute paths.
* Moved some evaluation theorems from wordFunctor.sml to wordFunctorLib.sml.
* Renamed help/entries files.

Fix for bug #851064, which was caused by the parser's overload tables
retaining information about constants that had been outdated by a call
to new_theory.

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.

Welcome to the 1980s... type and overloading errors now report
source-file locations!

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.

Further improve error reporting:

* make_atom failures (e.g., update of nonexistent field) now give
located errors; ditto all friends in Parse_support. Modified
absyn_to_preterm and Parse_suport.* to pass locations downward to
accommodate this.

* Fix a bug in parse_term that was causing ranges to be confused for
certain sequences of tokens (was reporting left edge of last token
to right edge of first token, oops!).

* Add text " (possibly missing semicolon)" to error "May not use
record update functions at top level", as this is a common error.

* Fix a small bug in location-handling in type_tokens.

Other changes:

* Remove another printing of the tail of the input (no longer
necessary).

* Various code tidy-ups.

* Reduce Loc_Near (Loc_Near locn) to Loc_Near locn (otherwise they
pile up dramatically!).

Miscellanous minor changes to error message reporting:

* Fix locn.move_start and locn.split_at to accommodate new absolute
locations - they were giving incorrect results, oops!

* No longer print the tail of the input file on a lex error (2
places).

* Give both locations in a "Don't expect to find a X in this position
after a Y" term parse error.

Alter the representation of Absyn.absyn and Absyn.vstruct to include
locations. Fill these in in Parse.sml and parse_term.sml as
appropriate. Make sure everything else still builds.

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.

Change to type of new_specification, and made it tell that parser about
the introduced constants. Lots of knock-on (trivial) mods.

Made more parse errors appear automatically (by using Raise).

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.

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

Modified the after_new_theory function's type so that registered functions
are given both the old theory segment's name as well as the new one. This
makes catching the "grammar update before new_theory call" slightly cleaner
and also doesn't stop users from experimenting in scratch with things
like Hol_datatype. Now, if they do this, and then do a new_theory call,
it will be made clear that they are throwing away stuff.

Modified the code in Parse responsible for storing up pending changes
to the exported grammar to warn if someone attempts to do this in theory
scratch. These changes won't be exported because a subsequent call
to new_theory will wipe them.
The change to TypeBase is needed because the old line there tried
to export an overloading, which was always wiped. Now that line
would cause a warning every time HOL started.

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 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.

Added new facilities for dropping or preferring certain numeric types
all at once. Documented one of the new functions, and fixed the
documentation for add_numeral_form, which now automatically adds the
appropriate overloading for "&" (I realised that we didn't need to
force the user to do this themselves).

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.

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.

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

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

Latest mods for making everything paired.

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.

Made overload_info type opaque, and added a reverse map to it, under the
hood, which remembers how constants should be printed. Also reworked
Preterm slightly to stop it carking on type-checking errors involving
overloaded constants (things like `0:bool`, if nothing else).

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.

Treatment of known constants and overloading was bogus. Now known constants
are just the domain of the map in the overloading info. reveal now
puts all constants of the given name into the overloading map. Will
have to add a precise function for removing pairs from this.

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.

Slight change needed to make this compile under mosml1.44. Have checked
that it still works under mosml2.00.

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.

add_rule with a Prefix fixity issues a warning message reminding the
user that this does nothing. In a variety of other places, code has
changed to ensure that add_rule is never called internally with Prefix
as the fixity. This reduces the size of theory files quite a bit.

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.

Parse.sml: pass on OVERLOAD_ERRs as HOL_ERRs.
parse_term.sml: forbid use of un-suffixed numerals when there are no
overloadings for the fromNum string (i.e., "&").

Having changed the name of new_type_definition in Type_def, change the
reference to it here. See log message for Type_def.{sig,sml} for
rationale behind change.

parse_in_context doesn't print out messages now when it invents type
variables.

Fixed a bug where the old form of temp_remove_rules_for_term was being
written out to the theory file.

Revised in light of change to Lib.quote; now the appropriate function
is Lib.mlquote for the generation of all the ML code that is added
to theory files.

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

Updated parse_in_context; fixing a blatant error in the way in which it
was implemented.

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.

Two bugs fixed:
1. `foo bar baz)` was parsing OK, because I wasn't requiring that the
lookahead component of the PStack be empty
2. `foo $` and `foo $^t` were both raising Subscript errors; this has
been improved to raise appropriate LEX_ERRORs.

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.

Changed implementation of add_numeral_form to check that arithmetic is
either the theory in question or a parent. Also modified the order in
which things were done in add_numeral_form so that if a bogus character
is specified (and an exception is raised by term_grammar.add_numeral_form),
no overloading is done.

The poorly named remove_term has been renamed to remove_rules_for_term.

Brought across remaining ParenStyle constructors from term_grammar.

Updated add_rule and add_infix to add error handling to code put into
theory files.

Fixed a bug whereby fragstr.parse wasn't grabbing trailing empty QUOTE
constructors (i.e., it wasn't calling its own fragstr.eof). Unfortunately,
MoscowML puts QUOTE "" on the end of frag lists, if you write
`... ^t`
This was confusing the Type parser. Bug spotted by Konrad.
(Change to Parse simply makes precedence of open fragstr more explicit.)

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.

Quite radical changes which allow for "." to be used as the record
field selection operator. Lexer has changed quite dramatically:
it is no longer responsible for determining whether or not a token
is a "keyword" or not. Instead this is done at the parsing level.

The lexer is also now unable to cope with identifiers that are a mix
of alphabetically acceptable and symbolically acceptable characters.

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.

Record field selection implemented as far as parsing and pretty-printing are
concerned.

Quote function can be taken from Lib. Hey, this must be code reuse.

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.

Added .sig file to type_pp.
Fixed bug which was pretty-printing :(bool |-> bool) |-> bool without any
parentheses.
Removed some spurious reference variables from term_pp.

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.

Small changes to accomodate new-look of portableML.

Calls to Term now trap the PrecConflict error that can be raised by the
parser as it constructs its precedence matrix. The messages are better
but still not really much help.

Also, fixed the pretty-printer to be more intelligent about quoting things
with $s. In the old system (both in the Taupo development and before it)
``f $=> /\ p`` could be parsed, but would be printed as ``f => /\ p``,
which would ensure that what was printed couldn't be parsed back.
That behaviour is now fixed.

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.

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.

Made changes to allow slightly better feedback on a term_grammar error,
and also changed the construction of the precedence matrix to allow
equality relations to simply overwrite others without causing an error.
This allows { | } (set comprehension) to co-exist with the old style
conditional expression.

When let removal is done, the code now checks from occurrences of the
reserved word "and" and complains if it finds it.

Improved treatment of trailing characters left after a parse is complete,
both when it has failed and succeeded. In particular, need to have a version
of eof in fragstr to cope with trailing empty QUOTE frags.

Changes in Parse to call now-zeroed versions of export_theory etc in Theory.
Changes elsewhere to implement string literals.

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

Initial revision