darcs-2.18.1: harness/Darcs/Test/Patch/Properties/Generic.hs
-- Copyright (C) 2007 David Roundy
--
-- This program is free software; you can redistribute it and/or modify
-- it under the terms of the GNU General Public License as published by
-- the Free Software Foundation; either version 2, or (at your option)
-- any later version.
--
-- This program is distributed in the hope that it will be useful,
-- but WITHOUT ANY WARRANTY; without even the implied warranty of
-- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-- GNU General Public License for more details.
--
-- You should have received a copy of the GNU General Public License
-- along with this program; see the file COPYING. If not, write to
-- the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor,
-- Boston, MA 02110-1301, USA.
module Darcs.Test.Patch.Properties.Generic
( invertInvolution
, inverseComposition
, invertRollback
, recommute
, commuteInverses
, effectPreserving
, inverseDoesntCommute
, permutivity
, squareCommuteLaw
, mergeEitherWay
, showRead
, mergeEitherWayValid
, mergeCommute
, mergeConsistent
, mergeArgumentsConsistent
, coalesceEffectPreserving
, coalesceCommute
, PatchProperty
, MergeProperty
, SequenceProperty
, propPrimPairCoverage
) where
import Darcs.Prelude
import Darcs.Test.Patch.RepoModel
( ModelOf
, RepoModel
, RepoState
, eqModel
, maybeFail
, repoApply
, showModel
)
import Darcs.Test.Util.TestResult
( TestResult
, failed
, maybeFailed
, rejected
, succeeded
)
import Darcs.Test.Patch.WithState ( WithState(..) )
import Darcs.Test.Patch.Arbitrary.Generic
( MightBeEmptyHunk(..)
, MightHaveDuplicate(..)
, TestablePrim
)
import Darcs.Test.Patch.Types.Pair ( Pair(..) )
import Darcs.Test.Patch.Properties.Check ( checkAPatch, Check )
import Control.Monad ( msum )
import Darcs.Patch.Witnesses.Show ( Show2(..), show2 )
import Darcs.Patch.Read ( ReadPatch )
import Darcs.Patch.Show
( ShowPatchBasic, displayPatch, showPatch, ShowPatchFor(ForStorage) )
import Darcs.Patch ()
import Darcs.Patch.Apply ( Apply, ApplyState )
import Darcs.Patch.Commute ( Commute, commute, commuteFL )
import Darcs.Patch.CommuteFn ( CommuteFn )
import Darcs.Patch.Merge ( Merge(merge) )
import Darcs.Patch.Read ( readPatch )
import Darcs.Patch.Invert ( Invert(..) )
import Darcs.Patch.Witnesses.Eq ( Eq2(..), EqCheck(..) )
import Darcs.Patch.Witnesses.Ordered
( (:/\:)(..)
, (:>)(..)
, (:\/:)(..)
, FL(..)
, RL(..)
, mapFL
)
import Darcs.Patch.Witnesses.Sealed ( Sealed(..) )
import Darcs.Util.Printer ( Doc, renderPS, redText, greenText, ($$), text, vcat )
--import Darcs.ColorPrinter ( traceDoc )
import Test.QuickCheck (Property, checkCoverage, cover)
type PatchProperty p = forall wA wB. p wA wB -> TestResult
-- type PairProperty p = forall wA wB. (p :> p) wA wB -> TestResult
type MergeProperty p = forall wA wB. (FL p :\/: FL p) wA wB -> TestResult
type SequenceProperty p = forall wA wB. RL p wA wB -> TestResult
-- | @A^^=A@
invertInvolution :: (Invert p, Eq2 p, ShowPatchBasic p) => p wA wB -> TestResult
invertInvolution p =
let p' = invert (invert p)
in case p =\/= p' of
IsEq -> succeeded
NotEq ->
failed $ redText "p /= p^^, where"
$$ text "##p=" $$ displayPatch p
$$ text "##p^^=" $$ displayPatch p'
displayPatchFL :: ShowPatchBasic p => FL p wX wY -> Doc
displayPatchFL = vcat . mapFL displayPatch
-- | @(AB)^ = B^A^@
inverseComposition :: (Invert p, Eq2 p, ShowPatchBasic p)
=> Pair p wX wY -> TestResult
inverseComposition (Pair (a :> b)) =
let ab = a:>:b:>:NilFL
iab = invert ab
ibia = invert b:>:invert a:>:NilFL
in case iab =\/= ibia of
IsEq -> succeeded
NotEq ->
failed $ redText "ab^ /= b^a^, where"
$$ text "##ab=" $$ displayPatchFL ab
$$ text "##(ab)^=" $$ displayPatchFL iab
$$ text "##b^a^=" $$ displayPatchFL ibia
-- | @ apply A x = y ==> apply A^ y = x@
invertRollback
:: ( ApplyState p ~ RepoState model
, Invert p
, Apply p
, ShowPatchBasic p
, RepoModel model
, model ~ ModelOf p
)
=> WithState p wA wB
-> TestResult
invertRollback (WithState a x b) =
case maybeFail $ repoApply b (invert x) of
Nothing -> failed $ redText "x^ not applicable to b."
Just a' ->
if a' `eqModel` a
then
succeeded
else
failed $
redText "##original repo a:" $$ text (showModel a) $$
redText "##with patch x:" $$ displayPatch x $$
redText "##results in b:" $$ text (showModel b) $$
redText "##but (invert x):" $$ displayPatch (invert x) $$
redText "##applied to b is a':" $$ text (showModel a') $$
redText "##which is not equal to a."
-- | recommute AB ↔ B′A′ if and only if B′A′ ↔ AB
recommute :: (ShowPatchBasic p, Eq2 p, MightHaveDuplicate p)
=> CommuteFn p p
-> Pair p wA wB -> TestResult
recommute c (Pair (x :> y)) =
case c (x :> y) of
Nothing -> rejected
Just (y' :> x')
-- this test unfortunately fails on some V2 patches that contain duplicates
-- after the commute. While in theory the underlying bug should be fixed,
-- we don't know how to and even if we did, it would probably involve a repository
-- migration to a new patch type.
| hasDuplicate y' || hasDuplicate x' -> rejected
| otherwise ->
case c (y' :> x') of
Nothing -> failed (redText "failed, where x" $$ displayPatch x $$
redText ":> y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText ":> x'" $$ displayPatch x')
Just (x'' :> y'') ->
case y'' =/\= y of
NotEq -> failed (redText "y'' =/\\= y failed, where x" $$ displayPatch x $$
redText ":> y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText ":> x'" $$ displayPatch x' $$
redText "x''" $$ displayPatch x'' $$
redText ":> y''" $$ displayPatch y'')
IsEq -> case x'' =/\= x of
NotEq -> failed (
redText "x'' /= x, where x" $$ displayPatch x $$
redText ":> y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText ":> x'" $$ displayPatch x' $$
redText "x''" $$ displayPatch x'' $$
redText ":> y''" $$ displayPatch y'')
IsEq -> succeeded
-- | commuteInverses AB ↔ B′A′ if and only if B⁻¹A⁻¹ ↔ A′⁻¹B′⁻¹
commuteInverses :: (Invert p, ShowPatchBasic p, Eq2 p)
=> CommuteFn p p
-> Pair p wA wB -> TestResult
commuteInverses c (Pair (x :> y)) =
case c (x :> y) of
Nothing ->
-- check that inverse commute neither
case c (invert y :> invert x) of
Just _ -> failed $
redText "second commute did not fail"
$$ redText "x" $$ displayPatch x
$$ redText "y" $$ displayPatch y
$$ redText "invert y" $$ displayPatch (invert y)
$$ redText "invert x" $$ displayPatch (invert x)
Nothing -> succeeded
Just (y' :> x') ->
case c (invert y :> invert x) of
Nothing -> failed $ redText "second commute failed" $$
redText "x" $$ displayPatch x $$ redText "y" $$ displayPatch y $$
redText "invert y" $$ displayPatch (invert y) $$ redText "invert x" $$ displayPatch (invert x)
Just (ix' :> iy') ->
case invert ix' =/\= x' of
NotEq -> failed $ redText "invert ix' /= x'" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText "x'" $$ displayPatch x' $$
redText "ix'" $$ displayPatch ix' $$
redText "iy'" $$ displayPatch iy' $$
redText "invert ix'" $$ displayPatch (invert ix') $$
redText "invert iy'" $$ displayPatch (invert iy')
IsEq -> case y' =\/= invert iy' of
NotEq -> failed $ redText "y' /= invert iy'" $$ displayPatch iy' $$ displayPatch y'
IsEq -> succeeded
-- | effect preserving AB <--> B'A' then effect(AB) = effect(B'A')
effectPreserving
:: ( Apply p
, MightBeEmptyHunk p
, RepoModel model
, model ~ ModelOf p
, ApplyState p ~ RepoState model
, ShowPatchBasic p
)
=> CommuteFn p p
-> WithState (Pair p) wA wB
-> TestResult
effectPreserving _ (WithState _ (Pair (x :> _)) _)
| isEmptyHunk x = rejected
effectPreserving c (WithState r (Pair (x :> y)) r') =
case c (x :> y) of
Nothing -> rejected
Just (y' :> x') ->
case maybeFail $ repoApply r y' of
Nothing ->
failed
$ redText "##x" $$ displayPatch x
$$ redText "##y" $$ displayPatch y
$$ redText "##y'" $$ displayPatch y'
$$ redText "##x'" $$ displayPatch x'
$$ redText "##y' is not applicable to r"
$$ displayModel r
Just r_y' ->
case maybeFail $ repoApply r_y' x' of
Nothing ->
failed
$ redText "##x" $$ displayPatch x
$$ redText "##y" $$ displayPatch y
$$ redText "##y'" $$ displayPatch y'
$$ redText "##x'" $$ displayPatch x'
$$ redText "##x' is not applicable to r_y'"
$$ displayModel r_y'
Just r_y'x' ->
if r_y'x' `eqModel` r'
then succeeded
else
failed
$ redText "##x" $$ displayPatch x
$$ redText "##y" $$ displayPatch y
$$ redText "##y'" $$ displayPatch y'
$$ redText "##x'" $$ displayPatch x'
$$ redText "##r_y'x'"
$$ displayModel r_y'x'
$$ redText "##is not equal to r'"
$$ displayModel r'
where
displayModel = text . showModel
-- | squareCommuteLaw If AB ↔ B′A′ then A⁻¹B′ ↔ BA′⁻¹
squareCommuteLaw
:: (Invert p, ShowPatchBasic p, Eq2 p)
=> CommuteFn p p
-> Pair p wA wB
-> TestResult
squareCommuteLaw c (Pair (x :> y)) =
case c (x :> y) of
Nothing -> rejected
Just (y' :> x') ->
case c (invert x :> y') of
Nothing ->
failed $
redText "-------- original (x :> y)" $$
displayPatch x $$ redText ":>" $$ displayPatch y $$
redText "-------- result (y' :> x')" $$
displayPatch y' $$ redText ":>" $$ displayPatch x' $$
redText "-------- failed commute (invert x :> y')" $$
displayPatch (invert x) $$ redText ":>" $$ displayPatch y'
Just (y'' :> ix') ->
case y'' =\/= y of
NotEq ->
failed $ redText "y'' /= y" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText "x'" $$ displayPatch x' $$
redText "y''" $$ displayPatch y'' $$
redText "ix'" $$ displayPatch ix'
IsEq ->
case x' =\/= invert ix' of
NotEq ->
failed $ redText "x' /= invert ix'" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "y'" $$ displayPatch y' $$
redText "x'" $$ displayPatch x' $$
redText "invert x" $$ displayPatch (invert x) $$
redText "y'" $$ displayPatch y' $$
redText "invert ix'" $$ displayPatch (invert ix')
IsEq -> succeeded
permutivity :: (ShowPatchBasic p, Eq2 p)
=> CommuteFn p p
-> (p :> p :> p) wA wB -> TestResult
permutivity c (x :> y :> z) =
case c (x :> y) of
Nothing -> rejected
Just (y1 :> x1) ->
case c (y :> z) of
Nothing -> rejected
Just (z2 :> y2) ->
case c (x :> z2) of
Nothing ->
case c (x1 :> z) of
Just _ -> failed $ redText "##partial permutivity:" $$
redText "##x" $$ displayPatch x $$
redText "##y" $$ displayPatch y $$
redText "##z" $$ displayPatch z $$
redText "##y1" $$ displayPatch y1 $$
redText "##x1" $$ displayPatch x1 $$
redText "##z2" $$ displayPatch z2 $$
redText "##y2" $$ displayPatch y2 $$
redText "##x :> z2 does not commute, whereas x1 :> z does"
Nothing -> succeeded
Just (z3 :> x3) ->
case c (x1 :> z) of
Nothing ->
failed $ redText "##permutivity1:" $$
redText "##x" $$ displayPatch x $$
redText "##y" $$ displayPatch y $$
redText "##z" $$ displayPatch z $$
redText "##y1" $$ displayPatch y1 $$
redText "##y2" $$ displayPatch y2 $$
redText "##failed commute with z of" $$
redText "##x1" $$ displayPatch x1 $$
redText "##whereas x commutes with" $$
redText "##z2" $$ displayPatch z2
Just (z4 :> x4) ->
--traceDoc (greenText "third commuted" $$
-- greenText "about to commute" $$
-- greenText "y1" $$ displayPatch y1 $$
-- greenText "z4" $$ displayPatch z4) $
case c (y1 :> z4) of
Nothing ->
failed $ redText "##permutivity2:" $$
redText "##failed to commute y1 with z4, where" $$
redText "##x" $$ displayPatch x $$
redText "##y" $$ displayPatch y $$
redText "##z" $$ displayPatch z $$
redText "##y1" $$ displayPatch y1 $$
redText "##x1" $$ displayPatch x1 $$
redText "##z2" $$ displayPatch z2 $$
redText "##y2" $$ displayPatch y2 $$
redText "##z3" $$ displayPatch z3 $$
redText "##x3" $$ displayPatch x3 $$
redText "##z4" $$ displayPatch z4 $$
redText "##x4" $$ displayPatch x4
Just (z3_ :> y4)
| IsEq <- z3_ =\/= z3 ->
--traceDoc (greenText "passed z3") $ error "foobar test" $
case c (y4 :> x4) of
Nothing -> failed $
redText "##permutivity5: input was" $$
redText "##x" $$ displayPatch x $$
redText "##y" $$ displayPatch y $$
redText "##z" $$ displayPatch z $$
redText "##z3" $$ displayPatch z3 $$
redText "##z4" $$ displayPatch z4 $$
redText "##failed commute of" $$
redText "##y4" $$ displayPatch y4 $$
redText "##x4" $$ displayPatch x4 $$
redText "##whereas commute of x and y give" $$
redText "##y1" $$ displayPatch y1 $$
redText "##x1" $$ displayPatch x1
Just (x3_ :> y2_)
| NotEq <- x3_ =\/= x3 ->
failed $
redText "##permutivity6: x3_ /= x3" $$
redText "##x3_" $$ displayPatch x3_ $$
redText "##x3" $$ displayPatch x3
| NotEq <- y2_ =/\= y2 ->
failed $
redText "##permutivity7: y2_ /= y2" $$
redText "##y2_" $$ displayPatch y2_ $$
redText "##y2" $$ displayPatch y2
| otherwise -> succeeded
| otherwise ->
failed $ redText "##permutivity failed" $$
redText "##z3" $$ displayPatch z3 $$
redText "##z3_" $$ displayPatch z3_
mergeArgumentsConsistent :: (ShowPatchBasic p) =>
(forall wX wY . p wX wY -> Maybe Doc)
-> (p :\/: p) wA wB -> TestResult
mergeArgumentsConsistent isConsistent (x :\/: y) =
maybeFailed $
msum [(\z -> redText "mergeArgumentsConsistent x" $$ displayPatch x $$ z) `fmap` isConsistent x,
(\z -> redText "mergeArgumentsConsistent y" $$ displayPatch y $$ z) `fmap` isConsistent y]
mergeConsistent :: (ShowPatchBasic p, Merge p) =>
(forall wX wY . p wX wY -> Maybe Doc)
-> (p :\/: p) wA wB -> TestResult
mergeConsistent isConsistent (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x' ->
maybeFailed $
msum [(\z -> redText "mergeConsistent x" $$ displayPatch x $$ z) `fmap` isConsistent x,
(\z -> redText "mergeConsistent y" $$ displayPatch y $$ z) `fmap` isConsistent y,
(\z -> redText "mergeConsistent x'" $$ displayPatch x' $$ z $$
redText "where x' comes from x" $$ displayPatch x $$
redText "and y" $$ displayPatch y) `fmap` isConsistent x',
(\z -> redText "mergeConsistent y'" $$ displayPatch y' $$ z) `fmap` isConsistent y']
-- merge (A\/B) = B'/\A' <==> merge (B\/A) = A'/\B'
-- or, equivalently,
-- merge . swap_par = swap_antipar . merge
-- where swap_par (A\/B) = B\/A and swap_antipar (A/\B) = B/\A
-- It should not be needed to test this, since it follows from
-- mergeCommute and recommute.
mergeEitherWay :: (Eq2 p, ShowPatchBasic p, Merge p)
=> (p :\/: p) wX wY -> TestResult
mergeEitherWay (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x' ->
case merge (y :\/: x) of
x'' :/\: y''
| IsEq <- x'' =\/= x'
, IsEq <- y'' =\/= y' -> succeeded
| otherwise ->
failed $
redText "##x" $$ displayPatch x $$
redText "##y" $$ displayPatch y $$
redText "##y'" $$ displayPatch y' $$
redText "##x'" $$ displayPatch x' $$
redText "##x''" $$ displayPatch x'' $$
redText "##y''" $$ displayPatch y'' $$
redText "##x'' /= x' or y'' /= y'"
-- merge (A\/B) = B'/\A' ==> AB' <--> BA'
mergeCommute :: (Eq2 p, ShowPatchBasic p, Commute p, Merge p, MightHaveDuplicate p)
=> (p :\/: p) wX wY -> TestResult
mergeCommute (x :\/: y) =
case merge (x :\/: y) of
y' :/\: x'
-- this test unfortunately fails on some V2 patches that contain duplicates
-- after the merge. While in theory the underlying bug should be fixed,
-- we don't know how to and even if we did, it would probably involve a repository
-- migration to a new patch type.
| hasDuplicate x' || hasDuplicate y' -> rejected
| otherwise ->
case commute (x :> y') of
Nothing -> failed $ redText "mergeCommute 1" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "x'" $$ displayPatch x' $$
redText "y'" $$ displayPatch y'
Just (y_ :> x'_)
| IsEq <- y_ =\/= y,
IsEq <- x'_ =\/= x' ->
case commute (y :> x') of
Nothing -> failed $ redText "mergeCommute 2 failed" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "x'" $$ displayPatch x' $$
redText "y'" $$ displayPatch y'
Just (x_ :> y'_)
| IsEq <- x_ =\/= x,
IsEq <- y'_ =\/= y' -> succeeded
| otherwise -> failed $ redText "mergeCommute 3" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "x'" $$ displayPatch x' $$
redText "y'" $$ displayPatch y' $$
redText "x_" $$ displayPatch x_ $$
redText "y'_" $$ displayPatch y'_
| otherwise -> failed $ redText "mergeCommute 4" $$
redText "x" $$ displayPatch x $$
redText "y" $$ displayPatch y $$
redText "x'" $$ displayPatch x' $$
redText "y'" $$ displayPatch y' $$
redText "x'_" $$ displayPatch x'_ $$
redText "y_" $$ displayPatch y_
-- | coalesce effect preserving
coalesceEffectPreserving
:: TestablePrim prim
=> (forall wX wY . (prim :> prim) wX wY -> Maybe (FL prim wX wY))
-> WithState (Pair prim) wA wB -> TestResult
coalesceEffectPreserving j (WithState r (Pair (a :> b)) r') =
case j (a :> b) of
Nothing -> rejected
Just x -> case maybeFail $ repoApply r x of
Nothing -> failed $ redText "x is not applicable to r."
$$ text (showModel r)
$$ displayPatch x
$$ redText "a:>b"
$$ displayPatch a $$ displayPatch b
$$ redText "r'="
$$ text (showModel r')
Just r_x -> if r_x `eqModel` r'
then succeeded
else failed $ redText "r_x /= r', r="
$$ text (showModel r)
$$ redText "a:>b="
$$ displayPatch a $$ displayPatch b
$$ redText "x="
$$ displayPatch x
$$ redText "r'="
$$ text (showModel r')
$$ redText "r_x="
$$ text (showModel r_x)
coalesceCommute
:: (TestablePrim prim, MightBeEmptyHunk prim)
=> (forall wX wY . (prim :> prim) wX wY -> Maybe (FL prim wX wY))
-> (prim :> prim :> prim) wA wB -> TestResult
coalesceCommute _ (a :> _ :> _) | isEmptyHunk a = rejected
coalesceCommute j (a :> b :> c) =
case j (b :> c) of
Nothing -> rejected
Just x ->
case commuteFL (a :> b :>: c :>: NilFL) of
Just (b' :>: c' :>: NilFL :> a') ->
case commuteFL (a :> x) of
Just (x' :> a'') ->
case a'' =/\= a' of
NotEq ->
failed $ greenText "a'' =/\\= a' failed"
$$ display1
$$ display2
IsEq ->
case j (b' :> c') of
Nothing ->
failed $ greenText "coalesce (b':>c') failed"
$$ display1
$$ display2
Just x'' ->
case x' =\/= x'' of
NotEq ->
failed $ greenText "x' =\\/= x'' failed"
$$ display1
$$ display2
$$ display3
IsEq -> succeeded
where
display3 = redText "## coalesce (b':>c') => x''"
$$ displayPatch x''
where
display2 =
redText "## commute (a:>x) => x'" $$ displayPatch x'
$$ redText "## :> a''" $$ displayPatch a''
_ -> failed $ greenText "commute a x failed" $$ display1
where
display1 =
redText "## a" $$ displayPatch a
$$ redText "## b" $$ displayPatch b
$$ redText "## c" $$ displayPatch c
$$ redText "## coalesce (b:>c) => x" $$ displayPatch x
$$ redText "## commute (a:>b:>c) => a'" $$ displayPatch a'
$$ redText "## b'" $$ displayPatch b'
$$ redText "## c'" $$ displayPatch c'
_ -> rejected
-- note: we would normally use displayPatch in the failure message
-- but that would be very misleading here
showRead :: (Show2 p, Eq2 p, ReadPatch p, ShowPatchBasic p) => p wA wB -> TestResult
showRead p =
let ps = renderPS (showPatch ForStorage p)
in case readPatch ps of
Left e -> failed (redText "unable to read " $$ showPatch ForStorage p $$ text e)
Right (Sealed p')
| IsEq <- p' =\/= p -> succeeded
| otherwise ->
failed $
redText "##trouble reading patch p" $$ showPatch ForStorage p $$
redText "##reads as p'" $$
showPatch ForStorage p' $$
redText "##aka" $$
greenText (show2 p) $$
redText "##and" $$
greenText (show2 p')
-- vim: fileencoding=utf-8 :
mergeEitherWayValid
:: (Check p, Merge p, Invert p, ShowPatchBasic p)
=> (p :\/: p) wX wY
-> TestResult
mergeEitherWayValid (p1 :\/: p2) =
case merge (p1 :\/: p2) of
_ :/\: p1' ->
case p2 :>: p1' :>: NilFL of
combo2 ->
case merge (p2 :\/: p1) of
_ :/\: p2' ->
case p1 :>: p2' :>: NilFL of
combo1
| not $ checkAPatch combo1 ->
failed $ text "combo1 invalid: p1="
$$ displayPatch p1
$$ text "p2="
$$ displayPatch p2
$$ text "combo1="
$$ vcat (mapFL displayPatch combo1)
| checkAPatch (invert combo1 :>: combo2 :>: NilFL) ->
succeeded
| otherwise ->
failed $ text "merge both ways invalid: p1="
$$ displayPatch p1
$$ text "p2="
$$ displayPatch p2
$$ text "combo1="
$$ vcat (mapFL displayPatch combo1)
$$ text "combo2="
$$ vcat (mapFL displayPatch combo2)
inverseDoesntCommute :: (ShowPatchBasic p, Invert p, Commute p)
=> p wY1 wY2 -> TestResult
inverseDoesntCommute x =
case commute (x :> invert x) of
Nothing -> succeeded
Just (ix' :> x') -> failed $ redText "x:" $$ displayPatch x
$$ redText "commutes with x^ to ix':" $$ displayPatch ix'
$$ redText "x':" $$ displayPatch x'
-- This property is just to check the coverage of pairs,
-- it doesn't test any actual property.
propPrimPairCoverage :: forall prim wX wY . (Eq2 prim, Commute prim) => Pair prim wX wY -> Property
propPrimPairCoverage (Pair pq) =
checkCoverage $
-- The coverage percentages should pass reliably, but
-- could be dropped a bit if not.
let theKind = classifyCommute pq (commute pq) in
cover 20 (theKind == Failed) "Not Commutable" $
cover 60 (theKind /= Failed) "Commutable" $
cover 20 (theKind == Changed) "Representation Changed" $
True
data CommuteKind = Failed | Unchanged | Changed
deriving (Eq, Show)
classifyCommute :: Eq2 prim => (prim :> prim) wX wY -> Maybe ((prim :> prim) wX wY) -> CommuteKind
classifyCommute _ Nothing = Failed
classifyCommute (p :> q) (Just (q' :> p'))
| unsafeCompare p p' && unsafeCompare q q' = Unchanged
| otherwise = Changed