1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
|
\DOC install_user_printer
\TYPE {install_user_printer : string * (term -> unit) -> unit}
\SYNOPSIS
Install a user-defined printing function into the HOL Light term printer.
\DESCRIBE
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.
\FAILURE
Never fails.
\EXAMPLE
The user might wish to print every variable with its type:
{
# let print_typed_var tm =
let s,ty = dest_var tm in
print_string("("^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.
\SEEALSO
delete_user_printer, try_user_printer.
\ENDDOC
|
