Hi Rob,
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.
Ah yes, I understand; that change appeals. I think, however, we should
additionally parametrise PfRetry in terms of the printer (language) to
be used for retrial. Such would, I believe, provide the control I need.
We would then avoid having to set the current language according to the
entry point for retrial, and also there would be no need to enable
pp_prefer_current_language.
Some modification to imp031.doc would surely be necessary to implement
the above design. The Z pretty printer in imp064.doc also may possibly
be altered to support the configuration of tests on terms that determine
which expressions should NOT be printed by the Z printer, but causing
invocation of a term-specific retrial printer. As illustrated in my
previous post, this adoption can be achieved without having to touch
imp064.doc i.e. by replacing the default Z printer, that is extracting
and wrapping its printing functions.
Finally, I would still suggest to alter PP_ENV to maintain a list of
languages whose printers have failed; maybe by virtue of a field
pe_failed : string list. This would effectively allow main_term_pp, the
global entry point for printing, to decided whether a retrial printer
should be tried or not, eliminating the risk of possibly indefinite
recursion.
Implementing the above should not be extremely difficult, I guess it
would probably take a day or two. I will email you if I get round to do
it, or can get a student who might; I think it would make a nice
addition to the printing framework to fine-tune the pretty-printing
mechanism. ;-)
> 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.
Yes, what I meant here was declaring "UTP" as a language for Z'App in
the context of the theory "z_relations" (!); the advantage of this is
that the declared language would be implicitly inherited by all theories
deriving from "z_relations", ultimately making use_pp_utp_theory
redundant. The error message I get here is "The current theory,
z_relations, is not open for writing".
Best regards,
Frank
--
Frank Zeyda, Dipl.-Inform. BSc PhD
Research Associate
High Integrity Systems Engineering Group
Department of Computer Science
University of York (UK)
Email: ze...@cs.york.ac.uk
Phone: 0044-(0)1904-433244
WWW: http://www-users.cs.york.ac.uk/~zeyda/
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
