Roger,

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.

Regards,

Phil


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
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

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

_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com

Reply via email to