Provide tiny bit more information in an exception message

Allow custom p/printers to fire more reliably when in "rator" pos'n

The treatment of COND worked because of special-handling for "case"
constants, and for LET it works because the special printer just
checks the underlying head constant. However, for trickier patterns,
you need to call Overload.strip_comb, and if this succeeds for the
larger term, it needs to succeed when called again on the rator
sub-term. Previously, for no obvious reason, the second call would
effectively report that there was no pattern to be had.

Add test-case showing desired behaviour with monad pretty-printer.

Closes #522

Remove some early code assuming term is an equality type

Handle add_numeral_form et al with user-deltas

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

Make overloading's print-data easier to inspect

Make PP.avoid_unicode also work for bare constant names.

Previously, unicode infixes, suffixes were avoided, but if one did an
outright

overload_on("unicode-ish thing", ``constant``)

then PP.avoid_unicode wouldn't help.

Pretty-printer now annotates consts with their real names and types.

In "complicated" overload situations, such as the overloads for NOTIN
and <>, the annotation can't point to a "real" underlying constant,
but does still provide the type for the emacs tool-tips.

In passing, also create a new annotation form, the SymConst as well as
the Const. This is done for the TeX backend's benefit, so that it can
avoid treating things like + the same as normal identifiers. This
works well for math-mode munging where you want "+" to map to $+$, but
want "INSERT" to map to \textsf{INSERT}.

Closes #39

Implement "ignore overloads for printing" feature.

Demonstrate with change to list, so that ``~MEM a l`` prints that way
rather than as ``a NOTIN set l``. Selftest checks this, and also that
``x NOTIN {2;3;4}`` continues to print the right way.

Closes #95.

Use sets instead of lists to keep Overload print_maps small.

Thanks to Scott to raising this issue. The use of a functor is so that
I can use the same code for Anthony's use of LVTermNet, but have the
underlying type be a list (this for the sake of backwards
compatibility).

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.

Slightly tweak the way overload patterns are 'sized'.

The effect is to make a pattern than binds a single variable 'p' to a pair
(x,y), the same size as a pattern that binds 'a' to the 'x', 'b' to the 'y'
and has (a,b) in the pattern.

Modify overload's internal timestamps to be successive integers rather than Time values.

This prevents two very quick overload events from getting the same time-stamp, which I just
observed happening (on Windows at least).

Fix pretty-printing of {} with Unicode off.

Requires a moderately substantial re-organisation of LVTermNet; this code
is now explicitly a map from keys (terms) to multiple possible forms
underneath. Its interface suggested this anyway, but the implementation
actually only mapped from a term to one possible printing form. This meant
that when a printing form was removed (as when switching Unicode off, which
removed the Unicode symbol as the form for {}), there was nothing left for
the term to map to, even though we'd earlier mapped term EMPTY to string
EMPTY.

Adjust the way multiple matching abbreviations are discriminated amongst.

In particular, it used to be that if an abbreviation required a smaller
type instantiation, it would be preferred. Now, something that requires
a smaller *term* instantiation gets the nod. Type instantiation size is
the second factor considered, and then recentness.

Also add raw_print_map entry-point to Overload module to add debugging.

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.

Fix for some bugs found while hacking at isPREFIX and
rich_list$IS_PREFIX. In particular, the syntactic pattern printing
was wrong in the situation where the name being overloaded wasn't the
basis for a rule (infix, mixfix..) in the concrete syntax. This also
prompted some reorganisation to ensure that special cases like numeric
literals get checked for earlier than they were.

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

A bunch of fixes for situations involving out-of-date constants
contaminating the overloading maps.
(I now think this was Konrad's real bug.)

Fix for a problem spotted by Konrad to do with the pretty-printing of
old constants. This code may end up not being called by the
pretty-printer, but keeping the code working is still worth doing.

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.

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

Fix for a bug detected by Tom Ridge. When two constants were overloaded to
the same name, and also shared the same type-operator name (but not the
same theory), the code figuring out the overloading got it wrong, and gave
any uses of the overloaded name just one type from the outset, totally
precluding the other constant.

Adapting to new Basis (and SML/NJ).

On a quest to eliminate bad uses of lists as a lookup structure. This
use in Overload is definitely bad because the number of constants in a
system can and does get quite large. The code here is called most
often as part of the pretty-printer, so this is not an issue of major
importance, but it's also an easy fix to make.

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.

Revised this in line with my post to hol-developers yesterday. Now
this flag is a registered trace. Also altered the message to only
print when the system is interactive.

*** empty log message ***

Changed a commonly-issued load message so that it fits on a line.

The way that parser directives get emitted onto theory files means
that these load messages from theories get duplicated (I think).

Minor changes.

Slightly improved messgae emitted when merging overload information
forces the system to choose a preferred name for a constant.

Improved pretty-printer so that it prints record functions that can't
be printed using special syntax with their real names, if this is
is in the forward direction part of the overload map (which is likely).
Also, cleaned up overload maps so that two copies of overloaded constants
with different types aren't stored.

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

Overload.sml now uses a Binarymap internally to store the map from
names to sets of constants. A slight change to Overload.sig affected
only term_grammar's internals, and only the grammar pretty-printer
at that.

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

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.

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

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.

Fixed this so that a call to overload_on will ensure that the
given resolution will be the first choice in ambiguous situations.

Made adding an overloaded thing properly idempotent. In particular, we
don't want duplicates of name-type pairs cluttering up the actual_ops
part of the overload_op_info record.

Implemented new operation of grammar merging. This will be used
to deal with the dodgy implementation of internal grammar value
calculation done in theories.

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.