Email Gateway (Mar 14 2021 at 16:39): Email Gateway (Mar 14 2021 at 16:39):From: Alex Meyer <alex153@outlook.lv>
I had this question https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2021-January/msg00187.html at the end of January, and there where some follow-up discussion in February and scala-isabelle emerged as fine library for this.
I had quick idea to get theory (as isabelle AST) in JSON format and for that tried the code:
val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")
import net.liftweb.json._
import net.liftweb.json.Serialization.write
implicit val formats = net.liftweb.json.DefaultFormatsval jsonString = write(ctxt)
println("before jsonString")
println(jsonString)
println("after jsonString")
but the output it scarce (my full stackoverflow question is https://stackoverflow.com/questions/66626741/isabelle-hol-theory-hol-imperative-hol-ex-imperative-quicksort-as-json-with-sc):
before jsonString
{"mlValue":{"id":{"_fun":{},"_ec":{},"_arg":null,"_xform":2}}}
after jsonString
Maybe I a overstretching the framework (error about which I have been extensively warned in the mentioned thread), but just quick qustion - is it possible to get AST JSON tree for the entire theory in scala-isabelle?
The quick thought is that I can load theory in string and then try to load it like term in the conext that is preloaded by the same theory. But maybe it is not good ide.
I am reading documentation, experimenting, doing some reasoning, etc.
But maybe there is answer in couple of words that can shortcut my path?
Alex
Email Gateway (Mar 15 2021 at 11:50):From: Dominique Unruh <unruh@ut.ee>
Hello,
I have answered this in the Stackoverflow post. However, let me quote
one of my claims here that goes beyond specifically scala-isabelle,
maybe someone (Makarius) can comment on that from the Isabelle side:
I am doubtful that there is a way to get an AST of a theory in any
way (no matter whether scala-isabelle is used or whether it is done
directly in Isabelle/ML). The only way, as far as I know, is to
implement your own parser that imperfectly mimics Isabelle's parsing
and constructs an AST.
If this is not true and there are some ways to get an AST, I would be
please to hear about it.
Best wishes,
Dominique.
Email Gateway (Mar 15 2021 at 12:17):From: Makarius <makarius@sketis.net>
The quoted statement is true, but the true truth is even stronger: Isabelle
theory content is produced by "semantics" in ML, and an overlall AST (syntax
tree) describing that does not exist.
You can only get approximations, e.g. the Isabelle/PIDE document markup from
"isabelle export" (better: official Isabelle/Scala functions to access it; see
how HTML output works in Isabelle2021).
An alternative is to access foundational types/terms/theorems etc. as
Isabelle/MMT does it, e.g. see the paper
https://drops.dagstuhl.de/opus/volltexte/2020/13065
Many more alternatives are possible, as long as the conceptual structure of
the system is taken seriously. "AI" is not going to make a wrong approach
right by magic.
Makarius
Last updated: Jan 04 2025 at 20:18 UTC