IDE 协议（IDE Protocol）

Idris REPL 支持两种交互模式：一种是面向终端直接使用的人类可读语法，另一种是为外部工具后端设计的机器可读语法。

IDE 协议与 Idris 编译器独立进行版本管理。Idris 的第一个版本（用 Haskell 编写，版本为 v1.3.3）实现了 IDE 协议的第一个版本，Idris2（自举，版本为 v0.3.0）实现了 IDE 协议的第二个版本。

该协议及其序列化/反序列化例程属于 Protocol 子模块层级，并打包在 idris2protocols.ipkg 包中。

启动 IDE 模式

要在标准输入/输出上启动 IDE 协议，请使用 --ide-mode 命令行选项。若需通过 TCP 套接字运行协议，请使用 --ide-mode-socket 选项：:

idris2 --ide-mode-socket
53864

默认情况下，将自动选择一个空闲端口，将端口号输出到标准输出并换行，然后在本地主机上监听该套接字。你也可以手动指定要监听的主机名和端口：:

idris2 --ide-mode-socket localhost:12345
12345

IDE 协议将在该套接字上运行，当客户端断开连接时 Idris 将退出。

协议概述

通信协议采用异步请求-响应模式：Idris 每次只处理来自客户端的一个请求。Idris 在标准输入流上等待请求，并将一个或多个响应输出到标准输出。请求的结果可以是成功、失败或中间输出；此外，在结果返回前，可能还会有额外的元消息。

一个回复可以包含多条消息：包括任意数量的进度或信息提示，最后以 ok 或 error 作为结果。

消息的传输格式为：消息长度（字符数，6 位十六进制编码）+ S 表达式（sexp）编码的消息内容。此外，每个请求都包含一个唯一的递增整数，该整数会在所有相关消息中重复出现。

加载文件 /home/hannes/empty.idr 时的协议交互示例如下：:

00002a((:load-file "/home/hannes/empty.idr") 1)
000039(:write-string "Type checking /home/hannes/empty.idr" 1)
000025(:set-prompt "/home/hannes/empty" 1)
000032(:return (:ok "Loaded /home/hannes/empty.idr") 1)

第一个消息是 idris-mode 请求加载特定文件的请求，长度为 hex 2a，decimal 42（包括换行符）。请求标识符设置为 1。Idris 发出的第一个消息是写入字符串 Type checking /home/hannes/empty.idr，另一个是设置提示符为 */home/hannes/empty。答案，以 :return 开头的是 ok，并且额外信息是文件已加载。

消息传输语言中有三个原子：数字、字符串和符号。唯一的复合对象是一个列表，由括号括起来。语法是:

A ::= NUM | '"' STR '"' | ':' ALPHA+
S ::= A | '(' S* ')' | nil

其中 NUM 是 0 或正整数，ALPHA 是字母字符，STR 是字符串的内容，用反斜杠 " 转义。原子 nil 被接受而不是 () 用于与某些正则表达式 pretty-printing 例程的兼容性。

Idris 进程的状态主要是在编辑器和 Idris 之间保持同步的活动文件。这是通过已经看到的 :load-file 命令实现的。

协议版本控制

当通过 IDE 协议与 Idris 交互时，运行中的 Idris 进程发送的初始消息是正在使用的 IDE 协议的版本（主要和次要）。

预期的消息格式如下：

(:protocol-version MAJOR MINOR)

IDE 客户端可以使用此功能来帮助支持多个 Idris 版本。

命令

以下是可用的命令列表。除非另有说明，它们与协议版本 1 和 2.0 兼容。

(:load-file FILENAME [LINE])

加载命名文件。如果提供了 LINE 号，则只加载该行之前的文件。否则，将加载整个文件。IDE 协议版本 2 要求文件名必须是带引号的字符串，如 (:load-file "MyFile.idr")，而不是 (:load-file MyFile.idr)。

(:cd FILEPATH)

将工作方向更改为给定的 FILEPATH。IDE 协议版本 2 要求路径必须是带引号的，如 (:cd "a/b/c")，而不是 (:cd a/b/c)。

(:interpret STRING)

在 Idris REPL 中解释 STRING，返回高亮结果。

(:type-of STRING)

返回名称的类型，用 Idris 语法在 STRING 中编写。 回复可能包含高亮信息。

(:case-split LINE NAME)

为程序行 LINE 上的模式变量 NAME 生成 case-split。返回一个没有高亮的字符串。

(:add-clause LINE NAME)

为程序行 LINE 上声明的函数 NAME 生成初始的 pattern-match 子句。返回一个没有高亮的字符串。

(:add-proof-clause LINE NAME)

添加一个由 <== 语法驱动的子句。

(:add-missing LINE NAME)

添加在程序行 LINE 上声明的函数 NAME 上发现的缺失情况。缺失子句以字符串形式返回，没有高亮。

(:make-with LINE NAME)

为函数 NAME 的子句在行 LINE 上创建一个 with-rule pattern-match 模板。返回的新代码没有高亮。

(:make-case LINE NAME)

为函数 NAME 的子句在行 LINE 上创建一个 case pattern-match 模板。返回的新代码没有高亮。

(:make-lemma LINE NAME)

在行 LINE 上创建一个具有类型的高级函数，以解决名为 NAME 的 hole。

(:proof-search LINE NAME HINTS)

通过证明搜索尝试填充 LINE 上的 hole 名为 NAME。HINTS 是搜索时可以尝试的其他可能为空的项目列表。此操作也称为 Idris 2 API 中的 ExprSearch。

(:refine LINE NAME TM)

使用术语 TM 细化 LINE 上的 hole 名为 NAME。

(:docs-for NAME [MODE])

查找 NAME 的文档，并返回高亮字符串。如果 MODE 是 :overview，则仅提供 NAME 的第一个段落。如果 MODE 是 :full，或省略，则返回 NAME 的完整文档。

(:apropos STRING)

搜索文档以查找 STRING 的提及，并返回任何找到的高亮字符串列表。

(:metavariables WIDTH)

列出当前活动的 holes，用 WIDTH 列打印它们的类型。

(:who-calls NAME)

获取 NAME 的调用者列表。

(:calls-who NAME)

获取 NAME 的被调用者列表。

(:browse-namespace NAMESPACE)

返回 NAMESPACE 的内容，就像在命令行 REPL 中使用 :browse 一样。

(:normalise-term TM)

返回一个高亮字符串，由序列化术语 TM 的结果组成（以前作为字符串的 tt-term 属性发送）。

(:show-term-implicits TM)

返回一个高亮字符串，由序列化术语 TM 的结果组成，将所有参数作为显式参数。参数在 TM 中以前作为字符串的 tt-term 属性发送。

(:hide-term-implicits TM)

返回一个高亮字符串，由序列化术语 TM 的结果组成，将所有参数作为默认隐式参数。参数在 TM 中以前作为字符串的 tt-term 属性发送。

(:elaborate-term TM)

返回一个高亮字符串，由序列化术语 TM 对应的核心语言术语组成。参数在 TM 中以前作为字符串的 tt-term 属性发送。

(:print-definition NAME)

返回名称 NAME 的高亮字符串。

(:repl-completions NAME)

搜索包含 NAME 的名称、类型和文档。返回将 NAME 作为 REPL 命令完成的结果。

:version

返回 Idris 编译器的版本信息。

版本 2 新增

版本 2 新增的协议功能包括：

(:generate-def LINE NAME)

尝试从类型生成完整定义。

(:generate-def-next)

用下一个生成的定义替换之前的定义。

(:proof-search-next)

用下一个证明搜索结果替换之前的证明搜索结果。

(:intro LINE NAME)

返回可以用于行 LINE 上的 hole 名为 NAME 的有效饱和构造函数列表。

可能的回复

可能的回复包括正常的最终回复：:

(:return (:ok SEXP [HIGHLIGHTING]) ID)
(:return (:error String [HIGHLIGHTING]) ID)

正常的中间回复：:

(:output (:ok SEXP [HIGHLIGHTING]) ID)
(:output (:error String [HIGHLIGHTING]) ID)

信息性和/或异常回复：:

(:write-string String ID)
(:set-prompt String ID)
(:warning (FilePath (LINE COL) (LINE COL) String [HIGHLIGHTING]) ID)

警告包括不会导致编译器停止的编译器错误。

输出高亮

Idris 模式支持高亮 Idris 输出。实际上，高亮控制由 Idris 编译器完成。Idris 返回的一些形式支持可选的额外参数：一个文本跨度列表映射到关于该文本的元数据。客户端可以使用此列表来高亮显示输出，并拥有更多元数据以实现更丰富的交互。例如，Emacs 模式允许右键单击标识符以获取访问文档和类型签名的菜单。

特定的语义跨度是一个三元素列表。列表的第一个元素是跨度的起始索引，第二个元素是跨度中包含的字符数，第三个是语义数据本身。语义数据是一个列表列表。每个列表的头部是一个键，表示列表中包含的元数据类型，尾部是元数据本身。

以下键可用：

name

给出完全限定的 Idris 名称的引用

implicit

提供一个布尔值，如果区域是隐式参数的名称，则为 True

decor

描述令牌的类别，可以是：

type: 类型构造函数

function: 定义的函数

data: 数据构造函数

bound: 绑定变量，或

keyword

source-loc

表示区域引用源代码位置。它的主体是键值对集合，具有以下可能性：

filename

提供文件名

start

提供源位置的起始行和列作为两个元素尾

end

提供源位置的结束行和列作为两个元素尾

text-formatting

提供格式化文本的属性。这是用于自然语言文本，而不是代码，目前仅从内联文档发出。可能的值是 bold, italic, 和 underline.

link-href

提供一个 URL，对应文本是链接到的 URL。

quasiquotation

表示区域是 quasiquoted。

antiquotation

表示区域是 antiquoted。

tt-term

序列化表示 Idris 核心术语对应于文本区域。

源代码高亮

Idris 支持指示编辑器如何为他们的代码着色。当完善源代码或 REPL 输入时，Idris 将定位源代码中对应于名称的区域，并使用与输出高亮相同的元数据发出关于这些名称的信息。

这些消息将作为回复到达，因为它们是由导致完善发生的命令引起的，例如 :load-file 或 :interpret。它们具有以下格式：:

(:output (:ok (:highlight-source POSNS)) ID)

其中 POSNS 是高亮位置的列表。每个位置都是两个元素的列表，第一个元素是位置（编码为 source-loc 属性），第二个元素是用于输出的高亮元数据。