ch:pattern-compilation: ch:pattern-compilation

Problem, result, and invariant. Build the exact five-case finite decision model over structured patterns, ordered rows, and frontier columns. Specializing constructor $c$ must replace one frontier column by $\mathsf{arity}(c)$ columns and the selected pattern of every retained row by exactly $\mathsf{arity}(c)$ patterns. Preserve source order, select the leftmost blocking pattern of the first candidate row, and compute the two accepted trees and three distinct rejections. This remains a closed acceptance slice, not the general typed compiler defined in the chapter.

Representation tradeoff. A general implementation would represent terms, typed frontier telescopes, rows, patterns, substitutions back to the original arguments, residual constraints, and constructor paths. That representation admits arbitrary new matrices and is the right setting for compilation typing and simulation, but it requires well-scoped substitution and restricted unification before the first end-to-end result can run.

The companion closes the input and output spaces while making the finite specialization mechanism real:

data Pattern : Type =
    VariablePattern
    ConstructorPattern Constructor (List Pattern)
    InaccessiblePattern DotTerm
    AbsurdPattern

data Row : Type =
    Row Nat (List Pattern) Body
      (List Binding) (List Obligation) (List Constructor)

data Tree : Type =
    Split Nat (List Constructor)
      (List (List Assignment)) (List Tree)
    Leaf Body Bool

data CompileResult : Type =
    Compiled (List Column) Tree Bool | Rejected Diagnostic

An accepted append branch carries the assignments AssignLengthZero and AssignVectorNil; there is no decorative substitution tag. The generic split tree obtains these assignments from the branch-specialization result rather than from an append-specific tree constructor. The selected-cell specializer implements all four pattern cases. Matching constructor heads expose their subpatterns, different heads delete the row, and variable, inaccessible, and absurd patterns each contribute a fresh pattern tuple of constructor arity. The latter two also record the obligation or reachable marker checked by ordered priority. If the branch substitution also eliminates another column, the separate recursive forced-image matcher consumes that cell without adding frontier cells. Thus append drops and validates its forced length pattern after specializing the vector cell once.

First complete version. Start with the two append rows. The leftmost-blocker scan selects vector column 1, after the inaccessible length column. Specialize against the empty and successor vector constructors; the derived branch substitution then force-matches and removes the old length cell. Require matrixFits on the resulting frontier and rows. Ordered priority selects the return-right body and the recursive-prepend body. Interpret that same derived tree on [1,2] and [3]: the empty leaf returns the right list, while the successor leaf prepends the head and recursively re-enters the tree on the direct child. The first record is accepted only when this interpretation of the derived tree, its assignment lists, the width invariant, and the value [1,2,3] all agree with the oracle. No independent append function participates.

Remaining cases. Compile overlap to a Boolean split and evaluate both constructors. In the true branch, constructor specialization retains the first row and variable specialization retains the wildcard row behind it; selectPriority therefore computes the shadowed-wildcard flag. A hidden guard exercises the selected inaccessible-pattern path: splitting an index successor must accept suc(k) and reject suc(zero). Comparing only the outer successor head is insufficient. A second hidden guard places the invalid dot before a later constructor pattern and requires the compiler to return that blocking column before checking the residual dot. Add three distinct diagnostics. For bad-dot, apply the derived vector-branch substitution $m:=\mathsf{suc}(k)$ through the inaccessible pattern; do not manufacture a second split on $m$. The diagnostics are UncoveredFalse, an inaccessible mismatch whose printed fields are forced suc(k) and written k, and the two reachable Boolean constructors refuting an absurd pattern. These categories cannot substitute for one another.

Observable result. The accepted transcript is exactly

append-123=ok:[1,2,3]
overlap-bool=ok:true->0,false->1,shadowed-wildcard=true
missing-false=reject:uncovered:path=false
bad-dot=reject:inaccessible:forced=suc(k),written=k
absurd-bool=reject:reachable:true,false
All 5 Chapter 121 corpus cases passed.

The two-constructor list is deliberately stronger finite instrumentation: it records both positive branches. It is not the seven-result compiler’s single declaration-order $\mathsf{badAbsurd}(1,\mathsf{tt},(\mathsf{tt}))$ diagnostic. These five outcome records and owner summary are the complete observable interface.

Missing-constructor mutation. In buildMissing, replace the empty specialized branch’s uncovered rejection by a well-typed compiled Boolean split. The program remains well typed, but the third record becomes missing-false=FAIL; exact acceptance rejects the mutant. Restore the coverage diagnostic before the final run.

Acceptance test. Accept the corpus only when the output is precisely the five records above, in order, and the audit is empty. Replay the coverage mutation once, require the third record to fail, restore the source, and repeat all four commands in appendix E.

Evidence boundary. The companion makes the five acceptance groups executable: it specializes finite structured rows, checks the row/frontier-width invariant, derives actual assignment lists, evaluates the compiled append and overlap trees, and distinguishes all requested diagnostic categories. The rendered path and residual terms are fixed observations of those categories. The model illustrates the positive-branch reasoning of theorem 121.19 and the two append leaves compared by theorem 121.23. It does not type arbitrary Timpl clauses or implement the general restricted unifier. Therefore it does not prove lemma 121.13. It proves neither theorem 121.17 nor theorem 121.19, and it does not prove theorem 121.23. It does not establish proposition 121.21. It also supplies no theorem about the larger pattern languages of Agda or Equations. Those claims remain the card-specific mathematical arguments in the chapter; implementing the general compiler requires adding typed terms and dependent telescopes to the generic finite pattern syntax, carrying branch-local unifier certificates, and preserving these named negative oracles.