Handle add_numeral_form et al with user-deltas

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

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

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.

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

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.

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.

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

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.

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.

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

Greatly improved the efficiency of the treatment of the overloading when
type-checking is done. This results in what appears to be a threefold
speed-up. However, parsing as a whole is still too slow and this is
because of the lexer being so inefficient.

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.