{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeApplications #-}
{-# Language CPP #-}
{-# Language DataKinds #-}
{-# Language ExplicitForAll #-}
{-# Language FlexibleInstances #-}
{-# Language LambdaCase #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneDeriving #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
#if __GLASGOW_HASKELL__ >= 805
{-# Language NoStarIsType #-}
#endif
module Test.Vector
  ( vecTests
  )
where

import           Data.Functor.Const (Const(..))
import           Data.Functor.WithIndex (imap)
import           Data.Foldable.WithIndex (ifoldMap)
import           Data.Maybe (isJust)
import qualified Data.List as List
import qualified Data.Parameterized.Context as Ctx
import           Data.Parameterized.Fin
import           Data.Parameterized.NatRepr
import           Data.Parameterized.Some
import           Data.Parameterized.Vector
import           Data.Semigroup
import           GHC.TypeLits (KnownNat)
import           Hedgehog
import qualified Hedgehog.Gen as HG
import           Hedgehog.Range
import           Numeric.Natural (Natural)
import           Prelude hiding (take, reverse, length)
import qualified Prelude as P
import           Test.Fin (genFin)
import           Test.Tasty
import           Test.Tasty.Hedgehog
import           Test.Context (genSomePayloadList, mkUAsgn)

#if __GLASGOW_HASKELL__ >= 806
import qualified Hedgehog.Classes as HC
import           Test.Tasty.HUnit (assertBool, testCase)
#endif

data SomeVector a = forall n. SomeVector (Vector n a)

instance Show a => Show (SomeVector a) where
  show (SomeVector v) = show v

genVectorOfLength :: (Monad m) => NatRepr n -> GenT m a -> GenT m (Vector (n + 1) a)
genVectorOfLength n genElem =
  do let w = widthVal n
     l <- HG.list (linear (w + 1) (w + 1)) genElem
     case testLeq (knownNat @1) (incNat n) of
       Nothing -> error "testLeq in genSomeVector"
       Just LeqProof ->
         case fromList (incNat n) l of
           Just v -> return v
           Nothing -> error ("fromList failure for size " <> show w)

genSomeVector :: (Monad m) => GenT m a -> GenT m (SomeVector a)
genSomeVector genElem =
  do Some len <- mkNatRepr <$> HG.integral (linear 0 (99 :: Natural))
     SomeVector <$> genVectorOfLength len genElem

genVectorKnownLength :: (1 <= n, KnownNat n, Monad m) => GenT m a -> GenT m (Vector n a)
genVectorKnownLength genElem =
  do let n = knownNat
         w = widthVal n
     l <- HG.list (constant w w) genElem
     case fromList n l of
       Just v -> return v
       Nothing -> error ("fromList failure for size " <> show w)

genOrdering :: Monad m => GenT m Ordering
genOrdering = HG.element [ LT, EQ, GT ]

instance Show (a -> b) where
  show _ = "unshowable"

-- Used to test e.g., 'fmap (g . f) = fmap g . fmap f' and 'imap (const f) =
-- fmap f'.
orderingEndomorphisms :: [Ordering -> Ordering]
orderingEndomorphisms =
  [ const EQ
  , id
  , \case
      EQ -> EQ
      LT -> GT
      GT -> LT
  , \case
      LT -> EQ
      EQ -> GT
      GT -> LT
  ]

-- We use @Ordering@ just because it's simple
vecTests :: IO TestTree
vecTests = testGroup "Vector" <$> return
  [ testProperty "reverse100" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       case testLeq (knownNat @1) (length v) of
         Nothing -> pure ()
         Just LeqProof -> v === (reverse $ reverse v)
  , testProperty "reverseSingleton" $ property $
    do l <- (:[]) <$> forAll genOrdering
       Just v <- return $ fromList (knownNat @1) l
       v === reverse v

  , testProperty "split-join" $ property $
    do let n = knownNat @5
       v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering
       v === (join n $ split n (knownNat @5) v)

  -- @cons@ is the same for vectors or lists
  , testProperty "cons" $ property $
    do let n = knownNat @20
           w = widthVal n
       l <- forAll $ HG.list (constant w w) genOrdering
       x <- forAll genOrdering
       (cons x <$> fromList n l) === fromList (incNat n) (x:l)

  -- @snoc@ is like appending to a list
  , testProperty "snoc" $ property $
    do let n = knownNat @20
           w = widthVal n
       l <- forAll $ HG.list (constant w w) genOrdering
       x <- forAll genOrdering
       (flip snoc x <$> fromList n l) === fromList (incNat n) (l ++ [x])

  -- @snoc@ and @unsnoc@ are inverses
  , testProperty "snoc/unsnoc" $ property $
    do let n = knownNat @20
           w = widthVal n
       l <- forAll $ HG.list (constant w w) genOrdering
       x <- forAll genOrdering
       (fst  . unsnoc . flip snoc x <$> fromList n l) === Just x

  -- @generate@ is like mapping a function over indices
  , testProperty "generate" $ property $
    do let n = knownNat @55
           w = widthVal n
           funs :: [ Int -> Ordering ]  -- some miscellaneous functions to generate Vector values
           funs =  [ const EQ
                   , \i -> if i < 10 then LT else if i > 15 then GT else EQ
                   , \i -> if i == 0 then EQ else GT
                   ]
       f <- forAll $ HG.element funs
       Just (generate n (f . widthVal)) === fromList (incNat n) (map f [0..w])

  -- @unfold@ works like @unfold@ on lists
  , testProperty "unfold" $ property $
    do let n = knownNat @55
           w = widthVal n
           funs :: [ Ordering -> (Ordering, Ordering) ]  -- some miscellaneous functions to generate Vector values
           funs =  [ const (EQ, EQ)
                   , \case
                       LT -> (LT, GT)
                       GT -> (GT, LT)
                       EQ -> (EQ, EQ)
                   ]
       f <- forAll $ HG.element funs
       o <- forAll $ HG.element [EQ, LT, GT]
       Just (unfoldr n f o) === fromList (incNat n) (P.take (w + 1) (List.unfoldr (Just . f) o))

  -- Converting to and from assignments preserves size and last element
  , testProperty "to-from-assignment" $ property $
    do vals <- forAll genSomePayloadList
       Some a <- return $ mkUAsgn vals
       let sz = Ctx.size a
       case Ctx.viewSize sz of
         Ctx.ZeroSize -> pure ()
         Ctx.IncSize _ ->
           let a' =
                 toAssignment
                   sz
                   (\_idx val -> Const val)
                   (fromAssignment Some a)
           in do assert $
                   isJust $
                     testEquality
                       (Ctx.sizeToNatRepr sz)
                       (Ctx.sizeToNatRepr (Ctx.size a'))
                 viewSome
                   (\lastElem ->
                      assert $
                        isJust $
                          testEquality
                            (a Ctx.! Ctx.lastIndex sz) lastElem)
                   (getConst (a' Ctx.! Ctx.lastIndex sz))

  -- NOTE: We don't use hedgehog-classes here, because the way the types work
  -- would require this to only tests vectors of some fixed size.
  --
  -- Also, for 'fmap-compose', hedgehog-classes only tests two fixed functions
  -- over integers.
  , testProperty "fmap-id" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       fmap id v === v

  , testProperty "fmap-compose" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       f <- forAll $ HG.element orderingEndomorphisms
       g <- forAll $ HG.element orderingEndomorphisms
       fmap (g . f) v === fmap g (fmap f v)

  , testProperty "iterateN-range" $ property $
    do Some len <- mkNatRepr <$> forAll (HG.integral (linear 0 (99 :: Natural)))
       toList (iterateN len (+1) 0) === [0..(natValue len)]

  , testProperty "indicesOf-range" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]

  , testProperty "imap-const" $ property $
    do f <- forAll $ HG.element orderingEndomorphisms
       SomeVector v <- forAll $ genSomeVector genOrdering
       imap (const f) v === fmap f v

  , testProperty "ifoldMap-const" $ property $
    do let funs :: [ Ordering -> String ]
           funs = [const "s", show]
       f <- forAll $ HG.element funs
       SomeVector v <- forAll $ genSomeVector genOrdering
       ifoldMap (const f) v === foldMap f v

  , testProperty "imap-const-indicesOf" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       imap const v === indicesOf v

  , testProperty "imap-elemAt" $ property $
    do SomeVector v <- forAll $ genSomeVector genOrdering
       imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v

  , testProperty "Ord-Eq-VectorIndex" $ property $
    do i <- forAll $ genFin (knownNat @10)
       j <- forAll $ genFin (knownNat @10)
       (i == j) === (compare i j == EQ)

#if __GLASGOW_HASKELL__ >= 806
  -- Test a few different sizes since the types force each test to use a
  -- specific size vector.
  , testCase "Eq-Vector-laws-1" $
      assertBool "Eq-Vector-laws-1" =<<
        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @1 genOrdering))
  , testCase "Eq-Vector-laws-10" $
      assertBool "Eq-Vector-laws-10" =<<
        HC.lawsCheck (HC.eqLaws (genVectorKnownLength @10 genOrdering))
  , testCase "Show-Vector-laws-1" $
      assertBool "Show-Vector-laws-1" =<<
        HC.lawsCheck (HC.showLaws (genVectorKnownLength @1 genOrdering))
  , testCase "Show-Vector-laws-10" $
      assertBool "Show-Vector-laws-10" =<<
        HC.lawsCheck (HC.showLaws (genVectorKnownLength @10 genOrdering))
  , testCase "Foldable-Vector-laws-1" $
      assertBool "Foldable-Vector-laws-1" =<<
        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @1))
  , testCase "Foldable-Vector-laws-10" $
      assertBool "Foldable-Vector-laws-10" =<<
        HC.lawsCheck (HC.foldableLaws (genVectorKnownLength @10))
  , testCase "Traversable-Vector-laws-1" $
      assertBool "Traversable-Vector-laws-1" =<<
        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @1))
  , testCase "Traversable-Vector-laws-10" $
      assertBool "Traversable-Vector-laws-10" =<<
        HC.lawsCheck (HC.traversableLaws (genVectorKnownLength @10))
#endif
  ]