我正在使用https://github.com/dominique-unruh/scala-isabelle/快速排序算法的Isabelle/HOL形式化https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html.我设法通过将快速排序理论导入上下文
val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")
现在我希望ctxt包含Impartive_Quicksort.thy的AST，所以我希望它能转换成JSON对象树。我正在使用Lift框架。我的建筑.sbt包含
libraryDependencies ++= {
val liftVersion = "3.4.3"
Seq(
"net.liftweb" %% "lift-webkit" % liftVersion % "compile",
"ch.qos.logback" % "logback-classic" % "1.2.3"
)
}
代码是
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")
它的产量很低：
before jsonString
{"mlValue":{"id":{"_fun":{},"_ec":{},"_arg":null,"_xform":2}}}
after jsonString
我想这是JSON序列化问题。Cxt肯定包含Impartive_Quicksort理论，但JSON的事务处理存在一些问题。
如何将整个理论输出为Imperative_Quicksort.thy的AST的JOSN对象树？
这种方法有几个问题：
使用Lift平移scala-isabelle对象：这通常不会起作用。我假设Lift使用反射(我不知道是运行时还是编译时(来序列化对象的内部结构。(它甚至对私有字段进行编码，即不属于API的一部分。(然而，scala-isabelle中的许多对象(包括Context或Term(具有更复杂的内部结构。例如，Context只包含对存储在Isabelle进程中的对象的引用。(我猜"_xform":2是引用Isabelle进程中对象的ID。(原则上，Isabelle上下文是不可序列化的(它是一种包含闭包的数据类型(，访问它的唯一方法是应用Isabelle提供的各种ML函数(可以在Scala端镜像(。另一方面，Term可以被串行化。在Isabelle方面，它是一个简单的数据类型。然而，由于效率的原因，标量isabelleTerm有点复杂。Isabelle流程中的数据仅按需传输。这就是为什么仅仅使用反射的东西不会得到整个术语，除非它已经被转移了。您可以通过使用模式匹配编写一个简单的递归函数来序列化Term(请参阅文档(。然而，请注意，一个术语可能是一个巨大的数据结构，有很多重复：例如，类型信息一遍又一遍地重复，并极大地破坏了这个术语。
获取Isabelle理论的AST：我觉得这里对什么是Isabelle上下文有一种误解。它不包含理论的AST(或与理论源代码相关的任何内容(。相反，它是对理论中的命令进行评估的结果。Isabelle处理模型的工作原理大致如下：理论文件被拆分为命令(例如，lemma ...、apply ...等(。每个命令都有自己的解析器，返回一个函数(闭包(，而不是AST。然后将该函数应用于理论/证明的当前状态，并对其进行转换(例如，为其添加新的定义(。在任何时候都不会生成AST。(这个处理的状态是scala-isabelle中的ToplevelState，它可能包含一个上下文、一个理论或其他东西，这取决于最后一个命令。(因此，我怀疑是否有办法以任何方式获得理论的AST(无论是使用scala-isabel还是直接在isabelle/ML中完成(。据我所知，唯一的方法是实现自己的解析器，该解析器不完全模仿Isabelle的解析并构造AST。