Теория Isabelle / HOL (HOL.Imperative_HOL.ex.Imperative_Quicksort) как Json с scala-isablle и лифтовой структурой

Я использую https://github.com/dominique-unruh/scala-isabelle/ дайджест формализации Isabelle / HOL алгоритма быстрой сортировки https://isabelle.in.tum.de/library/HOL/HOL-Imperative_HOL/Imperative_Quicksort.html. Мне удалось импортировать теорию быстрой сортировки в контекст через

val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

И теперь я ожидаю, что ctxt содержит AST Impeartive_Quicksort.thy, поэтому я хотел бы преобразовать его в дерево объектов JSON. Я использую для этого каркас Lift. Мой файл buil.sbt содержит

libraryDependencies ++= {
    val liftVersion = "3.4.3"
    Seq(
        "net.liftweb"       %% "lift-webkit" % liftVersion % "compile",
        "ch.qos.logback" % "logback-classic" % "1.2.3"
    )
}

И код

val ctxt = Context("HOL.Imperative_HOL.ex.Imperative_Quicksort")

import net.liftweb.json._
import net.liftweb.json.Serialization.write

implicit val formats = net.liftweb.json.DefaultFormats
val jsonString = write(ctxt)
println("before jsonString")
println(jsonString)
println("after jsonString")

что дает результат в скудном количестве:

before jsonString
{"mlValue":{"id":{"_fun":{},"_ec":{},"_arg":null,"_xform":2}}}
after jsonString

Думаю, это проблема сериализации JSON. Ctxt определенно содержит теорию Impeartive_Quicksort, но есть некоторая проблема с переводом JSON.

Как я могу вывести всю теорию в виде дерева объектов JOSN для AST Imperative_Quicksort.thy?


scala lift-json isabelle
person TomR    schedule 14.03.2021    source источник

Ответы (1)


arrow_upward
2
arrow_downward

При таком подходе есть несколько проблем:

Использование Lift для перевода объектов scala-isabelle: обычно это не сработает. Я предполагаю, что Lift использует отражение (я не знаю, во время выполнения или во время компиляции) для сериализации внутренней структуры объектов. (Он даже кодирует поля, которые являются частными, т.е. не являются частью API.) Однако многие объекты в scala-isabelle (включая Context или Term) имеют более сложную внутреннюю структуру. Например, Context просто содержит ссылку на объект, хранящийся внутри процесса Isabelle. (Я предполагаю, что "_xform":2 - это идентификатор, ссылающийся на объект внутри процесса Isabelle.) Контекст Isabelle в принципе не сериализуем (это тип данных, содержащий замыкания), единственный способ получить к нему доступ - применить к нему различные функции ML. что предоставляет Изабель (и это может быть отражено на стороне Scala). С другой стороны, Term можно сериализовать. Со стороны Изабель это простой тип данных. Однако scala-isabelle Term немного сложнее по соображениям эффективности. Данные из процесса Isabelle передаются только по запросу. Вот почему то, что просто использует отражение, не получит весь термин, если он еще не был передан. Вы можете сериализовать Term, написав простую рекурсивную функцию с использованием сопоставления с образцом (см. doc). Однако обратите внимание, что термин может быть огромной структурой данных с большим количеством повторений: например, информация о типе повторяется снова и снова и сильно увеличивает термин.

Получение AST теории Изабель: Я считаю, что здесь есть неправильное представление о том, что такое контекст Изабель. Он не содержит AST теории (или чего-либо, связанного с исходным кодом теории). Напротив, это результат теоретической оценки команд. Модель обработки Isabelle работает примерно так: файл теории разбивается на команды (например, lemma ..., apply ... и т. Д.). У каждой команды есть собственный синтаксический анализатор, который возвращает функцию (закрытие), а не AST. Затем эта функция применяется к текущему состоянию теории / доказательства и преобразует его (например, добавляет к нему новое определение). AST не создается. (Состояние этой обработки ToplevelState в scala-isabelle, и оно может содержать контекст, теорию или другие вещи в зависимости от последней команды.) Поэтому я сомневаюсь, что есть способ получить AST теории в любым способом (независимо от того, используется ли scala-isabelle или это делается непосредственно в Isabelle / ML). Насколько мне известно, единственный способ - реализовать собственный синтаксический анализатор, который несовершенно имитирует синтаксический анализ Изабель и создает AST.

person Dominique Unruh    schedule 15.03.2021