Thanks for the reply, it is very much appreciated. To
> 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 languages.
Yes, I was a little naive in my last email. I studied the code more
carefully, in particular main_term_pp, and noticed the previously
explained too. There is no differentiating fall-back mechanism, and the
declared languages merely determine what printer is to be initially used
when a constant is printed. Control which printer is used can only be
effectively exercised by use of the PP_ENV environment when calling
pp_main_term (or I guess the current language if
pp_prefer_current_language is set to true, but this is too crude). If
the respective printer fails we always fall back on HOL to print all
> 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?
Yes, PP_ENV seems to be a good point to store the fall-back printer. I
guess we would also require to record a value for the fall-back printer
for each language to set up the initial environment. It would be a
possible design, but I decided to implement it in a slightly different
way as I didn't want to incur too many change to ProofPower, and there
would be a few other issues with that solution too.
Instead what I did was to modify the Z printer, namely by first
obtaining the Z printing functions through initial_env, then `wrapping'
them into some auxiliary code, and finally replacing the Z printer with
those new functions. The way the new Z printing functions behave is to
initially test if an expression is printable by the UTP printer. If so
they branch directly into the UTP printer rather than printing the term
themselves. In turns, the UTP printer attempts to print the expression,
and if that fails falls back on the Z printer rather then returning
PfNotPossible which would result in branching into the HOL printer.
There is a risk for indefinite recursion here in a certain error
situation, but it can be avoided by defining a function that determines
whether and expression is printable by the UTP print and use that as a
kind of contract between both printers.
This mutual recursion seems to work well, in particular that the UTP
printer is only entered when necessary, reducing the number of language
quotes generated (a general fall-back would probably produce a lot of
superfluous quotes, unless we use some trickery to determine if an
expression can be printed by a printer before producing the opening
quote). A final advantage of this method is that we can keep Z as the
current language to print out the UTP stuff. This is important since
some of the Z parsing and processing features seem not to work anymore
if we change the language from Z to something else. I couldn't get to
the bottom of this problem, I think it might have to do with the way
names or keys are generated for axioms when Z is set as the language.
I have attached a doc file of the source in case anyone may find this
useful, e.g. integrating a custom printer with the Z language.
A PDF is temporarly uploaded to
Rob Arthan wrote:
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