Re: [isabelle] Asking for Isabelle/Isar language specification

On Mon, 21 Feb 2011, anhlevn at wrote:

Thank you very much for your reply. I am working on a domain specific language (DSL) whose one of the outputs is code in Isabelle/Isar. Actually, I may not need a complete language specification, but some syntactic forms that work in practice as you mentioned. It really helps if all syntax definitions are there, otherwise it takes me much more time.

Does that mean you merely want to generate Isar text, without parsing it? The full round trip would very hard indeed, but even just generating sources reliably is not easy.

The question here is if you generate sources for the system or for the user, or both. Generating sources just for the system is better avoided altogether --- it is much more robust to add language elements to the system that pull in the external DSL content into the logical environment. Thus you would benefit from the open-endedness of the Isar language, instead of struggling with it.

BTW, the real hard part is normally not the outer Isar language, but the inner term language. Even Isar itself just quotes the types, terms, propositions without looking into them. It is up to many layers of logical syntax (including specifications in user theories) that make up formal notation in Isabelle.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.