parser 设计

parser 包把文本转换为语法树，再把语法树转换为内核项。它不受信任，且刻意保持狭窄：它确定表面记法，在用户能够定位的位置报告错误，并把目标作为普通数据向上传递。本页解释文法、降级 (lowering) 路径以及与策略层的边界。

设计目标

• 为命题目标和证明脚本接受一种小而无歧义的记法，以 Unicode 为规范形式，ASCII 拼写仅作输入上的便利。
• 即使经过规范化，也要在用户所写文本的偏移处报告每个错误。
• 仅通过 elab 的解析边界和 logic 的联结词构造器降级为内核项，使解析器从不决定名称或联结词的含义。
• 保持在策略层之下：产生目标，绝不产生证明状态。

数学背景

文法

项遵循以下文法，其中 name 是标识符，应用即并置：

$$\begin{aligned} \mathit{term} &::= \mathit{term}\ \mathit{op}\ \mathit{term} \mid \neg\,\mathit{term} \mid \mathit{app} \\ \mathit{app} &::= \mathit{atom}^{+} \\ \mathit{atom} &::= \mathit{name} \mid (\,\mathit{term}\,) \\ \mathit{op} &::= {=} \mid {\wedge} \mid {\vee} \mid {\to} \end{aligned}$$

第一条产生式的歧义由优先级和结合性解决：

运算符	优先级	结合性	链的解读
=	40	无	a = b = c 是错误
∧	30	左	a ∧ b ∧ c 即 (a ∧ b) ∧ c
∨	20	左	a ∨ b ∨ c 即 (a ∨ b) ∨ c
->	15	右	a -> b -> c 即 a -> (b -> c)

目标是相继式 $h_1, \dots, h_n \vdash c$，目标可以以 forall (x : A), ... 开头。定理脚本增加了带绑定子的头部和由步骤组成的主体，在 split、left 和 right 之后可跟可选的 { ... } 分支块。

算符优先级解析

中缀链 $t_0\ o_1\ t_1\ \dots\ o_n\ t_n$ 用算符栈解析。当新算符 $o$ 到来而栈顶是算符 $o'$ 时，解析器恰在以下条件下先归约 $o'$

$$\mathrm{prec}(o') > \mathrm{prec}(o) \;\lor\; \big(\mathrm{prec}(o') = \mathrm{prec}(o) \land \text{both are left-associative}\big),$$

当优先级较低或两者均为右结合时保留 $o'$，而当优先级相等且其中之一为非结合时以 NonAssocChain 失败。每个算符恰好入栈和出栈一次，因此算法对链长是线性的，并产生遵循该表的唯一树。

降级

降级把语法映射为内核项：

$$\begin{aligned} [\![x]\!]_\Gamma &= x{:}\tau &&\text{if } (x:\tau) \in \Gamma \\ [\![c]\!]_\Gamma &= c^{\iota}{:}\sigma &&\text{if } c \text{ is declared with identity } \iota \text{ and schema } \sigma \\ [\![a\ b]\!]_\Gamma &= [\![a]\!]_\Gamma\,[\![b]\!]_\Gamma \\ [\![a = b]\!]_\Gamma &= ([\![a]\!]_\Gamma = [\![b]\!]_\Gamma) \\ [\![a \wedge b]\!]_\Gamma &= \texttt{prop\_mk\_and}([\![a]\!]_\Gamma, [\![b]\!]_\Gamma) &&\text{and likewise for } \vee, \to, \neg \end{aligned}$$

名称经过 elab（局部变量先于常量，标识冻结），联结词经过 logic 构造器，后者检查其参数是命题。目标 forall (x : A), body 的降级方式是把 $x{:}A$ 加入 $\Gamma$ 并降级 body：量词被丢弃，$x$ 在目标中保持自由，与定理头部绑定子 (x : A) 完全一样。含自由变量的定理对该变量的每个取值都成立，因为 INST 可以代换任何同类型的项，所以带自由 $x$ 的 $\vdash \mathit{body}$ 就是量化命题的 HOL 解读。

设计决策

先规范化，保留偏移映射

问题。 用户会键入 \and、|- 或多余的空格；错误信息必须指向他们所键入的内容。

选择。 normalize_parser_input 一次性将输入改写为规范文本，并为每个字符记录其原始偏移。词法分析器和解析器在规范文本上工作，每个错误偏移和跨度在离开该包之前都会映射回去。

原因。 单一的规范形式使文法保持精简，映射则使诊断保持诚实。旧的 ASCII 拼写 /\ 和 \/ 不再被接受，因此每个联结词只有一种 ASCII 拼写。

原始解析与降级分离

问题。 降级需要内核状态；而证明器等工具需要在任何状态存在之前就获得脚本结构，例如报告某一步的位置。

选择。 每种构造都有一个返回带位置、不带状态的语法树的 _raw 解析器，以及一个接受状态的降级函数。定理脚本只做原始解析；证明器自行降级其目标。

原因。 证明器可以按跨度和索引指出失败的步骤而无需重新解析，解析器也保持独立于证明执行。

解析器自有的目标

问题。 parse_goal 显而易见的返回类型是 tactics 包的 Goal，但这样解析器就会依赖策略层，那里的改动会波及语法。

选择。 解析器返回它自己的 ParsedGoal；证明器用 @tactics.mk_goal 对其进行转换。

原因。 这使层次顺序 kernel → logic/elab → parser → tactics → prover 保持无环，如代码治理所要求，同时也意味着解析器即使出错也无法构造证明对象。

联结词是构建的，而非查找的

联结词用 logic 构造器降级为基础项；解析器不要求名为 and 或 imp 的常量存在。这使每个联结词在每个状态下含义相同，并让解析器在降级时就把非命题参数报告为 Logic(NotBoolTerm)，而不是留给某个策略处理。

量词仅作为目标的语法糖

原始 forall 只在目标开头被接受，其他地方都不接受。项中的一般绑定子需要逻辑层中的量词常量及其规则，而已发布子集并不具备。只在目标开头接受它（此时它与定理头部绑定子含义相同），能使表面保持诚实：凡能解析的内容都能由现有机制证明，而项内部的 forall 会以清晰的 UnexpectedToken 失败。

每一步都带位置

每个脚本步骤都记录其索引、分支路径和跨度。这些字段是证明器和 CLI 在失败以及未完成证明时所报告的内容，因此用户看到的是 step: 3、branch: 1 和源文本，而不是光秃秃的错误。

正确性与不变量

• 无权限。 解析器构建项，并通过 parse_def_function 调用内核的 DefOK 闸门。它不经任何其他途径产生定理。
• 偏移指向原始输入。 对每个 ParseError 和 SourceSpan，偏移是原始字符串中的位置，位于 $[0, \text{raw length}]$ 内。
• 确定性结构。 优先级表为每条被接受的链定义唯一的树；= 的链被拒绝而不是靠猜测。
• 局部变量先于常量。 绑定子或 let 局部变量会遮蔽同名常量，与 elab 和策略层一致。
• 步骤编号。 step_index 在整个脚本中按源码顺序从 1 开始对步骤计数，包括分支块内的步骤，因此诊断中的编号与脚本的阅读顺序一致。

被否决的替代方案

• 解析器生成器。 文法足够小，手写词法分析器和算符优先级解析器更短，给出的错误偏移更好，也不需要构建步骤。
• 返回策略对象。 出于分层原因被拒绝，如上所述。
• 完整的 HOL 项语法，到处都有带类型的绑定子、类型标注和量词。它会引来策略层无法证明的脚本；语法只随证明机制一起增长。
• 隐式的 T 和 F。 它们是通过状态解析的普通常量名称，因此前奏缺失时脚本会明显失败，而不是悄悄使用另一种含义。

边界

• 没有类型推断：绑定子和 let 的类型须显式写出；项内部没有类型标注。
• 项内部没有 forall 或 exists，没有 λ 抽象语法，也没有用户自定义算符。
• 没有美化打印器：项由内核的结构化打印器渲染。
• 不执行证明：步骤被解析为 SynTacticStep 值，由 tactics 包运行，并由 prover 调度。