-- Copyright (C) 2002-2003,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. {-# OPTIONS_GHC -cpp -fno-warn-deprecations -fglasgow-exts -fno-warn-orphans #-} {-# LANGUAGE CPP #-} #include "gadts.h" module Darcs.Test.Patch.Test ( propReadShow, propInverseComposition, propCommuteTwice, propInverseValid, propOtherInverseValid, propCommuteEquivalency, propCommuteEitherOrder, propCommuteEitherWay, propMergeIsCommutableAndCorrect, propMergeIsSwapable, propMergeValid, propUnravelThreeMerge, propUnravelSeqMerge, propUnravelOrderIndependent, propSimpleSmartMergeGoodEnough, propElegantMergeGoodEnough, propPatchAndInverseIsIdentity, quickmerge, checkPatch, checkAPatch, verboseCheckAPatch, propResolveConflictsValid, testPatch, propCommuteInverse, subcommutesInverse, subcommutesNontrivialInverse, subcommutesFailure, join_patches ) where import Prelude hiding ( pi ) import System.IO.Unsafe ( unsafePerformIO ) import Test.QuickCheck import Control.Monad ( liftM, liftM2, liftM3, liftM4, replicateM ) import Darcs.Patch.Info ( PatchInfo, patchinfo ) import Darcs.Test.Patch.Check ( PatchCheck, checkMove, removeDir, createDir, isValid, insertLine, fileEmpty, fileExists, deleteLine, modifyFile, createFile, removeFile, doCheck, doVerboseCheck, FileContents(..) ) import Darcs.Patch.RegChars ( regChars ) import ByteStringUtils ( linesPS ) import qualified Data.ByteString as B ( ByteString, null, concat ) import qualified Data.ByteString.Char8 as BC ( break, pack ) import Darcs.Patch.FileName ( fn2fp ) import qualified Data.Map as M ( mapMaybe ) import Darcs.Patch.Patchy ( Commute ) import Darcs.Patch ( addfile, adddir, move, showPatch, hunk, tokreplace, joinPatches, binary, changepref, isMerger, invert, commute, merge, readPatch, resolveConflicts, effect, fromPrims, elegantMerge ) import Darcs.Patch.Core ( Patch(..) ) import Darcs.Patch.Commute ( unravel, merger ) import Darcs.Patch.Prim ( Prim(..), DirPatchType(..), FilePatchType(..), CommuteFunction, Perhaps(..), subcommutes ) import Printer ( renderPS ) import Darcs.Witnesses.Ordered import Darcs.Witnesses.Sealed ( Sealed(Sealed), unsafeUnseal, unseal ) #include "impossible.h" instance Eq Patch where x == y = IsEq == (x =\/= y) instance Eq Prim where x == y = IsEq == (x =\/= y) instance (Commute a, MyEq a) => Eq (FL a) where x == y = IsEq == (x =\/= y) instance Arbitrary Patch where arbitrary = sized arbpatch -- coarbitrary p = coarbitrary (show p) instance Arbitrary Prim where arbitrary = onepatchgen -- coarbitrary = impossible hunkgen :: Gen Prim hunkgen = do i <- frequency [(1,choose (0,5)),(1,choose (0,35)), (2,return 0),(3,return 1),(2,return 2),(1,return 3)] j <- frequency [(1,choose (0,5)),(1,choose (0,35)), (2,return 0),(3,return 1),(2,return 2),(1,return 3)] if i == 0 && j == 0 then hunkgen else liftM4 hunk filepathgen linenumgen (replicateM i filelinegen) (replicateM j filelinegen) tokreplacegen :: Gen Prim tokreplacegen = do f <- filepathgen o <- tokengen n <- tokengen if o == n then return $ tokreplace f "A-Za-z" "old" "new" else return $ tokreplace f "A-Za-z_" o n twofilegen :: (FilePath -> FilePath -> Prim) -> Gen Prim twofilegen p = do n1 <- filepathgen n2 <- filepathgen if n1 /= n2 && (checkAPatch $ fromPrims $ (p n1 n2 :>: NilFL)) then return $ p n1 n2 else twofilegen p chprefgen :: Gen Prim chprefgen = do f <- oneof [return "color", return "movie"] o <- tokengen n <- tokengen if o == n then return $ changepref f "old" "new" else return $ changepref f o n simplepatchgen :: Gen Prim simplepatchgen = frequency [(1,liftM addfile filepathgen), (1,liftM adddir filepathgen), (1,liftM3 binary filepathgen arbitrary arbitrary), (1,twofilegen move), (1,tokreplacegen), (1,chprefgen), (7,hunkgen) ] onepatchgen :: Gen Prim onepatchgen = oneof [simplepatchgen, (invert) `fmap` simplepatchgen] norecursgen :: Int -> Gen Patch norecursgen 0 = PP `fmap` onepatchgen norecursgen n = oneof [PP `fmap` onepatchgen,flatcompgen n] arbpatch :: Int -> Gen Patch arbpatch 0 = PP `fmap` onepatchgen arbpatch n = frequency [(3,PP `fmap` onepatchgen), -- (1,compgen n), (2,flatcompgen n), (0,rawMergeGen n), (0,mergegen n), (1,PP `fmap` onepatchgen) ] -- | Generate an arbitrary list of at least one element unempty :: Arbitrary a => Gen [a] unempty = do a <- arbitrary as <- arbitrary return (a:as) join_patches :: [Patch] -> Patch join_patches = joinPatches . unsafeFL where unsafeFL :: [a] -> FL a unsafeFL [] = NilFL unsafeFL (a:as) = a :>: unsafeFL as rawMergeGen :: Int -> Gen Patch rawMergeGen n = do p1 <- arbpatch len p2 <- arbpatch len if (checkAPatch $ join_patches [invert p1,p2]) && (checkAPatch $ join_patches [invert p2,p1]) then case merge (p2 :\/: p1) of _ :/\: p2' -> return p2' else rawMergeGen n where len = if n < 15 then n`div`3 else 3 mergegen :: Int -> Gen Patch mergegen n = do p1 <- norecursgen len p2 <- norecursgen len if (checkAPatch $ join_patches [invert p1,p2]) && (checkAPatch $ join_patches [invert p2,p1]) then case merge (p2:\/:p1) of p1' :/\: p2' -> if checkAPatch $ join_patches [p1,p2'] then return $ join_patches [p1,p2'] else return $ join_patches [PP $ addfile "Error_in_mergegen", PP $ addfile "Error_in_mergegen", p1,p2,p1',p2'] else mergegen n where len = if n < 15 then n`div`3 else 3 arbpi :: Gen PatchInfo arbpi = do n <- unempty a <- unempty l <- unempty d <- unempty return $ unsafePerformIO $ patchinfo n d a l instance Arbitrary PatchInfo where arbitrary = arbpi -- coarbitrary pi = coarbitrary (show pi) instance Arbitrary B.ByteString where arbitrary = liftM BC.pack arbitrary -- coarbitrary ps = coarbitrary (unpackPS ps) {- plistgen :: Int -> Int -> Gen [Patch] plistgen s n | n <= 0 = return [] | otherwise = do next <- arbpatch s rest <- plistgen s (n-1) return $ next : rest compgen :: Int -> Gen Patch compgen n = do size <- choose (0,n) myp <- liftM join_patches $ plistgen size ((n+1) `div` (size+1)) -- here I assume we only want to consider valid patches... if checkAPatch myp then return myp else compgen n -} flatlistgen :: Int -> Gen [Patch] flatlistgen n = replicateM n (PP `fmap` onepatchgen) flatcompgen :: Int -> Gen Patch flatcompgen n = do myp <- liftM (join_patches . regularizePatches) $ flatlistgen n if checkAPatch myp then return myp else flatcompgen n -- resize to size 25, that means we'll get line numbers no greater -- than 1025 using QuickCheck 2.1 linenumgen :: Gen Int linenumgen = frequency [(1,return 1), (1,return 2), (1,return 3), (3,liftM (\n->1+abs n) (resize 25 arbitrary)) ] tokengen :: Gen String tokengen = oneof [return "hello", return "world", return "this", return "is", return "a", return "silly", return "token", return "test"] toklinegen :: Gen String toklinegen = liftM unwords $ replicateM 3 tokengen filelinegen :: Gen B.ByteString filelinegen = liftM BC.pack $ frequency [(1,map fromSafeChar `fmap` arbitrary),(5,toklinegen), (1,return ""), (1,return "{"), (1,return "}") ] filepathgen :: Gen String filepathgen = liftM fixpath badfpgen fixpath :: String -> String fixpath "" = "test" fixpath p = fpth p fpth :: String -> String fpth ('/':'/':cs) = fpth ('/':cs) fpth (c:cs) = c : fpth cs fpth [] = [] newtype SafeChar = SS Char instance Arbitrary SafeChar where arbitrary = oneof $ map (return . SS) (['a'..'z']++['A'..'Z']++['1'..'9']++"0") fromSafeChar :: SafeChar -> Char fromSafeChar (SS s) = s badfpgen :: Gen String badfpgen = frequency [(1,return "test"), (1,return "hello"), (1,return "world"), (1,map fromSafeChar `fmap` arbitrary), (1,liftM2 (\a b-> a++"/"++b) filepathgen filepathgen) ] {- instance Arbitrary Char where arbitrary = oneof $ map return (['a'..'z']++['A'..'Z']++['1'..'9']++['0','~','.',',','-','/']) -} -- coarbitrary c = coarbitrary (ord c) checkPatch :: Patch -> PatchCheck Bool checkAPatch :: Patch -> Bool checkAPatch p = doCheck $ do checkPatch p checkPatch $ invert p verboseCheckAPatch :: Patch -> Bool verboseCheckAPatch p = doVerboseCheck $ do checkPatch p checkPatch $ invert p checkPatch p | isMerger p = do checkPatch $ fromPrims $ effect p checkPatch (Merger _ _ _ _) = impossible checkPatch (Regrem _ _ _ _) = impossible checkPatch (ComP NilFL) = isValid checkPatch (ComP (p:>:ps)) = checkPatch p >> checkPatch (ComP ps) checkPatch (PP Identity) = isValid checkPatch (PP (Split NilFL)) = isValid checkPatch (PP (Split (p:>:ps))) = checkPatch (PP p) >> checkPatch (PP (Split ps)) checkPatch (PP (FP f RmFile)) = removeFile $ fn2fp f checkPatch (PP (FP f AddFile)) = createFile $ fn2fp f checkPatch (PP (FP f (Hunk line old new))) = do fileExists $ fn2fp f mapM_ (deleteLine (fn2fp f) line) old mapM_ (insertLine (fn2fp f) line) (reverse new) isValid checkPatch (PP (FP f (TokReplace t old new))) = modifyFile (fn2fp f) (tryTokPossibly t old new) -- note that the above isn't really a sure check, as it leaves PSomethings -- and PNothings which may have contained new... checkPatch (PP (FP f (Binary o n))) = do fileExists $ fn2fp f mapM_ (deleteLine (fn2fp f) 1) (linesPS o) fileEmpty $ fn2fp f mapM_ (insertLine (fn2fp f) 1) (reverse $ linesPS n) isValid checkPatch (PP (DP d AddDir)) = createDir $ fn2fp d checkPatch (PP (DP d RmDir)) = removeDir $ fn2fp d checkPatch (PP (Move f f')) = checkMove (fn2fp f) (fn2fp f') checkPatch (PP (ChangePref _ _ _)) = return True regularizePatches :: [Patch] -> [Patch] regularizePatches patches = rpint [] patches where rpint ok_ps [] = ok_ps rpint ok_ps (p:ps) = if checkAPatch (join_patches $ p:ok_ps) then rpint (p:ok_ps) ps else rpint ok_ps ps propInverseComposition :: Patch -> Patch -> Bool propInverseComposition p1 p2 = invert (join_patches [p1,p2]) == join_patches [invert p2, invert p1] propInverseValid :: Patch -> Bool propInverseValid p1 = checkAPatch $ join_patches [invert p1,p1] propOtherInverseValid :: Patch -> Bool propOtherInverseValid p1 = checkAPatch $ join_patches [p1,invert p1] propCommuteTwice :: Patch -> Patch -> Property propCommuteTwice p1 p2 = (doesCommute p1 p2) ==> (Just (p1:>p2) == (commute (p1:>p2) >>= commute)) doesCommute :: Patch -> Patch -> Bool doesCommute p1 p2 = commute (p1:>p2) /= Nothing && (checkAPatch $ join_patches [p1,p2]) propCommuteEquivalency :: Patch -> Patch -> Property propCommuteEquivalency p1 p2 = (doesCommute p1 p2) ==> case commute (p1:>p2) of Just (p2':>p1') -> checkAPatch $ join_patches [p1,p2,invert p1',invert p2'] _ -> impossible propCommuteEitherWay :: Patch -> Patch -> Property propCommuteEitherWay p1 p2 = doesCommute p1 p2 ==> doesCommute (invert p2) (invert p1) propCommuteEitherOrder :: Patch -> Patch -> Patch -> Property propCommuteEitherOrder p1 p2 p3 = checkAPatch (join_patches [p1,p2,p3]) && doesCommute p1 (join_patches [p2,p3]) && doesCommute p2 p3 ==> case commute (p1:>p2) of Nothing -> False Just (p2':>p1') -> case commute (p1':>p3) of Nothing -> False Just (p3':>_) -> case commute (p2':>p3') of Nothing -> False Just (p3'' :> _) -> case commute (p2:>p3) of Nothing -> False Just (p3'a:>_) -> case commute (p1:>p3'a) of Just (p3''a:>_) -> p3''a == p3'' Nothing -> False propPatchAndInverseIsIdentity :: Patch -> Patch -> Property propPatchAndInverseIsIdentity p1 p2 = (checkAPatch $ join_patches [p1,p2]) && (commute (p1:>p2) /= Nothing) ==> case commute (p1:>p2) of Just (p2':>_) -> case commute (invert p1:>p2') of Nothing -> True -- This is a subtle distinction. Just (p2'':>_) -> p2'' == p2 Nothing -> impossible quickmerge :: (Patch :\/: Patch) -> Patch quickmerge (p1:\/:p2) = case merge (p1:\/:p2) of _ :/\: p1' -> p1' propMergeIsCommutableAndCorrect :: Patch -> Patch -> Property propMergeIsCommutableAndCorrect p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> case merge (p2:\/:p1) of p1' :/\: p2' -> case commute (p1:>p2') of Nothing -> False Just (p2'':>p1'') -> p2'' == p2 && p1' == p1'' propMergeIsSwapable :: Patch -> Patch -> Property propMergeIsSwapable p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> case merge (p2:\/:p1) of p1' :/\: p2' -> case merge (p1:\/:p2) of p2''' :/\: p1''' -> p1' == p1''' && p2' == p2''' propMergeValid :: Patch -> Patch -> Property propMergeValid p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> case merge (p2:\/:p1) of _ :/\: p2' -> checkAPatch $ join_patches [invert p1,p2,invert p2,p1,p2'] propSimpleSmartMergeGoodEnough :: Patch -> Patch -> Property propSimpleSmartMergeGoodEnough p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> smartMerge (p2:\/:p1) == simpleSmartMerge (p2:\/:p1) smartMerge :: (Patch :\/: Patch) -> Maybe (Patch :< Patch) smartMerge (p1 :\/: p2) = case simpleSmartMerge (p1:\/:p2) of Nothing -> Nothing Just (p1'a: case simpleSmartMerge (p2 :\/: p1) of Nothing -> Nothing Just (x: case commute (y:>x) of Nothing -> Nothing Just (p2b :> p1'b) -> if p1'a == p1'b && p2a == p2b && p2a == p2 then Just (p1'a :< p2) else Nothing simpleSmartMerge :: (Patch :\/: Patch) -> Maybe (Patch :< Patch) simpleSmartMerge (p1 :\/: p2) = case commute (invert p2 :> p1) of Just (p1':>_) -> case commute (p2:>p1') of Just (p1o:>_) -> if p1o == p1 then Just (p1' :< p2) else Nothing Nothing -> Nothing Nothing -> Nothing propElegantMergeGoodEnough :: Patch -> Patch -> Property propElegantMergeGoodEnough p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> (fst' `fmap` smartMerge (p2:\/:p1)) == (snd'' `fmap` elegantMerge (p2:\/:p1)) fst' :: p :< p -> p fst' (x:<_) = x snd'' :: q :/\: p -> p snd'' (_:/\:x) = x instance Eq p => Eq (p :< p) where (x: Eq (p :> p) where (x:>y) == (x':>y') = x == x' && y == y' instance Show p => Show (p :< p) where show (x :< y) = show x ++ " :< " ++ show y instance Show p => Show (p :> p) where show (x :> y) = show x ++ " :> " ++ show y testPatch :: String testPatch = testStr ++ testNote tp1, tp2 :: Patch tp1 = unsafeUnseal . fst . fromJust . readPatch $ BC.pack "\nmove ./test/test ./hello\n" tp2 = unsafeUnseal . fst . fromJust . readPatch $ BC.pack "\nmove ./test ./hello\n" tp1', tp2' :: Patch tp2' = quickmerge (tp2:\/:tp1) tp1' = quickmerge (tp1:\/:tp2) testNote :: String testNote = (if commute (tp1:>tp2') == Just (tp2:>tp1') then "At least they commutex right.\n" else "Argh! they don't even commutex right.\n") ++(if checkAPatch $ tp2 then "tp2 itself is valid!\n" else "Oh my! tp2 isn't even valid!\n") ++(if checkAPatch $ tp2' then "tp2' itself is valid!\n" else "Aaack! tp2' itself is invalid!\n") ++(if checkAPatch $ join_patches [tp1, tp2'] then "Valid merge tp2'!\n" else "Bad merge tp2'!\n") ++ (if checkAPatch $ join_patches [tp2, tp1'] then "Valid merge tp1'!\n" else "Bad merge tp1'!\n") ++ (if checkAPatch $ join_patches [tp2,tp1',invert tp2',invert tp1] then "Both agree!\n" else "The two merges don't agree!\n") ++ (if checkAPatch $ join_patches [invert tp2, tp1] then "They should be mergable!\n" else "Wait a minute, these guys can't be merged!\n") tp :: Patch tp = tp1' testStr :: String testStr = "Patches are:\n"++(show tp) ++(if checkAPatch tp then "At least the patch itself is valid.\n" else "The patch itself is bad!\n") ++"commute of tp2 and tp1' is "++show (commute (tp2:>tp1'))++"\n" ++"commute of tp1 and tp2' is "++show (commute (tp1:>tp2'))++"\n" {-++ "\nSimply flattened, it is:\n" ++ (show $ mapFL (joinPatches.flattenFL.merger_equivalent) $ flattenFL tp) ++ "\n\nUnravelled, it gives:\n" ++ (show $ map unravel $ flatten tp) ++ "\n\nUnwound, it gives:\n" ++ (show $ mapFL unwind $ flattenFL tp) ++(if checkAPatch (join_patches$ reverse $ unwind tp) then "Unwinding is valid.\n" else "Bad unwinding!\n") ++(if checkAPatch $ join_patches [tp,invert tp] then "Inverse is valid.\n" else "Bad inverse!\n") ++(if checkAPatch $ join_patches [invert tp, tp] then "Other inverse is valid.\n" else "Bad other inverse!\n")-} -- | The conflict resolution code (glump) begins by "unravelling" the merger -- into a set of sequences of patches. Each sequence of patches corresponds -- to one non-conflicted patch that got merged together with the others. The -- result of the unravelling of a series of merges must obviously be -- independent of the order in which those merges are performed. This -- unravelling code (which uses the unwind code mentioned above) uses probably -- the second most complicated algorithm. Fortunately, if we can successfully -- unravel the merger, almost any function of the unravelled merger satisfies -- the two constraints mentioned above that the conflict resolution code must -- satisfy. propUnravelThreeMerge :: Patch -> Patch -> Patch -> Property propUnravelThreeMerge p1 p2 p3 = (checkAPatch $ join_patches [invert p1,p2,invert p2,p3]) ==> (unravel $ unsafeUnseal $ merger "0.0" (unsafeUnseal (merger "0.0" p2 p3)) (unsafeUnseal (merger "0.0" p2 p1))) == (unravel $ unsafeUnseal $ merger "0.0" (unsafeUnseal (merger "0.0" p1 p3)) (unsafeUnseal (merger "0.0" p1 p2))) propUnravelSeqMerge :: Patch -> Patch -> Patch -> Property propUnravelSeqMerge p1 p2 p3 = (checkAPatch $ join_patches [invert p1,p2,p3]) ==> (unravel $ unsafeUnseal $ merger "0.0" p3 $ unsafeUnseal $ merger "0.0" p2 p1) == (unravel $ unsafeUnseal $ merger "0.0" (unsafeUnseal $ merger "0.0" p2 p1) p3) propUnravelOrderIndependent :: Patch -> Patch -> Property propUnravelOrderIndependent p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> (unravel $ unsafeUnseal $ merger "0.0" p2 p1) == (unravel $ unsafeUnseal $ merger "0.0" p1 p2) propResolveConflictsValid :: Patch -> Patch -> Property propResolveConflictsValid p1 p2 = (checkAPatch $ join_patches [invert p1,p2]) ==> and $ map (checkAPatch.(\l-> join_patches [p,mergeList l])) $ resolveConflicts p where p = case merge (p1:\/:p2) of _ :/\: p1' -> join_patches [p2,p1'] mergeList :: [Sealed (FL Prim C(x))] -> Patch mergeList patches = fromPrims `unseal` doml NilFL patches where doml mp (Sealed p:ps) = case commute (invert p :> mp) of Just (mp' :> _) -> doml (effect p +>+ effect mp') ps Nothing -> doml mp ps -- This shouldn't happen for "good" resolutions. doml mp [] = Sealed mp tryTokPossibly :: String -> String -> String -> (Maybe FileContents) -> (Maybe FileContents) tryTokPossibly t o n = liftM $ \contents -> let lines' = M.mapMaybe (liftM B.concat . tryTokInternal t (BC.pack o) (BC.pack n)) (fcLines contents) in contents { fcLines = lines' } tryTokInternal :: String -> B.ByteString -> B.ByteString -> B.ByteString -> Maybe [B.ByteString] tryTokInternal _ _ _ s | B.null s = Just [] tryTokInternal t o n s = case BC.break (regChars t) s of (before,s') -> case BC.break (not . regChars t) s' of (tok,after) -> case tryTokInternal t o n after of Nothing -> Nothing Just rest -> if tok == o then Just $ before : n : rest else if tok == n then Nothing else Just $ before : tok : rest propReadShow :: Patch -> Bool propReadShow p = case readPatch $ renderPS $ showPatch p of Just (Sealed p',_) -> p' == p Nothing -> False -- |In order for merges to work right with commuted patches, inverting a patch -- past a patch and its inverse had golly well better give you the same patch -- back again. propCommuteInverse :: Patch -> Patch -> Property propCommuteInverse p1 p2 = doesCommute p1 p2 ==> case commute (p1 :> p2) of Nothing -> impossible Just (_ :> p1') -> case commute (p1' :> invert p2) of Nothing -> False Just (_ :> p1'') -> p1'' == p1 subcommutesInverse :: [(String, Prim -> Prim -> Property)] subcommutesInverse = zip names (map prop_subcommute cs) where (names, cs) = unzip subcommutes prop_subcommute c p1 p2 = does c p1 p2 ==> case c (p2:< p1) of Succeeded (p1': case c (invert p2:< p1') of Succeeded (p1'': p1'' == p1 && case c (invert p1:< invert p2) of Succeeded (ip2':< ip1') -> case c (p2':< invert p1) of Succeeded (ip1o':< p2o) -> invert ip1' == p1' && invert ip2' == p2' && ip1o' == ip1' && p2o == p2 && p1'' == p1 && ip2x' == ip2' _ -> False _ -> False _ -> False _ -> False subcommutesNontrivialInverse :: [(String, Prim -> Prim -> Property)] subcommutesNontrivialInverse = zip names (map prop_subcommute cs) where (names, cs) = unzip subcommutes prop_subcommute c p1 p2 = nontrivial c p1 p2 ==> case c (p2:< p1) of Succeeded (p1': case c (invert p2:< p1') of Succeeded (p1'': p1'' == p1 && case c (invert p1:< invert p2) of Succeeded (ip2':< ip1') -> case c (p2':< invert p1) of Succeeded (ip1o':< p2o) -> invert ip1' == p1' && invert ip2' == p2' && ip1o' == ip1' && p2o == p2 && p1'' == p1 && ip2x' == ip2' _ -> False _ -> False _ -> False _ -> False subcommutesFailure :: [(String, Prim -> Prim -> Property)] subcommutesFailure = zip names (map prop cs) where (names, cs) = unzip subcommutes prop c p1 p2 = doesFail c p1 p2 ==> case c (invert p1 :< invert p2) of Failed -> True _ -> False doesFail :: CommuteFunction -> Prim -> Prim -> Bool doesFail c p1 p2 = fails (c (p2:: p2 :>: NilFL)) where fails Failed = True fails _ = False does :: CommuteFunction -> Prim -> Prim -> Bool does c p1 p2 = succeeds (c (p2:: p2 :>: NilFL)) where succeeds (Succeeded _) = True succeeds _ = False nontrivial :: CommuteFunction -> Prim -> Prim -> Bool nontrivial c p1 p2 = succeeds (c (p2:: p2 :>: NilFL)) where succeeds (Succeeded (p1' :< p2')) = p1' /= p1 || p2' /= p2 succeeds _ = False