Блог

#parsing #abstract-syntax-tree #isabelle

#синтаксический анализ #абстрактное синтаксическое дерево #isabelle

Вопрос:

Комментарии:

1. Какая информация вам нужна от AST? isabelle dump Инструмент предоставляет вам некоторую информацию о структуре и определении в формате, подобном Xml, но на самом деле это не AST.

2. Я хочу попробовать создать транспилятор на JavaScript, поэтому наличие какого-то псевдо-ast — это все, что мне действительно нужно. Некоторая структурированная форма исходного кода.

3. В этом случае я бы посмотрел на генератор кода для одного из существующих языков (например src/Tools/Code/code_scala.ML , ) и использовал его в качестве шаблона для генератора кода JS.

4. Ха, что за вопрос! Обсуждения пользователей Isabelle содержат некоторые темы по этому поводу, и Макариус сказал, что такой синтаксический анализ является весьма нетривиальной задачей, если это вообще возможно. Но, с другой стороны, есть dominique-unruh.github.io/scala-isabelle который я начал использовать для синтаксического анализа, и мне удалось его зажечь. Хотя я перешел к другим проектам. Isablle не является грамматикой onw, можно определить дополнительные правила грамматики, расширить грамматику, и именно поэтому не существует единой грамматики, которую можно использовать для ANTRL для генерации синтаксического анализа.

5. Ваш вопрос настолько глубок, насколько он актуален. Действительно, если кто-то может анализировать и создавать обратные выражения isablle, то их можно встроить в нейронные сети и использовать для всех видов обработки ИИ — автоматического доказательства теорем, автоматической генерации теорем и концепций и т. Д. Все используемые случаи, которые включают перевод на естественный язык в HOL и последующую обработку и перевод обратно. По сути, ваш запрос — это святой грааль.