Luna Flow
简体中文

elab 设计说明

elab 包在精化（elaboration）时一次性固定项中每个名称的含义，并在签名之后变化时保持该含义。本页解释它所解决的问题、它实现的两个判断，以及使得在内核检查任何东西之前就进行解析是安全的稳定性性质。

设计目标

用户书写名称；内核使用常量标识。两者之间是一个带作用域的签名，其中 push、add 和 pop 会改变名称所指的对象。目标是一个解析步骤，其结果不会在用户背后改变含义：在某个作用域中解析的项，要么恰好保持其解析到的常量，要么失败，但绝不会悄悄接纳同名的较新声明。

数学背景

形式规范区分了两个判断。

具名精化把局部上下文 Γ\Gamma 和签名 Σ\Sigma 中的具名项 tt 解析为已解析项 dd：

Σ;Γ⊢t⇓d\Sigma ; \Gamma \vdash t \Downarrow d

其规则为：在 Γ\Gamma 中绑定的名称成为变量；否则在 Σ\Sigma 中可见的名称成为常量 cτ⪯σιc^{\iota}_{\tau \preceq \sigma}，带有标识 ι\iota、声明的模式 σ\sigma 和出现类型 τ\tau；应用和抽象逐分量解析，绑定子被加入 Γ\Gamma。“先局部、后常量”的顺序是固定的。

核心类型检查在不查找名称的情况下检查已解析项：

(x:τ)∈ΓΣ;Γ⊢rx:τΣ(ι)=(c,σ)τ⪯σΣ;Γ⊢rcτ⪯σι:τΣ;Γ⊢rf:α→βΣ;Γ⊢ru:αΣ;Γ⊢rf u:β\frac{(x : \tau) \in \Gamma}{\Sigma ; \Gamma \vdash_r x : \tau} \qquad \frac{\Sigma(\iota) = (c, \sigma) \quad \tau \preceq \sigma}{\Sigma ; \Gamma \vdash_r c^{\iota}_{\tau \preceq \sigma} : \tau} \qquad \frac{\Sigma;\Gamma \vdash_r f : \alpha \to \beta \quad \Sigma;\Gamma \vdash_r u : \alpha}{\Sigma;\Gamma \vdash_r f\,u : \beta}

并且抽象规则扩展 Γ\Gamma。常量规则读取 Σ(ι)\Sigma(\iota)，即标识为 ι\iota 的声明，而不是当前在名称 cc 下可见的声明。在实现中，这是 elab_core_type_of 里的检查 id == rc.const_id && schema == rc.schema_ty。

设计决策

一次解析，冻结标识

问题。 如果项存储名称并在每次使用时查找，同一个项在作用域变化前后可能有两种不同的含义。

选项。 每次使用都重新解析；只存储内核项；存储带标识的已解析项。

选择。 RTerm 把每个常量存储为带标识、模式和实例类型的 ResolvedConst。核心类型检查把它们与状态比较，任何差异都会导致失败。

原因。 规范中的“Resolution Freeze under Scope Mutation”定理陈述了由此获得的性质：若 Σ;Γ⊢t⇓d\Sigma; \Gamma \vdash t \Downarrow d，且一系列 push、add 和 pop 操作把 Σ\Sigma 变成 Σ′\Sigma'，则 dd 不变，关于 dd 的每个判断要么仍然成立，要么明确失败。证明在于 dd 包含的是标识而非延迟的查找，且标识永远不会被复用（内核从单调计数器分配它们）。只存储内核项对内核而言同样可行，但前端需要模式来报告实例化错误，并在降级（lowering）之前检查项。

局部先于常量

局部名称总是遮蔽同名常量。这是通常的词法作用域，是规范所固定的规则，也是策略层处理假设名与定理名时遵循的规则。elab API 中的示例展示了局部 c 遮蔽常量 c。

独立的包

问题。 解析可以放在解析器（parser）中，它是解析的主要客户。

选择。 它是位于内核与解析器之间的独立包，只依赖内核。

原因。 解析契约是规范的一部分，并单独测试；解析器可以更改语法而不触及它，其他前端也可以复用它。代码治理中的分层 kernel → logic/elab → parser 记录了这一点。

错误作为数据，类型检查作为 option

解析返回 Result[_, ElabError]；核心类型检查返回 HolType?。查找失败有值得报告的原因（UnknownName、InvalidConstInstance），而类型检查失败只是单一事实（CoreTypingFailure），其细节内核本来也会重复给出。

正确性与不变量

  • 可靠性不受威胁。 elab 构建项，从不构建定理。错误的解析只会产生内核拒绝的项，或关于与预期不同的命题的定理；后者正是冻结所要防止的。
  • 降级保持标识。 elab_lower_to_term 把 cτ⪯σιc^{\iota}_{\tau \preceq \sigma} 映射为带标识 ι\iota 的内核常量 c:τc{:}\tau，因此内核的可容许性检查看到的是用户所解析的标识，并拒绝其常量此后已被遮蔽的定理。
  • 往返。 对于在状态 Σ\Sigma 中构建的项 tt，当且仅当在 Σ′\Sigma' 中重新解析 tt 得到相同的标识时，elab_roundtrip_term(Σ', Γ, t) 才成功，因此它能检测作用域漂移。
  • 相等是内建的。 在每个状态中，= 都解析为标识 -1，模式为 α→α→bool\alpha \to \alpha \to \mathit{bool}；它既不能被声明，也不能被遮蔽。

被否决的替代方案

  • 在内核时查找。 把名称传给内核并让它解析，会把作用域管理放进可信基，并使定理的含义依赖于使用时的状态。
  • 全局唯一名称。 要求每个常量名唯一可以消除遮蔽以及对标识的需要，但规范中带作用域的签名正是为了让局部开发可以复用名称。
  • 类型推断。 解析器检查已写出的类型；它不推断绑定子的类型，也不根据上下文实例化多态常量。

边界

  • 不做解析：parser 把文本转为语法并调用本包。
  • 不做类型推断或合一；每个绑定子的类型都是显式的，常量按其模式类型使用，除非请求了某个实例。
  • 没有重载、强制转换、隐式参数或类型类。
  • 没有定理，也没有权威性：降级只产生内核项。