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

Question

我正在尝试使用 https://github.com/dominique-unruh/scala-isabelle for parsing and decomposing the Isabelle terms and I am trying to decompose term - function declaration - from the formalization of quicksort 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")

我正在查看术语 class: https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html 的文档，我发现 Term:

有 Const 构造函数

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

我的问题是：Isabelle 函数声明是一个带有 class 构造函数 Const 的 Term 实例吗？ 我怎么能将我的 qs_term 转换为 class Const 以访问特定于 Const? 的字段我的目标是进行树搜索（DFS， BFS) 在 class 之上（以 Const class 为根对象）并以这种方式为这个函数声明构造 AST。

Answer 1

正在回答这个问题。我想出了代码：

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，大家都说这几乎是不可能的，但是这里几乎是可见的？

Answer 2

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

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

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

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

class Const 与你问的问题无关。伊莎贝尔的一个术语是一棵有不同种类叶子的树。有些叶子是变量，有些叶子是常量。例如，如果您遍历快速排序项，您会发现 partition 和 assert 是常量，因此使用 class Const.

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

Is function declaration a term of type Constant and how to cast such function declaration to Const class?

scala

isabelle