[darcs-devel] [patch2165] stop testing the internals of Prim.commute

[Ben Franksen]

Ben Franksen <ben.franksen at online.de> added the comment:

> I did look around for any properties that seemed to be exact duplicates, but
> it wasn't a very thorough search. I'm not adding anything new, just
> specialising what was already being run for the "commutex" case of
> subcommutes to be a normal property.

Okay, I failed to see that immediately.

> Very happy to drop them entirely if they are duplicates.

propCommuteFailurePrim is contained in Generic.commuteInverses
propReadShow is Generic.showRead
propCommuteTwice is Generic.recommute
propCommuteEitherWay is contained in Generic.commuteInverses
propCommuteEitherOrder is Generic.permutivity
...

and so on.

D.T.Patch.Arbitrary.Generic mostly covers all known generic patch
properties. Indeed, some of the properties in there are even redundant
(e.g. mergeEitherWay, see the haddocks).

The squareCommuteLaw got me thinking, though. This is in the two
properties propCommuteInversePrim and propPatchAndInverseIsIdentity
(both are badly named). However, the way it is formulated here checks
that we don't have a conflict. That is, it uses David's original
formulation of the law: if AB<-->B'A' *and* A^B' commutes, then it
commutes to BA'^. This makes it applicable to mergable patches (i.e.
non-prims) if they are invertible. I think a modern version that doesn't
rely on invertibility could be stated as a kind of partial inverse of
the mergeCommute law: if  AB'<-->BA', and
cleanMerge(A\/B)=Just(B''/\A'') then B''=B' and A''=A'. This is
currently missing from the Generic properties and it should be added and
tested. My fault, actually: when we dropped invertibility frommergable
patches I failed to define testable properties for cleanMerge instead.

__________________________________
Darcs bug tracker <bugs at darcs.net>
<http://bugs.darcs.net/patch2165>
__________________________________