install_user_printer : string * (formater -> term -> unit) -> unit

SYNOPSIS

Install a user-defined printing function into the HOL Light term printer.

DESCRIPTION

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

Never fails.

EXAMPLE

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
    install_user_printer("print_typed_var",print_typed_var);;

  val it : unit = ()
  # ADD_ASSOC;;
  val it : thm =
    |- !(m:num) (n:num) (p:num).
           (m:num) + (n:num) + (p:num) = ((m:num) + (n:num)) + (p:num)

USES

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.

COMMENTS

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