
\subsection{Commute}

We now define commutation of catches.

\begin{Idefinition}[catch-commute]
We extend $<->$ to operate on catches, as defined below.

We can break the rules down into 3 classes:
Those where the patches are the result of a conflicting merge, and the
conflicts gets reshuffled when they commute;
those where the patches are unrelated, and simply commute freely;
and a fail case for everything else.

% XXX To do:
Currently we don't give the commute rules for anything involving inverse
conflictors. We don't believe that those rules will raise any new
problems, though.

\subsubsection*{Conflicted merge}

First, if we have a patch, and a conflictor that has only conflicted
with that patch, then they swap places:\\
$\pair{\patch{p}}{\conflictor{p^}{\mkset{:p}}{:q}} <->
 \pair{\patch{q}}{\conflictor{q^}{\mkset{:q}}{:p}}$

\begin{Iexplanation}
This should make sense if you consider the result of merging two
patches:\\
$\patch{p} + \patch{q} = \pair{\conflictor{p^}{\mkset{:p}}{:q}}%
                              {\conflictor{q^}{\mkset{:q}}{:p}}$
\end{Iexplanation}

If we have two conflictors, but the one on the right only conflicts with
the one on the left, then it becomes a patch after it has commuted:\\
$\pair{\conflictor{\seq{r}}{X}{y}}%
      {\conflictor{\nopatches}{\mkset{y}}{\seq{r}^:q}} <->
 \pair{\patch{q}}{\conflictor{q^ \seq{r}}{\mkset{\seq{r}^:q} \union X}{y}}$

\begin{Iexplanation}
Again, this follows from the merge:\\
$\conflictor{\seq{r}}{X}{y} + \patch{q}
 = \pair{\conflictor{\nopatches}{\mkset{y}}{\seq{r}^ : q}}%
        {\conflictor{q^ \seq{r}}{\mkset{\seq{r}^ : q} \union X}{y}}$
\end{Iexplanation}

And the inverse of the previous case:\\
$\pair{\patch{p}}{\conflictor{p^ \seq{r}}{\mkset{\seq{r}^:p} \union X}{y}} <->
 \pair{\conflictor{\seq{r}}{X}{y}}%
      {\conflictor{\nopatches}{\mkset{y}}{\seq{r}^:p}}$

\begin{Iexplanation}
Again, this follows from the merge:\\
$\patch{p} + \conflictor{\seq{r}}{X}{y}
 = \pair{\conflictor{p^ \seq{r}}{\mkset{\seq{r}^ : p} \union X}{y}}%
        {\conflictor{\nopatches}{\mkset{y}}{\seq{r}^ : p}}$
\end{Iexplanation}

And now the case where both are conflictors, and conflict with each
other:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\conflictor{\seq{r} \seq{s}}{W}{x}}
      {\conflictor{\seq{t}}{\mkset{\seq{t}^x} \union Y}{z}} <->
 \pair{\conflictor{\seq{r} \seq{t'}}{\seq{s'}Y}{\seq{s'}z}}%
      {\conflictor{\seq{s'}}{\mkset{z} \union \seq{t}^W}{\seq{t}^x}}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{\seq{s}}{\seq{t}} <-> \pair{\seq{t'}}{\seq{s'}}\\
                        \names{\seq{r}^} \subseteq \names{Y}\\
                        \names{\seq{s}^} \cap \names{Y} = \emptyset\\
                        \end{array}
 \end{array}$

\begin{Iexplanation}
XXX Copy the merge rule and rewrite

In this case we just move the conflict from one to the other.
The splitting of the effect of the $z$ conflictor into two parts is the
same as we saw earlier, in the ``unrelated'' conflict-conflictor
commute.
\end{Iexplanation}

\subsubsection*{Unrelated}

First the simple non-conflicted patch case:\\
$\pair{\patch{p}}{\patch{q}} <-> \pair{\patch{q'}}{\patch{p'}}
    \textrm{ if } \pair{p}{q} <-> \pair{q'}{p'}$

\begin{Iexplanation}
If our catches just wrap up patches,
then they commute like the underlying patches.
\end{Iexplanation}

Now commute a conflictor past a patch, where everything goes
smoothly:\\
$\pair{\conflictor{\seq{r}}{X}{y}}{\patch{q}} <->
 \pair{\patch{q'}}{\conflictor{\seq{r'}}{X'}{y'}}
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \pair{\seq{r}}{q} <-> \pair{q'}{\seq{r'}}\\
                  \pair{q^}{y} -> \single{y'}\\
                  \pair{q^}{X} -> \single{X'}\\
                  \end{array}$

\begin{Iexplanation}
XXX explanation and pretty pictures will be later.
\end{Iexplanation}

Next we have the case where the patch and conflictor start off the other
way round:\\
$\pair{\patch{p}}{\conflictor{\seq{r}}{X}{y}} <->
 \pair{\conflictor{\seq{r'}}{X'}{y'}}{\patch{p'}}
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \pair{p}{\seq{r}} <-> \pair{\seq{r'}}{p'}\\
                  \pair{p'}{X} -> \single{X'}\\
                  \pair{p'}{y} -> \single{y'}\\
                  \end{array}$

\begin{Iexplanation}
XXX ditto
\end{Iexplanation}

And the last and most complex of the unrelated cases, commuting a
conflictor past another conflictor:\\
$\begin{array}[t]{@{}l@{}}
 \pair{\conflictor{\seq{r} \seq{s}}{W}{x}}{\conflictor{\seq{t}}{Y}{z}} <->
 \pair{\conflictor{\seq{r} \seq{t'}}{\seq{s'} Y}{z'}}%
      {\conflictor{\seq{s'}}{\seq{t}^ W}{x'}}\\
    \textrm{ if } \begin{array}[t]{@{}l@{}}
                  \names{\seq{r}^} \subseteq \names{Y}\\
                  \names{\seq{s}^} \cap \names{Y} = \emptyset\\
                  \pair{\seq{s}}{\seq{t}} <-> \pair{\seq{t'}}{\seq{s'}}\\
                  x <X> \seq{t} z\\
                  \forall w \in W . (w <X> \seq{t} z)\\
                  \forall y \in Y . (x <X> \seq{t} y)\\
                  \pair{\seq{t}^}{x} -> \single{x'}\\
                  \pair{\seq{s'}}{z} -> \single{z'}\\
                  \end{array}
 \end{array}$

\begin{Iexplanation}
XXX ditto
\end{Iexplanation}

\subsubsection*{Fail}

Finally, if none of the above hold, then\\
$\pair{c}{d} <-> \fail$
\end{Idefinition}

\start{definition}{catch-conflicts}
If $(\seq{c} d) \in \repos$ and $(\seq{c} e) \in \repos$,
We say $d$ \emph{conflicts} with $e$ if and only if
$\pair{d^}{e} <-> \fail$.
\begin{Iexplanation}
XXX
% This mirrors \refDefinition{patch-conflicts}.
\end{Iexplanation}
\end{Idefinition}

