Elaborating Dependent Copattern Definitions

Definition 125.1 — The dependent-copattern elaboration card¶

The source Tcop-clause inherits Timpl-clauses patterns and the Timpl-co stream evaluation discipline. It adds finite coinductive records whose fields form a telescope $$\mathrm{\Phi }=({\pi }_1:A_1,\dots ,{\pi }_m:A_m),$$ where $A_j$ may mention the record parameters, indices, the self object, and earlier projections ${\pi }_1,\dots ,{\pi }_{j-1}$. A clause left side is an ordered sequence of input patterns followed by one coprojection path. The path follows the declared field telescope and binds no variable. One finite definition group is written in indexed-fiber form $$d:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)({\mathrm{\Delta }}_d(\overrightarrow{ı}))\to R\overrightarrow{p}\overrightarrow{ı}(d\in \mathcal{G}).$$ This fibered header makes the state tag of a recursive call well typed; a surface declaration whose result index is computed from unconstrained inputs must first be elaborated to this form with its index-equality witness. That reindexing elaboration is outside Tcop-clause. For a nonrecursive field, a right side contains no call to the copattern definition group. For a recursive field, the entire right side is one saturated call $d^{\prime }{@}_{{\mathrm{\Delta }}^{\prime }}\overrightarrow{b}$ to that group, and every argument $b_l$ is group-free Timpl. Nested group calls and group calls in computational fields are outside Tcop-clause.

The intermediate Tcop-tree has leaves, indexed input-split nodes, and coprojection nodes. A coprojection node for ${\pi }_j$ carries the earlier field terms needed to instantiate $A_j$. The target Tcop-core is Timpl-rec-core plus the primitive record corecursor Rec-Corec of definition 125.9 for exactly these finite telescopes, and nothing else. An elaborated mutual group may generate one nonrecursive indexed state family through Timpl-data; the generated family, constructors, and eliminator are signature declarations rather than a new Tcop-core rule. Clause priority is first match. Coverage is required at every reachable constructor and coprojection node. Higher-order patterns, projection overloading, hidden eta laws, effects, and arbitrary coinductive families are outside the card.

Definition 125.2 — Tcop-clause typing and source observation¶

For an accepted record declaration $R:({\mathrm{\Delta }}_p)({\mathrm{\Delta }}_i)\to {\mathcal{U}}_{\ell }$ with field telescope $\mathrm{\Phi }=({\pi }_1:A_1,\dots ,{\pi }_m:A_m)$, the declarations are checked from left to right under $z:R\overrightarrow{p}\overrightarrow{ı}$. The generated projection rule is $$\frac{\mathrm{\Gamma }⊢r:R\overrightarrow{p}\overrightarrow{ı}}{\mathrm{\Gamma }⊢{\pi }_j(r):A_j[r/z]}\mathrm{Coproj}-\mathrm{Ty}.$$ Occurrences of ${\pi }_l(r)$ for in the conclusion are typed by the earlier generated rules; a mention of ${\pi }_l$ with $l\ge j$ makes the field telescope ill formed.

A source definition has one checked fibered header from the finite group $\mathcal{G}$ and finite ordered rows $${\mathcal{M}}_r=({\overrightarrow{p}}_r;{\pi }_{j_r};e_r).$$ The pattern telescope ${\overrightarrow{p}}_r$ covers $(\overrightarrow{ı}:{\mathrm{\Delta }}_i)({\mathrm{\Delta }}_d(\overrightarrow{ı}))$ and is checked by the matrix rules of definition 121.1. Static pattern elaboration produces the symbolic, dependency-preserving row map ${\hat{\rho }}_r:{\mathrm{\Theta }}_r\to ((\overrightarrow{ı}:{\mathrm{\Delta }}_i)({\mathrm{\Delta }}_d(\overrightarrow{ı})))$. If $u_{r,l}$ is the stored symbolic term for the earlier field ${\pi }_l$ on the same path, the right side must satisfy the single finite judgment where ${\mathrm{\Theta }}_r$ is the refined branch context. This is a static row check; it neither chooses closed inputs nor runs the matcher. Acceptance also checks the right-side shape fixed in definition 125.1: a field outside $N$ is group-free, while a field in $N$ is exactly one saturated group call with group-free arguments.

Write $t{\Downarrow }_{\mathsf{T}}v$ for the closed group-free Timpl evaluation recalled in definition 124.2. A closed copattern right side has one of two weak-head results $w::=v\mid d^{\prime }\overrightarrow{a}$. The auxiliary judgment $e{\Downarrow }_{\mathsf{C}}w$ is generated by $$\frac{\begin{array}{c}e\text{ contains no call to the copattern group}\\ e{\Downarrow }_{\mathsf{T}}v\end{array}}{e{\Downarrow }_{\mathsf{C}}v}\mathrm{Copat}-\mathrm{Result}-\mathrm{Val}.$$ The recursive-result rule is $$\frac{\begin{array}{c}{d}^{\prime }:({\mathrm{\Delta }}^{\prime })\to R\overrightarrow{p}{\overrightarrow{ı}}^{\prime }\\ (b_l{\Downarrow }_{\mathsf{T}}{a}_l{)}_{l\in {\mathrm{\Delta }}^{\prime }}\end{array}}{d^{\prime }{@}_{{\mathrm{\Delta }}^{\prime }}\overrightarrow{b}{\Downarrow }_{\mathsf{C}}{d}^{\prime }{@}_{{\mathrm{\Delta }}^{\prime }}\overrightarrow{a}}\mathrm{Copat}-\mathrm{Result}-\mathrm{Rec}.$$ Thus a recursive-field call is a weak-head record result, but its arguments must first be closed typed Timpl normal forms. No rule unfolds that record call. Source field observation is defined only for a closed tuple $\overrightarrow{a}$ that is ready for the indexed declaration telescope in the sense of definition 121.5. It reuses the relational matcher of definition 121.6; in particular, no new partial function named “match” is assumed. The root rule is Thus priority is least matching row for the demanded field, not least row in a different field. Finite paths have grammar $o::={\pi }_j\mid {\pi }_j\cdot o$. A one-field path uses Copat-Row; path extension uses $$\frac{\begin{array}{c}j\in N\\ s{\Downarrow }_{{\pi }_j}{s}^{\prime }\\ s^{\prime }{\Downarrow }_{o}v\end{array}}{s{\Downarrow }_{{\pi }_j\cdot o}v}\mathrm{Copat}-\mathrm{Path}-\mathrm{Step}.$$ The first premise restricts extension to the declared recursive set $N$. A nonrecursive field may itself have an unrelated record type, but such a field ends a path in this card; admitting observations through that record would require a second record signature and translation case.

Definition 125.3 — Tcop-tree syntax and execution¶

The intermediate syntax is A leaf stores its source row, typed branch substitution, checked right side, and its group-free or saturated-recursive shape certificate. A split node stores the indexed motive and branch substitutions generated by definition 121.1. A fields node stores the complete ordered frontier; its $j$-th child is checked at . These requirements define the judgment $\mathrm{\Theta }⊢Q:\mathrm{\Phi }$.

Execution is defined only for closed ready input tuples. It first selects the demanded field, then follows input splits, and finally evaluates the leaf: Input splitting uses $$\frac{\begin{array}{c}{a}_x{\Downarrow }_{\mathsf{T}}{c}_k(\overrightarrow{v})\\ Q_k[\overrightarrow{v}/{\overrightarrow{y}}_k]\Downarrow w\end{array}}{\mathsf{split}(x;\{c_l({\overrightarrow{y}}_l)\Rightarrow Q_l{\}}_l)[\overrightarrow{a}]\Downarrow w}\mathrm{Tree}-\mathrm{Split}.$$ Finally, leaf execution is $$\frac{e\sigma {\Downarrow }_{\mathsf{C}}w}{\mathsf{leaf}(r,\sigma ,e)\Downarrow w}\mathrm{Tree}-\mathrm{Leaf}.$$ For an accepted mutual group, write $Q_d$ for the covered tree generated for declaration $d$. Longer paths pass from a recursive leaf to the tree of the declaration named by that leaf: $$\frac{\begin{array}{c}j\in N\\ Q_d(\overrightarrow{a}){\Downarrow }_{{\pi }_j}{d}^{\prime }\overrightarrow{b}\\ Q_{d^{\prime }}(\overrightarrow{b}){\Downarrow }_{o}v\end{array}}{Q_d(\overrightarrow{a}){\Downarrow }_{{\pi }_j\cdot o}v}\mathrm{Tree}-\mathrm{Path}-\mathrm{Step}.$$ There is no rule for a missing constructor or field branch; coverage excludes those states for an accepted tree.

Definition 125.4 — Typed copattern frontier¶

A typed copattern frontier is a telescope $$\mathrm{\Theta }\mid z:R\overrightarrow{p}\overrightarrow{i}\mid {\pi }_1(z)=u_1,\dots ,{\pi }_{j-1}(z)=u_{j-1}⊢{\pi }_j(z):A_j[\overrightarrow{u}/\overrightarrow{\pi }].$$ The equations on the left are typed substitution data, not kernel equality reflection. The compiler realizes them by extending the branch substitution with the earlier field terms. A leaf at field ${\pi }_j$ must synthesize a right side at exactly $A_j[\overrightarrow{u}/\overrightarrow{\pi }]$.

Definition 125.5 — Copattern splitting¶

The clauses-to-tree judgment $$\mathrm{\Theta }\mid \mathcal{M}{⟹}_{\mathsf{ct}}Q:(\mathrm{\Phi },j)$$ uses the first blocking item of the first surviving row.

1. An input constructor pattern creates the indexed split and transports the whole frontier by the restricted substitution of definition 78.9.

2. A coprojection ${\pi }_j$ creates a field node only when every earlier field on that record path has already produced a term. It extends the frontier by ${\pi }_j(z)=u_j$ before compiling later fields.

3. A variable pattern extends the row map. An inaccessible pattern checks against the accumulated substitution and introduces no run-time branch.

4. A leaf checks the right side against the instantiated field type and retains the first surviving source row number.

Failure reports the blocking row, input or field path, expected type, and unresolved index or missing earlier projection.

Definition 125.9 — The Tcop-core record corecursor¶

Let $R:({\mathrm{\Delta }}_p)({\mathrm{\Delta }}_i)\to {\mathcal{U}}_{\ell }$ be a card record with field telescope $\mathrm{\Phi }=({\pi }_1:A_1,\dots ,{\pi }_m:A_m)$. Let $N\subseteq \{1,\dots ,m\}$ collect the fields whose type is a recursive occurrence $R\overrightarrow{p}{\overrightarrow{ı}}_j$ with ${\overrightarrow{ı}}_j$ a term over ${\mathrm{\Delta }}_p,{\mathrm{\Delta }}_i$; no other occurrence of $R$ is permitted in $\mathrm{\Phi }$. Fix a state family $S:({\mathrm{\Delta }}_i)\to {\mathcal{U}}_k$. In a provisional signature, declare the method-independent constant $${\mathsf{corec}}_R:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(s:S\overrightarrow{ı})\to R\overrightarrow{p}\overrightarrow{ı}.$$ The provisional signature is local to the rule check and is committed only after every method below has checked. Earlier results are not represented by arbitrary binders. Instead, after methods $h_1,\dots ,h_{j-1}$ have checked, define their actual outputs and decoded fields in the context $(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(s:S\overrightarrow{ı})$ by Abbreviate $z_s:={\mathsf{corec}}_R\overrightarrow{ı}s$. The output type of the next method uses the substitution Its output type is Thus a later field sees the actual output of each earlier method. A recursive output is decoded to the record generated from its state before substitution.

The sequential method judgment is generated by $$\frac{\phantom{X}}{{\mathrm{\Sigma }}^{+}⊢{\mathsf{methods}}_S():{\mathrm{\Phi }}_{\le 0}}\mathrm{Corec}-\mathrm{Meth}-\mathrm{Nil}.$$ The extension rule is The second premise is checked with the previously checked method terms substituted literally into its codomain. Their ordinary beta and definition rules are available; no coprojection equation is available during this check. The Rec-Corec transaction first declares the displayed corecursor provisionally, then checks this finite judgment, and only then commits the constant and the following $m$ computation rules together: Only a state, never a record, is returned by a recursive method: that is what makes the rule primitive. The decoded actual output ${\overline{v}}_l$, rather than a state or an unconstrained variable, is substituted into later field types. Tcop-core adds Rec-Corec for the finite record telescopes of definition 125.1 and nothing else.

Writing ${\mathrm{\Sigma }}^{+}$ for the provisional signature and $E_j(\overrightarrow{ı},s)$ for the corresponding displayed coprojection equation, the transaction is the signature rule $$\frac{\begin{array}{c}\mathrm{\Sigma }⊢R\mathsf{card}\mathsf{record}:\mathrm{\Phi }\mathrm{\Sigma }⊢S:({\mathrm{\Delta }}_i)\to {\mathcal{U}}_k\\ {\mathrm{\Sigma }}^{+}=\mathrm{\Sigma },{\mathsf{corec}}_R:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(s:S\overrightarrow{ı})\to R\overrightarrow{p}\overrightarrow{ı}\\ {\mathrm{\Sigma }}^{+}⊢{\mathsf{methods}}_S(h_1,\dots ,h_m):\mathrm{\Phi }\end{array}}{\mathrm{\Sigma },{\mathsf{corec}}_R,(E_j(\overrightarrow{ı},s){)}_{1\le j\le m}\mathsf{signature}}\mathrm{Rec}-\mathrm{Corec}.$$ All premises are checked before the conclusion extends $\mathrm{\Sigma }$; failure of one method therefore commits neither the constant nor any equation.

The occurrences of ${\mathsf{corec}}_R$ in ${\overline{v}}_l$ refer to the provisional constant introduced at stage one. Its type is method-independent, which makes the later stages well founded. Each such occurrence only reconstructs an earlier recursive projection from a state; no method returns an arbitrary $R$-value. A target that forbade the generated constant from method types would have to impose the stricter boundary that no later field depends on an earlier recursive projection. Tcop-core chooses the displayed simultaneous dependent-corecursor rule instead.

Definition 125.10 — Generated copattern state block¶

For a finite accepted group $\mathcal{G}$, set $$k_{\mathcal{G}}:=max(\mathsf{lev}({\mathrm{\Delta }}_i),\underset{d\in \mathcal{G}}{max}\mathsf{lev}({\mathrm{\Delta }}_d(\overrightarrow{ı}))),$$ using the telescope-level function of definition 122.13. The generated block is $${\mathsf{State}}_{\mathcal{G}}:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)\to {\mathcal{U}}_{k_{\mathcal{G}}},{\mathsf{in}}_d:(\overrightarrow{ı}:{\mathrm{\Delta }}_i)(\overrightarrow{a}:{\mathrm{\Delta }}_d(\overrightarrow{ı}))\to {\mathsf{State}}_{\mathcal{G}}(\overrightarrow{ı}).$$ The maximum is formed after the Timpl level solver has accepted every input telescope; a stuck or inconsistent maximum rejects the translation.

Definition 125.12 — Tree-to-core translation¶

Write $\Vert Q\Vert$ for the following translation.

1. A nonrecursive leaf becomes its checked group-free Timpl term. A recursive leaf is handled by item 4; no other leaf contains a group call.

2. An input-split node becomes the corresponding generated inductive eliminator. Its motive is the result field type transported by the node’s frontier substitution.

3. A complete sequence of coprojection nodes becomes the sequential method tuple $(h_j{)}_j$ of one Rec-Corec instance, using the generated state block of definition 125.10. Its formation is lemma 125.11, and its constructor ${\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a})$ records both the declaration tag and its fiber input. The method for ${\pi }_j$ is checked after the methods ${\pi }_1,\dots ,{\pi }_{j-1}$, and its type and body substitute their actual decoded outputs ${\overline{v}}_1,\dots ,{\overline{v}}_{j-1}$, and substitute ${\mathsf{corec}}_R\overrightarrow{ı}s$ for the source self object $z$. Thus a source occurrence of an earlier recursive projection becomes the guarded term ${\mathsf{corec}}_R{\overrightarrow{ı}}_l(h_l\overrightarrow{ı}s)$, not the state $h_l\overrightarrow{ı}s$. The compiled declaration itself is $$\Vert Q_d\Vert :=\lambda \overrightarrow{ı}.\lambda \overrightarrow{a}.{\mathsf{corec}}_R\overrightarrow{ı}({\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a})).$$ Field selection therefore precedes every translated input split: the $j$-th method contains the input-split tree compiled from the $j$-th child of the fields node.

4. A recursive leaf for the checked call $d^{\prime }{@}_{{\mathrm{\Delta }}_{d^{\prime }}({\overrightarrow{ı}}_j)}\overrightarrow{b}$, whose field lies in $N$, becomes the tagged state $${\mathsf{in}}_{d^{\prime }}({\overrightarrow{ı}}_j,\Vert \overrightarrow{b}\Vert ):{\mathsf{State}}_{\mathcal{G}}({\overrightarrow{ı}}_j).$$ Its group-free arguments are translated componentwise. The leaf does not call the method $h_j$ being defined and never returns a record of $R$.

Definition 125.15 — Compiled application preparation¶

A compiled declaration applied to closed inputs may still have outer lambda redexes before its primitive corecursor is visible. Write $$q{⟹}_{\mathsf{in}}c$$ when a nonempty deterministic sequence contracts exactly the outer beta-redexes of $\Vert Q_d\Vert \overrightarrow{ı}\overrightarrow{a}$, from left to right, and stops at $$c={\mathsf{corec}}_R\overrightarrow{ı}({\mathsf{in}}_d(\overrightarrow{ı},\overrightarrow{a})).$$ The sequence does not contract a Rec-Corec projection, enter a method body, evaluate a state field, or use a generated Block-comp equation. Translated input splits occur inside the demanded field method and are therefore not preparation steps.

Definition 125.17 — Tcop-core observation¶

The target observation relation is distinct from source ${\Downarrow }_o$. Its root-bridge rule is $$\frac{\begin{array}{c}q{⟹}_{\mathsf{in}}c\\ c{{\Downarrow }_{\mathsf{CC}}}_{o}v\end{array}}{q{{\Downarrow }_{\mathsf{CC}}}_{o}v}\mathrm{Core}-\mathrm{Prepare}.$$ For a closed generated object $c={\mathsf{corec}}_R\overrightarrow{ı}s$, a nonrecursive field uses $$\frac{\begin{array}{c}j\notin N\\ {\pi }_j(c){⇝}_{0}e\\ e{\Downarrow }_{\mathsf{T}}v\end{array}}{c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j}v}\mathrm{Core}-\mathrm{Field}-\mathrm{Val},$$ where the root contraction is the $j$-th committed Rec-Corec equation. A recursive field exposes the decoded next object: $$\frac{\begin{array}{c}j\in N\\ {\pi }_j(c){⇝}_0{\mathsf{corec}}_R{\overrightarrow{ı}}_j(h_j\overrightarrow{ı}s)\\ h_j\overrightarrow{ı}s{\Downarrow }_{\mathsf{T}}{s}^{\prime }\end{array}}{c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j}{\mathsf{corec}}_R{\overrightarrow{ı}}_j{s}^{\prime }}\mathrm{Core}-\mathrm{Field}-\mathrm{Rec}.$$ Longer observations are generated only through recursive fields: $$\frac{\begin{array}{c}j\in N\\ c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j}{c}^{\prime }\\ c^{\prime }{{\Downarrow }_{\mathsf{CC}}}_{o}v\end{array}}{c{{\Downarrow }_{\mathsf{CC}}}_{{\pi }_j\cdot o}v}\mathrm{Core}-\mathrm{Path}-\mathrm{Step}.$$ There is no target path rule through an unrelated record-valued field, matching the source restriction in definition 125.2.