Filter
Top Products
66 CHAPTER 7. PARSING AND PRINTING
7.1 Overloading
The parser and printer allow front-end symbols to be overloaded, and tries to resolve
ambiguities by exploiting type information. Before a symbol can be overloaded, it
must be given a most general type, and any term it maps to must have a type
that is an instance of this type. During typechecking, the overloaded symbol is
given its most general type. If the typechecking process fixes the type sufficiently
to disambiguate, then the appropriate target is picked. Otherwise some instance
is defaulted, and typechecking repeated until all symbols have been resolved. For
example, the addition symbol is made overloadable:
make_overloadable "+" ‘:A->A->A‘;;
Now in order to make ”+” overloaded to natural number, integer and real ad-
dition, we do:
overload_interface ("+",‘(+):num->num->num‘);
overload_interface ("+",‘int_add:int->int->int‘);
overload_interface ("+",‘real_add:real->real->real‘);
Now the symbol + will map to one of three terms in the underlying represen-
tation, decided according to type. The default chosen is always the most recently
declared version, real addition after the above sequence. If the user wants to avoid
any defaults, then type information sometimes needs to be supplied. All the follow-
ing are unambiguous:
#‘x + 1‘;;
it : term = ‘x + 1‘
#‘x:int + y‘;;
it : term = ‘x‘
#‘(x + y):real‘;;
it : term = ‘x + y‘
Instead of mapping a symbol to multiple targets, one can always choose just one.
The function override interface is similar to overload interface, except that
it removes any existing mappings for the symbol first. For example, the user who
dislikes the use of equality to mean logical equivalence could remap HOL Light’s
interface as follows:
#parse_as_infix("<=>",(2,"right"));;
it : unit = ()
#override_interface ("<=>",‘(=):bool->bool->bool‘);;
it : unit = ()
#‘x = F‘;;
it : term = ‘x <=> F‘
#‘x <=> F‘;;
it : term = ‘x <=> F‘