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