[isabelle] Formal BNF grammar (possibly for parser generation, e.g. with antlr 4) for Isar/HOL, for thy files?



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>



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