[darcs-devel] force-commute

[Benjamin Franksen]

I have been experimenting further, though not with V2 patches but with
conflictors a la camp. I went ahead and implemented them, first as in
the paper, and then with inverse conflictors internalized.

Let me shortly re-hash the camp theory of conflictors. A repo patch is
either a prim patch, written [p], or a conflictor, written [e,X,p],
where p is the (contexted) prim patch represented by the conflictor, e
is the effect (a list of prim patches), and X is the set of (contexted)
prim patches which conflict with p. Contexted patches are prim patches
preceded by a sequence of prim patches and are written c:p. They have
some invariants which roughly amount to saying that the context c is
supposed to be minimal, which is maintained by annihilating pp⁻¹ pairs
and commuting patches past the whole thing if possible when adding
anything to the context.

For conflictors, the general rule is that the conflicts and the
contexted patch we represent (that is: all contexted patches that are
contained in the conflictor) are anchored at the /end/ of the effect (by
which I mean that for contexted patches d:q, the patches e,d,q can be
applied in order).

In the paper, inverse conflictors are introduced with a special
constructor. I want to avoid that, though. In darcs and camp until now
conflictors are treated as second class citizens. The user is not
supposed to actually see them and the only place where they are created
is when we merge two conflictors that do /not/ conflict with each other,
and in that case the inverse conflictor is immediately inverted again.
But I want to explore force-commute, which produces inverse conflictors
that remain in the repo and can been seen by the user.

So what I did is to invert the internals of a conflictor, instead, like
this:

(1) [e,X,p]⁻¹ = [e⁻¹,eX⁻¹,ep⁻¹]

Here, X⁻¹ is the set of all x⁻¹ where x is in X. I haven't said yet how
to invert a contexted patch; well, we invert its internals in turn:

    (c:p)⁻¹ = (c⁻¹:p⁻¹)

When inverting a conflictor, we have to add its (old) effect e to all
contexts, so that the new contexted patches are again anchored at the
end of the effect of the (inverted) conflictor. Note that when we invert
the inverse of a conflictor, we add another e⁻¹ to all contexts, but
since inverses annihilate in a contexted patch we really get back the
original conflictor.

I had to actually implement this to understand one simple fact about
conflictors: A normal, un-inverted conflictor only ever refers to
patches in its past i.e. ones to the left of itself. But an inverted
conflictor refers to /future patches/, i.e. ones to the right of itself!

Conflictors (the normal sort) are introduced when we merge patches. Here
is the simplest rule, it applies when we merge two normal patches that
conflict:

    merge ([p],[q]) = ([p⁻¹,{:p},:q],[q⁻¹,{:q},:p])

Here, the contexts of the contexted patches are all still empty.

Now we come to the interesting part of this message.

Suppose we have a repo with two prim patches [p][q], where q depends on
p, that is p⁻¹q <-> fail. If we try to force-commute them, we must first
merge p⁻¹ with q. Since q depends on p, there is no clean
(non-conflicting) merge, so according to the above rule we get

    merge ([p⁻¹],[q]) = ([p,{:p⁻¹},:q],[q⁻¹,{:q},:p⁻¹])

The second conflictor here (the one that goes on top of [q]) is already
a strange beast: it looks like an inverted conflictor (it represents
p⁻¹), but it conflicts with q which is on its left.

The force-commute is then

    [p,{:p⁻¹},:q][q⁻¹,{:q},:p⁻¹]⁻¹
  =
    [p,{:p⁻¹},:q][q,{q⁻¹:q⁻¹},q⁻¹:p]

according to our conflictor inversion formula (1). The first of these
two patches is a normal conflictor representing q and conflicting with
p⁻¹. What bothers me is the second conflictor: its set of conflicts has
the form {q⁻¹:q⁻¹}. This makes no sense and is actually wrong. OTOH, the
camp theory demands that (named) prim patches never commute with
themselves or their inverse, so the q⁻¹ does not automatically disappear
(by being commoted past). I think I need to add another invariant to
contexted patches to avoid this situation, but I am not yet sure what it
needs to look like.

Anyway, looking at the effects is interesting: the first conflictor
represents q and has effect p, the second one represents p and has
effect q. So, these two conflictors do /not/ remove effects! Instead
they /exchange/ the effects of two patches.

This is weird but fascinating and perhaps we can learn something from it.

Cheers
Ben