{-# LANGUAGE CPP #-} {-# LANGUAGE DeriveDataTypeable #-} {-# LANGUAGE DeriveFoldable #-} {-# LANGUAGE DeriveFunctor #-} {-# LANGUAGE DeriveTraversable #-} {-# LANGUAGE TemplateHaskell #-} {-# OPTIONS_GHC -fno-warn-missing-signatures #-} module Agda.Utils.Permutation.Tests (tests) where import Data.Functor import Data.List as List import Data.Maybe import Test.QuickCheck import Agda.Utils.List (downFrom) import Agda.Utils.Permutation ------------------------------------------------------------------------ -- * Properties ------------------------------------------------------------------------ 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 -- | Extend a list by indefinitely many elements. withStream :: ([a] -> b) -- ^ Stream function. -> [a] -- ^ Initial segment. -> a -- ^ Default element, appended ad infinitum. -> b withStream k as a = k $ as ++ repeat a -- | Apply a permutation to a list which might be too short. -- Silently discard picks that go beyond the list's boundaries. permutePartial :: Permutation -> [a] -> [a] permutePartial perm xs = catMaybes $ permute perm $ map Just xs ++ repeat Nothing -- Note: we have to add @Nothing@s to make @permute@ total. -- | @perm([0..n-1]) == perm@ prop_permute_id_r :: Permutation -> Bool prop_permute_id_r perm@(Perm n picks) = permute perm [0..] == picks -- | @idP(xs) == xs@ prop_permute_id_l :: Int -> [A] -> A -> Bool prop_permute_id_l n = withStream $ \ xs -> permute (idP n) xs == take n xs -- | @takeP n perm = perm . take n@ prop_takeP :: Int -> Permutation -> [A] -> A -> Bool prop_takeP n perm = withStream $ \ xs -> permute (takeP n perm) xs == permutePartial perm (take n xs) -- Note: we have to add @Nothing@s to make @permute@ total. -- | @(droppedP perm)(xs) = xs \\ perm(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') -- | @(p1 ∘ p2)(xs) = p1(p2(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_flipP :: Permutation -> Bool prop_flipP p = permPicks (flipP p) == permute p (downFrom $ permRange p) -- | @p ∘ p⁻¹ ∘ p = p@ 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 -- NOT QUITE RIGHT YET: -- -- | @p⁻1 ∘ p ∘ p⁻¹ = p⁻¹@ -- prop_invertP_right :: Permutation -> Int -> [A] -> A -> Bool -- prop_invertP_right p err = withStream $ \ xs -> -- let pinv = invertP err p -- ys = permute pinv xs -- in permute pinv (permute p ys) == ys -- | @reverseP p = reverse . p . reverse@ 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)) -- | @permute p . inversePermute p = id@ 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 prop_inversePermute_invertP :: Permutation -> Bool prop_inversePermute_invertP p = inversePermute p (id :: Int -> Int) == safePermute (invertP (-1) p) [(0::Int)..] -- Template Haskell hack to make the following $quickCheckAll work -- under ghc-7.8. return [] -- KEEP! -- | All tests as collected by 'quickCheckAll'. tests :: IO Bool tests = do putStrLn "Agda.Utils.Permutation" $quickCheckAll