[darcs-devel] [patch1947] refactor simplifyPush (and 9 more)

[Ben Franksen]

Am 29.09.19 um 15:41 schrieb Ganesh Sittampalam:
>>> Thanks. I have one more question/doc request. It is not at all obvious
>>> to me why
>>>
>>> pushFixupItem
>>>   :: (PrimPatchBase p, Commute p, FromPrim p, Effect p)
>>>   => D.DiffAlgorithm
>>>   -> PushFixupFn
>>>        (RebaseFixup (PrimOf p)) (RebaseItem p)
>>>        (FL (RebaseItem p)) (FL (RebaseFixup (PrimOf p)))
>>>
>>> returns an FL of RebaseItem when what we take as input is a single one.
>>> Also, why does it return a trailing FL of RebaseFixups, when we push
>>> only a single fixup in?
>>
>> I have been searching for a reason for this asymmetry. I think it
>> ultimately comes down to (1) the canonizeFL call in pushFixupFixup and
>> (2) the canonizeNamePair in pushFixupName. And the fact that contrary to
> 
> Not exactly:
> 
> The FL RebaseItem is because if a fixup gets stuck, it gets turned into
> a RebaseItem itself, so now we have an extra one. Similarly if a fixup
> meets a RebaseItem that is its inverse, both it and the RebaseItem
> disappear.

Okay, so this is due to the (legacy?) mixing of fixups with suspended
patches.

> The FL RebaseFixup is temporary: once we move to prims it becomes a
> Maybe2. It's needed at present because after commuting a fixup with a
> named patch, we need to call effect which returns an FL - though in
> practice I think it would always have one element. See commutePrimNamed.

I see, thanks.

> It will always need to be a Maybe2 because a fixup can disappear if it
> meets its own inverse.

See below.

> The canonizeFL and canonizeNamePair are pretty much incidental because
> we only call it when we already have two fixups anyway. See
> pushFixupPrim and pushFixupName.

I will take a look at the functions.

>> Here are some random thoughts I had about this.
>>
>> The types here would be a lot simpler if we were just commuting things.
> 
> As well as commuting and canonizing we cancel inverses, which is one of
> the things that can lead to Maybe results.

Cancelling inverses is subsumed by canonizeFL because that starts with a
sortCoalesceFL which, among other things, cancels inverses.

>> So I wonder if it may be possible to separate that from cononizing. The
>> obvious objection to this idea is that canonizing may make things
>> commute that didn't before. But... we aren't making any use of it, do
>> we? I may be missing something, but it appears to me that during a push,
>> if a commute fails and we canonize, we don't try again to commute the
>> results of the canonization.
> 
> That's a good point. I think that's a bug.
> 
>> This suggests to me that we could perhaps simplify pushing a fixup
>> through an existing FL of fixups by first trying commuteFL, and if that
>> fails we prepend the new fixup and canonizeFL the whole thing. This
>> operation has type  p -> FL p -> FL p i.e. it looks like a cons. But
>> afterwards, assuming there is a suspended patch after the fixups, we
>> should try again to commute everything through the suspended patch,
>> starting with the last fixup.
> 
> I'm not sure this will find everything either. Suppose you have an FL of
> fixups (x1 :>: x2 :>: xs) and (x1 :> x2) doesn't commute with xs, but
> canonize (x1 :> x2) does commute with xs and then with the item
> immediately following the fixups.

Let us postulate an invariant: every FL of fixups is in canonized form.
Commuting a fixup fully through a canonized sequence leaves it
canonized. If that isn't possible we add the fixup at the head and
re-canonize the full sequence. So the invariant is always maintained.

Now, the scenario you describe is impossible: first, we never canonize a
subsequence. And even if we did, that could never make anything commute
that didn't commute before.

> I think the right algorithm is to
> detect if the canonizeFL changes anything and if it does then to try
> pushing all the results of canonizeFL again.

My idea was very similar: instead of checking if the canonizeFL has
changed anything, we reverseFL the complete sequence, then pull off
elements from the end and try to push them into the next item,
accumulating an FL of fixups for which this fails and which when we are
done become the new FL of fixups.

And now that I think a bit more about it, we can drop the initial
attempt to commute the fixup past and instead immediately add it to the
head and then canonize. This means that in this scheme a new fixup is
first pushed /into/ the FL. Afterwards we /extract/ fixups from it to
push them through the next item. So this treats an FL of fixups as a
black box, so ideally we would wrap it in a new type.