Prettyprinting HOL Expressions

For many of the types defined in HOL, there are prettyprinters available to print values of these types in an intelligible way. Among these types are hol_type, term, thm, lib, and rewrites. These have been installed in a system prettyprinter table, so that when the system prints values of these types, the special prettyprinter is automatically invoked on the value. This saves on explicit invocation of prettyprinters, making interaction more pleasant.

Extending the prettyprinters

Most of the HOL prettyprinters depend on the prettyprinters for types and terms. Thanks to Richard Boulton, these have been made extensible. The structure Extend_hol_pp contains functions for incrementally extending the system pretty-printers for HOL types and terms, and for resetting them to their original state. The signature of this structure is:
    sig
       datatype gravity = TOP | APPL | INFIX of int | WEAK | BOTTOM
       val gravity_geq : gravity -> gravity -> bool

       val extend_pp_type :
          (({depth:int, gravity:gravity} ->
            Term.Type.hol_type -> PP.ppstream -> unit) ->
           ({depth:int, gravity:gravity} ->
            Term.Type.hol_type -> PP.ppstream -> unit)) -> unit

       val extend_pp_term :
          (({boundvars:Term.term list, depth:int, gravity:gravity} ->
            Term.term -> PP.ppstream -> unit) ->
           ({boundvars:Term.term list, depth:int, gravity:gravity} ->
            Term.term -> PP.ppstream -> unit)) -> unit

       val reset_pp_type : unit -> unit
       val reset_pp_term : unit -> unit
    end
Considering terms (and by analogy, types), there are two functions: one to extend the printer; the other to reset it to the start-up state. Users can provide a special-purpose pretty-printing function for whatever special printing behaviour they require. This function will be tried first on each call (top-level and recursive) to the pretty-printer. If it fails for any reason, the original printer (or the previously extended version) is called.

The argument types to the extension functions are complex. Let's dissect the type of extend_pp_term; to start, it takes a function and returns `()' (the only value of type unit). This function has the following type:

    ({boundvars:Term.term list, depth:int, gravity:gravity} ->
        Term.term -> PP.ppstream -> unit) ->
    ({boundvars:Term.term list, depth:int, gravity:gravity} ->
        Term.term -> PP.ppstream -> unit)
Its first argument is a pretty-printing function. Let us forget about this argument for the moment, leaving us with a function of type:
    {boundvars:Term.term list, depth:int, gravity:gravity}
      -> Term.term -> PP.ppstream -> unit
If we also ignore the first argument of this function (it represents the changing context that the function will operate in), we are left with a function of type:
    Term.term -> PP.ppstream -> unit
which (ought to) make some sense as a pretty-printing function which takes a term and pretty-prints it on the specified ppstream before returning `()'. The documentation for SML of New Jersey should be consulted for more information on the ppstream type.

Now we return to the context parameter. The special-purpose prettyprinter must handle the context that it is called in. The context is a record with fields boundvars, depth, and gravity. These fields are used to decide how to print the current subterm, and are modified for recursive calls to the prettyprinter.

boundvars
The boundvars argument is a list of the bound variables of the abstractions passed through in descending the term, the scope in other words. The list is indexed by the de Bruijn number when a bound variable needs to be printed. Unless your prettyprinter is processing terms involving lambda-abstractions this value can be passed on unchanged. However, if you are doing processing of such binders, the binding occurrences of variables should be put on the boundvars list in order of textual occurrence, i.e., boundvars is treated like a stack.
depth
The depth argument to the print functions is the print depth; it should be decremented on each recursive call. When it reaches zero, the subterm is elided. Starting with a negative value prevents elision from occurring regardless of how deep the term is.
gravity
The datatype for precedence (called gravity) is available to the user. There are five constructors. TOP is the highest (most-tightly binding) precedence; APPL is for applications, INFIX is for the infix operators and takes an integer argument; WEAK is used for bindings and for mixfixes such as conditional expressions; and BOTTOM is the lowest precedence value. Generally, if the gravity of the context is greater or equal to that of the current subterm, then the current subterm should be bracketed.

Example

The use of the extensibility functions is illustrated in the session below in which a function to print conditional expressions as

    if term then term else term
instead of as
    term => term | term
is installed. Note that the call to dest_cond fails if the term is not a conditional expression and so forces the original printer to be used. The following is the definition of the custom prettyprinting function:
    local open PP Extend_hol_pp
    in
    fun pp_ite pp_tm {boundvars:term list,depth,gravity} tm ppstrm =
       if (depth = 0)
       then raise Fail "pp_ite"
       else let val {cond,larm,rarm} = dest_cond tm
                val parenth = gravity_geq gravity WEAK
                val params = {boundvars=boundvars,depth=depth-1,gravity=TOP}
            in  
                if parenth then add_string ppstrm "(" else ();
                begin_block ppstrm CONSISTENT 0;
                add_string ppstrm "if ";
                (pp_tm params cond ppstrm : unit);
                add_break ppstrm (1,0);
                add_string ppstrm "then ";
                pp_tm params larm ppstrm;
                add_break ppstrm (1,0);
                add_string ppstrm "else ";
                pp_tm params rarm ppstrm;
                end_block ppstrm;
                if parenth then add_string ppstrm ")" else ()
            end
      end;
Let us bind a test case:
    - val tm = (--`APPEND ((n = 0) => [] | [n]) [1;2;3]`--);

    val tm = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : term

Now, we extend the system prettyprinter and test it:
    - Extend_hol_pp.extend_pp_term pp_ite;

    val it = () : unit

    - tm;

    val it = (--`APPEND (if (n = 0) then [] else [n]) [1; 2; 3]`--) : term

    - Extend_hol_pp.reset_pp_term ();

    val it = () : unit

    - tm;

    val it = (--`APPEND ((n = 0) => [] | [n]) [1; 2; 3]`--) : term

How to develop a special-purpose prettyprinter

It's not so simple to see how to go about writing a custom prettyprinter, so we will step through an example of such a development. (The example and a lot of the accompanying commentary has been taken from a message Richard Boulton sent to the info-hol mailing list on June 24, 1994.)

Suppose we want to pretty-print the list APPEND function as an infix (@). First let's bind an example term:

    val tm = (--`APPEND [1;2] [3;4;5]`--);

and set-up a ppstream to write to std_out:
    - val std_pps =
       System.PrettyPrint.mk_ppstream
          {consumer = (fn s => output (std_out,s)),
           flush = (fn () => ()),
           linewidth = 78};

    val std_pps = - : System.PrettyPrint.ppstream
Now, a first attempt at defining a pretty-printing function would be the following:
    fun pp_append tm ppstrm =
       let val {Rator,Rand = list2} = dest_comb tm
           val {Rator,Rand = list1} = dest_comb Rator
       in  if #Name(dest_const Rator) = "APPEND"
           then (System.PrettyPrint.begin_block ppstrm
                    System.PrettyPrint.INCONSISTENT 3;
                 pp_term ppstrm list1;
                 System.PrettyPrint.add_break ppstrm (1,0);
                 System.PrettyPrint.add_string ppstrm "@";
                 System.PrettyPrint.add_break ppstrm (1,0);
                 pp_term ppstrm list2;
                 System.PrettyPrint.end_block ppstrm)
           else raise Fail ""
       end;
The applications of the destructor functions (dest_comb and dest_const) cause an exception to be raised if the term is anything other than a constant applied to two arguments. An explicit test is included to make sure the constant is APPEND. To process the arguments of APPEND, pp_term (the top-level pretty-printing function for terms) is applied to them.

Let's try this function on our example term:

    - pp_append tm std_pps;

    val it = () : unit
Nothing is displayed because the ppstream has not been flushed! Let's do that:
    - System.PrettyPrint.flush_ppstream std_pps;

    [1; 2] @ [3; 4; 5]val it = () : unit
To avoid tedium later, we define a function to apply a pretty-printing function and flush the ppstream (and add a newline):
    - fun display f x =
       (System.PrettyPrint.begin_block std_pps 
                          System.PrettyPrint.INCONSISTENT 0;
        f x std_pps;
        System.PrettyPrint.add_newline std_pps;
        System.PrettyPrint.end_block std_pps;
        System.PrettyPrint.flush_ppstream std_pps);
Trying the example again we get:
    - display pp_append tm;

    [1; 2] @ [3; 4; 5]
    val it = () : unit
The custom prettyprinter must fail on non-conforming terms:
    - display pp_append (--`1 + 3`--);

    uncaught exception Fail ""

    - display pp_append (--`T`--);

    uncaught exception HOL_ERR
In principle, this is all that needs to be done for this example. We can now define a function suitable for the extension facility by just throwing away the first two arguments:
    - fun pp_append_extension _ _ tm = pp_append tm;

    val pp_append_extension = fn
      : 'a -> 'b -> term -> System.PrettyPrint.ppstream -> unit
Let's install this extension and see whether it works:
    - Extend_hol_pp.extend_pp_term pp_append_extension;

    val it = () : unit

    - tm;

    val it = (--`[1; 2] @ [3; 4; 5]`--) : term

    - Extend_hol_pp.reset_pp_term ();

Handling context

So what are the first two arguments for? They are for making recursive calls and making use of the context. Let us go back to the definition of pp_append.
    fun pp_append tm ppstrm =
     let val {Rator,Rand = list2} = dest_comb tm
         val {Rator,Rand = list1} = dest_comb Rator
     in  if #Name(dest_const Rator) = "APPEND"
         then (System.PrettyPrint.begin_block ppstrm
                  System.PrettyPrint.INCONSISTENT 3;
               pp_term ppstrm list1;
               System.PrettyPrint.add_break ppstrm (1,0);
               System.PrettyPrint.add_string ppstrm "@";
               System.PrettyPrint.add_break ppstrm (1,0);
               pp_term ppstrm list2;
               System.PrettyPrint.end_block ppstrm)
         else raise Fail ""
     end;
To pretty-print the arguments of APPEND we are calling the top-level term printing function pp_term (bound to Hol_pp.pp_term, in a vanilla hol90 system). This appears to work for the example, but it is not apt to be satisfactory in general because pp_term resets the parameters of the pretty-printer to initial values suitable for a top-level prettyprint. These parameters appear in the second argument to pp_append_extension, which we ignored, the context:
    {boundvars:Term.term list, depth:int, gravity:gravity}

So, how do we pass the current context to recursive calls of the term printer when pp_term doesn't take its context as an argument? Well, that's what the first argument we ignored is for; it's a recursor, a "context-sensitive" version of the current pp_term with type:

    {boundvars:Term.term list, depth:int, gravity:gravity}
     -> Term.term -> PP.ppstream -> unit
At run time the system will pass a recursor and a context {boundvars, depth,gravity} as arguments to the following improved version of pp_append_extension. To perform a recursive prettyprint, the recursor should be invoked on an appropriately adjusted context. For example, we might have the following recursive calls and context-sensitive actions in a realistic HOL prettyprinter extension:
    local open PP Extend_hol_pp
    in
    fun pp_append_extension' recursor {boundvars,depth,gravity} tm ppstrm =
       if (depth = 0) then add_string ppstrm "<term>"
       else
       let val {Rator,Rand = list2} = dest_comb tm
           val {Rator,Rand = list1} = dest_comb Rator
       in
       if #Name(dest_const Rator) = "APPEND"
       then let val my_gravity = INFIX 600
                fun parenth s = 
                     if (gravity_geq gravity my_gravity)
                     then add_string ppstrm s else ()
                 val context' = {depth=depth-1,gravity=my_gravity,
                               boundvars=boundvars}
            in 
               begin_block ppstrm System.PrettyPrint.INCONSISTENT 3;
               parenth "(";
               recursor context' list1 ppstrm;
               System.PrettyPrint.add_break ppstrm (1,0);
               System.PrettyPrint.add_string ppstrm "@";
               System.PrettyPrint.add_break ppstrm (1,0);
               recursor context' list2 ppstrm;
               parenth ")";
               end_block ppstrm
            end
       else raise Fail ""
       end
    end;
The following examples show how context is being tracked. The first shows that brackets are appropriately added when the APPEND occurs in a higher binding context; the second shows the opposite situation.
    - Extend_hol_pp.extend_pp_term pp_append_extension';

    - --`P (APPEND [1;2;3] [4;5;6]):bool`--;

    val it = (--`P ([1; 2; 3] @ [4; 5; 6])`--) : term

    - --`APPEND [1;2;3] [4;5;6] = APPEND [1] [7;8;9]`--;

    val it = (--`[1; 2; 3] @ [4; 5; 6] = [1] @ [7; 8; 9]`--) : term
The last examples show that depth is being monitored appropriately. Notice that the standard prettyprinter has a different notion of ellipsis!
    - Globals.max_print_depth := 2;
    val it = () : unit

    - --`P (APPEND [1;2;3] [4;5;6]):bool`--;

    val it = (--`P (<term> @ <term>)`--) : term

    - --`[APPEND [1;2;3] [4;5;6];[1];[7;8;9]]`--;

    val it = (--`[<term> @ <term>; [ ... ]; [ ... ;  ... ;  ... ]]`--) : term

User Manual Table of Contents
Beginning of HOL syntax
Beginning of Prettyprinting HOL Expressions
Konrad Slind, slind@informatik.tu-muenchen.de