Как использовать Agda из командной строки / с другого языка? - PullRequest
Новая
       9

Как использовать Agda из командной строки / с другого языка?

0 голосов
/ 10 октября 2018

Большая часть взаимодействия с Agda осуществляется с помощью EMACS, но есть ли способ сделать это программно?Т.е. возможно ли все сделать из командной строки или из какого-то API?Основная цель - создать тонкую оболочку, чтобы мы могли вызывать Agda с другого языка, например: 

var Agda = require("agda");

var code = `
    data Bool: Set where
        true: Bool
        false: Bool

    not : Bool -> Bool
    not true = false
    not false = true

    val : Bool
    val = not true
`;

console.log(Agda.infer(code, "true")); // prints "Bool"
console.log(Agda.normalize(code, "val")); // prints "false"

Ранее я уже спрашивал, как использовать Agda в качестве библиотеки , но этоочевидно, только крышка Haskell.Я попытался просмотреть расширение VIM Agda, чтобы увидеть, как оно это делает, и похоже, что оно отправляет команды в Agda, но я точно не знаю, как именно.Указатели на соответствующую документацию будут высоко оценены!

1 Ответ

0 голосов
/ 11 октября 2018

Насколько я знаю, в настоящее время (в основной ветке) есть два способа взаимодействия с Agda из командной строки:

  1. Оригинальный бэкэнд для Emacs agda --interaction
  2. Новый основанный на JSON бэкэнд agda --interaction-json

Бэкэнд Emacs

  • Emacs будет отправлять сообщения в формате Типы данных Haskell вAgda (легкий)
  • Agda ответит в виде Emacs Lisp для потребления Emacs (жесткий)

Как видите, этот бэкэнд был разработан специально для Emacs.Потребовалось бы некоторое обратное проектирование, чтобы выяснить, что они говорят друг с другом.

Я сделал несколько замечаний о протоколе Emacs, когда я реализовывал agda-mode на Atom .Но я боюсь, что это отклонилось от фактической реализации на момент написания.

Вот некоторая соответствующая часть исходного кода Agda, которая может оказаться полезной, если вы хотите взаимодействовать с бэкэндом Emacs:

Бэкэнд JSON

Само собой разумеется, работать с Emacs больнопротокол.
Так что мне удалось заменить Emacs Lisp на JSON в новом бэкэнде.

  • Вам все равно нужно будет отправлять сообщения в формате Haskell в Agda какв Emacs
  • Agda ответит в JSON

Теперь вам не придется иметь дело с S-выражениями Emacs Lisp.Вот как ответы кодируются как JSON

Однако полезные данные по-прежнему сериализуются в виде строк, что затрудняет извлечение полезной информации из Agda.Поэтому я все еще работаю над json ответвлением , пытаясь кодировать полезную нагрузку в JSON.

...