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 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

Reply via email to