Frank Zeyda wrote:
Hi Rob,
> 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.
That wasn't quite what I meant. I was suggesting that you could makeyour
pretty-printing functions return PfRetry (as opposed to PfOK or
whatever) if you want the system to try with another language. This
would give something like what you want without changing Z
pretty-printer provided you set the flag pp_prefer_current_language
true, so that the inside a Z term your UTP pretty-printer would get
tried first in cases where both the UTP pretty-printer and the Z
pretty-printer would be applicable.
However, the way you are doing it gives you more control and doesn't
seem to involve too much duplication of code.
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
http://www-users.cs.york.ac.uk/~zeyda/tp/utp-pretty.pdf
Thanks for that. Let me know if there are any changes to ProofPower that
would help you with this.
By the way, your document has a comment suggesting that you can't
declare "UTP" as an extra language for Z'App but you should be able to.
Regards,
Rob.
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
