Isabelle/HOL theory (HOL.Imperative_HOL.ex.Imperative_Quicksort) as Json with scala-isablle and lift framework

Question

I am using https://github.com/dominique-unruh/scala-isabelle/ to digest Isabelle/HOL formalization of quicksort algorithm https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html. I managed to import Quicksort theory into Context via

val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

And now I expecting that ctxt containts the AST of Impeartive_Quicksort.thy, so I would like it to convert into JSON object tree. I am using Lift framwork for that. My buil.sbt contains

libraryDependencies ++= {
    val liftVersion = "3.4.3"
    Seq(
        "net.liftweb"       %% "lift-webkit" % liftVersion % "compile",
        "ch.qos.logback" % "logback-classic" % "1.2.3"
    )
}

And the code is

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.DefaultFormats
val jsonString = write(ctxt)
println("before jsonString")
println(jsonString)
println("after jsonString")

which is giving an output in meagre quantity:

before jsonString
{"mlValue":{"id":{"_fun":{},"_ec":{},"_arg":null,"_xform":2}}}
after jsonString

I guess - this is JSON serialization issue. Ctxt definitely contains the Impeartive_Quicksort theory, but there is some problem with transaltion ot JSON.

How can I output the entire theory as JOSN object tree for the AST of Imperative_Quicksort.thy?

Dominique Unruh Dominique Unruh · Accepted Answer · 2021-03-15T11:09:46

There are several problems with this approach:

Using Lift to translate scala-isabelle objects: This will generally not work. I assume that Lift uses reflection (I don't know whether runtime or compile-time) to serialize the internal structure of the objects. (It even encodes fields that are private, i.e., not part of the API.) However, many objects in scala-isabelle (including Context or Term) have a more complex internal structure. For example, Context simply contains a reference to an object stored inside the Isabelle process. (I guess that "_xform":2 is the ID referencing the object inside the Isabelle process.) An Isabelle context is not serializable in principle (it is a datatype that contains closures), the only way to access it is by applying the various ML functions to it that Isabelle provides (and that can be mirrored on the Scala side). A Term on the other hand can be serialized. On the Isabelle side it is a simple datatype. However, the scala-isabelle Term is a bit more complex for efficiency reasons. Data from the Isabelle process are transferred only on-demand. This is why something that simply uses reflection will not get the whole term unless it already has been transferred. You can serialize a Term by writing a simple recursive function using pattern matching (see the doc). However, note that a term can be a huge datastructure with a lot of repetition: For example, type information is repeated over and over and blows up the term hugely.

Getting an AST of the Isabelle theory: I feel there is a misconception here about what an Isabelle context is. It does not contain an AST of a theory (or anything related to the source code of the theory). Instead, it is the result of evaluating the commands in the theory. The Isabelle processing model works very roughly as follows: The theory file is split into commands (e.g., lemma ..., apply ... etc). Each command comes with its own parser that returns a function (a closure), not an AST. This function is then applied to the current state of the theory/proof and transforms it (e.g., adds a new definition to it). At no point is an AST generated. (The state of this processing is ToplevelState in scala-isabelle, and it may contain a context or a theory or other things depending on the last command.) So, 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.

Isabelle/HOL theory (HOL.Imperative_HOL.ex.Imperative_Quicksort) as Json with scala-isablle and lift framework

1 Answers