Compiling Dependent Pattern Matching

Definition 121.1 — The Timpl-clauses system card¶

The target Timpl is exactly the kernel frozen in convention 112.1; this chapter adds no target former or computation rule. The source restriction below permits splitting only the finite constructor families named by that card and permits recursion only through a displayed structural eliminator.

Timpl-clauses adds an untrusted, first-order clause layer with the following exact boundary.

1. A declaration has one Timpl argument telescope $$\mathrm{\Delta }=(x_1:A_1,\dots ,x_r:A_r)$$ and a result type $B$ in that telescope. The only inductive families that may be split are the finite constructor families declared in Timpl.

2. Patterns have the grammar $$p::=x\mid c(p_1,\dots ,p_k)\mid .t\mid !$$ Pattern variables are linear, and constructor patterns are first order. The term $t$ in $.t$ is a Timpl term in the full pattern-variable context of its row; it binds no variable. Pattern elaboration rejects a cyclic dependency among inaccessible terms.

3. Clause rows are ordered. At a compiler node, the first surviving row is the earliest row not deleted by an earlier constructor-branch filter. A blocking pattern in that row is an unresolved constructor or absurd pattern in a runtime column; variables and inaccessible terms do not block. The compiler scans the first surviving row from left to right and chooses the column of its first blocking pattern. An unresolved constructor or absurd pattern in an erased column instead produces a relevance error. When two rows overlap, the earlier row has priority.

4. Every binder retains its inherited runtime or erased annotation. Index constraints and inaccessible terms may mention erased variables, but the compiler never branches on their run-time values. A right side may use an erased pattern variable only where the Timpl relevance rules permit it.

5. Splitting $x:D(\overrightarrow{u})$ with $c:(\overrightarrow{y}:{\mathrm{\Delta }}_c)\to D({\overrightarrow{v}}_c)$ generates the homogeneous index constraint $(\overrightarrow{u};x){\equiv }_{\mathrm{\Xi };D}({\overrightarrow{v}}_c;c(\overrightarrow{y}))$, where $\mathrm{\Xi }$ is the index telescope of $D$. The compiler uses exactly the restricted unifier of definition 78.9. A positive result carries a dependency-preserving most general substitution, a negative result carries a conflict or cycle certificate, and a stuck result rejects the declaration. Such a substitution $\sigma :{\mathrm{\Theta }}^{\prime }\to \mathrm{\Theta }$ is dependency preserving when its solution and injectivity transitions are those of definition 78.9, up to the stable adjacent exchange of independent declarations needed to expose a solution. Every such exchange preserves the relative order of all declarations not exchanged, and every dependency of a declaration remains earlier than that declaration in ${\mathrm{\Theta }}^{\prime }$.

6. When a row becomes the first surviving candidate, each inaccessible term in that row is checked, never inspected at run time. It is accepted only when the accumulated substitution makes the pattern position judgmentally equal to that term. The compiler rejects a merely plausible but unforced inaccessible term. An absurd pattern in that row is accepted only when every constructor gives a negative unification certificate. Assertions in a shadowed later row are discarded by ordered priority; they are neither validated nor accepted as equations or impossibility evidence.

7. A right side is a Timpl term at the result type instantiated by its written row map, in a context containing the declared identifier at its complete iterated function type. A nonrecursive declaration requires that identifier not to occur in a right side. A single structurally recursive definition may contain it only as a saturated call. Its designated argument must be a direct recursive child made available by the split, and the branch path must carry the corresponding child certificate. Mutual recursion, nested recursion, guards, views, higher-order patterns, nonlinear patterns, and unification outside the restricted constructor fragment are not in Timpl-clauses.

8. The intermediate target is an ordered case tree. The kernel target is the Timpl term obtained from that tree using the declared eliminators. The observable operation is evaluation of the target term at closed argument tuples satisfying the relevance-indexed readiness judgment of definition 121.5.

The layer adds no conversion rule, universe rule, identity principle, coinductive object, or erasure rule. In particular, its compiler may not delete a reflexive equality constraint and does not assume K.

Definition 121.3 — Nondependent clause matrices¶

Fix finite constructor signatures, and let $$p::=\mathrm{\_}\mid c(p_1,\dots ,p_k)$$ be nondependent patterns. A simple clause matrix $P\Rightarrow \overrightarrow{a}$ is a finite ordered list of equal-width pattern rows, each carrying an action $a_i$. Matching a constructor-value tuple returns the action on its least matching row; $\mathrm{\_}$ matches every value.

With the selected column first, write $S_c(P\Rightarrow \overrightarrow{a})$ for constructor specialization. It processes rows in order:

1. replace a $c$-cell by its child patterns;

2. a cell headed by $d\ne c$ deletes the row; and

3. a wildcard is replaced by $k$ wildcards.

The other cells and the action are unchanged. The default matrix $D(P\Rightarrow \overrightarrow{a})$ retains, in order, just the rows whose selected cell is a wildcard and removes that cell. It is the branch action for a constructor whose head does not occur in the selected column. Selecting another column first means permuting that column to the front, applying these operations, and restoring the residual order.

Definition 121.5 — Readiness by relevance¶

Every Timpl binder has relevance $\varrho \in \{\mathsf{runtime},\mathsf{erased}\}$. The typed readiness judgment for a supplied argument is generated by $$\begin{array}{c}\frac{\cdot ⊢v:Av\text{ is a closed runtime value}}{\cdot ⊢v{\mathsf{ready}}_{\mathsf{runtime}}:A}\\ \frac{\cdot ⊢n:An\text{ is in closed normal form}}{\cdot ⊢n{\mathsf{ready}}_{\mathsf{erased}}:A}.\end{array}$$ Runtime values are lambdas, pairs of runtime values, and declared constructors whose runtime children are runtime values. The erased children stored under such a constructor need only be closed and well typed: they are not themselves tested by the readiness judgment, and no value grammar or evaluation-context position descends into them. By contrast, an erased argument supplied to a function binder satisfies the displayed erased rule and hence is a closed normal form before beta reduction. A tuple is ready when every component satisfies the rule indexed by its declared relevance. Only a runtime-relevant family component may be split, and then its weak-head form must be a declared constructor. Parameters such as $A:{\mathcal{U}}_i$ need not themselves have constructor form. For the vector constructor used below, the index argument of $\mathsf{vcons}$ is erased, while its element and tail arguments are runtime.

Definition 121.6 — Pattern matching and the source step¶

First define the binding judgment $\mathsf{binds}(p,a,\theta ;\mathcal{O})$. It collects the bindings and the finite set $\mathcal{O}$ of inaccessible obligations made by a pattern at a closed ready argument. Such an argument may be an erased type, lambda, or index. Constructor form is required only when the pattern at that exact position is a constructor pattern. Write ${\epsilon }_{\mathsf{sub}}$ for the empty pattern-variable substitution.

1. $\mathsf{binds}(x,a,[a/x];\varnothing )$ holds for any closed, well-typed argument $a$.

2. The judgment $$\mathsf{binds}(c(p_1,\dots ,p_k),c(v_1,\dots ,v_k),\theta ;\mathcal{O})$$ holds if the component binding judgments hold, their substitutions have disjoint domains whose union is $\theta$, and their obligation sets have union $\mathcal{O}$. Runtime children satisfy the runtime readiness rule; an erased constructor child is merely a closed well-typed payload and is not traversed by evaluation. Distinct constructor heads do not match.

3. $\mathsf{binds}(.t,a,{\epsilon }_{\mathsf{sub}};\{(a,t)\})$ holds for any closed well-typed argument $a$; an inaccessible pattern contributes no binding and records the value at its exact nested position.

4. $\mathsf{binds}(!,a,\theta ;\mathcal{O})$ never holds.

The relation $\mathsf{matches}(\overrightarrow{p},\overrightarrow{a},\theta )$ holds if the component binding substitutions have disjoint union $\theta$ and every recorded $(a,t)\in \mathcal{O}$ satisfies $a\equiv t[\theta ]$. Thus all pattern variables are collected before inaccessible terms are checked. Given ordered rows $f{\overrightarrow{p}}_i=e_i$, the source root step at $\overrightarrow{a}$ selects the least $i$ for which $\mathsf{matches}({\overrightarrow{p}}_i,\overrightarrow{a},\theta )$ holds, where $\theta :\cdot \to {\mathrm{\Theta }}_i$, and returns $e_i[{\theta }^f]$, leaving the explicitly typed recursive identifier $f:F_{\mathrm{\Delta }}$ unchanged. In the source dynamics, that remaining variable is interpreted by the declared head $f$. The tuple $\overrightarrow{a}$ is ready in the sense of definition 121.5. Consequently a runtime split-family position has constructor form when a constructor pattern inspects it, while an unrelated erased type or lambda in the same tuple need not have constructor form.

Definition 121.8 — Raw rows and their written maps¶

Let $f:F_{\mathrm{\Delta }}$. A nonabsurd raw row consists of a pattern-variable context ${\mathrm{\Theta }}_i$, a written pattern tuple ${\overrightarrow{p}}_i$, and its written row map ${\hat{\rho }}_i:{\mathrm{\Theta }}_i\to \mathrm{\Delta }$. This map reads a variable as that variable, a constructor pattern as the corresponding constructor term, and an inaccessible cell $.t$ as the term $t$ the programmer actually wrote. It does not assert that $t$ is forced. The row also carries a derivation in the explicit recursive-identifier context $$f:F_{\mathrm{\Delta }},{\mathrm{\Theta }}_i⊢e_i:B[{\hat{\rho }}_i].$$ Every occurrence of $f$ in $e_i$ is therefore typed at $F_{\mathrm{\Delta }}$. The source card further requires each such occurrence to be a saturated call whose designated argument is a certified direct child. Thus $e_i[{\sigma }^f]$ specializes the pattern variables and preserves the recursive identifier with its type. Formation of ${\hat{\rho }}_i$ checks each written dot term at its exact pattern position in ${\mathrm{\Theta }}_i$, after the stable reordering of independent declarations permitted by its acyclic dependency graph. It checks no forced-term equality. An absurd source row has the same well-scoped pattern data but no total written map at the absurd cell and no right side. It asserts that the cell has no reachable constructor. Every pattern variable occurs once.

During compilation, a surviving row carries its original number $i$, its residual patterns, a partial assignment of its pattern variables, and a finite ordered list $\mathcal{O}$ of typed residual obligations. New obligations are appended in left-to-right pattern order. An obligation is either an equality $u\equiv t:A$, or a suspended forced match $p\mathsf{forcedBy}u:A$. A selected dot creates an equality from the forced branch term $u$ and the written term $t$. A constructor pattern against a neutral forced image creates the second form instead of assuming that the pattern was accepted. Later matrix specialization substitutes through both forms. At a frontier map $\rho :\mathrm{\Theta }\to \mathrm{\Delta }$, the row-map invariant says that every well-typed match of all residual patterns by a substitution $\upsilon :\mathrm{\Omega }\to \mathrm{\Theta }$, with completed pattern-variable assignment $\tau :\mathrm{\Omega }\to {\mathrm{\Theta }}_i$, satisfies $$(\mathcal{O}[\upsilon ]\text{ holds})⟹{\hat{\rho }}_i\tau \equiv \rho \upsilon .$$ Here $\mathcal{O}[\upsilon ]$ holds when every equality is judgmental and every forced match succeeds structurally at the instantiated constructor head. The initial row state has no residual obligations. The implication follows componentwise from the definition of matching: constructor cells recurse, variables supply the assignment, and written dots supply exactly the equality premise that was not assumed when the raw row was formed.

A clause matrix at a frontier $\mathrm{\Theta }$ is a finite ordered list of such residual row states. Every state has one pattern for each declaration of $\mathrm{\Theta }$, in frontier order, followed by either its original right side checked under $f:F_{\mathrm{\Delta }}$, or an absurd marker.

Definition 121.9 — Typed case trees¶

A typed case tree for a frontier $\mathrm{\Theta }$, a frontier map $\rho :\mathrm{\Theta }\to \mathrm{\Delta }$, and result $B[\rho ]$ is generated by the following forms.

1. $\mathsf{leaf}(i,e)$ records the least surviving source row $i$ and a derivation $f:F_{\mathrm{\Delta }},\mathrm{\Theta }⊢e:B[\rho ]$. In a nonrecursive declaration, $f$ is not free in $e$.

2. $\mathsf{split}(x,\{c\mapsto ({\sigma }_c,{\mathcal{C}}_c)\})$ requires $x:D(\overrightarrow{u})$ in $\mathrm{\Theta }$. For every constructor $c:(\overrightarrow{y}:{\mathrm{\Delta }}_c)\to D({\overrightarrow{v}}_c)$, restricted unification of $(\overrightarrow{u};x){\equiv }_{\mathrm{\Xi };D}({\overrightarrow{v}}_c;c(\overrightarrow{y}))$ is either positive or negative. A positive result supplies the dependency-preserving substitution ${\sigma }_c$ and the subtree ${\mathcal{C}}_c$ at the specialized frontier. A negative result supplies a conflict or cycle certificate and has no subtree.

3. $\mathsf{absurd}(x,\{{\nu }_c\})$ records a negative certificate ${\nu }_c$ for every constructor of the family of $x$.

There is no node for a stuck unification problem. Reading the branches in constructor declaration order fixes a printed representation, while source row order fixes leaf priority.

Definition 121.10 — Valid Timpl-clauses tree¶

A typed case tree is valid when:

1. every split result is positive with its typed substitution, or negative with a conflict or cycle certificate; no stuck result occurs;

2. every specialized leaf has the checked result type at its frontier;

3. positive and negative alternatives together account for every declared constructor of the selected family, in declaration order; and

4. every occurrence of $f$ in a recursive leaf is a saturated call, and its designated argument uses the direct-child component supplied by the corresponding structural eliminator together with the branch-path child certificate.

These are the four premises of the indexed valid-tree interface used by theorem 78.19, instantiated here by ordered Timpl-clauses rows.

Definition 121.11 — Restricted-unifier schedule¶

This chapter gives the transition system of definition 78.9 one fixed schedule. Maintain an ordered equation list, always inspect its leftmost equation, and use deterministic weak-head forms. Tag a variable old when it was in the frontier before the selected constructor split and fresh when it belongs to that constructor’s telescope. For an equation between two distinct variables, list the two possible orientations in this order: eliminate a fresh variable before an old one, and otherwise eliminate the variable later in the ordered frontier telescope before the earlier one. An orientation is admissible only when its occurs check succeeds and the following stable move is legal. For a candidate $x:=t$, move $x$ rightward to immediately after the rightmost declaration free in $t$, if any such declaration is later than $x$, crossing declarations one at a time and preserving the order of every other declaration. The move is legal exactly when every crossed declaration is independent of $x$; it is then unique. Choose the first admissible orientation. Thus an injectivity equation $r=q$, with old $r$ and fresh $q$, has the canonical solution $q:=r$. For any other equation whose left side is not a variable and whose right side is, orient that right-hand variable to the left; then try the solution transition, the indexed self-unifiability check followed by injectivity, conflict, and cycle, in that order. If none applies, return the remaining ordered list as stuck. Equations exposed by an injectivity step replace the selected equation in constructor-telescope order. A solution in any equation uses the same stable move and is applied immediately to the telescope and the whole remaining list. An equation $x=x$ is not a distinct-variable equation and remains stuck unless a constructor rule changes its form; the schedule adds no reflexive deletion. The recursive index self-check uses this same schedule.

This policy makes every finite transition trace and every returned answer unique. It does not add reflexive deletion, and it is not a local proof that all weak-head computations or recursively requested index self-checks terminate. The totality result below therefore states that missing premise explicitly.

Definition 121.12 — The leftmost compiler¶

Let $M$ be an ordered matrix at a typed frontier. The partial function $\mathsf{compile}(M)$ has exactly the following result forms: Here $\pi$ is the constructor path, $\mathcal{E}$ is the ordered unsolved unification problem, and $\mathsf{stuckForce}(i,z,c,u)$ says that row $i$ demands head $c$ at the eliminated declaration $z$, but its typed forced image $u$ is neutral. The remaining three errors carry, respectively, the forced and written terms at their type, a reachable constructor and path, or the erased blocking declaration. There are no implicit abort outcomes. The function is defined as follows.

1. If $M$ is empty, return $\mathsf{uncovered}(\mathrm{\Theta },\pi )$ for frontier $\mathrm{\Theta }$ and constructor path $\pi$.

2. Apply ordered-row priority before inspecting later assertions. If the first surviving row carries a row-local reachable-absurd marker, take its leftmost marker and return $\mathsf{badAbsurd}(i,c,\pi )$ using the constructor recorded by the marker. If it carries a suspended forced match, retry the leftmost such task’s forced-image matcher after the accumulated substitution. A matching constructor consumes that task structurally; a different head deletes the row and restarts priority; a still-neutral image returns $\mathsf{stuckForce}(i,z,c,u)$.

   If the first row has no suspended forced match and no unresolved constructor or absurd pattern, turn each remaining dot cell into the equality between its image under the accumulated frontier substitution and its written term. Check only that row’s equality obligations, in list order, against the accumulated substitution. If they hold, complete its partial pattern-variable assignment to ${\tau }_{\ell }$, return $\mathsf{ok}(\mathsf{leaf}(i,e_i[{\tau }_{\ell }^f]))$, and discard every later row without validating any dot or absurd assertion in those rows. The factorization needed to type this leaf is lemma 121.15. If an obligation of the first row is not forced, return $\mathsf{badDot}(i,u,t,A)$.

   The returned tree carries no redundancy warning: Timpl-clauses accepts an unreachable later row silently because ordered priority never selects it.

   Otherwise scan the patterns of that first surviving row from left to right and select its leftmost blocking pattern, in the sense of definition 121.1. Encountering an unresolved constructor or absurd pattern in an erased column returns $\mathsf{badRelevance}(i,z)$.

3. If the leftmost blocking column contains $x:D(\overrightarrow{u})$, enumerate the constructors of $D$. For each constructor $c$, run restricted unification with the schedule of definition 121.11 on $(\overrightarrow{u};x){\equiv }_{\mathrm{\Xi };D}({\overrightarrow{v}}_c;c(\overrightarrow{y}))$. A stuck result returns $\mathsf{stuckEq}(\mathcal{E})$ with the unsolved equation list. A negative result is recorded in the node. For a positive result, specialize the selected pattern cell exactly once, in original row order, against $c(\overrightarrow{y})$, by the following four exhaustive clauses.

   1. A selected $c(p_1,\dots ,p_k)$ contributes its $k=|{\mathrm{\Delta }}_c|$ subpatterns; a selected $d(\overrightarrow{p})$ with $d\ne c$ deletes the row.

   2. A selected variable row is retained, records the binding $x:=c(\overrightarrow{y})$, and contributes the fresh variable-pattern tuple $\overrightarrow{y}$ of length $|{\mathrm{\Delta }}_c|$.

   3. A selected inaccessible row $.t$ is retained with the residual obligation $c(\overrightarrow{y})\equiv t$, after applying the positive substitution to both sides, and contributes the fresh variable-pattern tuple $\overrightarrow{y}$. Later specialization continues to substitute through the obligation. It is checked only if that row becomes the first nonblocking candidate; judgmental equality then discharges it, while failure reports the forced and written terms.

   4. A selected absurd row is retained with a row-local reachable-absurd marker in every positive constructor branch and contributes the fresh variable-pattern tuple $\overrightarrow{y}$. The recursive compiler invocation raises the marker only if that row becomes the least surviving candidate. A prior successful row instead discards it as redundant. The same priority convention applies to an invalid dot row.

   After row specialization, apply ${\sigma }_c$ to the frontier and row annotations. This frontier contains both surviving old declarations and the newly introduced constructor-telescope declarations. For every declaration $z$ eliminated by ${\sigma }_c$ after the selected cell has been expanded, run the recursive forced-image matcher ${\mathsf{force}}_{{\sigma }_c}(p_z,{\sigma }_c(z))$. A variable records its forced image; a dot records their residual judgmental equality; an absurd pattern records a reachable-absurd marker; and a constructor pattern requires the forced image to expose the same head and recursively matches its subpatterns against the forced constructor arguments. Different heads delete the row. A neutral forced image against a constructor pattern stores the typed suspended task $c(\overrightarrow{p})\mathsf{forcedBy}u$; it is retried, and can return $\mathsf{stuckForce}$, only if that row becomes the first surviving candidate. This matcher consumes the one pattern cell for $z$ and creates no frontier cell. In particular, the append successor branch uses $m:=\mathsf{suc}(k)$ to validate and remove $.\mathsf{suc}(k)$; it does not expose a second $k$-column.

   Thus a retained row replaces the selected pattern by exactly $|{\mathrm{\Delta }}_c|$ patterns and removes one pattern for every other declaration eliminated by ${\sigma }_c$. The specialized frontier performs the same replacement and removals, so row and frontier arities agree. Recursively compile the resulting specialized matrix. Negative constructor branches have no matrix and therefore perform none of these row actions.

4. If every constructor is negative, return $\mathsf{ok}(\mathsf{absurd}(x,\{{\nu }_c\}))$. Otherwise return $\mathsf{ok}$ of the split node after every positive branch has compiled. A positive branch with an empty specialized matrix returns $\mathsf{uncovered}$ with that constructor appended to the path. Any other diagnostic returned by a recursive branch propagates unchanged.