module Agda.Utils.Permutation.Tests (tests) where
import Data.Functor
import Data.List as List
import Data.Maybe
import Test.QuickCheck
import Test.QuickCheck.All
import Agda.Utils.Permutation
instance Arbitrary Permutation where
arbitrary = do
is <- nub . map getNonNegative <$> arbitrary
NonNegative n <- arbitrary
return $ Perm (if null is then n else maximum is + n + 1) is
data ComposablePermutations = ComposablePermutations Permutation Permutation
deriving (Eq, Show)
instance Arbitrary ComposablePermutations where
arbitrary = do
p2@(Perm n is) <- arbitrary
let m = length is
p1 <- Perm m . filter (< m) . map getNonNegative <$> arbitrary
return $ ComposablePermutations p1 p2
type A = Int
withStream :: Testable b
=> ([a] -> b)
-> [a]
-> a
-> b
withStream k as a = k $ as ++ repeat a
permutePartial :: Permutation -> [a] -> [a]
permutePartial perm xs =
catMaybes $ permute perm $ map Just xs ++ repeat Nothing
prop_permute_id_r :: Permutation -> Bool
prop_permute_id_r perm@(Perm n picks) =
permute perm [0..] == picks
prop_permute_id_l :: Int -> [A] -> A -> Bool
prop_permute_id_l n = withStream $ \ xs ->
permute (idP n) xs == take n xs
prop_takeP :: Int -> Permutation -> [A] -> A -> Bool
prop_takeP n perm = withStream $ \ xs ->
permute (takeP n perm) xs == permutePartial perm (take n xs)
prop_droppedP :: Permutation -> [A] -> A -> Bool
prop_droppedP perm@(Perm n _) = withStream $ \ xs -> let xs' = take n xs in
sort (permute (droppedP perm) xs') == sort (xs' \\ permute perm xs')
prop_composeP :: ComposablePermutations -> [A] -> A -> Bool
prop_composeP (ComposablePermutations p1 p2) = withStream $ \ xs ->
permute (composeP p1 p2) xs == permutePartial p1 (permute p2 xs)
prop_invertP_left :: Permutation -> Int -> [A] -> A -> Bool
prop_invertP_left p err = withStream $ \ xs -> let ys = permute p xs in
permute p (permute (invertP err p) ys) == ys
prop_reverseP :: Permutation -> [A] -> A -> Bool
prop_reverseP p@(Perm n _) = withStream $ \ xs0 -> let xs = take n xs0 in
permute (reverseP p) xs == reverse (permute p (reverse xs))
prop_inversePermute :: Permutation -> [Maybe A] -> Maybe A -> Bool
prop_inversePermute p@(Perm _ is) = withStream $ \ xs0 ->
let xs = take (length is) xs0
ys = inversePermute p xs
in permute p ys == xs
return []
tests :: IO Bool
tests = do
putStrLn "Agda.Utils.Permutation"
$quickCheckAll