前排提示：本文完全使用 Aya 的文学编程模式书写。

「文学编程」(Literate Programming) 是一种新颖的“写注释”的方法。在传统编码过程中，注释是次要的； 但是在文学模式下，注释获得了和代码同等的地位，并且文学编程支持使用更多的注释格式，例如流程图、 数学公式，甚至是嵌入其他语言的代码，甚至可以运行这些被嵌入的代码。 人们虽然也能在传统的注释中通过一些特定的标记插入数学公式或者是图片，但是这种方式的可读性显然不如文学模式。

文学编程的最大用处是「写博客」。很多的静态博客生成器都支持使用 Markdown 进行写作，但是这样做有一些问题：

• Markdown 中嵌入的代码是无法被编译器检查的，这意味着你可以在 Markdown 中写出不一定正确的代码而不自知。
• Markdown 中的代码由于无法被编译器读取，所以任何跟代码相关的功能都无法使用，例如代码高亮、在定义之间跳转、 查看变量的类型等等。这对复杂的编程语言的阅读并不友好，对于教程类的文章来说影响更大。

考虑到以上的缺点，再加上 Aya 语言是一个依赖类型的编程语言， 用 Aya 写出来的复杂程序，很难在不借助类型信息等 IDE 功能的帮助下获得较为优秀的阅读体验。 我们希望 Aya 的编程语言具有如下特点（部分已经实现了，部分还在开发中）：

• Aya 的文学模式的代码可以被编译器检查，就像一个普通的 Aya 源文件一样。
• Aya 编译器的输出信息可以被反映到编译产生的文件中，以便在阅读时帮助读者理解程序。
• 支持多种注释格式，例如数学公式、流程图、嵌入其他语言的代码等等。
• 提供基本的 IDE 功能，例如跳转到定义、查看变量的类型、签名搜索等等。
• 提供交互式的文学编程体验，类似 Jupyter Notebook。
• 文学模式和普通模式的 Aya 代码不应该被区别对待。例如，你可以在文学模式下定义一个函数， 然后在普通模式下使用这个函数，反之亦然，我们鼓励尽可能将复杂的代码使用文学模式进行编写。
• 支持模块间跳转。例如，当你在阅读一个使用文学编程编写的模块，你可以点击里面对其他模块中定义的引用， 跳转到那个模块的文学编程模式下的定义处。

总之，我们希望提供的文学模式在进行编译后，向读者展示的页面是「不能编辑的 IDE」。

Aya 的文学编程模式支持哪些特性？

文件格式

Aya 目前支持在 Markdown 中进行文学编程。我们称这样的文件为 Aya Markdown，其文件拓展名为 .aya.md。 我们直接使用 Markdown 的代码块语法来嵌入 Aya 代码，例如：

以下代码定义了自然数类型 Nat:

open data Nat
  | zero
  | suc Nat

接着，我们可以定义自然数上的加法 (+):

overlap def infixl + : Nat → Nat → Nat
  | 0, a ⇒ a
  | a, 0 ⇒ a
  | suc a, b ⇒ suc (a + b)
  | a, suc b ⇒ suc (a + b)
  tighter =

上面的代码已经支持了一些 IDE 功能：

• 基于语义的代码高亮，例如归纳类型、归纳类型构造器、和函数名字的高亮颜色是不同的，例如 Nat，zero，(+)。
• 当鼠标悬停在一个名字上时显示该符号的类型，同时高亮出所有对这个名字的引用。
• 点击一个名字可以跳转到该符号的定义处。

上面的代码还用到了一个符号 (=)，其类型为 A → A → Type 0，但在这个页面中并没有任何地方的代码块定义了这个符号。 这是因为包含其定义的代码并未包含在 aya 代码块中，而是 aya-hidden。 顾名思义，这个代码块中的代码不会被渲染到页面上。

你可能注意到了，在文本中出现的内联代码也可以被编译器识别并进行高亮。 这是 Aya 对 Markdown 的第一个扩展：在内联代码（即类似这样的代码 code） 后面写一对大括号，在其内部指定你希望在编译后的 Markdown 中显示的内容，例如

• {} 将显示原始的符号名字: Nat
• {show=type} 将展示该符号的类型 : Type 0

显示编译器的输出

我们可以尝试证明自然数上的加法交换律:

overlap def +-comm (a b : Nat) : a + b = b + a
  | 0, a ⇒ idp
  | a, 0 ⇒ idp
  | suc a, b ⇒ pmap suc (+-comm _ {??})
  | a, suc b ⇒ pmap suc (+-comm _ _)

注意到，此处我在第三个分支上保留了一个“元变量”，即代码中展示的 {??}。 编译器在类型检查的过程中会尝试求解这个元变量。如果将鼠标放到上面代码中的这个元变量上， 可以得到编译器对这个元变量给出的提示：期望的类型、上下文、元变量可能的解，等等。

如果代码中含有错误，例如

def bad : 1 = 2 ⇒ idp

上面的代码尝试证明 1 = 2，但这显然是荒谬的。同样地，将鼠标放到错误的地方可以查看错误信息。

如果页面检测到一个错误信息不再被关注，那么该错误信息的窗口会被自动关闭（目前设计是失去焦点 1 秒自动关闭）。 如果点击了弹出信息内部任意一点，那么这个错误信息会被固定在页面上，只能通过关闭按钮手动关闭。 这在某些情况下非常好用：我希望将错误信息和整个代码进行对比，并通过前文提到的 IDE 功能，了解变量之间的引用关系。

如果一行代码包含多个错误信息，例如在上面的加法交换律中， 我可以手动将第四个分支里的 +-comm _ _ 写成 +-comm b a：

overlap def +-comm-bad (a b : Nat) : a + b = b + a
  | 0, a ⇒ idp
  | a, 0 ⇒ idp
  | suc a, b ⇒ pmap suc (+-comm-bad _ {??})
  | a, suc b ⇒ pmap suc (+-comm-bad b a)

数学公式

众所周知，Markdown 并不自带数学公式的支持，但是和很多其他 Markdown 解析器一样， Aya 内部实现的解析器支持了对数学公式块和内联公式。对于公式块，使用两个 $$ 符号 将公式包裹起来，例如

$$
\begin{align*}
\Gamma,\Delta,\Theta ::=  & \quad \varnothing      \\[-0.3em]
                     \mid & \quad \Gamma , x : A   \\[-0.3em]
\Sigma         ::=  & \quad \varnothing            \\[-0.3em]
               \mid & \quad \Sigma,\mathrm{decl}   \\[-0.3em]
\end{align*}
$$

将会渲染为

$$\newcommand\AyaFn[1]{\textcolor{00627a}{#1}} \newcommand\AyaConstructor[1]{\textcolor{067d17}{#1}} \newcommand\AyaCall[1]{#1} \newcommand\AyaStruct[1]{\textcolor{00627a}{#1}} \newcommand\AyaGeneralized[1]{\textcolor{00627a}{#1}} \newcommand\AyaData[1]{\textcolor{00627a}{#1}} \newcommand\AyaPrimitive[1]{\textcolor{00627a}{#1}} \newcommand\AyaKeyword[1]{\textcolor{0033b3}{#1}} \newcommand\AyaLocalVar[1]{\textit{#1}} \newcommand\AyaComment[1]{\textit{\textcolor{8c8c8c}{#1}}} \newcommand\AyaField[1]{\textcolor{871094}{#1}} \begin{align*} \Gamma,\Delta,\Theta ::= & \quad \varnothing \\[-0.3em] \mid & \quad \Gamma , x : A \\[-0.3em] \Sigma ::= & \quad \varnothing \\[-0.3em] \mid & \quad \Sigma,\mathrm{decl} \\[-0.3em] \end{align*}$$

Aya 的文学编程模式支持多种后端，即将 Markdown 编译成不同的格式。 在不同的后端中，数学公式的渲染方式可能不同，目前：

• HTML 后端：使用 KaTeX auto-render
• Markdown 后端：保留数学公式的所有内容，交给博客静态生成器处理
• TeX 后端：保留数学公式的所有内容，交给 LaTeX 编译器处理

YAML FrontMatter

博客生成器往往都支持在 Markdown 头部使用一种名为 FrontMatter 的格式来指定一些文章的元信息。例如

---
title: Aya 编程语言的「文学编程」介绍
date: 2023-4-2 21:01:16
category:
  - aya-prover
---

上面的就是本文的元信息。但是再次众所周知，原生 Markdown 并不支持这类格式， 并且三个短横线 --- 也是 Markdown 的分隔符，因此我们需要一种方法来区分这两种格式。 在代码实现上，这很简单，直接复用上面数学公式块的解析器即可。

---

文学模式实现细节

这部分我们关注这样一个问题：如何在 Aya 中实现一个文学编程的模式？

Doc: 一个统一的排版引擎

在编译器的开发中，很多情况会需要构建错误信息，并将它们向用户展示。 一般的做法是手工拼接错误信息，然后得到一个 String，最后将其打印出来。 这样的做法具有一些缺点：

• 对于不同的展示设备，例如终端和网页，我们需要为每种设备编写不同的错误信息格式以支持在这些展示设备上显示富文本。
• 由于错误信息的格式是手工拼接的，因此很难保证错误信息的一致性，例如空格、对其、代码缩进等。
• 由单纯的 String 承载的错误信息丢失了排版信息，因此很难支持漂亮的错误信息指引，例如 Rust 风格的错误信息。

为了解决这些问题，我们需要一个统一的排版引擎，它可以根据不同的参数，将错误信息进行不同的格式化。 而构建错误信息的时候，我们只需要关注错误信息的内容，不需要头疼最终的格式。

在这样的思想下，Aya 立项的最早期工作就是完成 Doc 引擎， 这个名字来源于 Haskell 的 prettyprinter (opens new window)。

Doc 的设计本质上是一套「排版 AST」和「组合子」。 它的每个叶子节点都是一个排版元素，例如文本、空格、换行等。 而每个非叶子节点都是一个排版操作，例如缩进、对齐、组合等。 此外还有其他组合子，例如

• Doc.sep 可以将多个 Doc 用「空格」连接起来，支持在页面宽度不够的时候自动折行。
• Doc.vcat 可以将多个 Doc 用「换行」连接起来。
• Doc.indent 可以将一个 Doc 缩进一定的空格数，并且在换行时保留缩进。
• Doc.styled 可以为一个 Doc 添加样式，例如颜色、粗体等。

Doc 的设计非常简单，但是它的功能却非常强大。 Aya 中所有的展示给用户的信息，都是使用 Doc 构建的（代码实现：Problem.java (opens new window)）。 甚至在 LSP 和 JetBrains 插件中，也是如此。

在 Doc 框架之上，Aya 实现了一个 Rust 风格的错误信息指引系统，例如这个报错 (opens new window)。 我们只需要提供基本的 Doc，然后给出错误发生的位置（这对于一个编译器来说是免费信息），这一套框架就能自动给出漂亮的错误信息。

一点小小的 Doc 震撼

在下面的 Doc 用例（使用 Java 代码进行展示）中，我们做了如下设置:

• 一段文本：“A univalent proof assistant designed for formalizing math and type-directed programming.”
• 将 “prefix” 纯文本放置在前面，然后添加一个空格（Doc.sep 会在 Doc 之间插入空格），然后将上一步的文本缩进 4 个空格
• 在页面宽度只有 20 个字符的情况下，将上一步得到的文档渲染成文本，并且不使用 Unicode（renderToString 的第二个参数）

class DocDemo {
  public static void main(String[] args) {
    var aya = Doc.english("A univalent proof assistant designed for " 
                        + "formalizing math and type-directed programming.");
    var doc = Doc.sep(Doc.plain("prefix"), Doc.indent(4, aya));
    System.out.println(doc.renderToString(20, false));
  }
}

得到的结果是

prefix     A
           univalent
           proof
           assistant
           designed
           for
           formalizing
           math and
           type-directed
           programming.

Doc 的多后端支持

之前提到，Doc 的设计本质上是一套「排版 AST」。 那么在编译器的思想指导下, Doc 的多后端支持本质上就是不同的「代码生成器」。

在 Aya 中，我们实现了如下后端：

• Doc → String：最基本的后端，生成纯文本。
• Doc → ANSI：带有 ANSI 颜色的文本，用于在终端中展示错误信息。
• Doc → HTML：用于在浏览器中展示错误信息。
• Doc → LaTeX：用于生成 PDF 文档，并用于论文写作。
• Doc → Markdown：用于生成文档网站。

以上的代码实现都可以在这里 (opens new window)找到。 如果你的项目使用的也是 Java，那么参考这里 (opens new window)的方法，可以给你的项目添加 Aya 中的 pretty 模块作为依赖，也就是 Doc 框架所在的地方。

Literate AST: 统一的文学编程 AST

一个文学编程的源文件不仅含有 Aya 源代码，还含有排版信息，例如 Markdown 中的标题、列表、连接等。 由于 Aya 支持将同一个文学编程的源代码编译成多种不同的目标，例如 Markdown、LaTeX 等， 我们自然需要一个统一的文学编程 AST，在编译过程中保留格式信息， 在编译完成后将它们转换成 Doc 从而实现“一次书写，到处渲染”：用户不需要关心最终生成的页面是什么格式的，哪怕用户只写了 Markdown。

这一部分的设计及其类似 Doc，不再赘述细节，让我们用 Aya 代码表达：

// Code block language
open data Language
  | Aya
  | Other String

// Supported styles
open data Style
  | Italic | Bold    | Underline
  | Error  | Warning | Goal
  // ... omitted

// Literate AST
open data Literate
  | Raw Doc
  | Many Style (List Literate)
  | Code Bool Language String
  | Math Bool String
  // ... omitted

从 Literate AST 解析出 Aya AST

这部分最关键的问题是：如何将 Literate AST 里与代码无关的东西都删除，但保留代码的位置信息（用于报错）。

Aya 的策略是：将非代码块的内容都替换成「等长」的注释。然后将得到的文本交给 Aya 的编译器进行正常的流程。

代码实现：AyaMdParser.java (opens new window).

将 Aya AST 编译的结果传播回 Literate AST

这是最难的地方，因为 Literate AST 中只含有代码的纯文本，而 Aya AST 中含有代码经过编译后的语法树，其中包含了类型信息。 我们就需要使用这些类型信息，给 Literate AST 中的代码文本「上色」：添加代码高亮、添加引用跳转等。

和传统的 pretty printer 不同，传统的 pretty printer 是代码格式化工具， 其只需要将语法树转换成文本，而不需要保留原来文本的格式（例如缩进、空格等）。 这意味着这样产生的文本，和用户写下来的文本，可能并不一样。

但是文学模式下，我们必须尊重用户的写法。这意味着我们只能根据 Aya AST 中的位置信息，对原代码文本中的片段设置样式。 这部分的代码实现在：FaithfulPrettier.java (opens new window)。 这个功能的实现经历了非常多的困难，但是我们的小伙伴非常厉害，只用了不到 3 天就做完了。

其实，这就是一个 IDE 在高亮阶段所作的事情。在 Aya 的 LSP 服务端中，就复用了这部分产生高亮信息的代码， 并通过协议将其发送给前端（通常是 VSCode）。但是值得一提的是，Aya 的 JetBrains 的插件并不是通过这种方法实现基于语义的语法高亮的， 详见 SemanticHighlight.java (opens new window)。 相反，JetBrains 插件的开发流程比 LSP 简单许多， 我们只需要提供一套通用的 AST，即 PsiElement (opens new window)， 对于编译器来说，这就是随手可得的；和其上的引用信息，即 PsiReference (opens new window)， 便可以直接免费获得大量功能：基于语义的语法高亮、跳转、重构、索引、符号搜索等。而这些功能每一个在 LSP 中都需要单独实现。 关于 LSP 和 JetBrains 插件的开发体验和功能实现复杂度，我可能会在未来单独写一篇文章，详细描述二者的优劣。

---

Aya 的文学编程是整个开发小组一起努力的结果。缺少了任何一个人，我们都不可能做到现在的成果。 我们非常感谢所有参与 Aya 开发的小伙伴，他们的贡献是 Aya 的灵魂。

欢迎成为我们的一员：aya-prover/aya-dev (opens new window)

相关链接

• Overhaul Literate
• Implement resolveLax, allow inline code to refer to variable
• Show compiler diagnostics in literate output