Re: [isabelle] Parsing term is easy with Scala, can similar approach be applied to the theory?



Hello,

And now I am wondering - what I am missing here? Why so many people have told me that this endeavour is so hard?

I don't think anyone said that it is hard to parse a term. That is easy and well-supported both in Isabelle/ML and via scala-isabelle.

What is difficult is to translate a theory into a data-structure.

So, to summarize, what is available is (both in ML and Scala):
What is not available (to the best of my knowledge):
What is available (but I don't know how to best extract it, for this Makarius' emails are relevant):
Best wishes,
Dominique.




On Sun, 4 Apr 2021 at 15:39, Alex Meyer <alex153 at outlook.lv> wrote:
I have came up with the code (using https://github.com/dominique-unruh/scala-isabelle/) that parses term into tree-like structure:


    val setup = Isabelle.Setup(isabelleHome = Path.of(isabelleHome), logic = "HOL", build=false)
    implicit val isabelle: Isabelle = new Isabelle(setup)
    val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

 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_report2(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_report2(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_report2(p_term_1, curr_string) + " ||| " + p_term_2.pretty(ctxt) + t_report2(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_report2(test_term, ""))

The resulting string representation is something like (I am still doing the right indentation):

[App (=) (two_integer_max_case_def a b)

[App (=) [Const HOL.eq] |||

two_integer_max_case_def a b

[App two_integer_max_case_def a

[App two_integer_max_case_def

[Free two_integer_max_case_def] |||

a [Free a]

] |||

b [Free b]

]

] |||

case b < a of True ⇒ a | False ⇒ b

[App case_bool a b

[App case_bool a

[App case_bool

[Const Product_Type.bool.case_bool] |||

a [Free a]

] ||| b [Free b] ] ||| b < a [App (<) b [App (<) [Const Orderings.ord_class.less] ||| b [Free b] ] ||| a [Free a] ] ] ]


This is the result which I tried to find all the time! And now I am wondering - what I am missing here? Why so many people have told me that this endeavour is so hard? But, currently, unfortunatly, it applies to the terms (inner syntax) only. Such can is possible because of the (from https://javadoc.io/doc/de.unruh/scala-isabelle_2.13/latest/de/unruh/isabelle/pure/Term.html):


sealed abstract class Term
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 '$'

(And I am still digesting what it means because in Java someone has have introspection/reflection into the function name and arguments but not into function body/code content, but this Scala approach seemingly allows to dive into the content of the body of the class or function!).

My question is - is there similar code (with mathc) possible for parsing theory? i.e. is there
sealed abstract class Theory (or MLValue)
final case class Theorem(...)
final case class Definition(...)

Something like that? Or something completely different one should use for the theory (outer syntax)?

Isabelle provides parsing and pretty-printing facilities for the terms.

Alex



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.