Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
Date: Thu, 23 Jun 94 18:32:36 BST
From: konrad <konrad@dcs.gla.ac.uk>
Message-Id: <9406231732.AA14949@hawaii.dcs.gla.ac.uk>
To: info-hol@leopard.cs.byu.edu
In-Reply-To: reetz's message of Thu, 23 Jun 1994 22:47:44 +0200 <"i80fs2.ira.048:23.05.94.14.47.48"@ira.uka.de>
Subject: How do I extend hol90.6's pretty printer?


Ralph Reetz writes

> I would like to extend the pretty printer of hol90.6 to pretty-print
> some sort of terms, e.g. I have defined an infix "sappend" and would
> like to get it pretty-printed as "^". 

There are a couple of problems here. The first is that you are using two
different names for the same thing. Usually, one wants the parser and
prettyprinter to agree, i.e., prettyprinting followed by parsing should
be the identity function. In my experience, this makes working in the
system more pleasant. Second, there is a snag in hol90, since occurrence
of "^" in a term is taken to signal an antiquote. Hence "^" is not an
allowed constant name.

> Assume I have a function fun my_term_2_string: term -> string, which
> takes a term of a certain type and transforms the term into a string. If
> the term has not the certain type, it will fail. I would like to extend
> the pretty-printer by this function.

I assume that you are using Richard Boulton's package for doing
prettyprinter extension. The interface for this prototype is undeniably
complex, but it seems to me that your basic assumption, i.e., that
my_term_2_string has type "term->string" is too simplistic.

The basic problem is to write a mini-prettyprinter for a fragment of hol
terms. On the face of it, this is not too difficult; use the routines
provided in the PP structure. If you don't know how to use the SML/NJ
prettyprinting routines provided there, consult the SML/NJ system
documentation. There's an example there and it works. 

Suppose you've passed that milestone and you are relatively happy about
writing prettyprinters, i.e., ML functions of type "ppstream -> ty ->
unit". Now assume that the fragment of hol terms you wish to print
specially is all terms of hol_type ":special". Write a custom
mini-prettyprinter that takes a term and checks if it is of hol_type
"special", raising an exception if it's not and otherwise prettyprinting
the term in the custom format. This custom function can be written and
(mostly) tested before worrying about how to add it to the system
prettyprinter.

Integrating the custom prettyprinter requires solving the problem of
recursive calls: a custom pp may make calls to itself on subterms, but
in the recursive world of terms, sometimes one wants to make an
intermediate call to the system prettyprinter, which must therefore
already know about the custom pp. This requires a delicate treatment of
circularity. Richard's package enables thinking about this circularity
to be mostly avoided, at the cost of having to deal with various ideas
of scope and precedence. Admittedly, it's a bit of a black art.

Konrad.