Re: [isabelle] Isabelle code for getting in-memory representation (abstract syntax trees) for complete theory file (tree of loaded theories)



Dear Alex,

2) maybe I would like to preprocess code of theory files for the processing with neural networks in the style of https://arxiv.org/abs/2006.09265 I have no clear thought yet, but I guess that this research can be extended if I can have full controle for the in-memory structurs of theory files.

Regarding https://arxiv.org/abs/2006.09265, I was writing a parser for .thy files in Python to extract information. The code should be available from the supplementary material of the ICLR submission (https://openreview.net/forum?id=Pzj6fzU6wkj). The framework is hacky and fragile but may be OK for early experimentation or quick prototyping. Feel free to reuse it as you see fit.

For serious and robust development, I, too, believe the Isabelle/Scala interface is the best option. Dominique’s scala-isabelle library (https://github.com/dominique-unruh/scala-isabelle) could be of great use.

Wenda






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