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



On 30/01/2021 03:00, Alex Meyer wrote:
> My intention is to have full control over the representation and manipulation
> of the code in theory files:
> 1) maybe I would like to parse or generate thy files with the grammatical
> framework, e.g., translate the sentence in natural language into thy file
> (similar efforts have been done in Coq). Just for the purposes of
> representation and open-ended deduction, no need to have certified proofs.
> 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.

This "full control" is not going to work: Isabelle cannot be put into a box
like that, it is far too flexible and powerful.

The language of Isabelle is an open-ended framework for arbitrary semantic
embeddings, usually implemented in Isabelle/ML. Over the decades, I have
provided means to "tap" some aspects of the internal representation of
Isabelle languages, with external markup in Isabelle/PIDE.


> I had the question with similar ideas but with different technologies in mind
> last summer:
> https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2020-July/msg00025.html
> and I was strongly discouraged from such parsing and in-memory manipulation of
> theory files.

That thread already provides good answers. In short: don't do it, but change
your perspective on the problem.


> So - it would be nice to have some pointers. Just pointers, all remaining I
> will explore myself.

https://github.com/Deducteam/isabelle_dedukti
https://github.com/UniFormal/MMT
https://github.com/qaware/isabelle-afp-search


At the bottom of these tools there are two different approaches:

  (1) heavy headless PIDE session (as in "isabelle dump"): one big
Isabelle/ML/Scala process to crunch everything and export certain aspects

  (2) session build + export database (as in "isabelle export" or
Isabelle/Dedukti above): this is a regular "isabelle build" with certain options


Generally note that the proper language for "Isabelle systems programming" is
Isabelle/Scala: not funny scripting languages like Python.

The Isabelle/Dedukti application shows how to wrap rather simple Scala modules
into Isabelle command line tools. That is for Isabelle2020, but it should be
easy to adapt to Isabelle2021 which will appear within approx. 2 weeks.


	Makarius





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