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

user_1375882 0
Viewed 74

I am trying to use 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 - this Isabelle code:

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

I am trying to use in 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")

I am checking the documentation for the Term class: https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html and I see that there is Const constructor for this Term:

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

My question is: is the Isabelle function declaration an instance of Term with class constructor Const? And how can I cast my qs_term to class Const with the aim to access fields that are specific to Const? My aim is to do tree-search (DFS, BFS) over the class (taking Const class as the root object) and in such way to construct AST for this function declaration.

isabelle scala
2 Answers

What you have constructed is not a definition of quicksort (at least not in the sense that it would define anything in Isabelle), but a simply a term that expresses the property that you want that quicksort should satisfy.

The function command in Isar (and also the definition command) takes the specification (e.g., the term you wrote) and transforms it internally into two parts: a name of the constant you define (here TheoryName.quicksort), and a term that says what quicksort should be defined as (here λarr left right. (if ...)).

If you want to create a definition programmatically in Isabelle (no matter whether Isabelle/ML), you need to:

  1. Get a context (e.g., Context("TheoryName")) (or a theory).
  2. Apply a suitable command for creating a definition. There is no predefined command for that in scala-isabelle, so you have to use the ML-code that does this and wrap it using MLValue.compileFunction (ScalaDoc). This function then takes your context (or theory) as well as the constant name and the term and further information, and returns a new theory or context that has the value defined. (E.g., Local_Defs.define in local_defs.ML is such a function, I think.)

The class Const has nothing to do with what you are asking. A term in Isabelle is a tree with different kinds of leafs. Some of the leafs are variables, and some of the leafs are constants. For example, if you traverse your quicksort-term, you will find, e.g., that partition and assert are constants and thus represented using class Const.

user_26462480

This is answer in progress. I have came up with the code:

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"))

And this code reported:

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

So - from this output one can deduce:

  1. The function declaration is Term of type App. Apparently = is some meta-level App that facilitates mapping from the function body to the arguments.
  2. There is no need to do Scala or Java reflection, all the types can be determined by the Scala match facility.

Actually - the most important point - I can construct Abstract Syntax Tree in XML or JSON from this t_report code, I just need to figure out the tree visitation order of this code construction. I have asked previously how to construct the AST from the Isabelle expression and everyone has said that this is almost impossible, but here it is almost visible?

user_13758820
Related