----------------------------------------------------------------------
overload_on                                                    (Parse)
----------------------------------------------------------------------
Parse.overload_on : string * term -> unit

SYNOPSIS
Establishes a term as one of the overloading possibilities for a string.

KEYWORDS
Parsing, pretty-printing, overloading.

LIBRARY
Parse

DESCRIBE
Calling {overload_on(name,tm)} establishes {tm} as a possible
resolution of the overloaded {name}.  The call to {overload_on} also
ensures that {tm} is the first in the list of possible resolutions
chosen when a string might be parsed into a term in more than one way,
and this is the only effect if this combination is already recorded as
a possible overloading.

When printing, this call causes {tm} to be seen as the operator
{name}.  The string {name} may prompt further pretty-printing if it is
involved in any of the relevant grammar’s rules for concrete syntax.

If {tm} is an abstraction, then the parser will perform
beta-reductions if the term is the function part of a redex position.

FAILURE
Never fails.

EXAMPLE
We define the equivalent of intersection over predicates:

   - val inter = new_definition("inter", Term`inter p q x = p x /\ q x`);
   <<HOL message: inventing new type variable names: 'a.>>
   > val inter = |- !p q x. inter p q x = p x /\ q x : thm

We overload on our new intersection constant, and can
be sure that in ambiguous situations, it will be preferred:

   - overload_on ("/\\", Term`inter`);
   <<HOL message: inventing new type variable names: 'a.>>
   > val it = () : unit
   - Term`p /\ q`;
   <<HOL message: more than one resolution of overloading was possible.>>
   <<HOL message: inventing new type variable names: 'a.>>
   > val it = `p /\ q` : term
   - type_of it;
   > val it = `:'a -> bool` : hol_type

Note that the original constant is considered overloaded to
itself, so that our one call to {overload_on} now allows for two
possibilities whenever the identifier {/\} is seen.  In order to make
normal conjunction the preferred choice, we can call {overload_on}
with the original constant:

   - overload_on ("/\\", Term`bool$/\`);
   > val it = () : unit
   - Term`p /\ q`;
   <<HOL message: more than one resolution of overloading was possible.>>
   > val it = `p /\ q` : term
   - type_of it;
   > val it = `:bool` : hol_type

Note that in order to specify the original conjunction
constant, we used the qualified identifier syntax, with the {$}.  If
we’d used just {/\}, the overloading would have ensured that this was
parsed as {inter}.  Instead of the qualified identifier syntax, we
could have also constrained the type of conjunction explicitly so that
the original constant would be the only possibility.  Thus:

   - overload_on ("/\\", Term`/\ :bool->bool->bool`);
   > val it = () : unit

The ability to overload to abstractions allows the use of simple
symbols for “complicated” effects, without needing to actually
define new constants.

   - overload_on ("|<", Term`\x y. ~(x < y)`);
   > val it = () : unit

   - set_fixity "|<" (Infix(NONASSOC, 450));
   > val it = () : unit

   - val t = Term`p |< q`;
   > val t = `p |< q` : term

   - dest_neg t;
   > Val it = `p < q` : term

This facility is used to provide symbols for “is-not-equal” ({<>}),
and “is-not-a-member” ({NOTIN}).

COMMENTS
Overloading with abandon can lead to input that is very hard to make
sense of, and so should be used with caution.  There is a temporary
version of this function: {temp_overload_on}.

SEEALSO
Parse.clear_overloads_on, Parse.set_fixity.

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