Frank Zeyda wrote:
Dear ProofPower Users,
I have the following problem, hope someone might be able to help.
At the moment I am trying to define a pretty printer "UTP" in order to
print certain terms in (mostly) Z expressions in a particular way. I
used the function set_printer from PrettyPrinterSupport to configure the
new pretty printer, providing the various functions for possible shapes
of basic HOL terms. (To introduce a custom symbol for the special quote
I also used set_start_quote).
My question is related to how to control which Z terms are printer using
the UTP printer. For that sake I defined a new theory in which I set the
language to "UTP" via set_current_language "UTP". This, however, did not
result in Z terms such as "a \cup b" being printed through the UTP
printer. It seems that the printer that is used for a particular
constant is determined by the language of the theory in which the
constant is defined. To solve the problem, declare_const_language can be
used to specify manually what printer should be used for a particular
constant in a particular theory context. What is in particular necessary
to channel printing of any kind of Z function applications through UTP
is to change the language for the Z'App function.
declare_const_language ("Z'App", "UTP");
The printing functions for the UTP printer, however, are not meant to
print all Z terms, only certain ones. In that, they may return
PfNotPossible as a result. In such a case I would like to fall back on
the original printer of the constant as specified in the theory where
the constant is defined. What seems to be the case, however, is that
then the HOL printer is used. I'm not sure why this happens, and whether
it is possible to circumvent this. Strangle, when I call
get_const_language "Z'App" in the context of the newly created theory,
it gives me ["Z", "UTP"] as a result. So if the UTP printer fails, it
somehow suggests that in the next instance the Z printer may be, and not
the HOL printer.
Unfortunately, this isn't how this works. This facility to have more
than one language for a constant is intended for things like the
propositional connectives which are identical (for example) in HOL or Z.
The pretty-printer expects all the pretty-printers for the languages in
the list to be able to handle the constant and falls back on a default
HOL pretty-printer if the chosen pretty-printer can't. This is just
intended to minimise the number of language changes in the printed form
of something that contains things that are in the intersection of two
Apologies this is rather a specific, but any advise on this would be
very much appreciated. I could think of one solution, that is to
manually invoke the printing functions of the Z printer within those of
the UTP printer if printing fails, but this is a bit tricky since they
are not directly exposed by the implementation. What are the mechanisms
for fall-back if one pretty-printer fails? This might be the key to
solving the problem.
As things stand it falls back to a default pretty-printer for HOL. I
think the safest way to give you the facility you want would be to add
an extra constructor (say PfRetry) to the data type PFUN_ANS allowing
your pretty-printer to indicate explicitly that it expects one of the
other languages to be able to cope. Would that do the job?
Proofpower mailing list