回溯式模式匹配编译

共享后续代码，允许重复观察 ​

最直接的策略是按源行逐个尝试：第一行失败，跳到第二行的入口；第二行失败，再去第三行。每行的动作和后续代码各生成一份。某个输入可能多次接受“根是不是Cons”的测试，因为不同源行各有自己的TEST。

一般回溯搜索理路回溯法Backtracking深度优先枚举部分解并在不可能完成时撤销选择的搜索范式。把失败转成另一个候选的探索，这里把候选顺序和成功提交点固定为模式语义。编译器生成的是有限无环分派代码，不是在运行时搜索所有程序状态，也没有改变源行的优先级。

静态失败标签可以直接编译成跳转。它不像任意动态异常，需要在调用栈中查找未知处理者；这个标签的目标在编译时已经确定。经典模式编译使用static exit/catch组织这样的控制流，本页用显式整数标签暴露同一机制。[1, §3.1]

or不是把整个后缀再复制一次 ​

编译p|q时，先生成q的入口，成功去共同s，失败去共同f；再生成p，成功也去s，失败才去q入口。两个替代共享后缀s。嵌套or因此不必先做笛卡尔积展开。

一旦左臂结构成功，就进入共同后缀。后面的guard失败应去下一源行，不能返回q。若后缀只是其它独立的结构字段，失败后也无需改试当前or：线性模式中其余字段的结构匹配不依赖本or选出的绑定，换臂不会把已经失败的其它字段变成成功。

一次重复测试是如何产生的 ​

沿用列表/Bool表：Nil/先返回empty；Cons(T,xs)/F返回take-tail；Cons(,)/T返回flagged；Cons(F,)/F返回false-head；最后还有被遮蔽的Nil/T行。

下载器保留全部五源行，生成23条指令。输入(Cons(T,Nil),F)先在第一行尝试Nil失败，再在第二行测试Cons、头T与标记F，得到take-tail及xs=Nil。标签测试共4次，根位置出现两次；完整指令执行8步，字段投影2次。对应决策树做3次标签测试，返回同一个环境。

输入(Cons(F,Nil),F)经过前三行失败，在第四行成功。标签测试8次、字段投影6次、完整指令13步；决策树标签测试3次、字段投影2次。多出的测试是真正执行的工作，不能只统计动作返回次数就说两者成本相同。

guard失败后的错误展开 ​

只用一个List输入，第一行如下，第二行是_ → fallback：

(Cons(_,xs) | xs) when nonempty(xs) → first

取单元素列表Cons(T,Nil)。左臂结构成功，xs绑定Nil，guard为假，所以进入第二行，返回fallback。右臂不会再把xs绑定为整个非空列表。

如果错误地展开成Cons(_,xs) when nonempty(xs) → first和xs when nonempty(xs) → first两个独立源行，第一行guard失败后就会执行第二行。xs这次成为原列表，guard为真，结果错误地变成first。无guard的or展开规则不能未经检查地搬到这个扩展上。

该例的全部8条目标指令为：

0  FAIL
1  ACCEPT fallback, [], true, 0
2  CLEAR 1
3  ACCEPT first, [xs], nonempty_xs, 2
4  BIND xs, root, 3
5  BIND xs, tail, 3
6  TEST root, Cons, [head,tail], 5, 4
7  CLEAR 6                       # 总入口

单元素执行标签7→6→5→3→2→1，guard只执行一次。Cons测试失败时才走6→4，尝试右臂；若Cons测试成功，右臂4就被越过。两元素列表的尾仍非空，因此7→6→5→3直接返回first。

临时绑定为何不会污染下一分支 ​

一次失败的左臂可能已经写入部分变量。编译器并不在失败时执行动作或guard；成功的右臂必须重新绑定两臂共同的完整变量集合，因而覆盖左臂留下的同名临时项。本行其它字段变量与它们不重名；进入下一源行则先CLEAR。

例如Cons(h,Cons(_,xs)) | Cons(h,xs)匹配单元素列表：左臂先绑定h，再因尾不是Cons失败；右臂重新绑定h和xs，最终得到正确的头与空尾。若允许两臂绑定不同变量集合，某个旧临时项可能被错误读出，所以下载器在入口拒绝这种模式，而不是寄希望于运行路径凑巧安全。

构造规则与正确性 ​

通配符直接返回成功标签s，不产生指令；变量产生一条BIND后去s。构造子先递归编译字段，从最后字段向前串联成功出口，再产生一条TEST：标签相同才投影字段并进入字段代码，不同就去f。每个字段失败都去当前构造子失败出口。

or的规则是right=compile(q,o,s,f)，再返回compile(p,o,s,right)。各源行从最后一行向前编译：先生成本行ACCEPT，其guard失败出口是下一源行CLEAR；再把各列串起来，最后生成本行CLEAR。所有行结束后落到唯一FAIL。

局部归纳不变量是：从模式入口执行，结构匹配失败就转f，成功就带着该模式的正确绑定转s；到s以前不执行本行guard或动作。构造子借字段顺序保持它；or借左臂优先与共同绑定集合保持它。行入口CLEAR和ACCEPT再把局部性质提升为第一条guard通过的源行结果。无guard时就得到与决策树共同核心相同的结果。

构造子后缀不会复制到每个or替代中，因此字节码中的共享是标签层面的真实共享。下载器先生成所有目标，再生成跳向它们的指令，每条非终止跳转都指向较小编号。程序计数器严格下降，故一次运行不会无限回溯，也不会执行同一条指令两次；重复的是不同指令对同一输入位置的观察。

线性体积与完整成本 ​

设m为源行数，C为模式语法中的构造子出现数，V为变量出现数；or两臂中的出现都分别计数。这个编译器恰好生成

条指令：一条FAIL，每行CLEAR与ACCEPT，各构造子一条TEST，各变量一条BIND。通配符和or节点只连接既有标签，不额外发指令。字段操作数和绑定名单另按其实际条目数计，总编码仍与源模式规模线性。

对n列全为F|T的一行，C=2n、V=0，所以只有2n+3条指令；n=4时11条，n=8时19条。相同输入若直接展开成无共享决策树，分别是31和511个树节点。回溯的单次标签测试最多2n，树是n；两者都返回yes，但花费不同。

令A包含行、模式节点、字段槽和已有绑定名单。完成类型/变量良构校验后，编译主体期望O(A+1)时间和空间，槽驻留使用字典。入口校验会合并变量字典，保守最坏O((A+1)²)，不把它藏进主体的线性界。递归生成需要与模式深度相应的调用栈；下载Python实现也受解释器栈限约束。

运行设I为实际访问指令数，p为成功TEST投影字段数，b为各ACCEPT构造绑定表的总项数，g为实际guard工作。期望成本O(n+I+p+b+g+1)，另计外部输入验证和输出展开。I不超过静态指令数，但代码尺寸、标签测试数、投影数和完整执行步数不能互相代称。下载器保存测试日志，并用显式检查保证普通与python -O都执行验收。

模式匹配终点要求交IR和实际轨迹，先在无guard核心对照源语义，再单独执行左偏or/guard反例。覆盖检查理路模式匹配覆盖检查Pattern-match coverage checking · Pattern usefulness · 模式有用性检查用模式矩阵的特化与默认分支计算有用性，返回真正漏掉的有限值，区别非穷尽、被遮蔽行与带guard的可达性。提供的无guard遮蔽结论仍有用，但不能拿它直接删除带guard的候选行。