I'll leave this a day or two before screening. Actually
refactoring the prim Commute implementation is for
another discussion, but I don't think these tests
add any value regardless of whether the current code
is kept.

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

patch 0e7ade582c107af13fbfbe076197da91088fe2e9
Author: Ganesh Sittampalam <ganesh@earth.li>
Date:   Sun May  2 08:36:03 BST 2021
  * stop testing the internals of Prim.commute
  
  The current structure of commute isn't very clear and
  should be refactored, but these tests inhibit that.

Attachments

• patch-preview.txt
• stop-testing-the-internals-of-prim_commute.dpatch
• unnamed

>   * stop testing the internals of Prim.commute
>   
>   The current structure of commute isn't very clear and
>   should be refactored, but these tests inhibit that.

I am absolutely d'accord with the idea. But why do add instead
properties that are already defined in Darcs.Test.Patch.Properties.Generic?

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. Very happy to drop them entirely if they
are duplicates.

> 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.

On 05/05/2021 07:49, Ben Franksen wrote:
> 
> Ben Franksen <ben.franksen@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.

FWIW the only ones coming from this specific refactor are:

> propCommuteFailurePrim

As you say this is completely subsumed by Generic.commuteInverses.

> V1Set2.propCommuteInversePrim
> V1Set2.propCommuteNontrivialInversePrim

These two do 4 separate commutes and compares them all. I think it's
probably subsumed by the combination of Generic.commuteInverses and
Generic.squareCommuteLaw, although the preconditions (on
V1Set2.propCommuteInverse*) mean we may get better coverage.

Shall I just drop all three?

We can review/remove the rest in a separate bundle.

First, I think you should screen things as they are. You can always
follow up with replacing redundant properties with the corresponding
ones from the Generic module, either in this or in a separate bundle.

>> V1Set2.propCommuteInversePrim
>> V1Set2.propCommuteNontrivialInversePrim
> 
> These two do 4 separate commutes and compares them all. I think it's
> probably subsumed by the combination of Generic.commuteInverses and
> Generic.squareCommuteLaw,

We cannot test Generic.squareCommuteLaw for RepoPatchV1, since it misses
a precondition. The general squareCommuteLaw only holds for prim patches
i.e. it holds only if there are no conflicts.

At least this is what I always thought to be true. See below.

> the preconditions (on
> V1Set2.propCommuteInverse*) mean we may get better coverage.

Looking closer ar propCommuteInverse I am surprised to see that it seems
to hold. It says (precisely) that A;B'<-->B;A' implies A';B'^<-->_;A.
This is (one formulation of) the squareCommute law. It *cannot* hold if
A and B are in conflict, because the conclusion (the RHS of the
implication) means they are *not* in conflict! So the fact that the
tests succeed suggest to me that either (1) we fail to generated
conflicting pairs or (2) I am completely confused about what it means
for two patches to be in conflict with each other.

It looks indeed as if we do not generate conflicted (sequential) pairs
for RepoPatchV1. So it's not surprising that the square commute law
tests succeed. I thought the generators for RepoPatchV1 were using
D.T.P.A.PatchTree.Tree but apparently they do not. This means that all
the property tests for RepoPatchV1 that take sequential pairs as input
actually only test prim patches. My conclusion is that they are useless
and can be eliminated.

I agree with the rationale and the changes are indeed pretty much 
straight forward and look good.