Thanks Rob My problem is that I need a lexical translation scheme that is not just specific to Z, but one that makes sense for any of the open-ended set of languages that ProofPower supports. I certainly don’t want to translate ASCII characters to non-ASCII.
I just don’t think ISO Z got this right. I’m certainly not going to disagree with you there! It is easy to design a grammar that allows the same symbol (a minus sign) to function both as an infix operator and a prefix operator. However, I failed to realise the importance of this before the Standards committee ran off and committed to the backwards incompatible change that gave you “a lot of trouble". I do sometimes wonder what they thought they were up to. I think sometimes people get so deep into solving a problem that they can’t step back and see that the problem isn’t real at all. As you say, a single symbol can perfectly well be used – and is, by everyone else in the world. As I said in a recent post to Phil Clayton, I abandoned my half-hearted hopes of providing Unicode support for ProofPower in general and some level of interoperability between ProofPower-Z and ISO Z at the same time. Inside ProofPower, interoperability with ISO Z and ProofPower-Z is best implemented using parsed syntax trees rather than lexical token streams. I can see the force of that – in fact the “lot of trouble” was precisely having to parse the specification rather than just lex it. Of course, perhaps one day, the Z Word Tools as a common front-end will also be an option. The trouble is that to go from ProofPower to ISO Z that translation would have to be done, and again I would have to have a parse tree from ProofPower to do it. I haven’t thought any more since our conversations of years ago about how a ZWT / Proofpower interface might work (and maybe such a thing wouldn’t be useful anyway), so my post was a bit of a knee-jerk reaction hoping to forestall a difficulty that will surely arise if we were ever to attempt such a thing. But I understand that force of your argument. The problem is certainly on the ISO Z side, and not of ProofPower’s makng! If you do ever think a Word interface would be useful, do get in touch, but I won’t hold my breath. I’ve not done any development on ZWT for ages – I don’t know whether anyone is using it in anger, though it still has a trickle of downloads. Good luck and best wishes Anthony
_______________________________________________ Proofpower mailing list Proofpower@lemma-one.com http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
