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.

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.

Many thanks as usual,

 Frank Zeyda, Dipl.-Inform. BSc PhD
 Research Associate
 High Integrity Systems Engineering Group
 Department of Computer Science
 University of York (UK)
 Phone: 0044-(0)1904-433244

Proofpower mailing list

Reply via email to