darcs-2.4.1: src/Darcs/Test/Patch/Test.hs
-- 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
( prop_read_show,
prop_inverse_composition, prop_commute_twice,
prop_inverse_valid, prop_other_inverse_valid,
prop_commute_equivalency, prop_commute_either_order,
prop_commute_either_way, prop_merge_is_commutable_and_correct,
prop_merge_is_swapable, prop_merge_valid,
prop_unravel_three_merge, prop_unravel_seq_merge,
prop_unravel_order_independent,
prop_simple_smart_merge_good_enough,
prop_elegant_merge_good_enough,
prop_patch_and_inverse_is_identity,
quickmerge, check_patch, check_a_patch, verbose_check_a_patch,
prop_resolve_conflicts_valid,
test_patch, prop_commute_inverse,
subcommutes_inverse, subcommutes_nontrivial_inverse,
subcommutes_failure,
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,
check_move, remove_dir, create_dir,
is_valid, insert_line, file_empty, file_exists,
delete_line, modify_file, create_file, remove_file,
do_check, do_verbose_check, 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,
unravel, merger, elegantMerge )
import Darcs.Patch.Core ( Patch(..) )
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 && (check_a_patch $ 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,raw_merge_gen n),
(0,mergegen n),
(1,PP `fmap` onepatchgen)
]
unempty :: Arbitrary a => Gen [a]
unempty = do
as <- arbitrary
case as of
[] -> unempty
_ -> return as
join_patches :: [Patch] -> Patch
join_patches = joinPatches . unsafeFL
raw_merge_gen :: Int -> Gen Patch
raw_merge_gen n = do p1 <- arbpatch len
p2 <- arbpatch len
if (check_a_patch $ join_patches [invert p1,p2]) &&
(check_a_patch $ join_patches [invert p2,p1])
then case merge (p2 :\/: p1) of
_ :/\: p2' -> return p2'
else raw_merge_gen 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 (check_a_patch $ join_patches [invert p1,p2]) &&
(check_a_patch $ join_patches [invert p2,p1])
then case merge (p2:\/:p1) of
p1' :/\: p2' ->
if check_a_patch $ 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 check_a_patch 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 . regularize_patches) $ flatlistgen n
if check_a_patch 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)
check_patch :: Patch -> PatchCheck Bool
check_a_patch :: Patch -> Bool
check_a_patch p = do_check $ do check_patch p
check_patch $ invert p
verbose_check_a_patch :: Patch -> Bool
verbose_check_a_patch p = do_verbose_check $ do check_patch p
check_patch $ invert p
check_patch p | isMerger p = do
check_patch $ fromPrims $ effect p
check_patch (Merger _ _ _ _) = impossible
check_patch (Regrem _ _ _ _) = impossible
check_patch (ComP NilFL) = is_valid
check_patch (ComP (p:>:ps)) =
check_patch p >> check_patch (ComP ps)
check_patch (PP Identity) = is_valid
check_patch (PP (Split NilFL)) = is_valid
check_patch (PP (Split (p:>:ps))) =
check_patch (PP p) >> check_patch (PP (Split ps))
check_patch (PP (FP f RmFile)) = remove_file $ fn2fp f
check_patch (PP (FP f AddFile)) = create_file $ fn2fp f
check_patch (PP (FP f (Hunk line old new))) = do
file_exists $ fn2fp f
mapM_ (delete_line (fn2fp f) line) old
mapM_ (insert_line (fn2fp f) line) (reverse new)
is_valid
check_patch (PP (FP f (TokReplace t old new))) =
modify_file (fn2fp f) (try_tok_possibly t old new)
-- note that the above isn't really a sure check, as it leaves PSomethings
-- and PNothings which may have contained new...
check_patch (PP (FP f (Binary o n))) = do
file_exists $ fn2fp f
mapM_ (delete_line (fn2fp f) 1) (linesPS o)
file_empty $ fn2fp f
mapM_ (insert_line (fn2fp f) 1) (reverse $ linesPS n)
is_valid
check_patch (PP (DP d AddDir)) = create_dir $ fn2fp d
check_patch (PP (DP d RmDir)) = remove_dir $ fn2fp d
check_patch (PP (Move f f')) = check_move (fn2fp f) (fn2fp f')
check_patch (PP (ChangePref _ _ _)) = return True
regularize_patches :: [Patch] -> [Patch]
regularize_patches patches = rpint [] patches
where rpint ok_ps [] = ok_ps
rpint ok_ps (p:ps) =
if check_a_patch (join_patches $ p:ok_ps)
then rpint (p:ok_ps) ps
else rpint ok_ps ps
prop_inverse_composition :: Patch -> Patch -> Bool
prop_inverse_composition p1 p2 =
invert (join_patches [p1,p2]) == join_patches [invert p2, invert p1]
prop_inverse_valid :: Patch -> Bool
prop_inverse_valid p1 = check_a_patch $ join_patches [invert p1,p1]
prop_other_inverse_valid :: Patch -> Bool
prop_other_inverse_valid p1 = check_a_patch $ join_patches [p1,invert p1]
prop_commute_twice :: Patch -> Patch -> Property
prop_commute_twice p1 p2 =
(does_commute p1 p2) ==> (Just (p1:>p2) == (commute (p1:>p2) >>= commute))
does_commute :: Patch -> Patch -> Bool
does_commute p1 p2 =
commute (p1:>p2) /= Nothing && (check_a_patch $ join_patches [p1,p2])
prop_commute_equivalency :: Patch -> Patch -> Property
prop_commute_equivalency p1 p2 =
(does_commute p1 p2) ==>
case commute (p1:>p2) of
Just (p2':>p1') -> check_a_patch $ join_patches [p1,p2,invert p1',invert p2']
_ -> impossible
prop_commute_either_way :: Patch -> Patch -> Property
prop_commute_either_way p1 p2 =
does_commute p1 p2 ==> does_commute (invert p2) (invert p1)
prop_commute_either_order :: Patch -> Patch -> Patch -> Property
prop_commute_either_order p1 p2 p3 =
check_a_patch (join_patches [p1,p2,p3]) &&
does_commute p1 (join_patches [p2,p3]) &&
does_commute 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
prop_patch_and_inverse_is_identity :: Patch -> Patch -> Property
prop_patch_and_inverse_is_identity p1 p2 =
(check_a_patch $ 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'
prop_merge_is_commutable_and_correct :: Patch -> Patch -> Property
prop_merge_is_commutable_and_correct p1 p2 =
(check_a_patch $ 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''
prop_merge_is_swapable :: Patch -> Patch -> Property
prop_merge_is_swapable p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
case merge (p2:\/:p1) of
p1' :/\: p2' ->
case merge (p1:\/:p2) of
p2''' :/\: p1''' -> p1' == p1''' && p2' == p2'''
prop_merge_valid :: Patch -> Patch -> Property
prop_merge_valid p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
case merge (p2:\/:p1) of
_ :/\: p2' ->
check_a_patch $ join_patches [invert p1,p2,invert p2,p1,p2']
prop_simple_smart_merge_good_enough :: Patch -> Patch -> Property
prop_simple_smart_merge_good_enough p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
smart_merge (p2:\/:p1) == simple_smart_merge (p2:\/:p1)
smart_merge :: (Patch :\/: Patch) -> Maybe (Patch :< Patch)
smart_merge (p1 :\/: p2) =
case simple_smart_merge (p1:\/:p2) of
Nothing -> Nothing
Just (p1'a:<p2a) ->
case simple_smart_merge (p2 :\/: p1) of
Nothing -> Nothing
Just (x:<y) ->
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
simple_smart_merge :: (Patch :\/: Patch) -> Maybe (Patch :< Patch)
simple_smart_merge (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
prop_elegant_merge_good_enough :: Patch -> Patch -> Property
prop_elegant_merge_good_enough p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
(fst' `fmap` smart_merge (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:<y) == (x':<y') = x == x' && y == y'
instance Eq p => 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
test_patch :: String
test_patch = test_str ++ test_note
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)
test_note :: String
test_note = (if commute (tp1:>tp2') == Just (tp2:>tp1')
then "At least they commutex right.\n"
else "Argh! they don't even commutex right.\n")
++(if check_a_patch $ tp2
then "tp2 itself is valid!\n"
else "Oh my! tp2 isn't even valid!\n")
++(if check_a_patch $ tp2'
then "tp2' itself is valid!\n"
else "Aaack! tp2' itself is invalid!\n")
++(if check_a_patch $ join_patches [tp1, tp2']
then "Valid merge tp2'!\n"
else "Bad merge tp2'!\n")
++ (if check_a_patch $ join_patches [tp2, tp1']
then "Valid merge tp1'!\n"
else "Bad merge tp1'!\n")
++ (if check_a_patch $ join_patches [tp2,tp1',invert tp2',invert tp1]
then "Both agree!\n"
else "The two merges don't agree!\n")
++ (if check_a_patch $ 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'
test_str :: String
test_str = "Patches are:\n"++(show tp)
++(if check_a_patch 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 check_a_patch (join_patches$ reverse $ unwind tp)
then "Unwinding is valid.\n"
else "Bad unwinding!\n")
++(if check_a_patch $ join_patches [tp,invert tp]
then "Inverse is valid.\n"
else "Bad inverse!\n")
++(if check_a_patch $ 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.
prop_unravel_three_merge :: Patch -> Patch -> Patch -> Property
prop_unravel_three_merge p1 p2 p3 =
(check_a_patch $ join_patches [invert p1,p2,invert p2,p3]) ==>
(unravel $ merger "0.0" (merger "0.0" p2 p3) (merger "0.0" p2 p1)) ==
(unravel $ merger "0.0" (merger "0.0" p1 p3) (merger "0.0" p1 p2))
prop_unravel_seq_merge :: Patch -> Patch -> Patch -> Property
prop_unravel_seq_merge p1 p2 p3 =
(check_a_patch $ join_patches [invert p1,p2,p3]) ==>
(unravel $ merger "0.0" p3 $ merger "0.0" p2 p1) ==
(unravel $ merger "0.0" (merger "0.0" p2 p1) p3)
prop_unravel_order_independent :: Patch -> Patch -> Property
prop_unravel_order_independent p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
(unravel $ merger "0.0" p2 p1) == (unravel $ merger "0.0" p1 p2)
prop_resolve_conflicts_valid :: Patch -> Patch -> Property
prop_resolve_conflicts_valid p1 p2 =
(check_a_patch $ join_patches [invert p1,p2]) ==>
and $ map (check_a_patch.(\l-> join_patches [p,merge_list l]))
$ resolveConflicts p
where p = case merge (p1:\/:p2) of
_ :/\: p1' -> join_patches [p2,p1']
merge_list :: [Sealed (FL Prim C(x))] -> Patch
merge_list 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
try_tok_possibly :: String -> String -> String
-> (Maybe FileContents) -> (Maybe FileContents)
try_tok_possibly t o n = liftM $ \contents ->
let lines' = M.mapMaybe (liftM B.concat
. try_tok_internal t (BC.pack o) (BC.pack n))
(fc_lines contents)
in contents { fc_lines = lines' }
try_tok_internal :: String -> B.ByteString -> B.ByteString
-> B.ByteString -> Maybe [B.ByteString]
try_tok_internal _ _ _ s | B.null s = Just []
try_tok_internal t o n s =
case BC.break (regChars t) s of
(before,s') ->
case BC.break (not . regChars t) s' of
(tok,after) ->
case try_tok_internal 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
prop_read_show :: Patch -> Bool
prop_read_show 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.
prop_commute_inverse :: Patch -> Patch -> Property
prop_commute_inverse p1 p2 =
does_commute p1 p2 ==> case commute (p1 :> p2) of
Nothing -> impossible
Just (_ :> p1') ->
case commute (p1' :> invert p2) of
Nothing -> False
Just (_ :> p1'') -> p1'' == p1
subcommutes_inverse :: [(String, Prim -> Prim -> Property)]
subcommutes_inverse = 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':<p2') ->
case c (invert p2:< p1') of
Succeeded (p1'':<ip2x') -> 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
subcommutes_nontrivial_inverse :: [(String, Prim -> Prim -> Property)]
subcommutes_nontrivial_inverse = 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':<p2') ->
case c (invert p2:< p1') of
Succeeded (p1'':<ip2x') -> 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
subcommutes_failure :: [(String, Prim -> Prim -> Property)]
subcommutes_failure = zip names (map prop cs)
where (names, cs) = unzip subcommutes
prop c p1 p2 =
does_fail c p1 p2 ==> case c (invert p1 :< invert p2) of
Failed -> True
_ -> False
does_fail :: CommuteFunction -> Prim -> Prim -> Bool
does_fail c p1 p2 =
fails (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
where fails Failed = True
fails _ = False
does :: CommuteFunction -> Prim -> Prim -> Bool
does c p1 p2 =
succeeds (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
where succeeds (Succeeded _) = True
succeeds _ = False
nontrivial :: CommuteFunction -> Prim -> Prim -> Bool
nontrivial c p1 p2 =
succeeds (c (p2:<p1)) && (check_a_patch $ fromPrims $ unsafeFL [p1,p2])
where succeeds (Succeeded (p1' :< p2')) = p1' /= p1 || p2' /= p2
succeeds _ = False