
\section{\label{sec:named_patches}Named patches}

From this point on, all patches will have unique names.
For the motivation for this decision, see
Appendix~\ref{sec:named_patch_motivation}.

\begin{Iexplanation}
Just to clarify what we mean by ``all patches will have unique names'':
When a patch is created, it is given a globally unique name. However, if
we copy a patch from one place to another, or commute a pair of patches,
then the names remain unchanged.
\end{Iexplanation}

\start{definition}{patch-name}
We define $\nameName$ to tell us the name of a patch, {\ie}
$\name{p}$ is the name of the patch $p$.
\end{Idefinition}

\start{definition}{names-invertible}
Names have an inverse.
\end{Idefinition}

\start{definition}{names-signed}
We say that a name is either positive or negative.

\begin{Iexplanation}
Here's some intuition for what this means: When you record a patch in
darcs, the patch name is positive (think: it adds something to the
repo). If you roll back that patch, then darcs makes the corresponding
negative patch (which removes something from the repo).
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{commute-preserves-names}
$(\pair{p}{q} <-> \pair{q'}{p'})
 =>
 (\name{p} = \name{p'} \wedge
  \name{q} = \name{q'})$
\begin{Iexplanation}
As we said earlier, commuting a patch does not change its name.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{patch-name-inverse-sign}
If $\name{p}$ is positive then $\name{p^}$ is negative.
If $\name{p}$ is negative then $\name{p^}$ is positive.

\begin{Iexplanation}
The inverse of a normal patch is a rollback, and vice-versa.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{patch-inverse-exists}
$\forall p \in \patches .
 \exists p^ \in \patches .
    \name{p} = \name{p^}$
\begin{Iexplanation}
Every patch has an inverse.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{patch-commute-square}
$\begin{array}[t]{@{}l@{}}
 \forall p \in \patches, q \in \patches,
 \forall p' \in \patches, q' \in \patches .\\
    (\pair{p}{q} <-> \pair{q'}{p'}) <=> (\pair{q'^}{p} <-> \pair{p'}{q^})
 \end{array}$
\begin{Iexplanation}
Axiom~\ref{axiom:patch-inverse-exists} tells us that all patches have an
inverse. Therefore we can augment our patch commutation diagram with
inverse patches:\\
\begin{mfpic}[2][1.3]{0}{4}{-2}{2}
    \pointdef{O}(0,0)
    \pointdef{midP}(0.8,1.2)
    \pointdef{midPinv}(1.2,0.8)
    \pointdef{P}(2,2)
    \pointdef{midQ}(0.8,-1.2)
    \pointdef{midQinv}(1.2,-0.8)
    \pointdef{Q}(2,-2)
    \pointdef{midPQ}(3.2,1.2)
    \pointdef{midPQinv}(2.8,0.8)
    \pointdef{midQP}(3.2,-1.2)
    \pointdef{midQPinv}(2.8,-0.8)
    \pointdef{PQ}(4,0)
    \point{\O,\P,\Q,\PQ}
    \arrlab{\O}{\midP}{\P}{br}{$p$}
    \arrlab{\P}{\midPinv}{\O}{tl}{$p^$}
    \arrlab{\P}{\midPQ}{\PQ}{bl}{$q$}
    \arrlab{\PQ}{\midPQinv}{\P}{tr}{$q^$}
    \arrlab{\O}{\midQ}{\Q}{tr}{$q'$}
    \arrlab{\Q}{\midQinv}{\O}{bl}{$q'^$}
    \arrlab{\Q}{\midQP}{\PQ}{tl}{$p'$}
    \arrlab{\PQ}{\midQPinv}{\Q}{br}{$p'^$}
\end{mfpic}\\
This axiom tells us that we can rotate the diagram 90 degrees clockwise
and we again have a valid commutation diagram. The arrows from left to
right along the top are $q'^ p$ and along the bottom are $p' q^$, thus
$\pair{q'^}{p} <-> \pair{p'}{q^}$.

In actual fact, by applying this axiom twice or three times, we can see
that all four of the rotations are equivalent, and thus
$\pair{p'^}{q'^} <-> \pair{q^}{p^}$ and
$\pair{q}{p'^} <-> \pair{p^}{q'}$.
\end{Iexplanation}
\end{Iaxiom}

