
\section{\label{sec:contexted_patches}Contexted patches}

\begin{Idefinition}[contexted-patch]
For all patches $r \in \patches$, $:r$ is a \emph{contexted patch} of $r$.
For all contexted patches $\seq{q} : r$ and patches $p \in \patches$,
$p \seq{q} : r$ is a \emph{contexted patch} of $r$ if and only if
$\pair{p}{\seq{q} r} <-> \fail$ and $\seq{q} \ne p^ \seq{q}'$ for some
sequence $\seq{q}'$.

\begin{Iexplanation}
Sometimes we will want to keep a ``reference'' to a patch $p$.
However, for a patch to be useful we have to know what context it should
be applied in. The purpose of a contexted patch is to keep track of a
patch, and the context in which it applies.

The patch sequence before the colon is the context; the patch after the
colon is the patch that we are interested in.
\end{Iexplanation}
\end{Idefinition}

\begin{Idefinition}[patch-commute-past]
Given a patch $p$ and a contexted patch $\seq{q} : r$, we define $->$,
pronounced \emph{commute past}, thus:\\
$\begin{array}[t]{@{}l@{\quad}l@{}}
 \pair{p}{\seq{q} : r} -> \single{\seq{q}' : r'}&\textrm{if}~
 (\pair{p}{\seq{q}} <-> \pair{\seq{q}'}{p'}) \wedge
 (\pair{p'}{r} <-> \pair{r'}{p''})\\
 \pair{p}{\seq{q} : r} -> \fail&\textrm{otherwise}
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[patch-commute-past-set]
We extend $->$ to work on sets of contexted patches in the natural way,
{\ie} for any patch $p$ and set of contexted patches $S$:\\
$\pair{p}{S} -> \single{\mkset{(\seq{q}' : r')
                 \mid   (\seq{q} : r) \in S
                 \wedge \pair{p}{\seq{q} : r} -> \single{\seq{q}' : r'}}}$\\
if all the commute pasts succeed, and $\pair{p}{S} -> \fail$ otherwise.
\end{Idefinition}

We assume that contexted patches magically maintain their invariant,
{\ie} if we have a patch $p$ and a contexted patch $\seq{q} : r$ then
when we write $p \seq{q} : r$ what we mean is, if
$\pair{p}{\seq{q}:r} -> \single{\seq{q}':r'}$ then $\seq{q}':r'$,
otherwise $p \seq{q} : r$.

\begin{Idefinition}[contexted-patch-conflict]
We define $<X>$, pronounced ``does not conflict with'', such that
$(\seq{p} : q) <X> (\seq{r} : s)$ holds if
$\pair{q^}{\seq{p}^ \seq{r} : s} -> \single{\_}$, and does not hold
otherwise.

\begin{Iexplanation}
Here $\seq{p} : q$ and $\seq{r} : s$ are two contexted patches starting
from the same context. By inverting one of them we can put them into a
single patch sequence $q^ \seq{p}^ \seq{r} s$. By building the contexted
patch $\seq{p}^ \seq{r} : s$ if $\seq{p}$ and $\seq{r}$ both contain a
patch $t$, that patch will be removed (as contexted patches magically
maintain their invariant).

This is almost, but not quite the same thing as saying $\seq{p} q$ and
$\seq{r} s$ can be cleanly merged. For a counter-example, consider
$:t$ and $t:u$. Clearly $t$ and $tu$ can be cleanly merged, giving $tu$,
but $\pair{t^}{t:u} -> \fail$. Likewise, starting with the contexted
patches the other way round, we get $\pair{u^}{t^:t} -> \fail$.
\end{Iexplanation}
% XXX Proove that this is symmetric
\end{Idefinition}

