大佬教程收集整理的这篇文章主要介绍了Isabelle/HOL 理论 (HOL.Imperative_HOL.ex.Imperative_Quicksort) 作为 Json 与 scala-isablle 和提升框架，大佬教程大佬觉得挺不错的，现在分享给大家，也给大家做个参考。
我正在使用 https://github.com/dominique-unruh/scala-isabelle/ 来消化快速排序算法 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html 的 Isabelle/Hol 形式化。我设法通过
将快速排序理论导入上下文val ctxt = Context("Hol.Imperative_Hol.ex.Imperative_Quicksort")
现在我希望 ctxt 包含 Impeartive_Quicksort.thy 的 AST，所以我希望它转换为 JsON 对象树。为此，我正在使用 lift 框架。我的 buil.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 序列化问题。 Ctxt 肯定包含 Impeartive_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 方面，它是一个简单的数据类型。但是，出于效率原因，scala-isabelle Term 有点复杂。来自 Isabelle 流程的数据仅按需传输。这就是为什么简单地使用反射的东西不会得到整个术语，除非它已经被转移。您可以通过使用模式匹配编写一个简单的递归函数来序列化 Term（请参阅 doc）。但是，请注意，术语可能是具有大量重复的巨大数据结构：例如，类型信息一遍又一遍地重复并极大地破坏了术语。
获得伊莎贝尔理论的 AST：
我觉得这里对 Isabelle 上下文是什么存在误解。它不包含理论的 AST（或任何与理论源代码相关的内容）。相反，它是评估理论中的命令的结果。 Isabelle 处理模型的工作原理大致如下：理论文件被拆分为命令（例如，lemma ...、apply ... 等）。每个命令都有自己的解析器，返回一个函数（一个闭包），而不是一个 AST。然后将此函数应用于理论/证明的当前状态并对其进行转换（例如，为其添加新定义）。绝不会生成 AST。 （此处理的状态在 scala-isabelle 中为 ToplevelState，它可能包含上下文或理论或其他内容，具体取决于最后一个命令。）因此，我怀疑是否有获取 AST 的方法任何方式的理论（无论是使用 scala-isabelle 还是直接在 Isabelle/ML 中完成）。据我所知，唯一的方法是实现您自己的解析器，该解析器不完美地模仿 Isabelle 的解析并构建一个 AST。
以上是大佬教程为你收集整理的Isabelle/HOL 理论 (HOL.Imperative_HOL.ex.Imperative_Quicksort) 作为 Json 与 scala-isablle 和提升框架全部内容，希望文章能够帮你解决Isabelle/HOL 理论 (HOL.Imperative_HOL.ex.Imperative_Quicksort) 作为 Json 与 scala-isablle 和提升框架所遇到的程序开发问题。
如果觉得大佬教程网站内容还不错，欢迎将大佬教程推荐给程序员好友。
本图文内容来源于网友网络收集整理提供，作为学习参考使用，版权属于原作者。
如您有任何意见或建议可联系处理。小编QQ：384754419，请注明来意。