Re: [isabelle] Asking for Isabelle/Isar language specification
I want to generate Isar text, and I also need to parse it. I generate code
using AST transformation, from my DSL ASTs to Isar ASTs. I have been
working on code generation for a while. The code is just for the system,
but it's necessary, can not be avoided.
And you're right. I only have troubles with types, terms, and
propositions; not with Isar outer language. But I don't need all kinds of
types, terms, propositions. I just need what I want to generate. So, it
takes more time, but is still manageable.
Thank you very much
On Wed, February 23, 2011 6:54 am, Makarius wrote:
> 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