> For now I'm just going to believe this is correct, as I haven't
> understood the core of the V3 logic well enough to know either way.
;-)
What happens here is this: when we commute two conflictors we need to
ensure that we maintain the invariant that a Conflictor reverts only
prims that have not already been reverted by any earlier Conflictor.
The case in question is the non-conflicting commute. We want to commute
A :> B, where effect A = r and effect B = s. We cannot just commute the
effects (r :> s), as this may violate the invariant. Instead we first
need to split r into those prims that B /also/ conflicts with, say c,
and the rest r'. We then commute (r' :> s), getting say (s' :> r'') and
then construct the effect of B' as (c +>+ s') and that of A' as r''.
The initial call to commuteToPrefix does the splitting. The subtlety
here is that what we store in the Conflictor is the effect, i.e.
/inverted/ prims. So when we test membership of PrimPatchIds of elements
of r in the set of PrimPatchIds of those that B conflicts with, we have
to invert either the identifiers from r or those we get from the
conflicts of B.
This was all correct for the case of commuting two Conflictors. For
commuting an inverted Conflictor with a plain Conflictor, I got confused
and thought that -- since the conflictor was already inverted -- I would
not have to invert the PrimPatchIds in the predicate passed to
commuteToPrefix. This was wrong, since we explicitly invert the effect
of the left hand side before passing it to commuteToPrefix, which
cancels the implicit inversion inherent in the inverted conflictor.
I am seriously considering the move from CommuteNoConflicts toward
MergeNoConflicts aka CleanMerge as the primitive notion, as you
suggested a while back. This would relieve us from ever having to handle
the internals of a Rotcilfnoc directly, avoiding mistakes like the one I
made. The direct definition of mergeNoConflicts aka cleanMerge of two
Conflictors is a lot easier to write and understand than the indirect
one of commuteNoConflicts between a Rotcilfnoc and a Conflictor.
|