Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
To: info-hol@leopard.cs.byu.edu
Subject: Re: How do I extend hol90.6's pretty printer?
In-Reply-To: Your message of "Thu, 23 Jun 94 16:47:44 EDT." <"i80fs2.ira.048:23.05.94.14.47.48"@ira.uka.de>
Date: Fri, 24 Jun 94 11:17:26 +0100
From: Richard Boulton <Richard.Boulton@cl.cam.ac.uk>
Message-Id: <"swan.cl.cam.:164900:940624101734"@cl.cam.ac.uk>

Further to Konrad's response to Ralf Reetz's question about extending the
hol90 pretty-printer, I will try to explain the details of the extension
facility.

The extension structure has the following signature in the version of hol90
I have here (Would someone please let me know if it has changed and I'll try
to rework my description.):

structure Extend_hol_pp :
   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

The function we are interested in when extending the pretty-printer for HOL
terms is extend_pp_term. This takes a pretty-printing function and returns
`()' (the only value of type `unit'). The pretty-printing function thus 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 itself a pretty-printing function. Let us forget about
this 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, we are left with a
function of type:

   Term.term -> PP.ppstream -> unit

which (hopefully) makes some sense as a pretty-printing function. It takes a
term and pretty-prints it on the specified ppstream returning `()'. As Konrad
has already said, the documentation for SML of New Jersey should be consulted
for more information on ppstreams.

Now let's look at an example similar to Ralf's. I will pretty-print the list
APPEND function as an infix `@'. For testing purposes, let's first bind `tm'
to an example term:

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

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:

- fun pp_append tm pps =
   let val {Rator,Rand = list2} = dest_comb tm
       val {Rator,Rand = list1} = dest_comb Rator
       val {Name,Ty} = dest_const Rator
   in  if Name = "APPEND"
       then (System.PrettyPrint.begin_block pps
                System.PrettyPrint.INCONSISTENT 3;
             pp_term pps list1;
             System.PrettyPrint.add_break pps (1,0);
             System.PrettyPrint.add_string pps "@";
             System.PrettyPrint.add_break pps (1,0);
             pp_term pps list2;
             System.PrettyPrint.end_block pps)
       else raise Fail ""
   end;
= = = = = = = = = = = = = = 
val pp_append = fn : term -> System.PrettyPrint.ppstream -> unit

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, I'll 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);
= = = = = 
val display = fn : ('a -> System.PrettyPrint.ppstream -> 'b) -> 'a -> unit

Trying the example again:

- display pp_append tm;
[1; 2] @ [3; 4; 5]
val it = () : unit

What about 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
define a function suitable for the extension facility by just throwing away
the first two arguments:

- fun pp_append_extension _ _ tm pps = pp_append tm pps;
val pp_append_extension = fn
  : 'a -> 'b -> term -> System.PrettyPrint.ppstream -> unit

Let's install this extension and see whether it works:

- tm;
val it = (--`APPEND [1; 2] [3; 4; 5]`--) : term
- Extend_hol_pp.extend_pp_term pp_append_extension;
val it = () : unit
- tm;
val it = (--`[1; 2] @ [3; 4; 5]`--) : term

Ok. And we can reset the pretty-printer to its original state:

- Extend_hol_pp.reset_pp_term ();
val it = () : unit
- tm;
val it = (--`APPEND [1; 2] [3; 4; 5]`--) : term

So what are the first two arguments for? Well, to pretty-print the arguments
of APPEND we are calling the top-level term printing function `pp_term'.
This appears to work for the example term, but it may not be satisfactory in
general because it resets the internal variables of the pretty-printer to
the values used for a top-level term. These variables appear in the second
argument we ignored:

   {boundvars:Term.term list, depth:int, gravity:gravity}

`boundvars' is a list of bound variables required because internally terms
are represented as deBruijn terms. Unless your pretty-printer is processing
terms involving lambda-abstractions this value can be passed on unchanged.
`depth' is the depth of the subterm being processed relative to the root of
the top-level term. It is used for eliding the display of subterms in large
terms. Normally its value should be decremented by one when making a recursive
call. `gravity' is a precedence value. This is used for controlling the
printing of parentheses. Since `@' is an infix, we might need to enclose the
`... @ ...' in parentheses or force arguments that are of lower precedence
to be printed in parentheses. I don't want to go into the details of the
various gravity values, but in the example the gravity to use is INFIX n
where n is the precedence value given to the infix `@'. Gravity values can be
compared using the function `gravity_geq' (a greater-than-or-equal-to
relation on gravity values).

So, how do we pass these values to recursive calls of the term printer when
pp_term doesn't take them as arguments? Well, that's what the first argument
we ignored is for:

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

At run time the system will pass a version of pp_term that takes boundvars,
depth and gravity as arguments to the function we have defined. Just call this
instead of pp_term.

I hope all this is of some help. I can go into more detail about the purpose
of the arguments if necessary, though perhaps the best approach to this is to
study the code for the pretty-printer in src/0/hol_pp.sml

I am also willing to answer individual queries by email.

Richard Boulton
University of Cambridge Computer Laboratory