作者:国务二局 | 来源:互联网 | 2022-12-02 16:49
与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发送命令,但我不确定具体如何。指向相关文档的指针将不胜感激!
1> 小智..:
据我所知,当前(在master分支上)有两种从命令行与Agda进行交互的方式:
Emacs的原始后端 agda --interaction
新的基于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。