
\subsection{Merge}

We now define merge for catches.

\begin{Idefinition}[merge]
We write the merge operator for catches as $+$. It cannot fail: It
introduces conflictors instead.\\
$\begin{array}[t]{@{}l@{}}
 \forall (\seq{c} d) \in \repos, (\seq{c} e) \in \repos .\\
 (\name{d} = \name{e}) \vee \\
 \exists d' \in \catches, e' \in \catches .\\
 d + e = \pair{e'}{d'}
 \end{array}$

\begin{Iexplanation}
What we're saying here is that if we have two repos that differ in only
their last patch then we can always merge them.
The two (equal up to commutation) results of the repo merge are
$\seq{c} d e'$ and $\seq{c} e d'$.
\end{Iexplanation}

We define $+$ thus:\\
$\begin{array}{l@{\null\mathop{+}\null}l@{\null\mathop{=}\null}l}
 c & d & \begin{array}[t]{@{}l@{}}
         \pair{d'}{c'}\\
         \qqqquad \textrm{\textbf{if} } \pair{c^}{d} <-> \pair{d'}{c'^}\\
         \end{array}\\
 \patch{p} & \patch{q} & \pair{\conflictor{p^}{\mkset{:p}}{:q}}%
                                      {\conflictor{q^}{\mkset{:q}}{:p}}\\
 \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}}\\
 \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}}\\
 \conflictor{\seq{r} \seq{s}}{W}{x} & \conflictor{\seq{r} \seq{t}}{Y}{z} &
     \begin{array}[t]{@{}l@{}}
     \pair{\conflictor{\seq{t}'}%
                      {\mkset{\seq{t}'^ x} \union (\seq{s}'^ Y)}%
                      {\seq{s}'^ z}}%
          {\conflictor{\seq{s}'}%
                      {\mkset{\seq{s}'^ z} \union (\seq{t}'^ W)}%
                      {\seq{t}'^ x}}\\
     \qqqquad \textrm{\textbf{if} }
              \begin{array}[t]{@{}l@{}}
              \names{\seq{s}} \cap \names{\seq{t}} = \emptyset\\
              \pair{\seq{s}^}{\seq{t}} <-> \pair{\seq{t}'}{\seq{s}'^}
              \end{array}
     \end{array}
 \end{array}$\\
Note that we haven't yet defined $<->$ on catches, but based on how
it works on patches you should have some intuition for what it means.

\begin{Iexplanation}
The first rule handles the case where there is no conflict. This works
just like patch merging.

The second rule handles the case where we have two patches, $p$ and $q$,
that conflict. If we have $p$ in our repo and we pull $q$, then we make
a conflictor that inverts $p$, conflicts with $p$, and represents $q$.

Pulling $p$ into a repo containing $q$ is analogous.

The third rule handles the case where we have a patch $\patch{p}$ in
one repository and a conflictor, $\conflictor{\seq{r}}{X}{y}$ in the
other repository, and they conflict.

If we pull the conflictor into the repository containing the patch then
the conflictor is the first catch to conflict with $p$, so it must
revert it (along with everything it already reverts). It also needs to
record that it conflicts with $p$, along with everything that it
conflicted with before. And finally, it records that its identity is
still $y$.

On the other hand, if we pull the patch into a repo containing the
conflictor, then the patch turns into a conflictor too. It doesn't need
to revert $y$ as it is not the first catch to conflict with it:
everything in $X$ has already conflicted with it (XXX lemma that $X$ is
not empty). Therefore it has no effect. It does need to record that it
conflicts with $y$ (and only $y$). And, of course, it records that its
identity is $p$.

The fourth rule is the same as the third rule, but with the catches in
the opposite order.

The fifth rule handles the case where we have a conflictor in each repo,
and the conflictors also conflict with each other. The mechanics of the
rule are similar to the previous two rules, but we need to do some setup
work before we can apply it. The $x$ conflictor is the first in its repo
to conflict with everything in $\seq{r}\seq{s}$, and the $z$ conflictor
is the first in its repo to conflict with everything in
$\seq{r}\seq{t}$. But if we pull the $z$ into the repo already
containing $y$ then the $z$ conflictor won't be the first catch to
conflict with $\seq{r}$, as $x$ already conflicts with it. So we need to
commute all common patches in the two conflictor effects to the left.
Furthermore, the details of the rule requires that the remaining effects
do not conflict with each other. As merging cannot fail, we will have to
show that this is the case!
\end{Iexplanation}
\end{Idefinition}

