函数声明是 Constant 类型的术语，以及如何将此类函数声明转换为 Const 类？

问题描述

我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle 来解析和分解 Isabelle 术语，并且我试图从快速排序 https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html 的形式化中分解术语 - 函数声明 - 这个 Isabelle 代码：

function quicksort :: "'a::{heap,linorder} array ⇒ nat ⇒ nat ⇒ unit Heap"
where
  "quicksort arr left right =
     (if (right > left)  then
        do {
          pivotNewIndex ← partition arr left right;
          pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;
          quicksort arr left (pivotNewIndex - 1);
          quicksort arr (pivotNewIndex + 1) right
        }
     else return ())"
by pat_completeness auto

我正在尝试在 Scala/Isabelle 中使用：

println("Before qs term")
val qs_term = Term(ctxt,"quicksort arr left right =" +
  "    (if (right > left)  then" +
  "        do {" +
  "          pivotNewIndex ← partition arr left right;" +
  "          pivotNewIndex ← assert (λx. left ≤ x ∧ x ≤ right) pivotNewIndex;" +
  "          quicksort arr left (pivotNewIndex - 1);" +
  "          quicksort arr (pivotNewIndex + 1) right" +
  "        }" +
  "     else return ())")
println("After qs term")

我正在检查 Term 类的文档：https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html，我看到这个 Const 有 Term 构造函数：

sealed abstract class Term
final case class Const(name: String,typ: Typ)            // Corresponds to ML constructor 'Const'
...

我的问题是：Isabelle 函数声明是具有类构造函数 Const 的 Term 实例吗？ 我如何将我的 qs_term 转换为类 {{ 1}} 的目的是访问特定于 Const 的字段？ 我的目标是对类（以 Const 类为根对象）进行树搜索（DFS、BFS）并在为这个函数声明构造 AST 的这种方式。

解决方法

您构建的不是 quicksort 的定义（至少不是在 Isabelle 中定义任何东西的意义上），而只是一个表达您想要的属性的术语强>quicksort 应该满足。

Isar 中的 function 命令（以及 definition 命令）采用规范（例如，您编写的术语）并将其内部转换为两部分：您定义的常量的名称（此处 TheoryName.quicksort)，以及一个说明 quicksort 应定义为什么的术语（此处为 λarr left right. (if ...)）。

如果您想在 Isabelle 中以编程方式创建定义（无论是 Isabelle/ML），您需要：

获取上下文（例如，Context("TheoryName")）（或理论）。
应用合适的命令来创建定义。 scala-isabelle 中没有预定义的命令，因此您必须使用执行此操作的 ML 代码并使用 MLValue.compileFunction (ScalaDoc) 对其进行包装。然后，此函数采用您的上下文（或理论）以及常量名称和术语以及更多信息，并返回具有定义值的新理论或上下文。（例如，Local_Defs.define 中的 local_defs.ML 就是这样一个函数，我认为。）

Const 类与您要问的内容无关。 Isabelle 中的一个术语是具有不同种类叶子的树。一些叶子是变量，一些叶子是常数。例如，如果您遍历快速排序项，您会发现，例如，partition 和 assert 是常量，因此使用类 Const 表示。

这是正在进行的回答。我想出了代码：

println("Before test term");
val test_term = Term(ctxt,"two_integer_max_case_def a b = (case a > b of True \\<Rightarrow> a | False \\<Rightarrow> b)")
println("After test term")
println(test_term.getClass())
println("test_term: " + test_term.pretty(ctxt))
val jsonString = write(test_term)
println("After write test term")

def t_report(term: Term,curr_string: String): String = term match {
  case Const(p_name,p_type) => curr_string + " Const " + p_name
  case Free(p_name,p_type) => curr_string + " Free " + p_name
  case Var(p_name,p_index,p_type) => curr_string + " Var " + p_name + p_index
  case Abs(p_name,p_type,p_body_term) => curr_string + " Abs " + p_name + p_body_term.pretty(ctxt) + t_report(p_body_term,curr_string)
  case Bound(p_index) => curr_string + " Bound " + p_index
  case App(p_term_1,p_term_2) => curr_string + " App " + p_term_1.pretty(ctxt) + t_report(p_term_1,curr_string) + p_term_2.pretty(ctxt) + t_report(p_term_2,curr_string)
    //final case class Const(name: String,typ: Typ)            // Corresponds to ML constructor 'Const'
    //final case class Free(name: String,typ: Typ)             // Corresponds to ML constructor 'Free'
    //final case class Var(name: String,index: Int,typ: Typ)  // Corresponds to ML constructor 'Var'
    //final case class Abs(name: String,typ: Typ,body: Term)  // Corresponds to ML constructor 'Abs'
    //final case class Bound private (index: Int)               // Corresponds to ML constructor 'Bound'
    //final case class App private (fun: Term,arg: Term)       // Corresponds to ML constructor '$'
  case _ => curr_string + " Other "
}
println(t_report(test_term,"zero"))

此代码报告：

zero App (=) (two_integer_max_case_def a b)zero App (=)zero Const HOL.eqtwo_integer_max_case_def a bzero App two_integer_max_case_def azero App two_integer_max_case_defzero Free two_integer_max_case_defazero Free abzero Free bcase b < a of True ⇒ a | False ⇒ bzero App case_bool a bzero App case_bool azero App case_boolzero Const Product_Type.bool.case_boolazero Free abzero Free bb < azero App (<) bzero App (<)zero Const Orderings.ord_class.lessbzero Free bazero Free a

所以 - 从这个输出可以推断：

函数声明是 App 类型的 Term。显然，= 是一些元级应用程序，可促进从函数体到参数的映射。
无需进行 Scala 或 Java 反射，所有类型都可以由 Scala match 工具确定。

实际上 - 最重要的一点 - 我可以从这个 t_report 代码中构造 XML 或 JSON 中的抽象语法树，我只需要弄清楚这个代码构造的树访问顺序。我之前问过如何从 Isabelle 表达式构造 AST，大家都说这几乎是不可能的，但在这里它几乎是可见的？

isabelle scala scala