[darcs-users] How to extend a patch theory to fully commute

[James Cook]

== Prologue ==

This is a story about how to extend a patch theory into one where any
sequence of patches can be permuted into any other order.

In particular, this means every merge is a clean merge in the new
theory. One small catch: after a conflict, it's not possible to continue
applying ordinary patches until a special "mark resolved" patch has been
applied to return the repository to a normal state (i.e. a context that
exists in the primitive patch theory). As explained in the remark at the
end, this could be viewed as an advantage, since it helps determine
whether pulling in additional conflicting patches should be considered a
new conflict, or just adding more to the current conflict.

It's long. I'd be happy to get comments even if you've only read a
prefix, and feel free to skip the story parts and just read the
definitions, propositions etc. The main idea is minimal context
addresses, defined in the first two chapters; the rest mostly seems to
fall out of that naturally.

Caveats: I've marked a few places I'm not sure about with the words
"Conjecture" or "Assumption". I suspect Assumption 2 in particular may
be false in the case of Darcs 2 due to duplicate patches, but maybe that
can be addressed somehow. Besides that, this is probably full of
mistakes, and turn out to just not work for some reason. The notation
and proofs are kind of dense. Sorry about that.

The setting: there's a universe of primitive contexts C, and a universe
U of primitive patches which go between contexts in C.

Now, suppose we have a sequence of n patches P1 ... Pn, and the n+1
contexts c0 ... cn which go between them. Our goal is to be able to
permute the patches at will.


== Chapter 1: Context Addresses ==

We begin by extending the set of contexts beyond C. To understand how
this works, let's follow the voyages of Vice Captain (VC) D'Arcs as she
sails the HMS Patchfinder from c0 to cn.

There is an old and well-mapped passage from c0 to cn via the patches P1
... Pn in order. Most VCs are content to follow that when making the
trip, stopping at Contexts c1 ... c(n-1) along the way, where the locals
have well-established businesses restocking ships passing through. Each
context has its own (usually unique) character and appearance,
technically called a Repository State.

VC D'Arcs, unlike the others, likes to use her knowledge of Commutation
to plot a new path from c0 to cn each time. Commutation allows her to
build new sequences of patches Q1 ... Qn, with the same names as P1 ...
Pn but in a different order.

When she follows a new sequence, she finds new contexts along the way.
One month, following a particularly difficult permutation, she came
across a context with an old and beautiful tradition of wireframe
sculpture which the locals claimed had magical properties. She keeps in
her quarters a top in the form of a wireframe cube that she obtained on
that trip.

When a newly-discovered context is notable, VC D'Arcs keeps a record of
its location. She does this as follows: first, she records the overall
starting and ending contexts c0 and cn, and the standard route P1...Pn.
Then, she records the set of names of patches she followed to get from
c0 to that new context (call the new context d).

Definition: A /context address/ is a tuple (a, b, (Qi), X, Y), where a
and b are (primitive) contexts, (Qi) is a sequence of patches going from
a to b, and X and Y are a partition of the names of the patches in (Qi).
The context address /points to/ a context c if there exists a
permutation of (Qi) such that all the patches with names in X come
before patches with names in Y, and c is the after-context of the k-th
patch in the sequence (equivalently, the before-context of the (k+1)-th
patch), where k = |X|.

Example: Suppose a is the starting context (empty repository), Q1
creates the file "foo" starting from a, Q2 creates the file "bar"
starting from there, and b and c are the contexts after P1 and then P2.
The address (a, c, [Q1, Q2], {}, {1, 2}) points to a,
(a, c, [P1, P2], {1}, {2}) points to b, and (a, c, [P1, P2], {2}, {1})
points to the new context you'd get if you applied just Q2 (the
repository has "bar" but not "foo").

Conjecture 1: Every context address points to at most one context.


== Chapter 2: Pseudo-Contexts and Minimal Addresses ==

VC D'Arcs respects the limitations of commutation. Sometimes, a
particular permutation of the patches P1 ... Pn is impossible.

Late one night, D'Arcs put her apprentice Pseudo in charge of navigation
and retired to her quarters. As she drowsily spun her cube-shaped top,
she thought about what strange new contexts she might encounter if she
were able to follow an impossible permutation.

In the morning, she emerged on deck to a strange sight. The Patchfinder
had arrived at a context that looked almost the same as the one they
should have arrived at (context ci), but it had a ghostly, shimmering
quality to it. The repository state was exactly the same as ci's, but
this context had a different name. Pseudo sheepishly explained that he
had mixed up her Patch Order, and had followed patch P(i+1) instead of
Pi.

As it happened, patches Pi and P(i+1) did not commute, so the physics of
commutation should have prevented this mistake. Over the next few weeks,
through trial and error, D'Arcs and Pseudo discovered that whenever
D'Arcs spun her wireframe cube-top, commutation physics was suspended,
and the Patchfinder was able to travel the patches P1...Pn in any order.

VC D'Arcs named the new contexts encountered in this way Pseudo-contexts
after her apprentice, and set to work cataloguing them. She recorded
their locations using context addresses. She had long ago built up a
complete catalogue of all contexts that could be reached using ordinary
commutation, so she felt it would be redundant to store the full
addresses of the new Pseudo-contexts. Instead, to record the address of
a Pseudo-context d, she would start by finding a pair of ordinary
contexts that was as close as possible to the Pseudo-context, and write
the address of d relative to that instead of the usual extreme contexts
c0 and cn. She called these "minimal addresses".

Definition: A context address (a, b, (Qi), X, Y) is /minimal/ if it is
impossible (in the primitive patch theory) to commute the sequence (Qi)
so that it begins with a patch in X or ends with a patch in Y.

Definition: Two minimal context addresses are /equivalent/ if they share
the same starting and ending contexts a, b and sets X, Y, and their
patch sequences are permutations of each other that can be achieved
through primitive commute operations. (In other words, (a, b, (Qi), X,
Y) and (a, b, (Ri), X, Y) are equivalent if (Qi) and (Ri) are
permutations of each other.)

Example: Say a = starting (empty repo), the patch sequence (Qi) is
[create directory "d"; create file "d/f"; create file "d/g"], (Ri) is
the same sequence with the file creation patches switched, and b is the
context after applying all three patches. Then
  (a, b, (Qi), {create "d/f", create "d/g"}, {create "d"})
is equivalent to
  (a, b, (Ri), {create "d/f", create "d/g"}, {create "d"}).

Definition: A minimal context address (a, b, (Qi), X, Y) is /canonical/
if it is not possible (within the primitive patch theory) to permute the
sequence (Qi) to a sequence (Ri) such that the sequence of patch names
in (Ri) is lexicographically earlier than the sequence of patch names in
(Qi).

Remark: Each equivalence class of minimal context addresses contains
exactly one canonical context address. So, we can use canonical
addresses to represent equivalence classes. It doesn't matter how we
choose the canonical addresses, as long as we're consistent (but see
Conjecture 2).

Conjecture 2: There is an efficient algorithm that, given any minimal
context address, finds the equivalent canonical context address.

Remark: Actually, we'll never need to explicitly store a canonical
context address. But our representation of patches will be closely
related, and we definitely want to store those, so we might as well put
the conjecture here.

Definition: Given any primitive patch theory, the /extended context
universe/ is the set of all canonical context addresses. The universe of
contexts from the original patch theory is embedded in this set by
representing a primitive context a with the canonical context
(a, a, [], {}, {}). (Any other element of this set is what VC D'Arcs
called a "Pseudo-context".)

Proposition 1: For every context a (in the original primitive patch
theory), there is exactly one minimal context address pointing to c,
namely the canonical address (a, a, [], {}, {}). (In particular, other
minimal addresses don't point to primitive contexts at all. This builds
our confidence that we've found a reasonable way to extend the set of
contexts.)

Proof: Suppose (a, b, (Qi), X, Y) points to a primitive context c. If X
is nonempty, then there is a way to order the patches (Qi) so that all
the patches in X come before patches in Y, and c is the |X|-th patch in
the sequence. But that ordering starts with a patch in X, so the address
is not minimal. Therefore X must be empty, and by a similar argument, Y
must be empty too. Since the empty sets X and Y partition the names in
(Qi), the sequence must be empty too. QED


== Chapter 3: Patches ==

Now that we've extended the universe of contexts beyond C, we're ready
to extend our universe of patches beyond U.

Landlubbers might think contexts are the important things to address,
but VC D'Arcs lives her true life on the sea of patches. As she tries
out new permutations of the journey from c0 to cn, she will often
encounter a particularly beautiful setting for a patch which she would
like to revisit. She records the location of such a patch in a way
similar to a context address. She first records the start and end
contexts c0 and cn and the standard route P1...Pn, as usual. Then, she
records the name of the patch being addressed, the set of patches she
crossed before crossing that patch, and the set of patches she crossed
after. Sometimes, she will address a sequence of multiple consecutive
patches in this way.

Definition: A /patch sequence address/ is a tuple
(a, b, (Qi), (nj), X, Y), where a and b are (primitive) contexts, (Qi)
is a sequence of (primitive) patches going from a to b, nj is a sequence
of unique names of patches in (Qi), and X and Y are a partition of the
remaining names in (Qi). The patch address /points/ to a patch sequence
(Rj) if each Rj's name is nj and (Qi) can be permuted to a sequence that
includes Rj as a substring and puts all patches with names in X before
(Rj) and all patches with names in Y after (Rj).

Definition: A /patch address/ is a patch sequence address where the
sequence (nj) has length one.

Remark: A context address can be thought of as a patch sequence address
where (nj) is empty.

Having long ago recorded the addresses of all the patches reachable
without her magic cube-top, VC D'Arcs decides to start cataloguing the
patches she has encountered when journeying to, from or between
Pseudo-contexts. She is tired of using the full notation, starting with
c0 and ending with cn, to record patch addresses, so she devises a
scheme for minimal patch addresses, similar to minimal context
addresses.

We define minimal, equivalent and canonical patch sequence addresses the
same ways as for context addresses.

Definition: A patch sequence address (a, b, (Qi), (nj), X, Y) is
/minimal/ if it is impossible (in the primitive patch theory) to commute
the sequence (Qi) so that it begins with a patch in X or ends with a
patch in Y.

Definition: Two minimal patch sequence addresses are /equivalent/ if all
their properties are the same except possibly the patch sequences (Qi),
and those two patch sequences are permutations of each other that can be
achieved in the primitive patch theory.

Definition: A minimal patch sequence address is /canonical/ if (Qi)
can't be permuted (using the primitive patch theory) so that its
sequence of patch names is lexicographically earlier.

Definition: Given any primitive patch theory, the /extended patch
universe/ is the set of all patch addresses. A primitive patch P going
from context a to b is embedded as (a, b, [P], name of P, {}, {}).

Assumption 1: In the primitive patch theory, if two patches have the
same name, the same starting context and the same ending context, then
they are equal.

Proposition 2: For every primitive patch P going from a to b, there is
exactly one minimal patch address pointing to P, namely the canonical
address (a, b, [P], name of P, {}, {}). (In particular, other minimal
patch addresses don't point to primitive patches at all.)

Proof: Suppose (c, d, (Qi), [n], X, Y) points to a primitive patch P
going from a to b. Then there is a way to order the patches in (Qi) that
starts with the patches in X and ends with the patches in Y. If X or Y
is nonempty, that contradicts the minimality condition. So, X and Y are
empty and (Qi) just has one patch, named n. By Assumption 1, that patch
must be equal to P.


== Chapter 4: Relating Patches and Contexts ==

>From here on, I'll use the term "extended context" to mean canonical
context address, "extended patch sequence" to mean canonical patch
sequence address, and "extended patch" to mean an extended patch
sequence of length one. Extended contexts and extended patches form our
new theory.


We'll start by describing a "simplification" process for turning
addresses into minimal addresses.

Definition: A context address (a, b, (Qi), X, Y) is a /simplification/
of a context address (a', b', (Q'i), X', Y') if X and Y are subsets of
(or equal to) X' and Y' and the sequence (Q'i) can be permuted so that
it first follows the patches in X' \ X from a' to a, then follows the
sequence (Qi), then follows the patches in Y' \ Y from b to b'.

Assumption 2: If a context address A has two different simplifications B
and B' that are both canonical addresses, then B = B'. (I suspect this
assumption may be false for Darcs 2 due to duplicate patches.)

Remark: This is essentially saying that if you move as many patches in Y
as possible to the end of the sequence, and as many patches in X as
possible to the beginning, the final set of remaining patches you end up
with is deterministic.

Definition: Given a context address (a, b, (Qi), X, Y), the /minimal
form/ of that address is its (unique, by assumption) canonical
simplification.


Now, we're ready to describe the relation that patches should have to
the contexts that go between them.

Definition: Given a patch sequence address A=(a, b, (Qi), (nj), X, Y),
the /starting context/ of A is the minimal form of (a, b, (Qi), X, Y
union {nj}), and its /ending context/ is the minimal form of (a, b,
(Qi), X union {nj}, Y).

Remark: The starting and ending contexts of an embedded primitive patch
(a, b, [P], name of P, {}, {}) are (a, a, [], {}, {}) and
(b, b, [], {}, {}), i.e. the embeddings of a and b.


Definition: A sequence of n extended patch sequences A1...An is
/consistent/ if for each i from 1..n-1, the ending context of Ai is the
starting context of A(i-1).


== Chapter 5: Permuting and Permutivity ==

Here we'll describe how to apply an arbitrary permutation to any
sequence of patches in our extended theory.

The overall procedure is this:

1. Merge the individual patches to be permuted into a patch sequence
address (a, b, (Qi), (nj), X, Y). (You could merge a pair of adjacent
patches, the whole sequence of patches in the repo, or anything in
between.)

2. Apply an arbitrary permutation to the names (nj), leaving the other
properties a, b, (Qi), X, Y unchanged.

3. Separate the sequence back into individual patches.

In this chapter, we'll describe steps 1 and 3, then prove that
permutivity is satisfied.


We'll start with step 3, separation.

Definition: Let A=(a, b, (Qi), (nj), X, Y) be an patch sequence address
of length n (i.e. (nj) has n names in it). The /separation/ of A is a
sequence of n extended patches. Patch j in the sequence is the minimal
form of (a, b, (Qi), nj, X U {before}, Y U {after}), where {before} is
the set of names that came before j in the sequence and {after} is the
names that came after.

Proposition 3: The separation of any patch sequence address (a, b, (Qi),
(nj), X, Y) is a consistent sequence of patches.

Proof:

Let E_j be the ending context of the j-th patch and S_j be the starting
context of the (j+1)-th patch in the sequence; we will show E_j and S_j
are both equal to the minimal form of M=(a, b, (Qi), [], X U {the first
j names in (nj)}, Y U {the rest of the names}).

Indeed, let the j-th patch be Aj =(c, d, (Ri), [nj], C, D). Note that
this is a simplification of
  (a, b, (Qi), [nj], X U {before}, Y U {after})
which means it is possible to move names in X U {before} to the start
and names in Y U {after} to the end of (Qi). This means
  (c, d, (Ri), [], C U {nj}, D)
is a simplification of M, so they have the same minimal form. The
minimal form of
  (c, d, (Ri), [], C U {nj}, D)
is by definition the ending context of Aj, so the ending context of Aj
equals the minimal form of M.

By a similar argument, the starting context of the (j+1)-th patch also
equals the minimal form of M.

QED


Next, we'll show step 1, merging, can be implemented. We'll start that
by showing how to merge two extended patch sequences.

Proposition 4: Let
  A=(a, b, (Qi), (nj), X, Y)
and
  B=(a', b', (Q'i), (n'j), X', Y')
be two extended patch sequences such that the ending context of A equals
the starting context of B. Then there exists an extended patch sequence
  C=(c, d, (Ri), (nj), V, W)
such that the separation of C equals the separation of A concatenated
with the separation of C.

Proof:

Let M=(e, f, (Si), J, K) be the ending context of A and starting context
of B. Since M is a simplification of (a, b, (Qi), X U {nj}, Y), it is
possible to permute (Qi) so that it starts with the patches in
{nj} U X \ J arranged to go from a to e, then follows the sequence (Si),
then follows the patches in Y \ K arranged to go from b to f. Since A is
minimal, Y \ K must be empty: K = Y and f=b. So, we've permuted (Qi) so
that it equals the concatenation of a sequence Qpre and S.

By a similar argument, J = X', e='a, and we can permute (Q'i) so that it
equals the concatenation of S with a sequence Q'post. Concatenating all
three pieces together, we can take the merged sequence to be
  AB=(a, b', Qpre ++ S ++ Q'post, (nj) ++ (n'j), X, Y').

Now, let's compare the sequence obtained by separating AB to that
obtained by separating A and B separately.

Let j be the index of a patch in A (i.e. a number up to the length of
(nj)). The j-th patch in the separation of A is by definition the
minimal form of
  Aj=(a, b, (Qi), nj, X U {before}, Y U {after}).
The j-th patch in the separation of AB is the minimal form of
  ABj=(a, b', Qpre ++ S ++ Q'post, nj, X U {before}, Y' U {after} U {n'j}).
Note that Qpre ++ S ++ Q'post = Q ++ Q'post, and the set of patches in
Q'post is equal to {n'j} U Y' \ K (and K=Y). So, chopping Q'post off the
end, we see that Aj is a simplification of ABj. So, they both have the
same minimal form.

QED

Corollary: Any consistent sequence (Aj) of extended patches can be
merged into a single extended patch sequence S such that the separation
of S equals (Aj).

Proof:

This follows from the previous proposition: start with the sequence
(Aj), and repeatedly merge adjacent pairs of extended patch sequences
until you have a sequence of just one extended patch sequence. The
proposition ensures that the separation of each step is the same.

QED


Theorem (Permutivity): The three-step permutation operation at the start
of this chapter satisfies permutivity. More precisely: let P1...Pn be a
sequence of extended patches, and consider any sequence of permutation
operations applied to substrings of P1...Pn. Let π be the overall
permutation: that is, the composition of the permutations induced by the
individual steps. Then the resulting sequence of extended patches
depends only on P1...Pn and π.

We'll start with a lemma which says that if you expand the sequence of
patches merged in Step 1 of the sequence, the overall effect is
unchanged.

Lemma: Let P1...Pn be a sequence of extended patches, 1<=i<=j<n, and σ
be a permutation on i..j. Then the following two operations have the
same effect: (a) run the three-step procedure with the patches Pi...Pj
and the permutation σ, and (b) run the three-step permutation with the
patches Pi...P(j+1), and the permutation σ extended to the range
i..(j+1) by setting σ(j+1)=j+1.

Proof:

Merging patches Pi..P(j+1) is the same thing as first merging patches
Pi..Pj and then merging the resulting sequence with P(j+1), since in
both cases the resulting separation is again Pi...Pj.

Therefore, operation (b) is equivalent to the following sequence of
steps:

A. Merge patches Pi..Pj.

B. Merge that with P(j+1).

C. Permute the name sequence (i.e. perform Step 2 of the permutation
operation at the start of this chapter).

D. Separate the result back into a sequence of patches.

Steps B and C in this process commute, since step B does not touch the
name sequence (except to append n(j+1)) and step C touches nothing other
than the name sequence. Therefore, it's the same as the following
sequence:

A'. Merge patches Pi...Pj

B'. Permute the name sequence.

C'. Merge that with P(j+1).

D'. Separate the result back into a sequence of patches.

Now, steps C' and D' are the same as just separating (Proposition 4 says
that doing extra merging before separating doesn't affect the output of
separation. So, this sequence of operations is just the same as
operation (a) in the Lemma statement.

QED

Proof of Theorem:

Each permutation operation consists of a choice of substring i..j of the
current sequence of patches, together with a permutation σ to apply to
that substring.

For each operation, replace the substring i..j to the full sequence
1..n, and extend the permutation σ so that it is the identity function
on 1..(i-1) and (j+1)..n.

(For example, suppose the original operation was a transposition of two
adjacent extended patches, which the three-step procedure implements as:
1. merge the two patches into one sequence; 2. swap the names in that
sequence; and 3. separate. Then we replace that with the following three
steps: 1. merge all n patches into one long sequence; 2. transpose just
the two appropriate names; and 3. separate back into n individual
patches.)

By the Lemma, the new operation has the same effect as the original.
(The Lemma needs to be applied several times, and also this uses the
fact that the Lemma is true when you extend the substring to cover i-1
instead of j+1, but I think that's all straightforward.)

The new sequence of operations looks like this:

A1. Merge all the patches into one sequence (a, b, (Qi), (nj), X, Y)

A2. Apply a permutation to the name sequence (nj).

A3. Separate back into individual patches.

B1. Merge all the patches into once sequence

B2. etc.

Now, steps A3 and B1 together do nothing, and similarly B3 and C1
together do nothing, etc. So, the entire sequence is equivalent to
merging all the patches into one sequence (a, b, (Qi), (nj), X, Y), then
applying all the steps 2 (A2, B2, C2, ...), then separating.

The composition of all the steps 2s applies the overall permutation π.
So, the overall effect of all the operations depends only on π.

QED


== Chapter 6: Effects ==

A patch theory is only useful if we know how to apply patches.

VC D'Arcs and her apprentice Pseudo noticed during their journies that
every Pseudo-context they encountered seemed to be a ghostly mirror
image of some other ordinary context, and in particular had the same
repository state.

They quickly noticed a simple rule of thumb: if they just made a quick
expedition to a single Pseudo-context by permuting two patches Pi and
P(i+1) --- that is, they followed P(i+1) then Pi instead of the usual
order, thus encountering one Pseudo-context on the way --- then the
resulting Pseudo-context always seemed to be a mirror image of the
context ci, as if if they had followed the patches in the order Pi
P(i+1).

However, it took them a long time to discover the general rule. Finally,
one day, Pseudo pieced together the evidence they'd gathered and figured
it out.

Remark: Here, we define an mapping from extended contexts to contexts.
This in turn induces a definition of the effect of an extended patch as
changing the repository from the state in its starting context to its
ending context. Other choices might be possible, but note that the proof
of Proposition 5 in the next chapter assumes this definition.

Definition: We associate a primitive context to every context address
(and in particular to every extended context) (a, b, (Qi), X, Y) using
the following recursive algorithm.

* If X=Y={}, then the context is a (=b). This is an embedded primitive
context.

* If the sequence (Qi) can be permuted so that it starts with a patch P
in X, then we recurse on (a', b, (Q'i), X \ {P}, Y), where a' is ending
context of P and Q'i is the rest of the sequence.

* Similarly, if (Qi) can be permuted so that it ends with a patch P in
Y, then we recurse on (a, b', (Q'i), X, Y \ {P}), where b' is the
starting context of P and (Q'i) is the rest of the sequence.

* Otherwise, we have a minimal context address. Swap X and Y and recurse
on the result (a, b, (Qi), Y, X).


== Chapter 7: We're not done! (How to continue after a conflict) ==

One of D'Arcs's duties as a VC is to help the User create new patches.
One day, while she was visiting a particularly nice Pseudo-context c
which was a mirror-image of the ordinary context c', she encountered a
problem.

The Author, seeing the repository state of c', composed a patch P which
could be applied to c', and asked D'Arcs to append it to the repository.
Unfortunately, the current context of the repository was c and not c',
and so the patch could not be applied.

Remark: In other words, the problem here is that after applying a
conflicted patch, e.g. after a conflicted merge, the user would like to
be able to get back to work applying ordinary patches. The starting
context of a primitive patch is always a primitive context, so it will
be impossible to apply any primitive patches after a conflict.

After some quick thinking, Pseudo managed to find a patch P' which was
equivalent in effect to P. However, this turned out not to be a great
solution, since although P' had the same effect as P, it had the name of
a completely different patch, which was confusing. Moreover, the space
required to store P', and computing power needed to commute it, was more
than one should rightfully expect from a simple primitive patch.

Unable to find a satisfactory way to apply the User's patch to context
c, D'Arcs eventually decided to simply navigate from context c' to the
real context c, and apply the User's patch there.

Proposition 5: For every extended context A=(a, b, (Qi), X, Y) there
exists an extended patch sequence whose starting context is A and whose
ending context is the primitive context c associated with A.

Proof:

Recall that the primitive context c is defined by the recursive
algorithm given at the end of Chapter 6. From the algorithm it is
possible to extract a sequence of patches which lead from b to c. Let
(Ri) be a sequence of copies of those patches, and let (nj) be the names
of those copies.

Our extended patch sequence will be the minimal form of (a, c, (Qi) ++
(Ri), (mk) ++ (nj), X, {}).

The starting context is then the minimal form of (a, c, (Qi) ++ (Ri), X,
{mk} U {nj}). Since the patches in nj are already at the end of the
sequence, that can be simplified to (a, b, (Qi), X, {mk}) = A.

The ending context is the minimal form of (a, c, (Qi) ++ (Ri), X U {mk}
U {nj}, {}). The minimal form of any extended context of the form (_, c,
_, _, {}) is just c.

Note: I think it's possible to make a shorter patch sequence.

QED

Remark: The suggestion here is that every time we arrive at a context
which is not a primitive context, we should apply the patch sequence
from Proposition 5 to restore it to an equivalent primitive context. It
might make sense to make this an explicit, manual step, so that the user
can pull in more arms of the conflict before finally declaring that the
conflict has been resolved --- adding on the Proposition 5 patch could
be considered to be the act that marks it "resolved". One advantage of
this approach is that if there are three conflicting changes P, Q, R all
based on the same primitive context a, then if one user merges P and Q,
and another merges Q and R, and neither invokes the manual "mark
resolved" step, then their repositories can be merged without
introducing much further trouble. On the other hand, if one of them
marks their partial merge (e.g. of just P and Q) as "resolved" and
continues work, then when they merge in R later, the repo will
rightfully tell them there's another conflict to be resolved, because
they didn't account for R in their original resolution.


James