如何从命令行/其他语言使用Agda？

Question

与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。我尝试查看Agda的VIM扩展以了解其工作方式，似乎它正在向Agda发送命令，但我不确定具体如何。指向相关文档的指针将不胜感激！

Answer 1

据我所知，当前（在master分支上）有两种从命令行与Agda进行交互的方式：

1. Emacs的原始后端 agda --interaction
2. 新的基于JSON的后端 agda --interaction-json

Emacs后端

• Emacs会将格式为Haskell数据类型的消息发送到Agda （简单）
• Agda将以Emacs Lisp的形式答复Emacs的使用情况（困难）

如您所见，此后端专为Emacs设计。需要进行一些逆向工程才能弄清楚他们彼此之间在说什么。

当我在Atom上实现agda-mode时，我对Emacs协议做了一些说明。但恐怕它在撰写本文时已偏离了实际的实现。

如果您想与Emacs后端交互，以下是Agda源代码中的一些相关部分，您可能会发现它们有用：

• 将响应编码为Emacs Lisp
• 请求的数据类型

JSON后端

不用说，使用Emacs协议会很痛苦。
因此，我设法在新的后端中用JSON替换了Emacs Lisp。

• 您仍然需要发送格式化为Haskell数据类型的消息像在Emacs中一样，将到Agda。
• Agda会以JSON进行回复

现在，您不必处理Emacs Lisp的S表达式。这是将响应编码为JSON的方式

但是，有效负载仍然被序列化为字符串，因此很难从Agda中提取有用的信息。所以我仍然工作在的json分支，尝试编码有效载荷的JSON。