install_user_printer : string * (formater -> term -> unit) -> unit
Install a user-defined printing function into the HOL Light term printer.
The call install_user_printer(s,pr) sets up pr inside the HOL Light
toplevel printer. On each subterm encountered, pr will be tried first, and
only if it fails with Failure ... will the normal HOL Light printing be
invoked. The additional string argument s is just to provide a convenient
handle for later removal through delete_user_printer. However, any previous
user printer with the same string tag will be removed when
install_user_printer is called. The printing function takes two arguments,
the second being the term to print and the first being the formatter to be
used; this ensures that the printer will automatically have its output sent to
the current formatter by the overall printer.
- FAILURE CONDITIONS
The user might wish to print every variable with its type:
# let print_typed_var fmt tm =
let s,ty = dest_var tm in
pp_print_string fmt ("("^s^":"^string_of_type ty^")") in
val it : unit = ()
val it : thm =
|- !(m:num) (n:num) (p:num).
(m:num) + (n:num) + (p:num) = ((m:num) + (n:num)) + (p:num)
Modification of printing in this way is particularly useful when the HOL logic
is used to embed some other formalism such as a programming language, hardware
description language or other logic. This can then be printed in a ``native''
fashion without any artifacts of its HOL formalization.
Since user printing functions are tried on every subterm encountered in the
regular printing function, it is important that they fail quickly when
inapplicable, or the printing process can be slowed. They should also not
generate exceptions other than Failure ... or the toplevel printer will start
- SEE ALSO