See attached for an example of adding a new object language (that can be mixed with existing HOL and Z terms). This makes use of HOL_reader which saves having to write a new reader but requires your lexer to consume Lex.INPUT values. The attached example does not actually provide the lexer/parser - I assume you're ok with that.

If you are producing a new object language, it is probably best to use HOL_reader. (One reason not to is if your language has any white space oddities.) HOL_reader is used for Z quotations in ProofPower-Z, for example.

If your object language allows nested term quotations, your lexer will need a token for terms that is produced when a Lex.Term input is encountered.



Roger Bishop Jones wrote:
Does anyone have a small/simple example of how to add a new language to ProofPower?

Roger Jones


Proofpower mailing list

Attachment: reader.sml.gz
Description: GNU Zip compressed data

Proofpower mailing list

Reply via email to