numeric_expr 设计

设计目标

floating 的符合性前端读取四种截然不同的语料格式（GDA .decTest、IEEE 1788 .itl、MPFR 数据文件、Berkeley TestFloat 向量），并针对四种数值类型运行它们。numeric_expr 为它们提供一种共享的、带类型的中间形式来表示”将此运算作用于这些操作数”，以及一个求值器，从而将解析、数值语义和错误报告分离开来：

前端将文本转换为 Expr，并保留源码位置；
后端以两个回调的形式给出，说明字面量和运算的含义；
evaluate 将二者结合起来，并报告是哪个节点失败了。

该包本身不包含任何算术、数值解析、IO 或全局状态。

数学背景

语法

设 $L$ 为字面量（带有区间范围的原始文本）的集合， $O$ 为运算（带有区间范围的名称）的集合。公开构造函数恰好生成如下文法的项

e \;::=\; \mathsf{lit}(\ell) \;\mid\; \mathsf{op}(o)(e_1, \dots, e_n), \qquad \ell \in L,\; o \in O,\; n \ge 0 .

在内部，一个项存储为 Luna-Flow/type_theory 包中的 @tt_syntax.Term[Atom]，其中 Atom 是一个私有枚举，包含字面量情形和原语运算情形。Expr::literal(ℓ) 即 Value(LiteralAtom(ℓ))，Expr::invoke(o, args) 即 Apply(Value(PrimitiveAtom(o)), args)。一般的 Term 类型还有 Variable 和 Bind 形式，并允许函数位置上出现任意项；公开构造函数从不创建这些形式。

语义

固定一个值集合 $V$ 、一个错误集合 $E$ 以及两个回调

d : L \to V + E, \qquad i : O \times V^{*} \to V + E .

记 $\mathrm{Err}$ 为 EvalError[E] 的错误集合 $L \times E \;+\; O \times E \;+\; \mathrm{Span}$ 。含义 $[\![e]\!] \in V + \mathrm{Err}$ 通过结构递归定义：

\begin{aligned} [\![\mathsf{lit}(\ell)]\!] &= \begin{cases} v & \text{if } d(\ell) = v,\\ \mathsf{LiteralFailure}(\ell, x) & \text{if } d(\ell) = \mathrm{err}\ x, \end{cases}\\[4pt] [\![\mathsf{op}(o)(e_1, \dots, e_n)]\!] &= \begin{cases} [\![e_k]\!] & \text{if } [\![e_1]\!], \dots, [\![e_{k-1}]\!] \in V \text{ and } [\![e_k]\!] \in \mathrm{Err},\\ v & \text{if all } [\![e_j]\!] = v_j \in V \text{ and } i(o, v_1 \dots v_n) = v,\\ \mathsf{OperationFailure}(o, x) & \text{if all } [\![e_j]\!] = v_j \in V \text{ and } i(o, v_1 \dots v_n) = \mathrm{err}\ x . \end{cases} \end{aligned}

这是语法树在错误单子 $V \mapsto V + \mathrm{Err}$ 中的折叠（catamorphism），参数从左到右依次求值。求值器是对它的直接转写：evaluate_term 匹配三种形状，在 for 循环中求值各参数，并在遇到第一个 Err 时返回。

设计决策

使用回调而非数值 trait

问题。 同一种行格式要针对多种数值类型执行，而每个前端都需要自己的值类型：gda_expr 求值为一个由十进制数、整数、布尔值和字符串组成的枚举，每个都带有十三个 GDA 状态标志。

备选方案。 一个诸如”V 能解析字面量并应用运算”的 trait；一个所有前端共享的固定值枚举；或者两个普通的函数参数。

选择。 两个函数参数。MoonBit 的 trait 只有 Self 参数，因此 trait 无法把运算表作为数据接收，而且一种值类型也无法拥有两种解释（例如，同一个 Decimal 分别在 IEEE 上下文和 GDA 上下文下读取）。函数还能捕获每行的状态：gda_expr 闭包捕获该行的 GdaContext，因此同样的字面量文本会以其所在指令块的精度和舍入方式读取。

基于 `type_theory` 语法的不透明 `Expr`

问题。 调用者应当能够构建和求值表达式，而无需依赖树的存储方式；同时该包日后应当能够扩展出变量和绑定子。

选择。 Expr 包装一个私有的 @tt_syntax.Term[Atom]。type_theory 负责组织内各语法树的绑定与代换，因此日后可以复用它来添加变量和 Bind，而无需第二种树类型。由于该字段是私有的，日后添加构造函数不会破坏只使用 Expr::literal、Expr::invoke 和 evaluate 的调用者。

从左到右、快速失败的求值

问题。 当有多个操作数无效时，报告哪个错误？求值是否继续？

选择。 参数从左到右求值，返回第一个错误而不再求值其余参数。因此报告的错误是确定的（后序遍历中最左侧失败的叶子或节点），并且不会对将被丢弃的值运行任何回调。想要获取文档所有诊断的前端应在解析时、求值之前收集它们，本仓库中的前端正是这样做的。

错误保留语法节点

LiteralFailure 和 OperationFailure 携带 Literal 或 Operation 本身，而不只是一条消息。节点包含原始文本或名称以及区间范围，这正是语料运行器要打印的内容。回调的错误 E 保持不变，因此带类型的错误能在求值后保留下来。

正确性 / 不变式

命题 1（封闭形状）。 用公开 API 构建的每个 Expr，要么是 Value(LiteralAtom(ℓ))，要么是 Apply(Value(PrimitiveAtom(o)), args)，且 args 的每个元素也都是这两种形状之一。因此对于这样的树，evaluate 绝不会返回 UnsupportedExpression。

证明。 对构造过程归纳。Expr::literal 产生第一种形状。Expr::invoke(o, args) 产生第二种形状，其参数是 Expr 值的项，由归纳假设它们具有所述形状。evaluate_term 仅在以下情况返回 UnsupportedExpression：子项根部为 Value(PrimitiveAtom(_))、Variable、Bind，或头部不是 Value(PrimitiveAtom(_)) 的 Apply；这些都不会出现。 $\square$

命题 2（后序前缀）。 设 $u_1, u_2, \dots, u_N$ 为树中节点的后序排列（子节点从左到右，然后是父节点）。evaluate 所做的回调调用序列为 $c(u_1), c(u_2), \dots, c(u_m)$ ，其中 $c$ 对字面量为 decode，对运算节点为 invoke，且

m = \begin{cases} N & \text{if evaluation succeeds,}\\ \min\{\, k : c(u_k) \text{ returns } \mathrm{Err} \,\} & \text{otherwise.} \end{cases}

证明概要。 对树归纳。叶子恰好调用一次。对于 $\mathsf{op}(o)(e_1, \dots, e_n)$ ，其后序是 $e_1, \dots, e_n$ 各自后序的拼接，再接上该节点本身。循环按顺序求值 $e_1, \dots, e_n$ ；由归纳假设，每个子节点都按自身后序进行调用，并在其第一个失败的调用处停止，而循环在某个子节点失败时立即返回。若所有子节点都成功，则对该节点调用一次 invoke。将这些拼接起来即得结论。 $\square$

推论：成功时，decode 对每个字面量运行一次，invoke 对每个调用节点运行一次；没有任何回调对同一节点运行两次；返回的错误属于节点 $u_m$ ，且恰好被包装一次（子节点的错误原样返回，不会被祖先节点再次包装）。

命题 3（纯性与确定性）。 evaluate 只读取树，并且只调用这两个回调。若回调是确定性函数，则 evaluate 也是。

复杂度。 对于具有 $N$ 个节点、高度为 $h$ 的树，求值至多进行 $N$ 次回调调用，为每个调用节点分配一个参数数组（总大小至多为 $N - 1$ ），递归深度为 $h$ 。用 Expr::invoke 构造时会复制参数数组，对 $n$ 个参数为 $O(n)$ 。

被否决的替代方案

为 Expr 使用公开枚举。 调用者可以对树进行模式匹配，但每一种新的语法形式（变量、绑定子）都会破坏他们的代码。不透明结构体保留了这种自由。
在求值期间收集所有错误。 在出错后仍继续的应用式（applicative）求值器将不得不为失败的操作数编造值或跳过运算，这会使后续错误的含义变得不清楚。前端改为在求值前收集解析诊断。
在 Operation 中记录元数。 声明的元数只会重复后端无论如何都要做的检查（后端还必须检查操作数种类），而且对变元运算也不适用。
使用显式栈代替递归。 语料行都很浅（对字面量施加一个运算），因此保留了更简单的递归折叠。

边界

不提供词法分析器、解析器或美化打印器：由前端将文本转换为 Expr。
不提供数值类型、舍入、精度、标志或上下文：所有数值语义都由回调负责。
不对运算做元数或类型检查。
尚未公开变量、绑定子、共享或用户自定义函数，尽管内部表示可以容纳它们。
不做 IO、日志记录，也没有全局状态；源码区间范围只是普通数据。
不支持对整个表达式进行相等比较或打印。