
\section{\label{sec:patch_sequences}Patch Sequences}

\begin{Idefinition}[patch-sequences]
We write the empty sequence of patches as $\nopatches$.

We compose patches with juxtaposition.
\end{Idefinition}

\begin{Idefinition}[patch-names]
We define $\namesName$ to tell us the names in a sequence of patches,
{\ie}\\
$\begin{array}[t]{@{}l@{}}
 \names{\nopatches} = \emptyset\\
 \names{p \seq{q}} = \name{p} \cup \names{\seq{q}}
 \end{array}$
\end{Idefinition}

\begin{Idefinition}[context]
A context is a set of names.

\begin{Iexplanation}
When making patch diagrams, we said that the arrows are patches, but
glossed over what the dots are. In fact, these dots are contexts.
Recall our commute diagram, now explicitly annotated with contexts:\\
\begin{mfpic}{0}{4}{-1}{1}
    \pointdef{O}(0,0)
    \pointdef{midP}(0.6,1.4)
    \pointdef{P}(2,2)
    \pointdef{midQ}(0.6,-1.4)
    \pointdef{Q}(2,-2)
    \pointdef{midPQ}(3.4,1.4)
    \pointdef{midQP}(3.4,-1.4)
    \pointdef{PQ}(4,0)
    \point{\O,\P,\Q,\PQ}
    \arrlab{\O}{\midP}{\P}{br}{$p$}
    \arrlab{\P}{\midPQ}{\PQ}{bl}{$q$}
    \arrlab{\O}{\midQ}{\Q}{tr}{$q'$}
    \arrlab{\Q}{\midQP}{\PQ}{tl}{$p'$}
    \tlpointsep{\pointsize}
    \tlabel[cr]\O{$B$}
    \tlabel[bc]\P{$B \cup \mkset{\name{p}}$}
    \tlabel[tc]\Q{$B \cup \mkset{\name{q}}$}
    \tlabel[cl]\PQ{$B \cup \mkset{\name{p}, \name{q}}$}
\end{mfpic}\\
Here we start in a context $B$ and add names to the context as we apply
patches.

Note that adding a name and its inverse to a context does not get us
back to where we started, {\ie} if $a$ is a name and $B$ is a context
(where $a \notin B$ and $a^ \notin B$) then
$B \ne B \union \mkset{a, a^}$.
In actual fact we are a little more lax in our diagrams, as we have
tended to represent $B$ and $B \union \mkset{a, a^}$ with the same dot.
\end{Iexplanation}
\end{Idefinition}

\begin{Idefinition}[patch-sequence-commute]
We extend $<->$ to work with combinations of patches and patch sequences
in the natural way:\\
$\begin{array}[t]{@{}l@{}}
 \pair{p}{q \seq{r}} <-> \pair{q' \seq{r}'}{p'}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{p}{q} <-> \pair{q'}{p''}\\
                        \pair{p''}{\seq{r}} <-> \pair{\seq{r}'}{p'}
                        \end{array}
 \end{array}$\\
$\begin{array}[t]{@{}l@{}}
 \pair{\seq{p} q}{r} <-> \pair{r'}{\seq{p}' q'}\\
    \quad \textrm{ if } \begin{array}[t]{@{}l@{}}
                        \pair{q}{r} <-> \pair{r''}{q'}\\
                        \pair{\seq{p}}{r''} <-> \pair{r'}{\seq{p}'}
                        \end{array}
 \end{array}$\\
$\begin{array}[t]{@{}l@{}}
 \pair{\seq{p} q}{r \seq{s}} <-> \pair{r'' \seq{s}''}{\seq{p}'' q''}\\
    \quad \textrm{ if }
        \begin{array}[t]{@{}l@{}}
        \pair{q}{r} <-> \pair{r'}{q'}\\
        \pair{\seq{p}}{r'} <-> \pair{r''}{\seq{p}'}\\
        \pair{q'}{\seq{s}} <-> \pair{\seq{s}'}{q''}\\
        \pair{\seq{p}'}{\seq{s}'} <-> \pair{\seq{s}''}{\seq{p}''}\\
        \end{array}
 \end{array}$

In all cases, if the above rules don't apply the commute fails.
\end{Idefinition}

\begin{Idefinition}[patch-sequences]
We classify some patch sequences as \emph{sensible}.

\begin{Iexplanation}
For example, the sequence `add file foo; insert ``hello world'' into
foo' is sensible, whereas `insert ``hello world'' into foo' is not
sensible, as it doesn't make sense to insert text into a file without
first adding the file.
\end{Iexplanation}
\end{Idefinition}

\start{axiom}{doing-nothing-is-sensible}
$\nopatches$ is sensible.
\begin{Iexplanation}
If you haven't done anything then you certainly haven't done anything
that isn't sensible.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{sensible-subsequences}
If $\seq{p} q$ is sensible then $\seq{p}$ is sensible.
\begin{Iexplanation}
If you are doing sensible things, then you can stop at any time, and the
rseult will be sensible.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{sensible-prefix-commute}
If $\seq{p} r$ is sensible, $\seq{q}$ is sensible and
$\names{\seq{p}} = \names{\seq{q}}$ then $\seq{q} r$ is sensible.
\begin{Iexplanation}
It doesn't matter how you get to a context (as long as it is via a
sensible route), what you can sensibly do from that context is always
the same.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{commute-preserves-sensibility}
If $\seq{p} q r$ is sensible and $\pair{q}{r} <-> \pair{r'}{q'}$
then $\seq{p} r' q'$ is sensible.
\begin{Iexplanation}
Successful commuting of patches doesn't affect whether a sequence
is sensible.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{sensible-inverse}
If $\seq{p} \seq{q}$ is sensible and all the patches in $\seq{q}$ are
positive then $\seq{p} \seq{q} \seq{q}^$ is sensible.
\begin{Iexplanation}
Undoing patches takes us back to an earlier sensible state.
\end{Iexplanation}
\end{Iaxiom}

\start{axiom}{patch-commute-associates}
$\begin{array}[t]{@{}r@{~}l@{}}
 \multicolumn{2}{@{}l@{}}{
 \forall p \in \patches, q \in \patches, r \in \patches,
         p_q \in \patches, p_r \in \patches, p_{qr} \in \patches,
         q_p \in \patches, q_r \in \patches, q_{pr} \in \patches,
         r_p \in \patches, r_q \in \patches, r_{pq} \in \patches .}\\
    &(\pair{q}{r}           <-> \pair{r_q}{q_r})   \wedge
     (\pair{p}{q}           <-> \pair{q_p}{p_q}) \wedge
     (\pair{p_q}{r}         <-> \pair{r_p}{p_{qr}})\\
 <=>&(\pair{q_p}{r_p}       <-> \pair{r_{pq}}{q_{pr}}) \wedge
     (\pair{q_{pr}}{p_{qr}} <-> \pair{p_r}{q_r}) \wedge
     (\pair{r_{pq}}{p_r}    <-> \pair{p}{r_q})
 \end{array}$
\begin{Iexplanation}
This is much clearer if we consider it in diagramatic form:\\
\begin{mfpic}{0}{3.6}{-0.8}{2.8}
    \tlabelsep{4pt}
    \pointdef{PQR}(0,0)
    \pointdef{PRQ}(0,2)
    \pointdef{RPQ}(1.8,2.8)
    \pointdef{RQP}(3.6,2)
    \pointdef{QRP}(3.6,0)
    \pointdef{QPR}(1.8,-0.8)
    \point{\PQR,\PRQ,\QPR,\QRP,\RPQ,\RQP}
    \tlabel[tr]\PQR{pqr}
    \tlabel[br]\PRQ{prq}
    \tlabel[bc]\RPQ{rpq}
    \tlabel[bl]\RQP{rqp}
    \tlabel[tl]\QRP{qrp}
    \tlabel[tc]\QPR{qpr}
    \lin{\PQR}{\PRQ}
    \lin{\PRQ}{\RPQ}
    \lin{\RPQ}{\RQP}
    \lin{\RQP}{\QRP}
    \lin{\QRP}{\QPR}
    \lin{\QPR}{\PQR}
\end{mfpic}\\
This is not like most of our diagrams; here the dots all represent the
same repository state, and we move from one to the other by commuting
the order of the patches.

We start off with the patch sequence $pqr$.
This axiom says that if $q$ and $r$ commute ({\ie} you can move from the
bottom left to the top left) and $p$ can be commuted past $qr$ (you can
move from bottom left to bottom right), then $q$ and $r$ still commute
after $p$ has been commuted past them (you can move from the bottom
right to the top right), and you can commute $p$ back again (move from
the top right to the top left).
\end{Iexplanation}
\end{Iaxiom}

Sequences will be considered equal if they are equal up to commutation;
in particular, when we talk about something like $\seq{p} \seq{q}$ we
mean ``a sequence $\seq{r}$ which, after some number of commutations, is
equal to $\seq{p} \seq{q}$''.

