Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pārs.: Entire theory in JSON forma using scal...


view this post on Zulip Email Gateway (Mar 14 2021 at 16:54):

From: Alex Meyer <alex153@outlook.lv>
To be sure - the JSON tree of term object is not AST either:

code:

val term = Term(ctxt, "x+0 = (y::nat)*1")
val jsonString2 = write(term)
println(jsonString2)

gives the structure that does not resmble AST, there is no evidence, that this term contains some structure, syntax tree, subelements:

{
"mlValue": {
"id": {
"_fun": {},
"_ec": {},
"_arg": null,
"_xform": 2
}
},
"isabelle": {
"setup": {
"isabelleHome": {
"fs": {
"provider": {}
},
"type": {},
"root": "C:\\",
"path": "C:\\Homes\\Isabelle2020\\Isabelle2020"
},
"logic": "HOL",
"workingDirectory": {
"fs": {
"provider": {}
},
"type": {},
"root": "",
"path": ""
},
"sessionRoots": [],
"build": false,
"verbose": false,
"isabelleCommandHandler": {}
}
},
"ec": {}
}

It was my expectation that Term object will have this structure (tree like structure) over which I could wander and build up my AST or let JSON serializer do it for me in default manner.

OK, I studying this, but - if there is quick suggestion, then it would be nice to hear.

A.


No: Alex Meyer
Nosūtīts: svētdiena, 2021. gada 14. marts 18:38
Kam: Isabelle Users <isabelle-users@cl.cam.ac.uk>
Tēma: Entire theory in JSON forma using scala-isabelle?

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


Last updated: Jul 15 2022 at 23:21 UTC