
\section{\label{sec:catches}Catches and Repos}

Now that we have laid the foundations, it is time to introduce
conflictors. We will now be dealing with another datatype, which may
either be a patch (as previously defined) or a \emph{conflictor}. We
will call these beasts \emph{catches}.

\begin{Iexplanation}
The basic idea is that, if two catches do not conflict, then we can
merge them and get the effect of both, as we described earlier. However,
if they do conflict then when we merge, we get the effect of neither.
Thus to compute the contents of a repository we take the effects of all
the patches that are in the repository and do not conflict with any
other patch in the repository.
\end{Iexplanation}

\begin{Idefinition}[catches]
A catch is either $\patch{p}$ (the non-conflicted patch $p \in \patches$),
$\conflictor{\seq{r}}{X}{\seq{p}:q}$ (a conflicted patch $q \in \patches$), or
$\invconflictor{\seq{r}}{X}{\seq{p}:q}$ (the inverse of a conflicted patch
$q \in \patches$). In both cases, $\seq{r}$ is a sequence of patches,
$X$ is a set of contexted patches, and $\seq{p}:q$ is a contexted patch.
\end{Idefinition}

\begin{Idefinition}[repos]
A \emph{repo} is a sequence of catches (up to commutation, to be
defined later) satisfying some requirements (that, again, we will give
later).

Let $\repos$ be the (possibly infinite) set of repos.
\end{Idefinition}

\begin{Iaside}
Do we really need inverse conflictors, or can we just use conflictors
and invert their internals?
\end{Iaside}

The meaning of $\patch{p}$ is hopefully clear, but what is the meaning
of $\conflictor{\seq{r}}{X}{\seq{p} : q}$? To answer this question, we need to
consider it in the context of a repo.

Suppose we have the repo $\seq{c} \conflictor{\seq{r}}{X}{\seq{p} : q}$.
The effect of the conflictor on the repo is $\seq{r}$, and as we have
already said, $\seq{p} : q$ is the (contexted) patch that this
conflictor represents. $X$ is the set of (contexted) patches in
$\seq{c}$ that $q$ conflicts with.

\begin{Iaside}
In darcs 2, the transitive set of conflicts is stored. I don't believe
that this is needed, and not having it makes things simpler.
Not having it may also mean more things commute.
\end{Iaside}

But how is $\seq{r}$ calculated? $\seq{r}$ is the inverses of the subset
of the patches in $X$ that do not appear in the effect of any conflictor
in $\seq{c}$. In other words, the first catch to conflict with any given
patch reverts that patch.

We can picture a conflictor $\conflictor{\seq{r}}{X}{\seq{p}:q}$ in a repo as
looking like this:\\
\begin{mfpic}{-2}{7}{-3}{4}
    \tlabelsep{3pt}
    \pointdef{from}(-2,0)
    \pointdef{O}(0,0)
    \pointdef{midr}(2,0)
    \pointdef{r}(4,0)
    \pointdef{to}(6,0)
    \pointdef{midp}(4.5,1)
    \pointdef{p}(5,2)
    \pointdef{midq}(5.5,3)
    \pointdef{q}(6,4)
    \pointdef{midXa}(4.5,-1.5)
    \pointdef{Xa}(5,-3)
    \pointdef{Xb}(6,-3)
    \pointdef{Xc}(7,-3)
    %
    \point{\O,\r,\p}
    \arrow\dashed\lin{\from}{\O}
    \arrlab{\O}{\midr}{\r}{tc}{$\seq{r}$}
    \arrlab{\r}{\midp}{\p}{br}{$\seq{p}$}
    \arrlab{\p}{\midq}{\q}{br}{$q$}
    \arrlab{\r}{\midXa}{\Xa}{tr}{$X$}
    \arrow\lin{\r}{\Xb}
    \arrow\lin{\r}{\Xc}
    \arrow\dashed\lin{\r}{\to}
\end{mfpic}

\begin{Idefinition}[catch-effect]
We define $\effectofName$ to tell us the effect that a catch has on the
repo:\\
$\begin{array}[t]{@{}l@{}}
 \effectof{\patch{p}} = p\\
 \effectof{\conflictor{\seq{r}}{X}{y}} = \seq{r}\\
 \effectof{\invconflictor{\seq{r}}{X}{y}} = \seq{r}^\\
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[catch-conflicts]
We define $\catchConflictsName$ to tell us the patches that a catch
conflicts with, {\ie}:\\
$\begin{array}[t]{@{}l@{}}
 \catchConflicts{\patch{p}} = \emptyset\\
 \catchConflicts{\conflictor{\seq{r}}{X}{y}} = \names{X}\\
 \catchConflicts{\invconflictor{\seq{r}}{X}{y}} = \names{X}^\\
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[catch-names]
We extend $\nameName$ and $\namesName$ to work on catches in the natural
way, {\ie}:\\
$\begin{array}[t]{@{}l@{}}
 \name{\patch{p}} = p\\
 \name{\conflictor{\seq{r}}{X}{\seq{p}:q}} = \name{q}\\
 \name{\invconflictor{\seq{r}}{X}{\seq{p}:q}} = \name{q}^\\
 \names{\nocatches} = \emptyset\\
 \names{c \seq{d}} = \mkset{\name{c}} \cup \names{\seq{d}}\\
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[repo-properties]
A repo must satisfy the following:

$\emptyrepo$ is a repo.

$\seq{c} \patch{p}$ is a repo if
\begin{itemize}
\item $\seq{c}$ is a repo
\item $\name{p}$ is positive
\item $\name{p} \notin \names{\seq{c}}$
\item $\effectof{c} p$ is sensible
\end{itemize}

$\seq{c} \seq{d} \seq{e} \conflictor{\seq{r}}{X}{\seq{p} : q}$
is a repo if:
\begin{itemize}
\item $\seq{c} \seq{d} \seq{e}$ is a repo
\item $\seq{e}$ is a sequence of patches ({\ie} there are no conflictors
      in $\seq{e}$)
\item $\effectof{\seq{e}} = \seq{r}^$
\item $\effectof{\seq{d}} = \seq{p}^$
\item $\names{\seq{d} \seq{e}} = \names{X}$
\item Every catch in $d$ is either a conflictor, or in
      $\catchConflicts{d}$
\item $\name{y}$ is positive
\item $\name{y} \notin \names{\seq{c} \seq{d} \seq{e}}$
\item There is no catch $f$ and catch sequence $\seq{g}$ such that
      $\seq{d} \seq{e} = f \seq{g}$ and $f$ does not conflict with
      $\patch{q}$.
\item $\effectof{c} q$ is sensible
\end{itemize}

$\seq{c} \seq{d} \seq{d}^$ is a repo if $\seq{c} \seq{d}$ is a repo and
all of $\names{\seq{d}}$ are positive.
\end{Idefinition}

\begin{Idefinition}[catch-inverse]
We define\\
$\begin{array}[t]{@{}l@{}}
 \patch{p}^ = \patch{p^}\\
 \conflictor{\seq{r}}{X}{y}^ = \invconflictor{\seq{r}}{X}{y}\\
 \invconflictor{\seq{r}}{X}{y}^ = \conflictor{\seq{r}}{X}{y}
 \end{array}$

% XXX this is if we don't have a special inverse comflictor constructor:
% \conflictor{Es}{Z}{Ps:p}^
% = \conflictor{Es^}{\mkset{(Es Qs q : q^) \mid (Qs : q) \in Z}}{Es Ps p:p^}
\end{Idefinition}

\import{}{catch_commute}

\subsection{Merge}

We now define merge; this has no equivalent in the land of patches.

\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 result of the merge
is going to be the repo $c d'$, or equivalently $d c'$.
\end{Iexplanation}

We define $+$ thus:\\
$c + d = \pair{d'}{c'}
 \qquad
 \textrm{ if } \pair{c^}{d} <-> \pair{d'}{c'^}$\\
$\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}}{X \union \mkset{\seq{r}^ : p}}{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}}{X \union \mkset{\seq{r}^ : q}}{y}}$\\
$\begin{array}[t]{@{}l@{}}
 \conflictor{\seq{r} \seq{s}}{W}{x} + \conflictor{\seq{r} \seq{t}}{Y}{z}
 = \pair{\conflictor{\seq{t}'}{(\seq{s}'^ Y)
                  \union \mkset{\seq{t}'^ x}}{\seq{s}'^ z}}%
        {\conflictor{\seq{s}'}{(\seq{t}'^ W)
                  \union \mkset{\seq{s}'^ z}}{\seq{t}'^ x}}\\
 \qquad
 \textrm{ 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}$

\begin{Iexplanation}
The first rule handles the case where there is no conflict when merging,
while the remaining four handle the various conflicting cases.

Note that the third and fourth rules are identical, but with the
arguments and results in the opposite order.

In the final case we need a side condition to ensure that we have
separated out all of the patches that both conflictors are currently
the first to conflict with.
\end{Iexplanation}
\end{Idefinition}

\start{conjecture}{merge-commute-cannot-fail}
The commute in the merge definition cannot fail.
\begin{Iexplanation}
If it fails then something has gone badly wrong, as merge is not allowed
to fail!
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{merge-makes-repos}
If
$(\seq{c} d) \in \repos, (\seq{c} e) \in \repos,
 d' \in \catches, e' \in \catches,
 d + e = \pair{e'}{d'}$
then $\seq{c} d e' \in \repos \wedge \seq{c} e d' \in \repos$.

\begin{Iexplanation}
This states that merging two valid repositories results in another valid
repository.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{merge-effect}
XXX This is rubbish. Fix it. Or just rely on the spec of the effect of
a repo, which we haven't given yet.

If $(\seq{c} d) \in \repos$, $(\seq{c} e) \in \repos$ and
$d + e = \pair{e'}{d'}$ then $\effectof{d e'} = \effectof{e d'}$ if
$\pair{d^}{e} <-> \pair{\_}{\_}$, and $\noeffect$ otherwise.

\begin{Iexplanation}
XXX Actually, I think this is wrong if the two catches are not both
patches.\\
Anyway, the idea is that we should apply the affects if the merge
succeeds, but there should be no net effect if it doesn't.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{merge-symmetric}
If $(\seq{c} d) \in \repos$, $(\seq{c} e) \in \repos$ and
$d + e = \pair{e'}{d'}$ then $e + d = \pair{d'}{e'}$.

\begin{Iexplanation}
Merging $d$ and $e$ is the same as merging $e$ and $d$.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{merge-commute}
If $(\seq{c} d) \in \repos$, $(\seq{c} e) \in \repos$ and
$d + e = \pair{e'}{d'}$ then $\pair{d}{e'} <-> \pair{e}{d'}$.

\begin{Iexplanation}
The two ways of constructing the result of a merge are equivalent.
\end{Iexplanation}
\end{Iconjecture}

\start{conjecture}{merge-commute2}
If
$(\seq{c} d e) \in \repos,
 (\seq{c} d f) \in \repos,
 e + f = \pair{f_r}{e_r},
 \pair{d}{e} <-> \pair{e'}{d_e},
 \pair{d}{f} <-> \pair{f'}{d_f}
$
then\\
$\pair{d_e}{f_r} <-> \pair{\_}{d'},
 \pair{d_f}{e_r} <-> \pair{\_}{d'},
 e' + f' = \pair{f_r'}{e_r'},
 d_e + f_r' = \pair{\_}{d'},
 d_f + e_r' = \pair{\_}{d'}$
 
\begin{Iexplanation}
First, a couple of diagrams may help make it clearer what is going on:\\
\begin{mfpic}{-2}{7}{-2}{2}
    \tlabelsep{3pt}
    \pointdef{O}(0,0)
    \pointdef{midD}(1.5,0)
    \pointdef{D}(3,0)
    \pointdef{midDE}(4,1)
    \pointdef{DE}(5,2)
    \pointdef{midDEF}(6,1)
    \pointdef{DEF}(7,0)
    \pointdef{midDF}(4,-1)
    \pointdef{DF}(5,-2)
    \pointdef{midDFE}(6,-1)
    %
    \point{\O,\D,\DE,\DEF,\DF}
    \arrlab{\O}{\midD}{\D}{tc}{$d$}
    \arrlab{\D}{\midDE}{\DE}{br}{$e$}
    \arrlab{\D}{\midDF}{\DF}{tr}{$f$}
    \arrlab{\DE}{\midDEF}{\DEF}{bl}{$f_r$}
    \arrlab{\DF}{\midDFE}{\DEF}{tl}{$e_r$}
\end{mfpic}
\hspace{5em}
\begin{mfpic}{-2}{7}{-3}{3}
    \tlabelsep{3pt}
    \pointdef{O}(0,0)
    \pointdef{midE}(1,1)
    \pointdef{E}(2,2)
    \pointdef{midEF}(3,1)
    \pointdef{EF}(4,0)
    \pointdef{midF}(1,-1)
    \pointdef{F}(2,-2)
    \pointdef{midFE}(3,-1)
    \pointdef{midD}(5.5,0)
    \pointdef{D}(7,0)
    \pointdef{midED}(3.5,2.5)
    \pointdef{ED}(5,3)
    \pointdef{midFD}(3.5,-2.5)
    \pointdef{FD}(5,-3)
    %
    \point{\O,\E,\EF,\F,\D}
    \arrlab{\O}{\midE}{\E}{br}{$e'$}
    \arrlab{\O}{\midF}{\F}{tr}{$f'$}
    \arrlab{\E}{\midEF}{\EF}{bl}{$f_r'$}
    \arrlab{\F}{\midFE}{\EF}{tl}{$e_r'$}
    \arrlab{\EF}{\midD}{\D}{tc}{$d'$}
    \arrlab{\E}{\midED}{\ED}{br}{$d_e$}
    \arrlab{\F}{\midFD}{\FD}{tr}{$d_f$}
\end{mfpic}\\
This conjecture says that if $d$ commutes past $e$ and $f$ then we can
commute it before or after merging, and get consistent results either
way.
\end{Iexplanation}
\end{Iconjecture}

