Re: [isabelle] Asking for Isabelle/Isar language specification
On Mon, 21 Feb 2011, anhlevn at cims.nyu.edu 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
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