Email Gateway (Aug 18 2022 at 17:05): Email Gateway (Aug 18 2022 at 17:05):From: anhlevn@cims.nyu.edu
Hi everyone,
I am Anh. In my current research, I parse and generate code in
Isabelle/Isar. I really need the language specification, especially the
syntax of Isabelle/Isar. In the current reference manual, the syntax of
the language is not fully described and it's really hard to get it from
separate parts of the manual.
It would be really helpful if someone shows me some source to get that
kind of information.
Thank you very much
Anh
Email Gateway (Aug 18 2022 at 17:05):From: Makarius <makarius@sketis.net>
That's tricky, since Isabelle/Isar consists of pure semantics with some
aspects modeled in concrete syntax (which can be extended in user space in
compotationally complete ways). The isar-ref manual merely provides some
reconstruction of syntactic forms that work in practice, but this cannot
be complete by construction.
So the challange is to overcome the above requirement "I really need the
language specification". What is your concrete application?
Makarius
Email Gateway (Aug 18 2022 at 17:06):From: Makarius <makarius@sketis.net>
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.
Makarius
Email Gateway (Aug 18 2022 at 17:06):From: anhlevn@cims.nyu.edu
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
Anh
Last updated: Apr 25 2024 at 20:15 UTC