[darcs-devel] V3.commuteNoConflicts side conditions

[Ganesh Sittampalam]

Following up to myself:

>>> If so, it suggests to me that once we have established that p and q >>> commute - i.e. that commutePast has succeded - any other commute >>>
failures should be errors rather than just causing commuteNoConflicts>>>
to return Nothing.>>
>> Hmm. Indeed, the patches referenced by the set of conflicts y must live>> somewhere in the past of p, so for p to become adjacent to the>>
conflictor, p must have already been commuted past them. I think Ian>>
made this argument somewhere in the paper where he discusses the
commute>> rules in detail. You could look that up and compare. > I think
this is Definition A.1, catch-commute. But he seems to be> arguing that
we do need the guard. I'll read through it carefully and> report back...
The example Ian gives is one where one of the patches we are trying to
commute was recorded after the conflicts. And of course this kind of
scenario conflicts the simplistic view that commuteNoConflicts should
work if the underlying prims commute - because if you record something
on top of conflicts then you can have a prim in a context it could never
reach with prim patches alone. So it's at least plausible that the
condition as it stands is required.

Ganesh