uptsms.tex

% !TEX root = omar-thesis.tex
\chapter{Simple Pattern TLMs (spTLMs)}\label{chap:uptsms}
In Chapter \ref{chap:uetsms}, our interest was in situations where the programmer needed to \emph{construct} (a.k.a. \emph{introduce}) a value. In this chapter, we consider situations where the programmer needs to \emph{deconstruct} (a.k.a. \emph{eliminate}) a value by pattern matching. For example, consider again the recursive labeled sum type \lstinline{rx} defined in Figure \ref{fig:datatype-rx}. We can pattern match over a value \lstinline{r} of type \lstinline{rx} using VerseML's \lstinline{match} construct as shown in the example below: 
\begin{lstlisting}
fun is_seq(r : rx) => 
  match r with 
    Seq(Str(name), Seq(Str "SSTR: ESTR", ssn)) => Some (name, ssn)
  | _ => None
  end
\end{lstlisting}
% \begin{lstlisting}
% fun is_dna_rx(r : rx) : boolean => 
%   match r with 
%   | Str "SSTRAESTR" => True
%   | Str "SSTRTESTR" => True
%   | Str "SSTRGESTR" => True
%   | Str "SSTRCESTR" => True
%   | Seq (r1, r2) => (is_dna_rx r1) andalso (is_dna_rx r2)
%   | Or  (r1, r2) => (is_dna_rx r1) andalso (is_dna_rx r2)
%   | Star(r') => is_dna_rx r'
%   | _ => False 
%   end
% \end{lstlisting}

Match expressions consist of a \emph{scrutinee}, here \li{r}, and a sequence of \emph{rules} separated by vertical bars, \li{|}, in the textual syntax. Each rule consists of a \emph{pattern} and an {expression} called the corresponding \emph{branch}, separated by a double arrow, \li{=>}, in the textual syntax. During evaluation, the value of the scrutinee is matched against each pattern sequentially. If a match occurs, evaluation proceeds along the corresponding branch. 

A variable can  appear at most once in a valid pattern. In the corresponding branch, the variable stands for the value it matched.  
For example, on Line 3 above, the pattern 
\begin{lstlisting}[numbers=none]
Seq(Str(name), Seq(Str "SSTR: ESTR", ssn))
\end{lstlisting}
matches values with the following structure: 
\begin{lstlisting}[numbers=none]
Seq(Str(#$e_1$#), Seq(Str "SSTR: ESTR", #$e_2$#))
\end{lstlisting}
where $e_1$ is a value of type \li{string} and $e_2$ is a value of type \li{rx}. The variables \li{name} and \li{ssn} stand for the values of $e_1$ and $e_2$, respectively, in the corresponding branch expression. 

On Line 4 above, the pattern \li{_} is the \emph{wildcard pattern} -- it matches any value, like the variable pattern, but binds no variables.

The behavior of the \li{match} construct when no pattern in the rule sequence matches a value is to raise an exception indicating \emph{match failure}. It is possible to statically determine whether match failure is possible (i.e. whether there exist values of the scrutinee that do not match any pattern in the rule sequence.) A rule sequence that cannot lead to match failure is said to be \emph{exhaustive}. Compilers warn the programmer when a rule sequence is non-exhaustive. In the example above, our use of the wildcard pattern ensures that match failure cannot occur. 

It is also possible to statically decide when a rule is \emph{redundant} relative to the preceding rules. For example, if we add  another rule at the end of the match expression above, it will be redundant because all values match the wildcard pattern. Again, compilers warn the programmer when a rule is redundant.

Nested pattern matching generalizes the projection and case analysis operators (i.e. the \emph{eliminators}) for products and sums (cf. $\miniVerseUE$ from the previous section.) 

In Sec. \ref{sec:syntax-examples-regexps}, we considered a hypothetical dialect of VerseML called $\mathcal{V}_\texttt{rx}$ with derived regex pattern forms. In this dialect, we can express the example above at lower syntactic cost using standard POSIX regex syntax extended with pattern splicing forms:

\begin{lstlisting}
fun f(r : rx) => 
  match r with 
    /SURL@EURLnameSURL: %EURLssn/ => Some (name, ssn)
  | _ => None
  end
\end{lstlisting}
\noindent
This dialect-oriented approach has problems, as  discussed in Chapter \ref{sec:problems-with-syntax-dialects}.

% seek language constructs that allow us to decrease the syntactic cost of expressing complex patterns to a similar degree.

Expression TLMs -- introduced in Chapter \ref{chap:uetsms} -- can decrease the syntactic cost of constructing a value, but expressions are syntactically and semantically distinct from patterns, so we cannot simply apply an expression TLM within a pattern.\footnote{The fact that certain concrete expression and pattern forms coincidentally overlap is immaterial to this fundamental distinction.} %For example, the expansion generated by an expression TLM might define or apply a function, but patterns do not contain functions or function applications. 
We need a new (albeit closely related) construct -- the \textbf{pattern TLM}. In this chapter, we consider only \textbf{simple pattern TLMs} (spTLMs), i.e. pattern TLMs that generate patterns that match values of a single specified type, like \li{rx}. In Chapter \ref{chap:ptsms}, we will consider both expression and pattern TLMs that specify type and module parameters (peTLMs and ppTLMs). 

The organization of the remainder of this chapter mirrors that of Chapter \ref{chap:uetsms}. We begin in Sec. \ref{sec:ptsms-by-example} with a ``tutorial-style'' introduction to spTLMs in VerseML. 
%In particular, we  discuss an spTLM for patterns matching values of type \li{rx}. 
Then, in Sec. \ref{sec:miniVerseUP}, we define an extension of $\miniVerseUE$ called $\miniVersePat$ that makes the intuitions developed in Sec. \ref{sec:ptsms-by-example} mathematically precise.

\section{Simple Pattern TLMs By Example}\label{sec:ptsms-by-example}

\subsection{Usage}\label{sec:ptsms-usage}
The VerseML function \li{f} defined at the beginning of this chapter can be expressed at lower syntactic cost by applying an spTLM named \li{#\dolla#rx} as follows:
\begin{lstlisting}
fun f(r : rx) => 
  match r with 
    $rx /SURL@EURLnameSURL: %EURLssn/ => Some (name, ssn)
  | _ => None
  end
\end{lstlisting}
Like expression TLMs, pattern TLMs are applied to \emph{generalized literal forms} (see Figure \ref{fig:literal-forms}.) During the  \emph{typed expansion} phase, the applied pattern TLM parses the body of the literal form to generate a \emph{proto-expansion}. The language validates the proto-expansion according to criteria that we will establish in Sec. \ref{sec:ptsms-validation}. If validation succeeds, the language generates the final expansion (or more concisely, simply the expansion) of the pattern. The expansion of the unexpanded pattern \li{#\dolla#rx /SURL@EURLnameSURL: %EURLssn/} 
from the example above is the following pattern:
\begin{lstlisting}[numbers=none]
Seq(Str(name), Seq(Str "SSTR: ESTR", ssn))
\end{lstlisting}

The checks for exhaustiveness and redundancy are performed post-expansion.

For convenience, the programmer can specify a TLM at the outset of a sequence of rules that is applied to every outermost generalized literal form. For example, the function \li{is_dna_rx} from Figure \ref{fig:is_dna_rx} and Figure \ref{fig:derived-pattern-syntax} can be expressed using the spTLM \li{#\dolla#rx} as follows:
\begin{lstlisting}[morekeywords={using}]
fun is_dna_rx(r : rx) : boolean => 
  match r using $rx with 
  | /SURLAEURL/ => True
  | /SURLTEURL/ => True
  | /SURLGEURL/ => True
  | /SURLCEURL/ => True
  | /SURL%(EURLr1SURL)%(EURLr2SURL)EURL/ => (is_dna_rx r1) andalso (is_dna_rx r2)
  | /SURL%(EURLr1SURL)|%(EURLr2SURL)EURL/ => (is_dna_rx r1) andalso (is_dna_rx r2)
  | /SURL%(EURLrSURL)*EURL/ => is_dna_rx r'
  | _ => False
  end
\end{lstlisting}

\subsection{Definition}\label{sec:ptsms-definition}
The definition of the pattern TLM \li{#\dolla#rx} shown being applied in the examples above takes the following form:
\begin{lstlisting}[numbers=none]
syntax $rx at rx for patterns by 
  static fn(b : body) : parse_result(proto_pat) =>
    (* regex pattern parser here *)
end 
\end{lstlisting}
This definition first names the pattern TLM \li{#\dolla#rx}. Pattern TLM names, like expression TLM names, must begin with the dollar sign (\li{#\dolla#}) to distinguish them from labels. Pattern TLM names and expression TLM names are tracked separately, i.e. an expression TLM and a pattern TLM can have the same name without conflict (as is the case here -- the expression TLM that was described in Sec. \ref{sec:uetsms-definition} is also named \li{#\dolla#rx}.) 

The \emph{sort qualifier} \li{for patterns} indicates that this is a pattern TLM definition, rather than an expression TLM definition (the sort qualifier \li{for expressions} can be written for expression TLMs, though when the sort qualifier is omitted this is the default.) Defining both an expression TLM and a pattern TLM with the same name at the same type is a common idiom, so VerseML defines a derived form for combining their definitions:
\begin{lstlisting}[numbers=none,morekeywords={andfor}]
syntax $rx at rx for expressions by
  static fn(body : body) : parse_result(proto_expr) => 
    (* regex expression parser here *)
for patterns by 
  static fn(body : body) : parse_result(proto_pat) => 
    (* regex pattern parser here *)
end
\end{lstlisting}

Pattern TLMs, like expression TLMs, must specify a static {parse function}. For pattern TLMs, the parse function must be of type \li{body -> parse_result(proto_pat)}, where \li{body} and \li{parse_result} are defined as in Figure \ref{fig:indexrange-and-parseresult}. 

The type \li{proto_pat}, defined in Figure \ref{fig:CEPat}, is analagous to the types \li{proto_expr} and \li{proto_typ} defined in Figure \ref{fig:candidate-exp-verseml}. This type classifies \emph{encodings of proto-patterns}. Every pattern form has a corresponding proto-pattern form, with the exception of variable patterns (for reasons explained in Sec. \ref{sec:ptsms-hygiene} below.) There is also an additional constructor, \li{SplicedP}, to allow a proto-pattern to refer indirectly to spliced patterns by their location within the literal body.

\begin{figure}
\begin{lstlisting}[numbers=none]
type proto_pat = rec(proto_pat => 
                 (* no variable pattern form *) 
                 Wild
               + (* ... *)
               + SplicedP of segment * proto_typ)
\end{lstlisting}
\caption[Abbreviated definition of \li{proto_pat} in VerseML]{Abbreviated definition of \li{proto_pat} in the VerseML prelude.}
\label{fig:CEPat}
\end{figure}

\subsection{Splicing}\label{sec:ptsms-splicing}
Spliced patterns are unexpanded patterns that appear directly within the literal body of another unexpanded pattern. For example, \li{name} and \li{ssn} appear within the unexpanded pattern \li{#\dolla#rx /SURL@EURLnameSURL: %EURLssn/}. 
When the parse function determines that a subsequence of the literal body should be taken as a spliced pattern (here, by recognizing the characters \li{@} or \li{%} followed by a variable or parenthesized pattern), 
it can refer to it within the proto-expansion that it computes using the \li{SplicedP} variant of the \li{proto_pat} type shown in Figure \ref{fig:CEPat}. This variant takes a value of type \li{segment} because proto-patterns refer to spliced patterns indirectly by their position within the literal body. This prevents pattern TLMs from ``forging'' a spliced pattern (i.e. claiming that some pattern is a spliced pattern, even though it does not appear in the literal body.) 
Like references to spliced expressions, each reference to a spliced pattern must also specify a type.

The proto-expansion generated by the pattern TLM \li{#\dolla#rx} for the example above, if written in a hypothetical concrete syntax where references to spliced patterns are written \li{spliced<startIdx; endIdx; ty>}, is:
\begin{lstlisting}[numbers=none]
Seq(Str(spliced<1; 4; string>), 
    Seq(Str "SSTR: ESTR", spliced<8; 10; rx>))
\end{lstlisting}
Here, \li{spliced<1; 4; string>} refers to the string subpattern \li{name} by location, and similarly, \li{spliced<8; 10; rx>} refers to the regex subpattern \li{ssn} by location.

\subsection{Segmentations}
The \emph{segmentation} of a proto-pattern is the finite set of references to spliced types or patterns. As with references to spliced expressions, the language checks that the references to spliced terms in a proto-expansion 1) are within bounds of the literal body; 2) are non-overlapping; and 3) operate at a consistent sort and type.

% An editor or pretty-printer can convey the summ information using color, as shown in the examples above.

\subsection{Proto-Expansion Validation}\label{sec:ptsms-validation}
After the pattern TLM generates a proto-expansion, the language must validate it to generate a final expansion. This also serves to maintain a reasonable type and binding discipline.

\subsubsection{Typing}
To maintain a reasonable type discipline, proto-expansion validation  checks:
\begin{enumerate}
\item that each spliced pattern matches values of the type indicated in the summary; and
\item that the final expansion matches values of the type specified in the type annotation on the pattern TLM definition, e.g. the type \li{rx} above.
\end{enumerate}

\subsubsection{Hidden Bindings}\label{sec:ptsms-hygiene}
%In order to check that the candidate expansion is well-typed, the language must parse, type and expand the spliced subpatterns that the candidate expansion refers to (by their position within the literal body, cf. above). 
To maintain a useful binding discipline, i.e. to allow programmers to reason about variable binding without examining TLM expansions directly, the validation process allows variable patterns to occur only in spliced patterns (just as variables bound at the use site can only appear in spliced expressions when using an expression TLM.) Indeed, there is no constructor for the type \li{proto_pat} corresponding to a variable pattern. This prohibition on ``hidden bindings'' is beneficial because the client can rely on the fact that no variables other than those that appear directly within the pattern at the application site are bound in the corresponding branch expression. This prohibition on hidden bindings is analagous to the prohibition on capture discussed in Sec. \ref{sec:uetsms-validation} (differing in that it is concerned with the bindings visible to the corresponding branch expression, rather than to spliced expressions.)

% \subsubsection{Context Independence}
% In VerseML, patterns are context-independent by construction (i.e. there is no way to refer to the surrounding bindings from within a pattern). It is only in the type annotations on spliced patterns that we need to enforce context independence.  (In languages that support, e.g., arbitrary expressions as \emph{guards} within patterns (e.g. OCaml \cite{ocaml-manual}), or in languages that support pattern synonyms, it would be necessary also to enforce context independence for these constructs as well.) 

\subsection{Final Expansion}\label{sec:ptsms-final-expansion}
If validation succeeds, the semantics generates the \emph{final expansion} of the pattern where the references to spliced patterns in the proto-pattern have been replaced by their respective final expansions. For example, the final expansion of \li{#\dolla#rx /SURL@EURLnameSURL: %EURLssn/} is:
\begin{lstlisting}[numbers=none]
Seq(Str(name), Seq(Str "SSTR: ESTR", ssn))
\end{lstlisting}

\section{\texorpdfstring{$\miniVersePat$}{miniVerseU}}\label{sec:miniVerseUP}
To make the intuitions developed in the previous section about pattern TLMs precise, we  now introduce $\miniVersePat$, a reduced dialect of VerseML with support for both seTLMs and spTLMs. Like $\miniVerseUE$, $\miniVersePat$ consists of an \emph{unexpanded language} (UL) defined by typed expansion to a standard \emph{expanded language} (XL). The full definition of $\miniVersePat$ is given in Appendix \ref{appendix:miniVerseSES} superimposed upon the definition of $\miniVerseUE$. We will focus on the rules specifically related to pattern matching and spTLMs below. 

Our formulation of pattern matching is adapted from  Harper's formulation in \emph{Practical Foundations for Programming Languages, First Edition} \cite{pfple1}.

\subsection{Syntax of the Expanded Language}\label{sec:UP-expanded-terms}\label{sec:inner-core-syntax-UP}
Figure \ref{sec:UP-expanded-terms} defines the syntax of the $\miniVersePat$ \emph{expanded language} (XL), which consists of \emph{types}, $\tau$, \emph{expanded expressions}, $e$, \emph{expanded rules}, $r$, and \emph{expanded patterns}, $p$. The $\miniVersePat$ XL differs from the $\miniVerseUE$ XL only by the addition of the pattern matching operator and related forms.\footnote{The projection and case analysis operators can be defined in terms of the match operator, but to simplify the appendix, we leave them in place.} %\footnote{The chapter on pattern matching has, of this writing, been removed from the draft second edition of \emph{PFPL}, but a copy of the first edition can be found online.}


The main syntactic feature of note is that the rule form places a pattern, $p$, in the binder position:
\[
\aematchrule{p}{e}
\]
This can be understood as binding all of the variables in $p$ for use within $e$. A small technical note: the ABT \emph{renaming} meta-operation (which underlies the notion of alpha-equivalence) requires that these variables appear as a sequence. Rather than redefining this metaoperation explicitly, we implicitly determine such a sequence by performing a depth-first traversal, with traversal of the labeled tuple pattern form, $\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}$, relying on some (arbitrary) total ordering on labels.

\begin{figure}
\[\begin{array}{lllllll}
\textbf{Sort} & & 
& \textbf{Operational Form} 
% & \textbf{Stylized Form} 
& \textbf{Description}\\
\mathsf{Typ} & \tau & ::= 
& \cdots
% & t 
& \text{(see Figure \ref{fig:U-expanded-terms})}\\
% &&& \aall{t}{\tau} & \forallt{t}{\tau} & \text{polymorphic}\\
% &&& \arec{t}{\tau} & \rect{t}{\t au} & \text{recursive}\\
% &&& \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}} & \prodt{\mapschema{\tau}{i}{\labelset}} & \text{labeled product}\\
% &&& \asum{\labelset}{\mapschema{\tau}{i}{\labelset}} & \sumt{\mapschema{\tau}{i}{\labelset}} & \text{labeled sum}\\
\mathsf{Exp} & e & ::= 
& \cdots 
% & x 
& \text{(see Figure \ref{fig:U-expanded-terms})}\\
% &&& \aelam{\tau}{x}{e} & \lam{x}{\tau}{e} & \text{abstraction}\\
% &&& \aeap{e}{e} & \ap{e}{e} & \text{application}\\
% &&& \aetlam{t}{e} & \Lam{t}{e} & \text{type abstraction}\\
% &&& \aetap{e}{\tau} & \App{e}{\tau} & \text{type application}\\
% &&& \aefold{e} & \fold{e} & \text{fold}\\
% &&& \aeunfold{e} & \unfold{e} & \text{unfold}\\
% &&& \aetpl{\labelset}{\mapschema{e}{i}{\labelset}} & \tpl{\mapschema{e}{i}{\labelset}} & \text{labeled tuple}\\
% &&& \aepr{\ell}{e} & \prj{e}{\ell} & \text{projection}\\
% &&& \aein{\ell}{e} & \inj{\ell}{e} & \text{injection}\\
% \LCC \lightgray & \lightgray & \lightgray 
%& \lightgray 
% & \lightgray & \lightgray \\
&&
& \aematchwith{n}{e}{\seqschemaX{r}}
% & \matchwith{e}{\seqschemaX{r}} 
& \text{match}\\
\mathsf{Rule} & r & ::= 
& \aematchrule{p}{e} 
%& \matchrule{p}{e} 
& \text{rule}\\
\mathsf{Pat} & p & ::= 
& x  
%& x 
& \text{variable pattern}\\
&&& \aewildp 
%& \wildp 
& \text{wildcard pattern}\\
&&& \aefoldp{p} 
%& \foldp{p} 
& \text{fold pattern}\\
&&& \aetplp{\labelset}{\mapschema{p}{i}{\labelset}} 
%& \tplp{\mapschema{p}{i}{\labelset}} 
& \text{labeled tuple pattern}\\
&&& \aeinjp{\ell}{p} 
%& \injp{\ell}{p} 
& \text{injection pattern} %\ECC
\end{array}\]
\caption{Syntax of the $\miniVersePat$ expanded language (XL)}
\label{fig:UP-expanded-terms}
\end{figure}


\subsection{Statics of the Expanded Language}\label{sec:inner-core-statics-UP}
The \emph{statics of the XL} is defined by judgements of the following form:
\[\begin{array}{ll}
\textbf{Judgement Form} & \textbf{Description}\\
\istypeU{\Delta}{\tau} & \text{$\tau$ is a well-formed type}\\
%\isctxU{\Delta}{\Gamma} & \text{$\Gamma$ is a well-formed typing context assuming $\Delta$}\\
\hastypeU{\Delta}{\Gamma}{e}{\tau} & \text{$e$ is assigned type $\tau$}\\
\ruleType{\Delta}{\Gamma}{r}{\tau}{\tau'} & \text{$r$ takes values of type $\tau$ to values of type $\tau'$}\\
\patType{\pctx}{p}{\tau} & \text{$p$ matches values of type $\tau$ and generates hypotheses $\pctx$} 
\end{array}\]

The types of $\miniVersePat$ are exactly those of $\miniVerseUE$, described in Sec. \ref{sec:miniVerseU}, so the \emph{type formation judgement}, $\istypeU{\Delta}{\tau}$, is inductively defined by Rules (\ref{rules:istypeU}) as before.

The \emph{typing judgement}, $\hastypeU{\Delta}{\Gamma}{e}{\tau}$, assigns types to expressions and is inductively defined by Rules (\ref{rules:hastypeU}), which consist of:
% \begin{subequations}\label{rules:hastypeUP}
% \refstepcounter{equation}%
\begin{itemize}
% \label{rule:hastypeUP-var}
% \refstepcounter{equation}\label{rule:hastypeUP-lam}
% \refstepcounter{equation}\label{rule:hastypeUP-ap}
% \refstepcounter{equation}\label{rule:hastypeUP-tlam}
% \refstepcounter{equation}\label{rule:hastypeUP-tap}
% \refstepcounter{equation}\label{rule:hastypeUP-fold}
% \refstepcounter{equation}\label{rule:hastypeUP-unfold}
% \refstepcounter{equation}\label{rule:hastypeUP-tpl}
% \refstepcounter{equation}\label{rule:hastypeUP-pr}
% \refstepcounter{equation}\label{rule:hastypeUP-in}
\item The typing rules of $\miniVerseUE$, i.e. Rules (\ref{rule:hastypeU-var}) through (\ref{rule:hastypeU-case}). %Note that we cannot defer directly to the typing rules from Sec. \ref{sec:miniVerseU} because $e$ has been redefined here.
\item The following rule for match expressions: 
\end{itemize}
\begin{equation*}\tag{\ref{rule:hastypeUP-match}}
\inferrule{
  \hastypeU{\Delta}{\Gamma}{e}{\tau}\\
  % \istypeU{\Delta}{\tau'}\\
  \{\ruleType{\Delta}{\Gamma}{r_i}{\tau}{\tau'}\}_{1 \leq i \leq n}\\
}{\hastypeU{\Delta}{\Gamma}{\aematchwith{n}{e}{\seqschemaX{r}}}{\tau'}}
\end{equation*}  
% \end{subequations}
The first premise of Rule (\ref{rule:hastypeUP-match}) assigns a type, $\tau$, to the scrutinee, $e$. The second premise then ensures that each rule $r_i$, for $1 \leq i \leq n$, takes values of type $\tau$ to values of the type of the match expression as a whole, $\tau'$, according to the \emph{rule typing judgement}, $\ruleType{\Delta}{\Gamma}{r}{\tau}{\tau'}$, which is defined mutually with Rules (\ref{rules:hastypeUP}) by the following rule:
\begin{equation*}\tag{\ref{rule:ruleType}}
\inferrule{
  \patType{\pctx'}{p}{\tau}\\
  \hastypeU{\Delta}{\Gcons{\Gamma}{\pctx'}}{e}{\tau'}
}{\ruleType{\Delta}{\Gamma}{\aematchrule{p}{e}}{\tau}{\tau'}}
\end{equation*}
The first premise invokes the \emph{pattern typing judgement}, $\patType{\pctx'}{p}{\tau}$, to check that the pattern, $p$, matches values of type $\tau$ (defined assuming $\Delta$), and to gather the typing hypotheses that the pattern generates in a {typing context}, $\pctx'$. (Algorithmically, the typing context is the ``output'' of the pattern typing judgement.) 
The second premise of Rule (\ref{rule:ruleType}) extends the incoming typing context, $\Gamma$, with the hypotheses generated by pattern typing, $\pctx$, and checks the branch expression, $e$, against the branch type, $\tau'$.%Pattern typing contexts are typing contexts. Algorithmically, however, one should consider the pattern typing context the ``output'' of the pattern typing judgement. 

The pattern typing judgement is inductively defined by Rules (\ref{rules:patType}).
Rule (\ref{rule:patType-var}) specifies that a variable pattern, $x$, matches values of any type, $\tau$, and generates the hypothesis that $x$ has type $\tau$:
\begin{equation*}\tag{\ref{rule:patType-var}}
\inferrule{ }{\patType{\Ghyp{x}{\tau}}{x}{\tau}}
\end{equation*}

Rule (\ref{rule:patType-wild}) specifies that a wildcard pattern also matches values of any type, $\tau$, but wildcard patterns generate no hypotheses:
\begin{equation*}\tag{\ref{rule:patType-wild}}
\inferrule{ }{\patType{\emptyset}{\aewildp}{\tau}}
\end{equation*}

Rule (\ref{rule:patType-fold}) specifies that a fold pattern, $\aefoldp{p}$, matches values of the recursive type $\arec{t}{\tau}$ if $p$ matches values of a single unrolling of the recursive type, $[\arec{t}{\tau}/t]\tau$:
\begin{equation*}\tag{\ref{rule:patType-fold}}
\inferrule{
  \patType{\pctx}{p}{[\arec{t}{\tau}/t]\tau}
}{
  \patType{\pctx}{\aefoldp{p}}{\arec{t}{\tau}}
}
\end{equation*}

Rule (\ref{rule:patType-tpl}) specifies that a labeled tuple pattern matches values of the labeled product type $\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}$. Labeled tuple patterns, $\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}$, specify a subpattern $p_i$ for each label $i \in \labelset$. The premise checks each subpattern $p_i$ against the corresponding type $\tau_i$, generating hypotheses $\pctx_i$. The conclusion of the rule gathers these hypotheses into a single pattern typing context, $\Gconsi{i \in \labelset}{\pctx_i}$:
\begin{equation*}\tag{\ref{rule:patType-tpl}}
\inferrule{
  \{\patType{\pctx_i}{p_i}{\tau_i}\}_{i \in \labelset}
}{
  \patType{\Gconsi{i \in \labelset}{\pctx_i}}{\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}}{\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}}
}
\end{equation*}
The definition of typing context extension, applied iteratively here,  implicitly requires that the pattern typing contexts $\pctx_i$ be mutually disjoint, i.e. \[\{\{\domof{\pctx_i} \cap \domof{\pctx_j} = \emptyset\}_{j \in \labelset \setminus i}\}_{i \in \labelset}\]

Finally, Rule (\ref{rule:patType-inj}) specifies that an injection pattern,  $\aeinjp{\ell}{p}$, matches values of labeled sum types of the form $\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}$, i.e. labeled sum types that define a case for the label $\ell$. The pattern $p$ must match value of type $\tau$ and generate hypotheses $\pctx$:
\begin{equation*}\tag{\ref{rule:patType-inj}}
\inferrule{
  \patType{\pctx}{p}{\tau}
}{
  \patType{\pctx}{\aeinjp{\ell}{p}}{\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}}
}
\end{equation*}


%These judgements obey standard lemmas, defined in Appendix \ref{appendix:SES-XL}: Weakening, Substitution, Decomposition and Regularity.





%\item The second premise of Rule (\ref{rule:ruleType}) ensures that pattern typing of $p$ has generated hypotheses for all of the variables that the branch expression, $e$, binds. This is merely a matter of ``metatheoretic bookkeeping''. In the stylized form for rules, $\matchrule{p}{e}$, the variables bound in $e$ are, implicitly, exactly those mentioned in p.% The bindings for $e$ would be extracted from the pattern implicitly. 

\subsection{Structural Dynamics}\label{sec:dynamics-UP}
The \emph{structural dynamics of }$\miniVersePat$ is defined as a transition system, and is organized around judgements of the following form:
\[\begin{array}{ll}
\textbf{Judgement Form} & \textbf{Description}\\
\stepsU{e}{e'} & \text{$e$ transitions to $e'$}\\
\isvalU{e} & \text{$e$ is a value}\\
\matchfail{e} & \text{$e$ raises match failure}
\end{array}\]
We also define auxiliary judgements for \emph{iterated transition}, $\multistepU{e}{e'}$, and \emph{evaluation}, $\evalU{e}{e'}$.

\begingroup
\def\thetheorem{\ref{defn:iterated-transition-UP}}
\begin{definition}[Iterated Transition] Iterated transition, $\multistepU{e}{e'}$, is the reflexive, transitive closure of the transition judgement, $\stepsU{e}{e'}$.\end{definition}
% \addtocounter{theorem}{-1}
\endgroup

\begingroup
\def\thetheorem{\ref{defn:evaluation-UP}}
\begin{definition}[Evaluation] $\evalU{e}{e'}$ iff $\multistepU{e}{e'}$ and $\isvalU{e'}$. \end{definition}
% \addtocounter{theorem}{-1}
\endgroup

As in Sec. \ref{sec:dynamics-U}, our subsequent developments do not make mention of particular rules in the dynamics, nor do they make mention of other judgements, not listed above, that are used only for defining the dynamics of the match operator, so we do not produce these details here. Instead, it suffices to state the following conditions.

The Canonical Forms condition, which characterizes well-typed values, is identical to the corresponding condition in the structural dynamics of $\miniVerseUE$, i.e. Condition \ref{condition:canonical-forms-UP}. 

The Preservation condition ensures that evaluation preserves typing, and is again identical to the corresponding condition in the structural dynamics of $\miniVerseUE$.
\begingroup
\def\thetheorem{\ref{condition:preservation-UP}}
\begin{condition}[Preservation] If $\hastypeUC{e}{\tau}$ and $\stepsU{e}{e'}$ then $\hastypeUC{e'}{\tau}$. \end{condition}
% \addtocounter{theorem}{-1}
\endgroup

The Progress condition ensures that evaluation of a well-typed expanded expression cannot ``get stuck''. We must consider the possibility of match failure in this condition.
\begingroup
\def\thetheorem{\ref{condition:progress-UP}}
\begin{condition}[Progress] If $\hastypeUC{e}{\tau}$ then either $\isvalU{e}$ or $\matchfail{e}$ or there exists an $e'$ such that $\stepsU{e}{e'}$. \end{condition}
% \addtocounter{theorem}{-1}
\endgroup

Together, these two conditions constitute the Type Safety Condition.
%\noindent
%Condition \ref{condition:preservation-UP} is identical to Condition \ref{condition:preservation-U}, while Condition \ref{condition:progress-UP} modifies Condition \ref{condition:progress-U} to allow for match failure. 

We do not define the semantics of exhaustiveness and redundancy checking here, because these can be checked post-expansion (but see \cite{pfple1} for a formal account.)


\subsection{Syntax of the Unexpanded Language}\label{sec:syntax-UP}
The syntax of the $\miniVersePat$ unexpanded language (UL) extends the syntax of the $\miniVerseUE$ unexpanded language as shown in Figure \ref{fig:UP-unexpanded-terms}.

\begin{figure}[h!]
\[\arraycolsep=4pt\begin{array}{lllllll}
\textbf{Sort} & & 
%& \textbf{Operational Form} 
& \textbf{Stylized Form} & \textbf{Description}\\
\mathsf{UTyp} & \utau & ::= 
% & ... 
& \cdots & \text{(see Figure \ref{fig:U-unexpanded-terms})}\\
\mathsf{UExp} & \ue & ::= 
%& \ux 
& \cdots 
& \text{(see Figure \ref{fig:U-unexpanded-terms})}\\
&&
%& \aumatchwith{n}{\utau}{\ue}{\seqschemaX{\urv}} 
& \matchwith{\ue}{\seqschemaX{\urv}} & \text{match}\\
% %\LCC &&& \gray & \gray & \gray \\
% &&
%& \audefuetsm{\utau}{e}{\tsmv}{\ue}
%& \texttt{syntax}~\tsmv~\texttt{at}~\utau~\texttt{for} & \text{seTLM definition}\\
% &&&                                    & \texttt{expressions}~\{e\}~\texttt{in}~\ue\\
% &&& \autsmap{b}{\tsmv} & \utsmap{\tsmv}{b} & \text{seTLM application}\\%\ECC
\LCC &&& \color{Yellow} & \color{Yellow}\\
&&
%& \audefuptsm{\utau}{e}{\tsmv}{\ue} 
& \usyntaxup{\tsmv}{\utau}{e}{\ue}
& \text{spTLM definition}\ECC\\
% &&&                                    & \texttt{patterns}~\{e\}~\texttt{in}~\ue\\\ECC
\mathsf{URule} & \urv & ::= 
%& \aumatchrule{\upv}{\ue} 
& \matchrule{\upv}{\ue} & \text{match rule}\\
\mathsf{UPat} & \upv & ::= 
%& \ux 
& \ux & \text{identifier pattern}\\
&&
%& \auwildp 
& \wildp & \text{wildcard pattern}\\
&&
%& \aufoldp{\upv} 
& \foldp{\upv} & \text{fold pattern}\\
&&
%& \autplp{\labelset}{\mapschema{\upv}{i}{\labelset}} 
& \tplp{\mapschema{\upv}{i}{\labelset}} & \text{labeled tuple pattern}\\
&&
%& \auinjp{\ell}{\upv} 
& \injp{\ell}{\upv} & \text{injection pattern}\\
\LCC &&& \color{Yellow} & \color{Yellow}\\
&&
%& \auapuptsm{b}{\tsmv} 
& \utsmap{\tsmv}{b} & \text{spTLM application}\ECC
\end{array}\]
\caption[Syntax of the $\miniVersePat$ unexpanded language]{Syntax of the $\miniVersePat$ unexpanded language}
\label{fig:UP-unexpanded-terms}
\end{figure}

As in $\miniVerseUE$, each expanded form has a corresponding unexpanded form. We refer to these as the \emph{common forms}. The correspondence is defined in Appendix \ref{appendix:SES-shared-forms}. There are two forms related specifically to spTLMs, highlighted in yellow above: the spTLM definition form and the spTLM application form.

In addition to the stylized syntax given in Figure \ref{fig:U-unexpanded-terms}, there is also a context-free textual syntax for the UL. Again, we need only posit the existence of partial metafunctions $\parseUTypF{b}$, $\parseUExpF{b}$ and $\parseUPatF{b}$ that go from character sequences, $b$, to unexpanded types, expressions and patterns, respectively. 
\begingroup
\def\thetheorem{\ref{condition:textual-representability-SES}}
\begin{condition}[Textual Representability] ~
\begin{enumerate}
\item For each $\utau$, there exists $b$ such that $\parseUTyp{b}{\utau}$. 
\item For each $\ue$, there exists $b$ such that $\parseUExp{b}{\ue}$.
\item For each $\upv$, there exists $b$ such that $\parseUPat{b}{\upv}$.
\end{enumerate}
\end{condition}
\endgroup

\subsection{Typed Expansion}\label{sec:typed-expansion-UP}
Unexpanded terms are checked and expanded simultaneously according to the \emph{typed expansion judgements}:

\vspace{10px}
\noindent$\arraycolsep=2pt\begin{array}{ll}
\textbf{Judgement Form} & \textbf{Description}\\
\expandsTU{\uDelta}{\utau}{\tau} & \text{$\utau$ has well-formed expansion $\tau$}\\
\expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\ue}{e}{\tau} & \text{$\ue$ has expansion $e$ of type $\tau$}\\
\ruleExpands{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\urv}{r}{\tau}{\tau'} & \text{$\urv$ has expansion $r$ taking values of type $\tau$ to values of type $\tau'$}\\
\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau} & \text{$\upv$ has expansion $p$ matching against $\tau$ generating hypotheses $\upctx$}
% & \text{hypotheses $\upctx$}\\
\end{array}$

\subsubsection{Type Expansion}
The \emph{type expansion judgement}, $\expandsTU{\uDelta}{\utau}{\tau}$, is inductively defined by Rules (\ref{rules:expandsTU}) as before.

\subsubsection{Typed Expression, Rule and Pattern Expansion}
%\emph{Unexpanded pattern typing contexts}, $\upctx$, are defined identically to unexpanded typing contexts (i.e. we only use a distinct metavariable to emphasize their distinct roles in the judgements above). % and the definition of seTLM definition contexts is reproduced below. \emph{spTLM contexts}, $\uPhi$, are defined in Sec. \ref{sec:uptsm-definition} below.

The \emph{typed expression expansion} judgement, $\expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\ue}{e}{\tau}$, and the \emph{typed rule expansion judgement}, $\ruleExpands{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\urv}{r}{\tau}{\tau'}$ are defined mutually inductively by Rules (\ref{rules:expandsU}) and Rule (\ref{rule:ruleExpands}). The \emph{typed pattern expansion judgement}, $\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}$, is inductively defined by Rules (\ref{rules:patExpands}).

Rules (\ref{rule:expandsU-var}) through (\ref{rule:expandsU-tsmap}) are adapted directly from $\miniVerseUE$, differing only in that the {spTLM context}, $\uPhi$, passes opaquely through them. 

There is one new common unexpanded expression form in $\miniVersePat$: the unexpanded match form. Rule (\ref{rule:expandsU-match}) governs this form:
\begin{equation*}\tag{\ref{rule:expandsU-match}}
\inferrule{
  % \uDelta = \uDD{\uD}{\Delta}\\\\
  \expandsUP{\uDelta}{\uGamma}{\uPhi}{\uPsi}{\ue}{e}{\tau}\\
  % \istypeU{\Delta}{\tau'}\\
  \{\ruleExpands{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\urv_i}{r_i}{\tau}{\tau'}\}_{1 \leq i \leq n}\\
}{
  \expandsUP
    {\uDelta}{\uGamma}{\uPsi}{\uPhi}
    {\matchwith
      {\ue}
      {\seqschemaX{\urv}}
    }{\aematchwith
      {n}
      % {\tau'}
      {e}
      {\seqschemaX{r}}
    }{\tau'}
}
\end{equation*}  

% We can express this scheme more precisely with the following rule transformation. For each rule in Rules (\ref{rules:hastypeUP}),
% \begin{mathpar}
% %\refstepcounter{equation}
% %\label{rule:expandsU-case}
% \inferrule{J_1\\ \cdots \\ J_k}{J}
% \end{mathpar}
% the corresponding typed expansion rule is 
% \begin{mathpar}
% \inferrule{
%   \Uof{J_1} \\
%   \cdots\\
%   \Uof{J_k}
% }{
%   \Uof{J}
% }
% \end{mathpar}
% where
% \[\begin{split}
% \Uof{\istypeU{\Delta}{\tau}} & = \expandsTU{\Uof{\Delta}}{\Uof{\tau}}{\tau} \\
% \Uof{\hastypeU{\Gamma}{\Delta}{e}{\tau}} & = \expandsUP{\Uof{\Gamma}}{\Uof{\Delta}}{\uPsi}{\uPhi}{\Uof{e}}{e}{\tau}\\
% \Uof{\ruleType{\Gamma}{\Delta}{r}{\tau}{\tau'}} & = \ruleExpands{\Uof{\Gamma}}{\Uof{\Delta}}{\uPsi}{\uPhi}{\Uof{r}}{r}{\tau}{\tau'}\\
% \Uof{\{J_i\}_{i \in \labelset}} & = \{\Uof{J_i}\}_{i \in \labelset}
% \end{split}\]
% and where $\Uof{\Delta}$, $\Uof{\Gamma}$ and $\Uof{\tau}$ are defined as in Sec. \ref{sec:typed-expansion-U} and:
% \begin{itemize}
% \item $\Uof{e}$ is defined as follows
% \begin{itemize}
% \item When $e$ is of definite form, $\Uof{e}$ is defined as in Sec. \ref{sec:syntax-UP}. 
% \item When $e$ is of indefinite form, $\Uof{e}$ is a uniquely corresponding metavariable of sort $\mathsf{UExp}$ also of indefinite form. For example, $\Uof{e_1}=\ue_1$ and $\Uof{e_2}=\ue_2$.
% \end{itemize}
% \item $\Uof{r}$ is defined as follows:
% \begin{itemize}
% \item When $r$ is of definite form, $\Uof{r}$ is defined as in Sec. \ref{sec:syntax-UP}.
% \item When $e$ is of indefinite form, $\Uof{r}$ is a uniquely corresponding metavariable of sort $\mathsf{URule}$ also of indefinite form.
% \end{itemize}
% \end{itemize}

% It is instructive to use this rule transformation to generate Rules (\ref{rule:expandsUP-var}) through (\ref{rule:expandsUP-tap}) and Rule (\ref{rule:expandsUP-match}) above. We omit the remaining rules generated by this transformation, i.e. Rules (\ref*{rule:expandsUP-tlam}) through (\ref*{rule:expandsUP-in}). 

The typed rule expansion judgement is defined by Rule (\ref{rule:ruleExpands}), below:
\begin{equation*}\tag{\ref{rule:ruleExpands}}
\inferrule{
  \patExpands{\uAS{\uG'}{\pctx'}}{\uPhi}{\upv}{p}{\tau}\\
  \expandsUP{\uDelta}{\uGG{\uGcons{\uG}{\uG'}}{\Gcons{\Gamma}{\pctx'}}}{\uPsi}{\uPhi}{\ue}{e}{\tau'} 
}{
  \ruleExpands{\uDelta}{\uGG{\uG}{\Gamma}}{\uPsi}{\uPhi}{\aumatchrule{\upv}{\ue}}{\aematchrule{p}{e}}{\tau}{\tau'}
}
\end{equation*}
Because unexpanded terms mention only expression identifiers, which are given meaning by expansion to variables, the pattern typing rules must generate both an identifier expansion context, $\uG'$, and a typing context, $\pctx'$. %The second and third premises check that the domains of $\uG'$ and $\pctx$ correspond to the bindings in the unexpanded and expanded rule, respectively, with the second and third premise. 
In the second premise of the rule above, we update the ``incoming'' identifier expansion context, $\uG$, with the new identifier expansions, $\uG'$, and correspondingly, extend the ``incoming'' typing context, $\Gamma$, with the new typing hypotheses, $\pctx'$. 

Rules (\ref{rule:patExpands-var}) through (\ref{rule:patExpands-in}), reproduced below, define typed expansion  of unexpanded patterns of common form.
\begin{equation*}\tag{\ref{rule:patExpands-var}}
{\inferrule{ }{
  \patExpands{\uGG{\vExpands{\ux}{x}}{\Ghyp{x}{\tau}}}{\uPhi}{\ux}{x}{\tau}
}}
\end{equation*}
\begin{equation*}\tag{\ref{rule:patExpands-wild}}
{\inferrule{ }{
  \patExpands{\uGG{\emptyset}{\emptyset}}{\uPhi}{\wildp}{\aewildp}{\tau}
}}
\end{equation*}
\begin{equation*}\tag{\ref{rule:patExpands-fold}}
{\inferrule{ 
  \patExpands{\upctx}{\uPhi}{\upv}{p}{[\arec{t}{\tau}/t]\tau}
}{
  \patExpands{\upctx}{\uPhi}{\foldp{\upv}}{\aefoldp{p}}{\arec{t}{\tau}}
}}
\end{equation*}
\begin{equation*}\tag{\ref{rule:patExpands-tpl}}
{
  \inferrule{
    \tau = \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}\\\\
    \{\patExpands{{\upctx_i}}{\uPhi}{\upv_i}{p_i}{\tau_i}\}_{i \in \labelset}
  }{
    % \left(\shortstack{
    %   $\Delta \vdash_{\uPhi} \tplp{\mapschema{\upv}{i}{\labelset}}$\\
    %   $\leadsto$\\
    %   $\aetplp{\labelset}{\mapschema{p}{i}{\labelset}} : \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}$\vspace{-1.2em}}\right)
    \patExpands{\GIconsi{i \in \labelset}{\upctx_i}}{\uPhi}{\tplp{\mapschema{\upv}{i}{\labelset}}}{\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}}{\tau}
  }
}
% \graybox{\inferrule{
%   \{\patExpands{{\upctx_i}}{\uPhi}{\upv_i}{p_i}{\tau_i}\}_{i \in \labelset}\\
% }{
%   % \patExpands{\Gconsi{i \in \labelset}{\pctx_i}}{\Phi}{
%   %   \autplp{\labelset}{\mapschema{\upv}{i}{\labelset}}
%   % }{
%   %   \aetplp{\labelset}{\mapschema{p}{i}{\labelset}}
%   % }{
%   %   \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}
%   % } %{\autplp{\labelset}{\mapschema{\upv}{i}{\labelset}}}{\aetplp{\labelset}{\mapschema}{p}{i}{\labelset}}{...}
%   \left(\shortstack{$\Delta \vdash_{\uPhi} \autplp{\labelset}{\mapschema{\upv}{i}{\labelset}}$\\$\leadsto$\\$\aetplp{\labelset}{\mapschema{p}{i}{\labelset}} : \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}} \dashV \Gconsi{i \in \labelset}{\upctx_i}$\vspace{-1.2em}}\right)
% }}
\end{equation*}
\begin{equation*}\tag{\ref{rule:patExpands-in}}
{\inferrule{
  \patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}
}{
  \patExpands{\upctx}{\uPhi}{\injp{\ell}{\upv}}{\aeinjp{\ell}{p}}{\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}}
}}
\end{equation*}
Again, the unexpanded and expanded pattern forms in the conclusion correspond and the premises correspond to those of the corresponding pattern typing rule, i.e. Rules (\ref{rule:patType-var}) through (\ref{rule:patType-inj}), respectively. The spTLM context, $\uPhi$, passes through these rules opaquely. In Rule (\ref{rule:patExpands-tpl}), the conclusion of the rule collects all of the identifier expansions and hypotheses generated by the subpatterns. We define $\upctx_i$ as shorthand for $\uGG{\uG_i}{\pctx_i}$ and $\GIconsi{i \in \labelset}{\upctx_i}$ as shorthand for \[\uGG{\GIconsi{i \in \labelset}{\uG_i}}{\Gconsi{i \in \labelset}{\pctx_i}}\] By the definition of iterated extension of finite functions, we implicitly have that no identifiers or variables can be duplicated, i.e. that 
\[\{\{\domof{\uG_i} \cap \domof{\uG_j} = \emptyset\}_{j \in \labelset \setminus i}\}_{i \in \labelset}\]
and
\[\{\{\domof{\pctx_i} \cap \domof{\pctx_j} = \emptyset\}_{j \in \labelset \setminus i}\}_{i \in \labelset}\]
%By instead defining these rules by the rule transformation just described, we avoid having to list a number of rules that are individually uninteresting. Moreover, this approach makes our exposition somewhat robust to changes to the inner core (though not to changes to the judgement forms in the statics of the inner core).

\paragraph{spTLM Definition and Application}
Two rules remain: Rules (\ref{rule:expandsU-defuptsm}) and (\ref{rule:patExpands-apuptsm}), which define spTLM definition and application, respectively. These rules are  defined in the next two subsections, respectively.





\subsection{spTLM Definition}\label{sec:uptsm-definition}

The spTLM definition form is \[\usyntaxup{\tsmv}{\utau}{\eparse}{\ue}\] 
%The operational form corresponding to this stylized form is \[\audefuetsm{\utau}{\eparse}{\tsmv}{\ue}\]
An unexpanded expression of this form defines a {spTLM} identified as $\tsmv$ with \emph{unexpanded type annotation} $\utau$ and \emph{parse function} $\eparse$ for use within $\ue$. 

%The parse function is an expanded expression because parse functions are applied statically (i.e. during typed expansion of $\ue$), as we will discuss when describing seTLM application below, and evaluation is defined only for closed expanded expressions. This construction simplifies our exposition, though it is not entirely practical because it provides no way for TLM providers to share values between parse functions, nor any way to use TLMs when defining other TLMs. We discuss enriching the language to eliminate these limitations in Sec. \ref{sec:uetsms-static-language}, but it is pedagogically simpler to leave the necessary machinery out of our calculus for now.%$\miniVerseUE$.

Rule (\ref{rule:expandsU-defuptsm}) defines typed expansion of spTLM definitions:
% \begin{equation}\label{rule:expandsU-syntax}
% \inferrule{
%   \istypeU{\Delta}{\tau}\\
%   \expandsU{\emptyset}{\emptyset}{\emptyset}{\ueparse}{\eparse}{\aparr{\tBody}{\tParseResultExp}}\\\\
%   \expandsU{\Delta}{\Gamma}{\uPsi, \xuetsmbnd{\tsmv}{\tau}{\eparse}}{\ue}{e}{\tau'}
% }{
%   \expandsUX{\audefuetsm{\tau}{\ueparse}{\tsmv}{\ue}}{e}{\tau'}
% }
% \end{equation}
\begin{equation*}\tag{\ref{rule:expandsU-defuptsm}}
\inferrule{
  \expandsTU{\uDelta}{\utau}{\tau}\\
  \hastypeU{\emptyset}{\emptyset}{\eparse}{\aparr{\tBody}{\tParseResultPat}}\\\\
  \evalU{\eparse}{\eparse'}\\
  \expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi, \uPhyp{\tsmv}{a}{\tau}{\eparse'}}{\ue}{e}{\tau'}
}{
  \expandsUPX{\usyntaxup{\tsmv}{\utau}{\eparse}{\ue}}{e}{\tau'}
}
\end{equation*}
This rule is similar to Rule (\ref{rule:expandsU-syntax}), which governs seTLM definitions. The premises of this rule can be understood as follows, in order:
\begin{enumerate}
\item The first premise expands the unexpanded type annotation.

\item The second premise checks that the parse function, $\eparse$, is a closed expanded function of the following type: \[\aparr{\tBody}{\tParseResultExp}\] %to generate the \emph{expanded parse function}, $\eparse$. 
 %Notice that this occurs under empty contexts, i.e. parse functions cannot refer to the surrounding bindings. 
%The parse function must be of type $\aparr{\tBody}{\tParseResultExp}$ where the type abbreviations $\tBody$ and $\tParseResultExp$ are defined as follows.

The assumed type $\tBody$ is characterized as before by Condition \ref{condition:body-isomorphism}.

$\tParseResultPat$, like $\tParseResultExp$, abbreviates a labeled sum type that distinguishes parse errors from successful parses:
\begin{align*}
L_\mathtt{SP} & \defeq \lbltxt{ParseError}, \lbltxt{SuccessP}\\
\tParseResultPat & \defeq \asum{L_\mathtt{SP}}{
  \mapitem{\lbltxt{ParseError}}{\prodt{}}, 
  \mapitem{\lbltxt{SuccessP}}{\tCEPat}
}
\end{align*} %[\mapitem{\lbltxt{ParseError}}{\prodt{}}, \mapitem{\lbltxt{SuccessE}}{\tCEExp}]

The type abbreviated $\tCEPat$ classifies encodings of \emph{proto-patterns}, $\cpv$. The syntax of proto-patterns, defined in Figure \ref{fig:UP-candidate-terms}, will be described when we describe proto-expansion validation in Sec. \ref{sec:ce-syntax-UP}. The mapping from proto-patterns to values of type $\tCEPat$ is defined by the \emph{proto-pattern encoding judgement}, $\encodeCEPat{\cpv}{e}$. An inverse mapping is defined by the \emph{proto-pattern decoding judgement}, $\decodeCEPat{e}{\cpv}$.

\[\begin{array}{ll}
\textbf{Judgement Form} & \textbf{Description}\\
\encodeCEPat{\cpv}{e} & \text{$\cpv$ has encoding $e$}\\
\decodeCEPat{e}{\cpv} & \text{$e$ has decoding $\cpv$}
\end{array}\]

Again, rather than picking a particular definition of $\tCEPat$ and defining the judgements above inductively against it, we only state the following condition, which establishes an isomorphism between values of type $\tCEPat$ and proto-patterns.

\begingroup
\def\thetheorem{\ref{condition:proto-pattern-isomorphism}}
\begin{condition}[Proto-Pattern Isomorphism] ~
\begin{enumerate}
\item For every $\cpv$, we have $\encodeCEPat{\cpv}{\ecand}$ for some $\ecand$ such that $\hastypeUC{\ecand}{\tCEPat}$ and $\isvalU{\ecand}$.
\item If $\hastypeUC{\ecand}{\tCEPat}$ and $\isvalU{\ecand}$ then $\decodeCEPat{\ecand}{\cpv}$ for some $\cpv$.
\item If $\encodeCEPat{\cpv}{\ecand}$ then $\decodeCEPat{\ecand}{\cpv}$.
\item If $\hastypeUC{\ecand}{\tCEPat}$ and $\isvalU{\ecand}$ and $\decodeCEPat{\ecand}{\cpv}$ then $\encodeCEPat{\cpv}{\ecand}$.
\item If $\encodeCEPat{\cpv}{\ecand}$ and $\encodeCEPat{\cpv}{\ecand'}$ then $\ecand=\ecand'$.
\item If $\hastypeUC{\ecand}{\tCEPat}$ and $\isvalU{\ecand}$ and $\decodeCEPat{\ecand}{\cpv}$ and $\decodeCEPat{\ecand}{\cpv'}$ then $\cpv=\cpv'$.
\end{enumerate}
\end{condition}
\endgroup

\item The third premise of Rule (\ref{rule:expandsU-defuptsm}) evaluates the parse function to a value.
\item The final premise of Rule (\ref{rule:expandsU-defuptsm}) extends the spTLM context, $\uPhi$, with the newly determined {spTLM definition}, and proceeds to assign a type, $\tau'$, and expansion, $e$, to $\ue$. The conclusion of Rule (\ref{rule:expandsU-defuptsm}) assigns this type and expansion to the spTLM definition as a whole.% i.e. TLMs define behavior that is relevant during typed expansion, but not during evaluation. 



\emph{spTLM contexts}, $\uPhi$, are of the form $\uAS{\uA}{\Phi}$, where $\uA$ is a {TLM identifier expansion context}, defined previously, and $\Phi$ is a \emph{spTLM definition context}. 

%A \emph{TLM naming context}, $\uA$, is a finite function mapping each TLM name $\tsmv \in \domof{\uA}$ to the \emph{TLM name-symbol mapping}, $\vExpands{\tsmv}{a}$, for some \emph{symbol}, $a$. We write $\ctxUpdate{\uA}{\tsmv}{a}$ for the seTLM naming context that maps $\tsmv$ to $\vExpands{\tsmv}{a}$, and defers to $\uA$ for all other TLM names (i.e. the previous mapping, if it exists, is updated).

An \emph{spTLM definition context}, $\Phi$, is a finite function mapping each TLM name $a \in \domof{\Phi}$ to an \emph{expanded spTLM definition}, $\xuptsmbnd{a}{\tau}{\eparse}$, where $\tau$ is the spTLM's type annotation, and $\eparse$ is its parse function. We write $\Phi, \xuptsmbnd{a}{\tau}{\eparse}$ when $a \notin \domof{\Phi}$ for the extension of $\Phi$ that maps $a$ to $\xuptsmbnd{a}{\tau}{\eparse}$. %We write $\uptsmenv{\Delta}{\Phi}$  when all the type annotations in $\Phi$ are well-formed assuming $\Delta$, and the parse functions in $\Phi$ are closed and of type $\parr{\tBody}{\tParseResultPat}$.
%\begin{definition}[spTLM Definition Context Formation]\label{def:spTLM-def-ctx-formation} $\uptsmenv{\Delta}{\Phi}$ iff for each $\xuptsmbnd{a}{\tau}{\eparse} \in \Phi$, we have $\istypeU{\Delta}{\tau}$ and $\hastypeU{\emptyset}{\emptyset}{\eparse}{\parr{\tBody}{\tParseResultPat}}$.\end{definition}
We define $\uPhi, \uPhyp{\tsmv}{a}{\tau}{\eparse}$, when $\uPhi=\uAS{\uA}{\Phi}$, as an abbreviation of \[\uAS{\ctxUpdate{\uA}{\tsmv}{a}}{\Phi, \xuptsmbnd{a}{\tau}{\eparse}}\]
% and $\uPhi \cup \uPhi'$ when $\uPhi=\uAS{\uA}{\Phi}$ and $\uPhi'=\uAS{\uA'}{\Phi'}$ as an abbreviation of \[\uAS{\uA \cup \uA'}{\Phi \cup \Phi'}\]
\end{enumerate}
\subsection{spTLM Application}\label{sec:uptsm-application}
The unexpanded pattern form for applying an spTLM named $\tsmv$ to a literal form with literal body $b$ is:
\[
\utsmap{\tsmv}{b}
\] 
This stylized form is identical to the stylized form for seTLM application, differing in that appears within the syntax of unexpanded patterns, $\upv$, rather than unexpanded expressions, $\ue$. %It uses forward slashes as delimiters, though stylized variants of any of the literal forms specified in Figure \ref{fig:literal-forms} would be straightforward to add to the syntax table in Figure \ref{fig:UP-unexpanded-terms} (we omit them for simplicity). 
% The corresponding operatio?nal form is $\auapuptsm{b}{\tsmv}$.%, i.e. there is an operator $\texttt{uapuptsm}[b]$ for each literal body $b$ indexed by the TLM name $\tsmv$ and taking no arguments.

Rule (\ref{rule:patExpands-apuptsm}), below, governs spTLM application. 
\begin{equation*}\tag{\ref{rule:patExpands-apuptsm}}
\inferrule{
  \uPhi = \uPhi', \uPhyp{\tsmv}{a}{\tau}{\eparse}\\\\
  \encodeBody{b}{\ebody}\\
  \evalU{\ap{\eparse}{\ebody}}{\aein{\mathtt{SuccessP}}{\ecand}}\\
  \decodeCEPat{\ecand}{\cpv}\\\\
  \segOK{\segof{\cpv}}{b}\\
  \cvalidP{\upctx}{\pscene{\uDelta}{\uPhi}{b}}{\cpv}{p}{\tau}
}{
  \patExpands{\upctx}{\uPhi}{\utsmap{\tsmv}{b}}{p}{\tau}
}
\end{equation*}
This rule is similar to Rule (\ref{rule:expandsU-tsmap}), which governs seTLM application. Its premises can be understood as follows, in order:
\begin{enumerate}
\item The first premise ensures that $\tsmv$ has been defined and extracts the type annotation and parse function.
\item The second premise determines the encoding of the literal body, $\ebody$.
\item The third premise applies the parse function $\eparse$ to the encoding of the literal body. If parsing succeeds, then $\ecand$ will be a value of type $\tCEPat$ (assuming a well-formed spTLM context, by application of the Preservation assumption, Assumption \ref{condition:preservation-UP}.) We call $\ecand$ the \emph{encoding of the proto-expansion}.

If the parse function produces a value labeled $\lbltxt{ParseError}$, then typed expansion fails. No rule is necessary to handle this case. 

\item The fourth premise decodes the encoding of the proto-expansion to produce the \emph{proto-expansion}, $\cpv$, itself.

\item The fifth premise ensures that the proto-expansion induces a valid segmentation of $b$, i.e. that the spliced pattern locations are within bounds and non-overlapping.

\item The final premise of Rule (\ref{rule:expandsU-tsmap}) \emph{validates} the proto-expansion and simultaneously generates the \emph{final expansion}, $e$, and generates hypotheses $\uGamma$, which appear in the conclusion of the rule. The proto-pattern validation judgement is discussed next.
\end{enumerate}

\subsection{Syntax of Proto-Expansions}\label{sec:ce-syntax-UP}

\begin{figure}[h!]
\hspace{-5px}$\arraycolsep=4pt\begin{array}{lllllll}
\textbf{Sort} & & & \textbf{Operational Form} & \textbf{Stylized Form} & \textbf{Description}\\
\mathsf{PrTyp} & \ctau & ::= & \cdots & \cdots & \text{(see Figure \ref{fig:U-candidate-terms})}\\
\mathsf{PrExp} & \ce & ::= & \cdots & \cdots &\text{(see Figure \ref{fig:U-candidate-terms})}\\
&&& \acematchwith{n}{\ce}{\seqschemaX{\crv}} & \matchwith{\ce}{\seqschemaX{\crv}} & \text{match}\\
%\LCC &&& \gray & \gray & \gray\\
\mathsf{PrRule} & \crv & ::= & \acematchrule{p}{\ce} & \matchrule{p}{\ce} & \text{rule}\\
\mathsf{PrPat} & \cpv & ::= & \acewildp & \wildp & \text{wildcard pattern}\\
&&& \acefoldp{p} & \foldp{p} & \text{fold pattern}\\
&&& \acetplp{\labelset}{\mapschema{\cpv}{i}{\labelset}} & \tplp{\mapschema{\cpv}{i}{\labelset}} & \text{labeled tuple pattern}\\
&&& \aceinjp{\ell}{\cpv} & \injp{\ell}{\cpv} & \text{injection pattern}\\
\LCC &&& \color{Yellow} & \color{Yellow} & \color{Yellow}\\
&&& \acesplicedp{m}{n}{\ctau} & \splicedp{m}{n}{\ctau} & \text{spliced pattern ref.}\ECC
\end{array}$
\caption{Syntax of $\miniVersePat$ proto-expansions}
\label{fig:UP-candidate-terms}
\end{figure}

Figure \ref{fig:UP-candidate-terms} defines the syntax of proto-types, $\ctau$, proto-expressions, $\ce$, proto-rules, $\crv$, and proto-patterns, $\cpv$. %The syntax of ce-types is identical to that given in Figure \ref{fig:U-candidate-terms}, which was described in Sec. \ref{sec:ce-syntax-U}. 
Proto-expansion terms are identified up to $\alpha$-equivalence in the usual manner.

Each expanded form, with the exception of the variable pattern form, maps onto a proto-expansion form. We refer to these collectively as the \emph{common proto-expansion forms}. The mapping is given explicitly in Appendix \ref{appendix:proto-expansions-SES}. 

The main proto-expansion form of interest here, highlighted in yellow, is the proto-pattern form for \emph{references to spliced unexpanded patterns}.

% Notice that patterns, $p$, rather than proto-patterns, $\upv$, appear in the match proto-expression form. This is because proto-expressions arise by the action of seTLMs. It would not be sensible for an seTLM to spliced a pattern out of a literal body.

\subsection{Proto-Expansion Validation}\label{sec:ce-validation-UP}
The \emph{proto-expansion validation judgements} validate proto-expansion terms and simultaneously generate their final expansions.

\vspace{10px}\noindent$\arraycolsep=2pt\begin{array}{ll}
\textbf{Judgement Form} & \textbf{Description}\\
\cvalidT{\Delta}{\tscenev}{\ctau}{\tau} & \text{$\ctau$ has well-formed expansion $\tau$}\\
\cvalidE{\Delta}{\Gamma}{\escenev}{\ce}{e}{\tau} & \text{$\ce$ has expansion $e$ of type $\tau$}\\
\cvalidR{\Delta}{\Gamma}{\escenev}{\crv}{r}{\tau}{\tau'} & \text{$\crv$ has expansion $r$ taking values of type $\tau$ to values of type $\tau'$}\\
\cvalidP{\upctx}{\pscenev}{\cpv}{p}{\tau} & \text{$\cpv$ has expansion $p$ matching against $\tau$ generating assumptions $\upctx$}
\end{array}$\vspace{10px}

\emph{Type splicing scenes}, $\tscenev$, are of the form $\tsceneUP{\uDelta}{b}$. \emph{Expression splicing scenes}, $\escenev$, are of the form $\esceneUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{b}$. \emph{Pattern splicing scenes}, $\pscenev$, are of the form $\pscene{\uDelta}{\uPhi}{b}$. As in $\miniVerseUE$, their purpose is to ``remember'', during proto-expansion validation, the contexts and the literal body from the TLM application site (cf. Rules (\ref{rule:expandsU-tsmap}) and (\ref{rule:patExpands-apuptsm})), because these are necessary to validate references to spliced terms. We write $\tsfrom{\escenev}$ for the type splicing scene constructed by dropping unnecessary contexts from $\escenev$:
\[\tsfrom{\esceneUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{b}} = \tsceneUP{\uDelta}{b}\]

\subsubsection{Proto-Type Validation}
The \emph{proto-type validation judgement}, $\cvalidT{\Delta}{\tscenev}{\ctau}{\tau}$, is inductively defined by Rules (\ref{rules:cvalidT-U}), which were already described in Sec. \ref{sec:SE-proto-type-validation}.

\subsubsection{Proto-Expansion Expression and Rule Validation}
The \emph{proto-expression validation judgement}, $\cvalidE{\Delta}{\Gamma}{\escenev}{\ce}{e}{\tau}$, and the \emph{proto-rule validation judgement}, $\cvalidR{\Delta}{\Gamma}{\escenev}{\crv}{r}{\tau}{\tau'}$, are defined mutually inductively with Rules (\ref{rules:expandsU}) and Rule (\ref{rule:ruleExpands}) by Rules (\ref{rules:cvalidE-U}) and Rule (\ref{rule:cvalidR-UP}), respectively.

Rules (\ref{rule:cvalidE-U-var}) through (\ref{rule:cvalidE-U-splicede}) were described in Sec. \ref{sec:ce-validation-U}. Rule (\ref{rule:cvalidE-U-match}) governs match proto-expressions:
\begin{equation*}\tag{\ref{rule:cvalidE-U-match}}
\inferrule{
  \cvalidE{\Delta}{\Gamma}{\escenev}{\ce}{e}{\tau}\\
  % \cvalidT{\Delta}{\tsfrom{\escenev}}{\ctau'}{\tau'}\\\\
  \{\cvalidR{\Delta}{\Gamma}{\escenev}{\crv_i}{r_i}{\tau}{\tau'}\}_{1 \leq i \leq n}
}{\cvalidE{\Delta}{\Gamma}{\escenev}{\acematchwith{n}{\ce}{\seqschemaX{\crv}}}{\aematchwith{n}{e}{\seqschemaX{r}}}{\tau'}}
\end{equation*}
Rule (\ref{rule:cvalidR-UP}) governs proto-rules:
\begin{equation*}\tag{\ref{rule:cvalidR-UP}}
\inferrule{
  \patType{\pctx}{p}{\tau}\\
  \cvalidE{\Delta}{\Gcons{\Gamma}{\pctx}}{\escenev}{\ce}{e}{\tau'}
}{
  \cvalidR{\Delta}{\Gamma}{\escenev}{\acematchrule{p}{\ce}}{\aematchrule{p}{e}}{\tau}{\tau'}
}
\end{equation*}
Notice that proto-rules bind expanded patterns, rather than proto-patterns. This is because proto-rules appear in proto-expressions, which are generated by seTLMs. Proto-patterns are generated exclusively by spTLMs.

% \begin{equation}\label{rule:cvalidE-UP-var}
% \inferrule{ }{
%   \cvalidE{\Delta}{\Gamma, \Ghyp{x}{\tau}}{\escenev}{x}{x}{\tau}
% }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-lam}
% \inferrule{
%   \cvalidT{\Delta}{\tsfrom{\escenev}}{\ctau}{\tau}\\
%   \cvalidE{\Delta}{\Gamma, \Ghyp{x}{\tau}}{\escenev}{\ce}{e}{\tau'}
% }{
%   \cvalidE{\Delta}{\Gamma}{\escenev}{\acelam{\ctau}{x}{\ce}}{\aelam{\tau}{x}{e}}{\aparr{\tau}{\tau'}}
% }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-ap}
%   \inferrule{
%     \cvalidE{\Delta}{\Gamma}{\escenev}{\ce_1}{e_1}{\aparr{\tau}{\tau'}}\\
%     \cvalidE{\Delta}{\Gamma}{\escenev}{\ce_2}{e_2}{\tau}
%   }{
%     \cvalidE{\Delta}{\Gamma}{\escenev}{\aceap{\ce_1}{\ce_2}}{\aeap{e_1}{e_2}}{\tau'}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-tlam}
%   \inferrule{
%     \cvalidE{\Delta, \Dhyp{t}}{\Gamma}{\escenev}{\ce}{e}{\tau}
%   }{
%     \cvalidEX{\acetlam{t}{\ce}}{\aetlam{t}{e}}{\aall{t}{\tau}}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-tap}
%   \inferrule{
%     \cvalidEX{\ce}{e}{\aall{t}{\tau}}\\
%     \cvalidT{\Delta}{\tsfrom{\escenev}}{\ctau'}{\tau'}
%   }{
%     \cvalidEX{\acetap{\ce}{\ctau'}}{\aetap{e}{\tau'}}{[\tau'/t]\tau}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-fold}
%   \inferrule{
%     \cvalidT{\Delta, \Dhyp{t}}{\escenev}{\ctau}{\tau}\\
%     \cvalidEX{\ce}{e}{[\arec{t}{\tau}/t]\tau}
%   }{
%     \cvalidEX{\acefold{t}{\ctau}{\ce}}{\aefold{e}}{\arec{t}{\tau}}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-unfold}
%   \inferrule{
%     \cvalidEX{\ce}{e}{\arec{t}{\tau}}
%   }{
%     \cvalidEX{\aceunfold{\ce}}{\aeunfold{e}}{[\arec{t}{\tau}/t]\tau}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-tpl}
%   \inferrule{
%     \{\cvalidEX{\ce_i}{e_i}{\tau_i}\}_{i \in \labelset}
%   }{
%     \cvalidEX{\acetpl{\labelset}{\mapschema{\ce}{i}{\labelset}}}{\aetpl{\labelset}{\mapschema{e}{i}{\labelset}}}{\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-pr}
%   \inferrule{
%     \cvalidEX{\ce}{e}{\aprod{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}}
%   }{
%     \cvalidEX{\acepr{\ell}{\ce}}{\aepr{\ell}{e}}{\tau}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-in}
%   \inferrule{
%     \{\cvalidT{\Delta}{\tsfrom{\escenev}}{\ctau_i}{\tau_i}\}_{i \in \labelset}\\
%     \cvalidT{\Delta}{\tsfrom{\escenev}}{\ctau}{\tau}\\
%     \cvalidEX{\ce}{e}{\tau}
%   }{
%     \left\{\shortstack{$\Delta~\Gamma \vdash_\uPsi \acein{\labelset, \ell}{\ell}{\mapschema{\ctau}{i}{\labelset}; \mapitem{\ell}{\ctau}}{\ce}$\\$\leadsto$\\$\aein{\labelset, \ell}{\ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}{e} : \asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}$\vspace{-1.2em}}\right\}
%   }
% \end{equation}
% \begin{equation}\label{rule:cvalidE-UP-case}
%   \inferrule{
%     \cvalidEX{\ce}{e}{\asum{\labelset}{\mapschema{\tau}{i}{\labelset}}}\\
%     \{\cvalidE{\Delta}{\Gamma, \Ghyp{x_i}{\tau_i}}{\escenev}{\ue_i}{e_i}{\tau}\}_{i \in \labelset}
%   }{
%     \cvalidEX{\acecase{\labelset}{\tau}{\ce}{\mapschemab{x}{\ce}{i}{\labelset}}}{\aecase{\labelset}{e}{\mapschemab{x}{e}{i}{\labelset}}}{\tau}
%   }
% \end{equation}
% \end{subequations}
%The \emph{ce-rule validation judgement}, $\cvalidR{\Delta}{\Gamma}{\escenev}{\crv}{r}{\tau}{\tau'}$, is defined mutually inductively with Rules (\ref{rules:cvalidE-UP}) by 


\subsubsection{Proto-Pattern Validation}
spTLMs generate candidate expansions of proto-pattern form, as described in Sec. \ref{sec:uptsm-application}. The \emph{proto-pattern validation judgement}, $\cvalidP{\upctx}{\pscenev}{\cpv}{p}{\tau}$, which appears as the final premise of Rule (\ref{rule:patExpands-apuptsm}), validates proto-patterns and simultaneously generates the final expansion, $p$, and the unexpanded typing hypotheses $\upctx$.

The proto-pattern validation judgement is defined mutually inductively with Rules (\ref{rules:patExpands}) by Rules (\ref{rules:cvalidP-UP}), reproduced below.
\begin{equation*}\tag{\ref{rule:cvalidP-UP-wild}}
\inferrule{ }{
  \cvalidP{\uGG{\emptyset}{\emptyset}}{\pscenev}{\acewildp}{\aewildp}{\tau}
}
\end{equation*}
\begin{equation*}\tag{\ref{rule:cvalidP-UP-fold}}
\inferrule{
  \cvalidP{\upctx}{\pscenev}{\cpv}{p}{[\arec{t}{\tau}/t]\tau}
}{
  \cvalidP{\upctx}{\pscenev}{\acefoldp{\cpv}}{\aefoldp{p}}{\arec{t}{\tau}}
}
\end{equation*}
\begin{equation*}\tag{\ref{rule:cvalidP-UP-tpl}}
\inferrule{
  \tau = \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}\\\\
  \{\cvalidP{\upctx_i}{\pscenev}{\cpv_i}{p_i}{\tau_i}\}_{i \in \labelset}
}{
% \left(\shortstack{$\vdash^{\pscenev} \acetplp{\labelset}{\mapschema{\cpv}{i}{\labelset}}$\\$\leadsto$\\$\aetplp{\labelset}{\mapschema{p}{i}{\labelset}} : \aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}~\dashVx^{\,\Gconsi{i \in \labelset}{\upctx_i}}$\vspace{-1.2em}}\right)
  \cvalidP{\GIconsi{i \in \labelset}{\upctx_i}}{\pscenev}{\acetplp{\labelset}{\mapschema{\cpv}{i}{\labelset}}}{\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}}{\tau}
}
\end{equation*}
\begin{equation*}\tag{\ref{rule:cvalidP-UP-in}}
\inferrule{
  \cvalidP{\upctx}{\pscenev}{\cpv}{p}{\tau}
}{
  \cvalidP{\upctx}{\pscenev}{\aceinjp{\ell}{\cpv}}{\aeinjp{\ell}{p}}{\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau}}}
}
\end{equation*}
\begin{equation*}\tag{\ref{rule:cvalidP-UP-spliced}}
\inferrule{
  \cvalidT{\emptyset}{\tsceneUP{\uDelta}{b}}{\ctau}{\tau}\\
  \parseUPat{\bsubseq{b}{m}{n}}{\upv}\\
  \patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}
}{
  \cvalidP{\upctx}{\pscene{\uDelta}{\uPhi}{b}}{\acesplicedp{m}{n}{\ctau}}{p}{\tau}
}
\end{equation*}

Rules (\ref{rule:cvalidP-UP-wild}) through (\ref{rule:cvalidP-UP-in}) govern proto-patterns of common form, and behave like the corresponding pattern typing rules, i.e. Rules (\ref{rule:patType-wild}) through (\ref{rule:patType-inj}). Rule (\ref{rule:cvalidP-UP-spliced}) governs references to spliced unexpanded patterns. The first premise validates the type annotation. The second premise parses the indicated subsequence of the literal body, $b$, to produce the referenced unexpanded pattern, $\upv$, and the third premise types and expands $\upv$ under the spTLM context $\uPhi$ from the spTLM application site, generating the hypotheses $\upctx$. These are the hypotheses generated in the conclusion of the rule.

Hypotheses can be generated only by spliced subpatterns, so there is no proto-pattern form corresponding to variable patterns. This achieves the prohibition on hidden bindings described in Sec. \ref{sec:ptsms-hygiene}. We consider this invariant formally below.

\subsection{Metatheory}
The following theorem establishes that typed pattern expansion produces an expanded pattern that matches values of the specified type and generates the specified hypotheses. We must mutually state the corresponding proposition about proto-patterns, because the relevant judgements are mutually defined.
\begingroup
\def\thetheorem{\ref{thm:typed-pattern-expansion}}
\begin{theorem}[Typed Pattern Expansion] ~
\begin{enumerate}
  \item If $\pExpandsSP{\uDD{\uD}{\Delta}}{\uAS{\uA}{\Phi}}{\upv}{p}{\tau}{\uGG{\uG}{\pctx}}$ then $\patType{\pctx}{p}{\tau}$.
  \item If $\cvalidP{\uGG{\uG}{\pctx}}{\pscene{\uDD{\uD}{\Delta}}{\uAP{\uA}{\Phi}}{b}}{\cpv}{p}{\tau}$ then $\patType{\pctx}{p}{\tau}$.
\end{enumerate}
\end{theorem}
\begin{proof}
  By mutual rule induction on Rules (\ref{rules:patExpands}) and Rules (\ref{rules:cvalidP-UP}). The full proof is given in Appendix \ref{appendix:SES-typed-pattern-expansion}. We will reproduce only the interesting cases below.
  \begin{enumerate}
  \item The only interesting case in the proof of part 1 is the case for spTLM application. In the following, let $\uDelta=\uDD{\uD}{\Delta}$ and $\upctx=\uGG{\uG}{\pctx}$ and $\uPhi=\uAP{\uA}{\Phi}$.
  \begin{byCases}
%     \item[\text{(\ref{rule:patExpands-var})}] ~
%       \begin{pfsteps*}
%         \item $\upv=\ux$ \BY{assumption}
%         \item $p=x$ \BY{assumption}
%         \item $\pctx=\Ghyp{x}{\tau}$ \BY{assumption}
%         \item $\patType{\Ghyp{x}{\tau}}{x}{\tau}$ \BY{Rule (\ref{rule:patType-var})}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:patExpands-wild})}] ~
%       \begin{pfsteps*}
%         \item $p=\aewildp$ \BY{assumption}
%         \item $\pctx = \emptyset$ \BY{assumption}
%         \item $\patType{\emptyset}{\aewildp}{\tau}$ \BY{Rule (\ref{rule:patType-wild})}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:patExpands-fold})}] ~
%       \begin{pfsteps*}
%         \item $\upv=\foldp{\upv'}$ \BY{assumption}
%         \item $p=\aefoldp{p'}$ \BY{assumption}
%         \item $\tau=\arec{t}{\tau'}$ \BY{assumption}
%         %\item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\patExpands{\upctx}{\uPhi}{\upv'}{p'}{[\arec{t}{\tau'}/t]\tau'}$ \BY{assumption} \pflabel{patExpands}
%         \item $\patType{\pctx}{p'}{[\arec{t}{\tau'}/t]\tau'}$ \BY{IH, part 1 on \pfref{patExpands}} \pflabel{patType}
%         \item $\patType{\pctx}{\aefoldp{p'}}{\arec{t}{\tau'}}$ \BY{Rule (\ref{rule:patType-fold}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:patExpands-tpl})}] ~
%       \begin{pfsteps*}
%         \item $\upv=\tplp{\mapschema{\upv}{i}{\labelset}}$ \BY{assumption}
%         \item $p=\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}$ \BY{assumption}
%         \item $\tau=\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}$ \BY{assumption}
%         \item $\{\patExpands{\uGG{\uG_i}{\pctx_i}}{\uPhi}{\upv_i}{p_i}{\tau_i}\}_{i \in \labelset}$ \BY{assumption} \pflabel{patExpands}
%         \item $\pctx = \Gconsi{i \in \labelset}{\pctx_i}$ \BY{assumption}
%         %\item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\{\patType{\pctx_i}{p_i}{\tau_i}\}_{i \in \labelset}$ \BY{IH, part 1 over \pfref{patExpands}}\pflabel{patType}
%         \item $\patType{\Gconsi{i \in \labelset}{\pctx_i}}{\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}}{\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}}$ \BY{Rule (\ref{rule:patType-tpl}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:patExpands-in})}] ~
%       \begin{pfsteps*}
%         \item $\upv=\injp{\ell}{\upv'}$ \BY{assumption}
%         \item $p=\aeinjp{\ell}{p'}$ \BY{assumption}
%         \item $\tau=\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau'}}$ \BY{assumption}
%         \item $\patExpands{\upctx}{\uPhi}{\upv'}{p'}{\tau'}$ \BY{assumption} \pflabel{patExpands}
% %        \item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\patType{\pctx}{p'}{\tau'}$ \BY{IH, part 1 on \pfref{patExpands}} \pflabel{patType}
%         \item $\patType{\pctx}{\aeinjp{\ell}{p'}}{\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau'}}}$ \BY{Rule (\ref{rule:patType-inj}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
    \item[\text{(\ref{rule:patExpands-apuptsm})}] ~
      \begin{pfsteps*}
        \item $\upv=\utsmap{\tsmv}{b}$ \BY{assumption}
        \item $\uA=\uA', \vExpands{\tsmv}{a}$ \BY{assumption}
        \item $\Phi=\Phi', \xuptsmbnd{a}{\tau}{\eparse}$ \BY{assumption}
        \item $\encodeBody{b}{\ebody}$ \BY{assumption}
        \item $\evalU{\eparse(\ebody)}{\aein{\mathtt{SuccessP}}{\ecand}}$ \BY{assumption}
        \item $\decodeCEPat{\ecand}{\cpv}$ \BY{assumption}
        \item $\cvalidP{\uGG{\uG}{\pctx}}{\pscene{\uDelta}{\uAP{\uA}{\Phi}}{b}}{\cpv}{p}{\tau}$ \BY{assumption} \pflabel{cvalidP}
%        \item $\uptsmenv{\Delta}{\Phi', \xuptsmbnd{a}{\tau}{\eparse}}$ \BY{assumption} \pflabel{env}
        \item $\patType{\pctx}{p}{\tau}$ \BY{IH, part 2 on \pfref{cvalidP}}
      \end{pfsteps*}
      \resetpfcounter
  \end{byCases}

  \item The only interesting case in the proof of part 2 is the case for spliced patterns. In the following, let $\upctx=\uGG{\uG}{\pctx}$ and $\uDelta=\uDD{\uD}{\Delta}$ and $\uPhi=\uAP{\uA}{\Phi}$.
  \begin{byCases}
%     \item[\text{(\ref{rule:cvalidP-UP-wild})}] ~
%       \begin{pfsteps*}
%         \item $p=\aewildp$ \BY{assumption}
%         \item $\pctx=\emptyset$ \BY{assumption}
%         \item $\patType{\emptyset}{\aewildp}{\tau}$ \BY{Rule (\ref{rule:patType-wild})}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:cvalidP-UP-fold})}] ~
%       \begin{pfsteps*}
%         \item $\cpv=\acefoldp{\cpv'}$ \BY{assumption}
%         \item $p=\aefoldp{p'}$ \BY{assumption}
%         \item $\tau=\arec{t}{\tau'}$ \BY{assumption}
%         % \item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\cvalidP{\upctx}{\pscene{\Delta}{\uPhi}{b}}{\cpv'}{p'}{[\arec{t}{\tau'}/t]\tau'}$ \BY{assumption} \pflabel{cvalidP}
%         \item $\patType{\pctx}{p'}{[\arec{t}{\tau'}/t]\tau'}$ \BY{IH, part 2 on \pfref{cvalidP}} \pflabel{patType}
%         \item $\patType{\pctx}{\aefoldp{p'}}{\arec{t}{\tau'}}$ \BY{Rule (\ref{rule:patType-fold}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:cvalidP-UP-tpl})}] ~
%       \begin{pfsteps*}
%         \item $\cpv=\acetplp{\labelset}{\mapschema{\cpv}{i}{\labelset}}$ \BY{assumption}
%         \item $p=\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}$ \BY{assumption}
%         \item $\tau=\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}$ \BY{assumption}
%         \item $\{\cvalidP{\uGG{\uG_i}{\pctx_i}}{\pscene{\Delta}{\uPhi}{b}}{\cpv_i}{p_i}{\tau_i}\}_{i \in \labelset}$ \BY{assumption} \pflabel{cvalidP}
%         \item $\pctx = \Gconsi{i \in \labelset}{\pctx_i}$ \BY{assumption}
%         %\item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\{\patType{\pctx_i}{p_i}{\tau_i}\}_{i \in \labelset}$ \BY{IH, part 2 over \pfref{cvalidP}}\pflabel{patType}
%         \item $\patType{\Gconsi{i \in \labelset}{\pctx_i}}{\aetplp{\labelset}{\mapschema{p}{i}{\labelset}}}{\aprod{\labelset}{\mapschema{\tau}{i}{\labelset}}}$ \BY{Rule (\ref{rule:patType-tpl}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
%     \item[\text{(\ref{rule:cvalidP-UP-in})}] ~
%       \begin{pfsteps*}
%         \item $\cpv=\aceinjp{\ell}{\cpv'}$ \BY{assumption}
%         \item $p=\aeinjp{\ell}{p'}$ \BY{assumption}
%         \item $\tau=\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau'}}$ \BY{assumption}
%         \item $\cvalidP{\upctx}{\pscene{\Delta}{\uPhi}{b}}{\cpv'}{p'}{\tau'}$ \BY{assumption} \pflabel{cvalidP}
% %        \item $\uptsmenv{\Delta}{\Phi}$ \BY{assumption} \pflabel{env}
%         \item $\patType{\pctx}{p'}{\tau'}$ \BY{IH, part 2 on \pfref{cvalidP}} \pflabel{patType}
%         \item $\patType{\pctx}{\aeinjp{\ell}{p'}}{\asum{\labelset, \ell}{\mapschema{\tau}{i}{\labelset}; \mapitem{\ell}{\tau'}}}$ \BY{Rule (\ref{rule:patType-inj}) on \pfref{patType}}
%       \end{pfsteps*}
%       \resetpfcounter
    \item[\text{(\ref{rule:cvalidP-UP-spliced})}] ~
      \begin{pfsteps*}
        \item $\cpv=\acesplicedp{m}{n}{\ctau}$ \BY{assumption}
        \item $\cvalidT{\emptyset}{\tsceneUP{\uDelta}{b}}{\ctau}{\tau}$ \BY{assumption}
        \item $\parseUExp{\bsubseq{b}{m}{n}}{\upv}$ \BY{assumption}
        \item $\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}$ \BY{assumption} \pflabel{patExpands}
        \item $\patType{\pctx}{p}{\tau}$ \BY{IH, part 1 on \pfref{patExpands}}
      \end{pfsteps*}
      \resetpfcounter
  \end{byCases}
  \end{enumerate}
The mutual induction can be shown to be well-founded by showing that the following numeric metric on the judgements that we induct on is decreasing:
\begin{align*}
\sizeof{\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}} & = \sizeof{\upv}\\
\sizeof{{\cvalidP{\upctx}{\pscene{\uDelta}{\uPhi}{b}}{\cpv}{p}{\tau}}} & = \sizeof{b}
\end{align*}
where $\sizeof{b}$ is the length of $b$ and $\sizeof{\upv}$ is the sum of the lengths of the literal bodies in $\upv$ (see Appendix \ref{appendix:SES-body-lengths}.)

The only case in the proof of part 1 that invokes part 2 is Case (\ref{rule:patExpands-apuptsm}). There, we have that the metric remains stable: \begin{align*}
 & \sizeof{\patExpands{\upctx}{\uPhi}{\utsmap{\tsmv}{b}}{p}{\tau}}\\
=& \sizeof{{\cvalidP{\upctx}{\pscene{\uDelta}{\uPhi}{b}}{\cpv}{p}{\tau}}}\\
=&\sizeof{b}\end{align*}

The only case in the proof of part 2 that invokes part 1 is Case (\ref{rule:cvalidP-UP-spliced}). There, we have that $\parseUPat{\bsubseq{b}{m}{n}}{\upv}$ and the IH is applied to the judgement $\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}$. Because the metric is stable when passing from part 1 to part 2, we must have that it is strictly decreasing in the other direction:
\[\sizeof{\patExpands{\upctx}{\uPhi}{\upv}{p}{\tau}} < \sizeof{{\cvalidP{\upctx}{\pscene{\uDelta}{\uPhi}{b}}{\acesplicedp{m}{n}{\ctau}}{p}{\tau}}}\]
i.e. by the definitions above, 
\[\sizeof{\upv} < \sizeof{b}\]

This is established by appeal to Condition \ref{condition:body-subsequences}, which states that subsequences of $b$ are no longer than $b$, and the following condition, which states that an unexpanded pattern constructed by parsing a textual sequence $b$ is strictly smaller, as measured by the metric defined above, than the length of $b$, because some characters must necessarily be used to apply the pattern TLM and delimit each literal body.
\begingroup
\def\thetheorem{\ref{condition:pattern-parsing}}
\begin{condition}[Pattern Parsing Monotonicity] If $\parseUPat{b}{\upv}$ then $\sizeof{\upv} < \sizeof{b}$.\end{condition}
\endgroup

Combining Conditions \ref{condition:body-subsequences} and \ref{condition:pattern-parsing}, we have that $\sizeof{\ue} < \sizeof{b}$ as needed.
\end{proof}
\endgroup

Finally, the following theorem establishes that typed expression and rule expansion produces expanded expressions and rules of the same type under the same contexts. Again, it must be stated mutually with the corresponding theorem about candidate expansion expressions and rules because the judgements are mutually defined.
\begin{theorem}[Typed Expansion] ~
\begin{enumerate}
  \item \begin{enumerate}
    \item If $\expandsUP{\uDD{\uD}{\Delta}}{\uGG{\uG}{\Gamma}}{\uPsi}{\uPhi}{\ue}{e}{\tau}$ then $\hastypeU{\Delta}{\Gamma}{e}{\tau}$.
    \item If $\ruleExpands{\uDD{\uD}{\Delta}}{\uGG{\uG}{\Gamma}}{\uPsi}{\uPhi}{\urv}{r}{\tau}{\tau'}$  then $\ruleType{\Delta}{\Gamma}{r}{\tau}{\tau'}$.
  \end{enumerate}
  \item \begin{enumerate}
    \item If $\cvalidE{\Delta}{\Gamma}{\esceneUP{\uDD{\uD}{\Delta_\text{app}}}{\uGG{\uG}{\Gamma_\text{app}}}{\uPsi}{\uPhi}{b}}{\ce}{e}{\tau}$ and $\Delta \cap \Delta_\text{app}=\emptyset$ and $\domof{\Gamma} \cap \domof{\Gamma_\text{app}}=\emptyset$ then $\hastypeU{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gamma}{\Gamma_\text{app}}}{e}{\tau}$. 
    \item If $\cvalidR{\Delta}{\Gamma}{\esceneUP{\uDD{\uD}{\Delta_\text{app}}}{\uGG{\uG}{\Gamma_\text{app}}}{\uPsi}{\uPhi}{b}}{\crv}{r}{\tau}{\tau'}$ and $\Delta \cap \Delta_\text{app}=\emptyset$ and $\domof{\Gamma} \cap \domof{\Gamma_\text{app}}=\emptyset$ then $\ruleType{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gamma}{\Gamma_\text{app}}}{r}{\tau}{\tau'}$.
  \end{enumerate}
\end{enumerate}
\end{theorem}
\begin{proof}
By mutual rule induction on Rules (\ref{rules:expandsU}), Rule (\ref{rule:ruleExpands}), Rules (\ref{rules:cvalidE-U}) and Rule (\ref{rule:cvalidR-UP}). The full proof is given in Appendix \ref{appendix:metatheory-SES}. We will reproduce only the cases that have to do with pattern matching below.

\begin{enumerate}
\item In the following cases, let $\uDelta=\uDD{\uD}{\Delta}$ and $\uGamma=\uGG{\uG}{\Gamma}$.
  \begin{enumerate}
  \item The only  cases in the proof of part 1(a) that have to do with pattern matching are the cases involving the unexpanded match expression and spTLM definition. 
  \begin{byCases}
    \item[\text{(\ref{rule:expandsU-match})}] ~
      \begin{pfsteps*}
        \item $\ue=\matchwith{\ue'}{\seqschemaX{\urv}}$ \BY{assumption}
        \item $e=\aematchwith{n}{e'}{\seqschemaX{r}}$ \BY{assumption}
        \item $\expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\ue'}{e'}{\tau'}$ \BY{assumption} \pflabel{expandsUP}
        % \item $\istypeU{\Delta}{\tau}$ \BY{assumption}\pflabel{istype}
        % \item $\expandsTU{\uDelta}{\utau}{\tau}$ \BY{assumption} \pflabel{expandsTU}
        \item $\{\ruleExpands{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\urv_i}{r_i}{\tau'}{\tau}\}_{1 \leq i \leq n}$ \BY{assumption}\pflabel{ruleExpands}
        \item $\hastypeU{\Delta}{\Gamma}{e'}{\tau'}$ \BY{IH, part 1(a) on \pfref{expandsUP}}\pflabel{hasType}
        \item $\{\ruleType{\Delta}{\Gamma}{r_i}{\tau'}{\tau}\}_{1 \leq i \leq n}$ \BY{IH, part 1(b) over \pfref{ruleExpands}}\pflabel{ruleType}
        \item $\hastypeU{\Delta}{\Gamma}{\aematchwith{n}{\tau}{e'}{\seqschemaX{r}}}{\tau}$ \BY{Rule (\ref{rule:hastypeUP-match}) on \pfref{hasType} and \pfref{ruleType}}
      \end{pfsteps*}
      \resetpfcounter

    \item[\text{(\ref{rule:expandsU-defuptsm})}] ~
      \begin{pfsteps}
          \item \ue=\usyntaxup{\tsmv}{\utau'}{\eparse}{\ue'} \BY{assumption}
          \item \expandsTU{\uDelta}{\utau'}{\tau'} \BY{assumption} \pflabel{expandsTU}
         \item \hastypeU{\emptyset}{\emptyset}{\eparse}{\aparr{\tBody}{\tParseResultPat}} \BY{assumption}\pflabel{eparse}
          \item \expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi, \uPhyp{\tsmv}{a}{\tau'}{\eparse}}{\ue'}{e}{\tau} \BY{assumption}\pflabel{expandsU}
        %  \item \uetsmenv{\Delta}{\Psi} \BY{assumption}\pflabel{uetsmenv1}
         \item \istypeU{\Delta}{\tau'} \BY{Lemma \ref{lemma:type-expansion-U} to \pfref{expandsTU}} \pflabel{istype}
        %  \item \uetsmenv{\Delta}{\Psi, \xuetsmbnd{\tsmv}{\tau'}{\eparse}} \BY{Definition \ref{def:seTLM-def-ctx-formation} on \pfref{uetsmenv1}, \pfref{istype} and \pfref{eparse}}\pflabel{uetsmenv3}
          \item \hastypeU{\Delta}{\Gamma}{e}{\tau} \BY{IH, part 1(a) on \pfref{expandsU}}
        \end{pfsteps}
        \resetpfcounter 
  \end{byCases}
  \item There is only one case.
  \begin{byCases}
    \item[\text{(\ref{rule:ruleExpands})}] ~
      \begin{pfsteps*}
        \item $\urv=\matchrule{\upv}{\ue}$ \BY{assumption}
        \item $r=\aematchrule{p}{e}$ \BY{assumption}
        \item $\patExpands{\uGG{\uA'}{\pctx'}}{\uPhi}{\upv}{p}{\tau}$ \BY{assumption} \pflabel{patExpands}
        \item $\expandsUP{\uDelta}{\uGG{{\uA}\uplus{\uA'}}{\Gcons{\Gamma}{\pctx'}}}{\uPsi}{\uPhi}{\ue}{e}{\tau'}$ \BY{assumption} \pflabel{expandsUP}
        \item $\patType{\pctx'}{p}{\tau}$ \BY{Theorem \ref{thm:typed-pattern-expansion}, part 1 on \pfref{patExpands}}\pflabel{patType}
        \item $\hastypeU{\Delta}{\Gcons{\Gamma}{\pctx'}}{e}{\tau'}$ \BY{IH, part 1(a) on \pfref{expandsUP}} \pflabel{hasType}
        \item $\ruleType{\Delta}{\Gamma}{\aematchrule{p}{e}}{\tau}{\tau'}$ \BY{Rule (\ref{rule:ruleType}) on \pfref{patType} and \pfref{hasType}}
      \end{pfsteps*}
      \resetpfcounter
  \end{byCases}
  \end{enumerate}
\item In the following, let $\uDelta=\uDD{\uD}{\Delta_\text{app}}$ and $\uGamma=\uGG{\uG}{\Gamma_\text{app}}$. \begin{enumerate}
  \item The only case in the proof of part 2(a) that has to do with pattern matching is the case involving the match proto-expression. 
  \begin{byCases}
    \item[\text{(\ref{rule:cvalidE-U-match})}] ~
      \begin{pfsteps*}
        \item $\ce=\acematchwith{n}{\ce'}{\seqschemaX{\crv}}$ \BY{assumption}
        \item $e=\aematchwith{n}{e'}{\seqschemaX{r}}$ \BY{assumption}
        \item $\cvalidE{\Delta}{\Gamma}{\esceneUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{b}}{\ce'}{e'}{\tau'}$ \BY{assumption} \pflabel{cvalidE}
        % \item $\cvalidT{\Delta}{\tsceneUP{\uDelta}{b}}{\ctau}{\tau}$ \BY{assumption} \pflabel{cvalidT}
        \item $\{\cvalidR{\Delta}{\Gamma}{\esceneUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{b}}{\crv_i}{r_i}{\tau'}{\tau}\}_{1 \leq i \leq n}$ \BY{assumption} \pflabel{cvalidR}
        \item $\Delta \cap \Delta_\text{app} = \emptyset$ \BY{assumption} \pflabel{delta-disjoint}
        \item $\domof{\Gamma} \cap \domof{\Gamma_\text{app}} = \emptyset$ \BY{assumption} \pflabel{gamma-disjoint}
        \item $\hastypeU{\Delta \cup \Delta_\text{app}}{\Gamma \cup \Gamma_\text{app}}{e'}{\tau'}$ \BY{IH, part 2(a) on \pfref{cvalidE}, \pfref{delta-disjoint} and \pfref{gamma-disjoint}} \pflabel{hastype}
        % \item $\istypeU{\Delta \cup \Delta_\text{app}}{\tau}$ \BY{Lemma \ref{lemma:candidate-expansion-type-validation} on \pfref{cvalidT}} \pflabel{istype}
        \item $\ruleType{\Delta \cup \Delta_\text{app}}{\Gamma \cup \Gamma_\text{app}}{r}{\tau'}{\tau}$ \BY{IH, part 2(b) on \pfref{cvalidR}, \pfref{delta-disjoint} and \pfref{gamma-disjoint}} \pflabel{ruleType}
        \item $\hastypeU{\Delta \cup \Delta_\text{app}}{\Gamma \cup \Gamma_\text{app}}{\aematchwith{n}{e'}{\seqschemaX{r}}}{\tau}$ \BY{Rule (\ref{rule:hastypeUP-match}) on \pfref{hastype} and \pfref{ruleType}}
      \end{pfsteps*}
      \resetpfcounter
    % \item[\text{(\ref{rule:cvalidE-U-splicede})}] ~
    %   \begin{pfsteps*}
    %     \item $\ce=\acesplicede{m}{n}$ \BY{assumption}
    %     \item $\parseUExp{\bsubseq{b}{m}{n}}{\ue}$ \BY{assumption}
    %     \item $\expandsUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{\ue}{e}{\tau}$ \BY{assumption} \pflabel{expands}
    %   %  \item $\uetsmenv{\Delta_\text{app}}{\Psi}$ \BY{assumption} \pflabel{uetsmenv}
    %     \item $\Delta \cap \Delta_\text{app}=\emptyset$ \BY{assumption} \pflabel{delta-disjoint}
    %     \item $\domof{\Gamma} \cap \domof{\Gamma_\text{app}}=\emptyset$ \BY{assumption} \pflabel{gamma-disjoint}
    %     \item $\hastypeU{\Delta_\text{app}}{\Gamma_\text{app}}{e}{\tau}$ \BY{IH, part 1(a) on \pfref{expands}} \pflabel{hastype}
    %     \item $\hastypeU{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gamma}{\Gamma_\text{app}}}{e}{\tau}$ \BY{Lemma \ref{lemma:weakening-UP} over $\Delta$ and $\Gamma$ and exchange on \pfref{hastype}}
    %   \end{pfsteps*}
    %   \resetpfcounter

  \end{byCases}
  \item There is only one case.
  \begin{byCases}
     \item[\text{(\ref{rule:cvalidR-UP})}] ~
      \begin{pfsteps*}
        \item $\crv=\acematchrule{p}{\ce}$ \BY{assumption}
        \item $r=\aematchrule{p}{e}$ \BY{assumption}
        \item $\patType{\pctx}{p}{\tau}$ \BY{assumption} \pflabel{patType}
        \item $\cvalidE{\Delta}{\Gcons{\Gamma}{\pctx}}{\esceneUP{\uDelta}{\uGamma}{\uPsi}{\uPhi}{b}}{\ce}{e}{\tau'}$ \BY{assumption} \pflabel{cvalidE}
        \item $\Delta \cap \Delta_\text{app} = \emptyset$ \BY{assumption}\pflabel{delta-disjoint}
        \item $\domof{\Gamma} \cap \domof{\pctx} = \emptyset$ \BY{identification convention}\pflabel{gamma-disjoint1}
        \item $\domof{\Gamma_\text{app}} \cap \domof{\pctx} = \emptyset$ \BY{identification convention}\pflabel{gamma-disjoint2}
        \item $\domof{\Gamma} \cap \domof{\Gamma_\text{app}} = \emptyset$ \BY{assumption}\pflabel{gamma-disjoint3}
        \item $\domof{\Gcons{\Gamma}{\pctx}} \cap \domof{\Gamma_\text{app}} = \emptyset$ \BY{standard finite set definitions and identities on \pfref{gamma-disjoint1}, \pfref{gamma-disjoint2} and \pfref{gamma-disjoint3}}\pflabel{gamma-disjoint4}
        \item $\hastypeU{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gcons{\Gamma}{\pctx}}{\Gamma_\text{app}}}{e}{\tau'}$ \BY{IH, part 2(a) on \pfref{cvalidE}, \pfref{delta-disjoint} and \pfref{gamma-disjoint4}}\pflabel{hastype}
        \item $\hastypeU{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gcons{\Gamma}{\Gamma_\text{app}}}{\pctx}}{e}{\tau'}$ \BY{exchange of $\pctx$ and $\Gamma_\text{app}$ on \pfref{hastype}}\pflabel{hastype2}
        \item $\ruleType{\Dcons{\Delta}{\Delta_\text{app}}}{\Gcons{\Gamma}{\Gamma_\text{app}}}{\aematchrule{p}{e}}{\tau}{\tau'}$ \BY{Rule (\ref{rule:ruleType}) on \pfref{patType} and \pfref{hastype2}}
      \end{pfsteps*}
      \resetpfcounter
   \end{byCases} 
\end{enumerate}
\end{enumerate}

The mutual induction can be shown to be well-founded essentially as described in Sec. \ref{sec:SE-metatheory}. Appendix \ref{appendix:metatheory-SES} gives the complete details.
\end{proof}

\subsubsection{Abstract Reasoning Principles}\label{sec:uptsms-abstract-reasoning-principles}
The following theorem summarizes the abstract reasoning principles available to programmers when applying an spTLM. Descriptions of labeled clauses are given inline.
\begingroup
\def\thetheorem{\ref{thm:spTLM-Typing-Segmentation}}
\begin{theorem}[spTLM Abstract Reasoning Principles]
% \label{thm:spTLM-Typing-Segmentation}
If $\patExpands{\upctx}{\uPhi}{\utsmap{\tsmv}{b}}{p}{\tau}$ where $\uDelta=\uDD{\uD}{\Delta}$ and $\uGamma=\uGG{\uG}{\Gamma}$ then all of the following hold:
\begin{enumerate}
        \item (\textbf{Typing 1}) $\uPhi=\uPhi', \uPhyp{\tsmv}{a}{\tau}{\eparse}$ and $\patType{\pctx}{p}{\tau}$
          \begin{quote}
            The final expansion matches values of the type specified by the spTLM's type annotation.
          \end{quote}
        \item $\encodeBody{b}{\ebody}$
        \item $\evalU{\eparse(\ebody)}{\aein{\mathtt{SuccessP}}{\ecand}}$
        \item $\decodeCEPat{\ecand}{\cpv}$
        \item (\textbf{Segmentation}) $\segOK{\segof{\cpv}}{b}$
          \begin{quote}
            The segmentation determined by the proto-expansion actually segments the literal body (i.e. each segment is in-bounds and the segments are non-overlapping.)
          \end{quote}
        \item $\segof{\cpv} = \sseq{\acesplicedt{n'_i}{m'_i}}{\nty} \cup \sseq{\acesplicedp{m_i}{n_i}{\ctau_i}}{\npat}$
        \item (\textbf{Typing 2}) $\sseq{
              \expandsTU{\uDelta}
              {
                \parseUTypF{\bsubseq{b}{m'_i}{n'_i}}
              }{\tau'_i}
            }{\nty}$ and $\sseq{\istypeU{\Delta}{\tau'_i}}{\nty}$
            \begin{quote}
              Each spliced type has a well-formed expansion at the application site.
            \end{quote}
        \item (\textbf{Typing 3}) $\sseq{
          \cvalidT{\emptyset}{
            \tsceneUP
              {\uDelta}{b}
          }{
            \ctau_i
          }{\tau_i}
        }{\npat}$ and $\sseq{\istypeU{\Delta}{\tau_i}}{\npat}$
          \begin{quote}
            Each type annotation on a reference to a spliced pattern has a well-formed expansion at the application site.
          \end{quote}
        \item (\textbf{Typing 4}) $\sseq{
          \patExpands
            {\uGG{\uG_i}{\pctx_i}}
            {\uPhi}
            {\parseUPatF{\bsubseq{b}{m_i}{n_i}}}
            {p_i}
            {\tau_i}
        }{\npat}$  and $\sseq{\patType{\pctx_i}{p_i}{\tau_i}}{\npat}$
          \begin{quote}
            Each spliced pattern has a well-typed expansion that matches values of the type indicated by the corresponding type annotation in the segmentation.
          \end{quote}
      \item (\textbf{No Hidden Bindings}) $\uG = \biguplus_{0 \leq i < \npat} \uG_i$ and $\Gamma = \bigcup_{0 \leq i < \npat} \pctx_i$
        \begin{quote}
          The hypotheses generated by the TLM application are exactly those generated by the spliced patterns.
        \end{quote}
  \end{enumerate}
\end{theorem}
\begin{proof} The proof relies on a lemma about decomposing proto-patterns. The proof is given in Appendix \ref{appendix:SES-reasoning-principles}.\end{proof}
\endgroup


% The following theorem, together with Theorem \ref{thm:typed-pattern-expansion} part 1, establishes \textbf{Typing} and \textbf{Segmentation}, as discussed in Sec. \ref{sec:ptsms-validation}.

% \begingroup
% \def\thetheorem{\ref{thm:spTLM-Typing-Segmentation}}
% \begin{theorem}[spTLM Typing and Segmentation]
% If $\patExpands{\upctx}{\uPhi}{\utsmap{\tsmv}{b}}{p}{\tau}$ then 
% \begin{enumerate}
%         \item (\textbf{Typing}) $\uPhi=\uPhi', \uPhyp{\tsmv}{a}{\tau}{\eparse}$
%         \item $\encodeBody{b}{\ebody}$
%         \item $\evalU{\eparse(\ebody)}{{\lbltxt{SuccessP}}\cdot{\ecand}}$
%         \item $\decodeCEPat{\ecand}{\cpv}$
%         \item (\textbf{Segmentation}) $\segOK{\segof{\cpv}}{b}$
% \end{enumerate}
% \end{theorem}
% \begin{proof} By rule induction over Rules (\ref{rules:patExpands}). The only rule that applies is Rule (\ref{rule:patExpands-apuptsm}). The conclusions are premises of this rule.
% \end{proof}
% \endgroup