darcs-cabalized-2.0.2: src/Darcs/Patch/Test.lhs
% 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.
\begin{code}
{-# OPTIONS_GHC -cpp -fno-warn-deprecations -fglasgow-exts #-}
#include "gadts.h"
module Darcs.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 Test.QuickCheck
import Control.Monad ( liftM, liftM2, liftM3, liftM4, replicateM )
import Darcs.Patch.Info ( PatchInfo, patchinfo )
import Darcs.Patch.Check ( PatchCheck, Possibly(..),
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,
)
import RegChars ( regChars )
import FastPackedString ( PackedString, packString,
linesPS, nullPS, concatPS, breakPS,
)
import FileName ( fn2fp )
import Darcs.Patch.Patchy ( Commute )
import Darcs.Patch ( addfile, adddir, move, showPatch,
hunk, tokreplace, joinPatches, binary,
changepref, is_merger, invert, commute, commutex, merge,
readPatch, resolve_conflicts,
effect, fromPrims,
unravel, merger, elegant_merge )
import Darcs.Patch.Core ( Patch(..) )
import Darcs.Patch.Prim ( Prim(..), DirPatchType(..), FilePatchType(..),
CommuteFunction, Perhaps(..),
subcommutes )
import Printer ( renderPS )
import Darcs.Patch.Ordered
import Darcs.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
\end{code}
\begin{code}
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 = liftM4 patchinfo unempty unempty unempty unempty
instance Arbitrary PatchInfo where
arbitrary = arbpi
-- coarbitrary pi = coarbitrary (show pi)
instance Arbitrary PackedString where
arbitrary = liftM packString 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
linenumgen :: Gen Int
linenumgen = frequency [(1,return 1), (1,return 2), (1,return 3),
(3,liftM (\n->1+abs n) 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 PackedString
filelinegen = liftM packString $
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)
\end{code}
\begin{code}
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 | is_merger 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
\end{code}
\begin{code}
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]
\end{code}
\begin{code}
prop_commute_twice :: Patch -> Patch -> Property
prop_commute_twice p1 p2 =
(does_commute p1 p2) ==> (Just (p2:<p1) == (commutex (p2:<p1) >>= commutex))
does_commute :: Patch -> Patch -> Bool
does_commute p1 p2 =
commutex (p2:<p1) /= Nothing && (check_a_patch $ join_patches [p1,p2])
prop_commute_equivalency :: Patch -> Patch -> Property
prop_commute_equivalency p1 p2 =
(does_commute p1 p2) ==>
case commutex (p2:<p1) of
Just (p1':<p2') -> check_a_patch $ join_patches [p1,p2,invert p1',invert p2']
_ -> impossible
\end{code}
\begin{code}
prop_commute_either_way :: Patch -> Patch -> Property
prop_commute_either_way p1 p2 =
does_commute p1 p2 ==> does_commute (invert p2) (invert p1)
\end{code}
\begin{code}
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 commutex (p2:<p1) of
Nothing -> False
Just (p1':<p2') ->
case commutex (p3:<p1') of
Nothing -> False
Just (_:<p3') ->
case commutex (p3':<p2') of
Nothing -> False
Just (_:< p3'') ->
case commutex (p3:<p2) of
Nothing -> False
Just (_:<p3'a) ->
case commutex (p3'a:<p1) of
Just (_:<p3''a) -> p3''a == p3''
Nothing -> False
\end{code}
\begin{code}
prop_patch_and_inverse_is_identity :: Patch -> Patch -> Property
prop_patch_and_inverse_is_identity p1 p2 =
(check_a_patch $ join_patches [p1,p2]) && (commutex (p2:<p1) /= Nothing) ==>
case commutex (p2:<p1) of
Just (_:<p2') -> case commutex (p2':<invert p1) of
Nothing -> True -- This is a subtle distinction.
Just (_:<p2'') -> p2'' == p2
Nothing -> impossible
\end{code}
\begin{code}
quickmerge :: (Patch :\/: Patch) -> Patch
quickmerge (p1:\/:p2) = case merge (p1:\/:p2) of
_ :/\: p1' -> p1'
\end{code}
\begin{code}
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 commutex (p2':<p1) of
Nothing -> False
Just (p1'':<p2'') -> 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']
\end{code}
\begin{code}
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) >>= commutex of
Nothing -> Nothing
Just (p1'b :< p2b) ->
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 commutex (p1 :< invert p2) of
Just (_:<p1') ->
case commutex (p1':< p2) 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` elegant_merge (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 Show p => Show (p :< p) where
show (x :< y) = show x ++ " :< " ++ show y
\end{code}
\begin{code}
test_patch :: String
test_patch = test_str ++ test_note
tp1, tp2 :: Patch
tp1 = unsafeUnseal . fst . fromJust . readPatch $ packString "\nmove ./test/test ./hello\n"
tp2 = unsafeUnseal . fst . fromJust . readPatch $ packString "\nmove ./test ./hello\n"
tp1', tp2' :: Patch
tp2' = quickmerge (tp2:\/:tp1)
tp1' = quickmerge (tp1:\/:tp2)
test_note :: String
test_note = (if commutex (tp2':<tp1) == Just (tp1':<tp2)
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")
++"commutex of tp1' and tp2 is "++show (commutex (tp1':<tp2))++"\n"
++"commutex of tp2' and tp1 is "++show (commutex (tp2':<tp1))++"\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")-}
\end{code}
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.
\begin{code}
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))
\end{code}
\begin{code}
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)
\end{code}
\begin{code}
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)
\end{code}
\begin{code}
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]))
$ resolve_conflicts 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
\end{code}
\begin{code}
try_tok_possibly :: String -> String -> String
-> [Possibly PackedString] -> Maybe [Possibly PackedString]
try_tok_possibly t o n mss =
mapM (silly_maybe_possibly $ liftM concatPS .
try_tok_internal t (packString o) (packString n))
$ take 1000 mss
silly_maybe_possibly :: (PackedString -> Maybe PackedString) ->
(Possibly PackedString -> Maybe (Possibly PackedString))
silly_maybe_possibly f =
\px -> case px of
PNothing -> Just PNothing
PSomething -> Just PSomething
PJust x -> case f x of
Nothing -> Nothing
Just x' -> Just $ PJust x'
try_tok_internal :: String -> PackedString -> PackedString
-> PackedString -> Maybe [PackedString]
try_tok_internal _ _ _ s | nullPS s = Just []
try_tok_internal t o n s =
case breakPS (regChars t) s of
(before,s') ->
case breakPS (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
\end{code}
\begin{code}
prop_read_show :: Patch -> Bool
prop_read_show p = case readPatch $ renderPS $ showPatch p of
Just (Sealed p',_) -> p' == p
Nothing -> False
\end{code}
%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.
\begin{code}
prop_commute_inverse :: Patch -> Patch -> Property
prop_commute_inverse p1 p2 =
does_commute p1 p2 ==> case commutex (p2:< p1) of
Nothing -> impossible
Just (p1':<_) ->
case commutex (invert p2:< p1') of
Nothing -> False
Just (p1'':<_) -> p1'' == p1
\end{code}
\begin{code}
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
\end{code}