> I have noted the open question about whether we can remove
> the intermediate before/after pairs as a conjecture in the
> definition of fullUnwind for Named. I wonder if we should
> anyway make a best efforts attempt to cancel them there,
> even if we don't rely on it succeeding. It's not necessary
> for rebase, as the simplifyPush code will also do it, but
> it might be more elegant.
I think a good way to test your conjecture is to try and unwind every
patch in our darcs repo (e.g. screened), using sortCoalesceFL to squash
the intermediate after/before fixups inside each Named.
An even better way would be to write a property and test it using QC.
However that means writing a new generator for Named patches or perhaps
generalizing the existing one. An investment that will pay off quickly.
If you don't find any counter examples for RepoPatchV3, then I would be
willing to believe it without hard proof. If it fails, then we may learn
something from studying the counter example. If it fails only for
RepoPatchV1 or V2, then we may learn something else from that.
As to structure: I know I suggested to include fullUnwind as a method of
class Conflict instead of a separate class. I am having second thoughts
about that. We are really talking about a new way of representing
conflicts, one with different properties compared to the classical
RepoPatchV1/2/3 types. And I see fullUnwind as a converter between
RepoPatchV1/2/3 and this new patch type.
With your original idea of a separate class Unwind we could avoid the FL
in the return type of fullUnwind and get back
class Unwind p where
fullUnwind :: p wX wY -> Unwound (PrimOf p) wX wY
With that, Named cannot have an instance Unwind, but I think that's
okay. We can add a function instead:
fullUnwindNamed :: Unwind p => Named p wX wY -> Named (Unwound (PrimOf
p)) wX wY
For Rebase you would in turn convert
Named (Unwound (PrimOf p)) -> Named (RebasePatch p) :> FL (PrimOf p)
and I guess this would happen first thing when a Named enters rebase
i.e. on suspend.
To address one TODO comment
-- TODO the comment about context patches meaning a conflict
-- implies that this representation has to be kept normalised
-- We could define that as the context not containing any
-- patches that would commute with the underlying, but is it
-- guaranteed that we can always establish that? When they came
-- from a RepoPatch it ought to be the case, but what about
-- subsequently?
I think this depends on how we view the role that Unwound plays. You
could regard it as merely an intermediate step from RepoPatchV1/2/3
toward some RebasePatch type. In that case it is unnecessary to invest
the effort to establish and maintain such an invariant because you would
do this for RebasePatch anyway. This would be the pragmatic approach and
perfectly okay IMO. If some day we happen to find a different use for
Unwound that needs the invariant, then we can refactor. Until then let's
try and keep things simple.
The other one:
-- TODO perhaps one of the FLs should be an RL, for symmetry
If the trailing fixups are an RL then some operations will become
simpler e.g. commuting a prim past. May cost a bit upfront when we
construct the Unwound, but I guess it will pay off. But again, as long
as Unwound is just an intermediate step toward RebasePatch and you don't
define functions that operate on an Unwound, it hardly matters.
Naming: I am not too fond of "unwind" etc but ATM I cannot think of
anything better.
|
