Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Formal BNF grammar (possibly for parser genera...

view this post on Zulip Email Gateway (Aug 23 2022 at 09:19):

From: Alex Meyer <alex153@outlook.lv>
Hello!

I am trying to ignite my framework (in very early, experimental stage, I still don’t know whether I can succeed) for program synthesis/algorithm synthesis and all of that reduces to the generation of the thy files, like one for the insertion sort algorithm https://www.isa-afp.org/browser_info/current/AFP/Imperative_Insertion_Sort/Imperative_Insertion_Sort.html (from https://www.isa-afp.org/entries/Imperative_Insertion_Sort.html). For that to happen I am going to try to read thy files, translate concrete syntax to AST, manipulate, translate from AST to concrete Isabelle syntax and write back thy files. To set up such infrastructure more or less automatically, the BNF files for the HOL/Isar grammar should be available. I am trying to find them, so far I have found:

https://isabelle.in.tum.de/dist/Isabelle2020/doc/logics.pdf

Fig. 2.2. is HOL grammar (inner grammar)

https://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf

Fig. 2.2 is Isabelle outer grammar, Isar reference contains lot of grammar rules apart from this picture – I wonder – whether they are available as one file.

Repository https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/ (and others) contain BNF_... files that may hint to Backus-Naur Form, but I have heard that BNF can be abbreviation for something else too in Isabelle context.

So – maybe there is some set of complete BNF grammar files for thy files, than contain both inner and outer syntax. E.g. there is https://github.com/antlr/grammars-v4/blob/master/fol/fol.g4 grammar which ANTLR 4 uses for generation of Java parser for FOL (classical syntax), and from that parser I can easily build processors that extracts AST from the parsed FOL text. I would like to gather full grammar for thy files and use it with ANTLR to generate Java parser for thy files. And then I can write AST manipulate code in Java.

___Is it achievable task, are there similar efforts and are there complete grammars for thy files?___

I guess that already found grammars (HOL and Isar outers syntax) is sufficient for me to continue my effort, but maybe there are some roadblocks ahead?

I have heard about Czech efforts to set up neural theorem provers and possibly they use some custom thy parsers and thy AST manipulators as well.

Thanks, Alex

[https://ipmcdn.avast.com/images/icons/icon-envelope-tick-green-avg-v1.png]<http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail> Virus-free. www.avg.com<http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail>

view this post on Zulip Email Gateway (Aug 23 2022 at 09:19):

From: Simon Wimmer <wimmersimon@gmail.com>
---------- Forwarded message ---------
Von: Simon Wimmer <wimmersimon@gmail.com>
Date: Do., 9. Juli 2020 um 10:04 Uhr
Subject: Re: [isabelle] Formal BNF grammar (possibly for parser generation,
e.g. with antlr 4) for Isar/HOL, for thy files?
To: Alex Meyer <alex153@outlook.lv>

Hi Alex,

there is no such thing as a BNF for Isabelle's inner or outer syntax.
To be able to fully parse theory files, you need to have loaded the full
context information by checking the underlying stack of theories first.
This means that theory files can only really be parsed by Isabelle.

You can get various versions of the "AST" by hooking into Isabelle/Scala or
using the "isabelle dump" tool.
However, it seems to me that you have in mind would work much better as a
fancy parser for inner syntax.
You can find examples of this in these AFP entries:

Simon

Am Do., 9. Juli 2020 um 09:44 Uhr schrieb Alex Meyer <alex153@outlook.lv>:

Hello!

I am trying to ignite my framework (in very early, experimental stage, I
still don’t know whether I can succeed) for program synthesis/algorithm
synthesis and all of that reduces to the generation of the thy files, like
one for the insertion sort algorithm
https://www.isa-afp.org/browser_info/current/AFP/Imperative_Insertion_Sort/Imperative_Insertion_Sort.html
(from https://www.isa-afp.org/entries/Imperative_Insertion_Sort.html).
For that to happen I am going to try to read thy files, translate concrete
syntax to AST, manipulate, translate from AST to concrete Isabelle syntax
and write back thy files. To set up such infrastructure more or less
automatically, the BNF files for the HOL/Isar grammar should be available.
I am trying to find them, so far I have found:

https://isabelle.in.tum.de/dist/Isabelle2020/doc/logics.pdf

Fig. 2.2. is HOL grammar (inner grammar)

https://isabelle.in.tum.de/dist/Isabelle2020/doc/isar-ref.pdf

Fig. 2.2 is Isabelle outer grammar, Isar reference
contains lot of grammar rules apart from this picture – I wonder – whether
they are available as one file.

Repository
https://isabelle-dev.sketis.net/source/isabelle/browse/default/src/HOL/
(and others) contain BNF_... files that may hint to Backus-Naur Form, but I
have heard that BNF can be abbreviation for something else too in Isabelle
context.

So – maybe there is some set of complete BNF grammar files for thy files,
than contain both inner and outer syntax. E.g. there is
https://github.com/antlr/grammars-v4/blob/master/fol/fol.g4 grammar which
ANTLR 4 uses for generation of Java parser for FOL (classical syntax), and
from that parser I can easily build processors that extracts AST from the
parsed FOL text. I would like to gather full grammar for thy files and use
it with ANTLR to generate Java parser for thy files. And then I can write
AST manipulate code in Java.

___Is it achievable task, are there similar efforts and are there complete
grammars for thy files?___

I guess that already found grammars (HOL and Isar outers syntax) is
sufficient for me to continue my effort, but maybe there are some
roadblocks ahead?

I have heard about Czech efforts to set up neural theorem provers and
possibly they use some custom thy parsers and thy AST manipulators as well.

Thanks, Alex

[https://ipmcdn.avast.com/images/icons/icon-envelope-tick-green-avg-v1.png
]<
http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail>
Virus-free. www.avg.com<
http://www.avg.com/email-signature?utm_medium=email&utm_source=link&utm_campaign=sig-email&utm_content=webmail
>

view this post on Zulip Email Gateway (Aug 23 2022 at 09:19):

From: Manuel Eberl <eberlm@in.tum.de>
People are also generally discouraged from generating .thy files
textually. It is usually a better approach to write an Isabelle command
that does what the generated theory file is supposed to do (definitions,
proofs, etc.) in ML.

However, generating small snippets (like Sledgehammer does) might be
okay; maybe that's what you were thinking of.

Manuel

Last updated: Apr 24 2024 at 20:16 UTC