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



It may be strange that Pure Theory.ML have functions for axioms/deps/defs only and not for theorems and that Pure Context.ML have not functions for getting theorems, but Thm.scala (from Scala/Isabelle) has code:

 /** Retrieves a theorem from the Isabelle process by name. The theorem needs to be available in the given context.
   * Both short and fully qualified names work. (I.e., `Thm(context, "TrueI")` and `Thm(context, "HOL.TrueI)`
   * return the same theorem.)
   **/
  def apply(context: Context, name: String)(implicit isabelle: Isabelle, ec: ExecutionContext): Thm = {
    val mlThm : MLValue[Thm] = Ops.getThm(MLValue((context, name)))
    new Thm(mlThm)
  }

that gives answer how to handle theorems - apparently there is OperationCollection.scala and operations framework that acts on context and that can retrievie theorems. So, there is path forward for me to digest theory content. Thanks.

Alex


No: Alex Meyer
Nosūtīts: svētdiena, 2021. gada 4. aprīlis 15:36
Kam: Isabelle Users <isabelle-users at cl.cam.ac.uk>
Tēma: Parsing term is easy with Scala, can similar approach be applied to the theory?
 
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.