darcs

Patch 1946 WIP: introduce concept of unwinding a conflict

Title WIP: introduce concept of unwinding a conflict
Superseder Nosy List ganesh
Related Issues
Status needs-screening Assigned To
Milestone

Created on 2019-09-27.15:40:20 by ganesh, last changed 2019-09-27.23:17:10 by bf.

Files
File name Status Uploaded Type Edit Remove
patch-preview.txt ganesh, 2019-09-27.15:40:20 text/x-darcs-patch
unnamed ganesh, 2019-09-27.15:40:20 text/plain
wip_-introduce-concept-of-unwinding-a-conflict.dpatch ganesh, 2019-09-27.15:40:20 application/x-darcs-patch
See mailing list archives for discussion on individual patches.
Messages
msg21638 (view) Author: ganesh Date: 2019-09-27.15:40:20
I've cleaned up my previous fullUnwind code, minus the
commuting/squashing of inverses in the FL/Named instances,
so we can start discussing more of the details, e.g.
names, structure etc.

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.

1 patch for repository darcs-unstable@darcs.net:screened:

patch 2310d46db25c57f3b8a880b0613ac95ce93ac3eb
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Fri Sep 27 16:40:23 BST 2019
  * WIP: introduce concept of unwinding a conflict
  
  This provides a generic way to get at the underlying
  primitive patch in the conflict.
Attachments
msg21641 (view) Author: bf Date: 2019-09-27.17:53:09
> 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.
msg21647 (view) Author: ganesh Date: 2019-09-27.21:58:07
I'm happy to go back to the Unwind class. Do you think this belongs
in a new module or in Darcs.Patch.Conflict?
msg21649 (view) Author: bf Date: 2019-09-27.23:17:10
> I'm happy to go back to the Unwind class. Do you think this belongs
> in a new module or in Darcs.Patch.Conflict?

It would be more in line with how we do things elsewhere to have a
separate module for it. Make it Darcs.Patch.Unwind and put the data type
there, too, and I'll be happy ;-)
History
Date User Action Args
2019-09-27 15:40:20ganeshcreate
2019-09-27 17:53:10bfsetmessages: + msg21641
2019-09-27 21:58:07ganeshsetmessages: + msg21647
2019-09-27 23:17:10bfsetmessages: + msg21649