{-# OPTIONS_GHC -fno-warn-missing-signatures #-}

{-# LANGUAGE CPP #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveFoldable #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE DeriveTraversable #-}
{-# LANGUAGE TemplateHaskell #-}

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

------------------------------------------------------------------------
-- * Properties
------------------------------------------------------------------------

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

-- | Extend a list by indefinitely many elements.
withStream :: Testable b
  => ([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)

-- | @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

-- 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