[isabelle] Pārs.: Parsing term is easy with Scala, can s... · Mirror: Isabelle Users Mailing List

Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] Pārs.: Parsing term is easy with Scala, can s...

Email Gateway (Apr 04 2021 at 13:16):

From: Alex Meyer <alex153@outlook.lv>
I am looking into code and documentation in Scala Theory, Context, MLValue code and also Isabelle/Isar reference manual (which describes all the hierarchy of Terms, Proofs etc.) and I see that for type Theorem there is proposition attribute which contains Term.

But I wonder - why there are no (why can I not find) properties on Theory/Context/MLValue that would let someone to retrieve all definitions, all theorems from the specified Theory/Conext/MLValue? How to access all available theorems?

ThmTest.scala from scala-isabelle shows how to access Theorem if the name of the theorem is known:

class ThmTest extends AnyFunSuite {
test("retrieve thm") {
val ctxt = Context("Main")
val thm = Thm(ctxt, "HOL.TrueI")
thm.proposition match {
case App(Const("HOL.Trueprop",_), Const("HOL.True", _)) =>
case _ => fail("Proposition is: "+thm.proposition.pretty(ctxt))
}
}

But if some is eager to programmitcally parse unknown theory then she needs to retreivei all the theorem names or theorems from the Context/Theory. Is there method for such list?

Alex

No: Alex Meyer
Nosūtīts: svētdiena, 2021. gada 4. aprīlis 15:36
Kam: Isabelle Users <isabelle-users@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

Email Gateway (Apr 04 2021 at 22:49):

From: Alex Meyer <alex153@outlook.lv>
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

I have came up with the code (using https://github.com/dominique-unruh/scala-isabelle/) that parses term into tree-like structure:

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] ] ] ]

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

Last updated: Apr 24 2024 at 12:33 UTC