{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE TypeApplications #-}
{-# Language CPP #-}
{-# Language DataKinds #-}
{-# Language ExplicitForAll #-}
{-# Language FlexibleInstances #-}
{-# Language LambdaCase #-}
{-# Language OverloadedStrings #-}
{-# Language ScopedTypeVariables #-}
{-# Language StandaloneDeriving #-}
{-# Language TypeFamilies #-}
{-# Language TypeOperators #-}
{-# OPTIONS_GHC -fno-warn-orphans #-}
#if __GLASGOW_HASKELL__ >= 805
{-# Language NoStarIsType #-}
#endif
module Test.Vector
  ( vecTests
  , SomeVector(..)
  , genSomeVector
  , genVectorOfLength
  , genOrdering
  , orderingEndomorphisms
  , orderingToStringFuns
  )
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
  ]
  
-- | Used to test ifoldMap.
orderingToStringFuns :: [ Ordering -> String ]
orderingToStringFuns =
  [ const "s"
  , show
  ]

prop_reverse100 :: Property
prop_reverse100 = property $
  do SomeVector v <- forAll $ genSomeVector genOrdering
     case testLeq (knownNat @1) (length v) of
       Nothing -> pure ()
       Just LeqProof -> v === (reverse $ reverse v)

prop_reverseSingleton :: Property
prop_reverseSingleton = property $
  do l <- (:[]) <$> forAll genOrdering
     Just v <- return $ fromList (knownNat @1) l
     v === reverse v

prop_splitJoin :: Property
prop_splitJoin = property $
  do let n = knownNat @5
     v <- forAll $ genVectorKnownLength @(5 * 5) genOrdering
     v === (join n $ split n (knownNat @5) v)

prop_cons :: Property
prop_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)

prop_snoc :: Property
prop_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])

prop_snocUnsnoc :: Property
prop_snocUnsnoc = 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

prop_generate :: Property
prop_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])

prop_unfold :: Property
prop_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))

prop_toFromAssignment :: Property
prop_toFromAssignment = 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))

prop_fmapId :: Property
prop_fmapId = property $
  do SomeVector v <- forAll $ genSomeVector genOrdering
     fmap id v === v

prop_fmapCompose :: Property
prop_fmapCompose = 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)

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

prop_indicesOfRange :: Property
prop_indicesOfRange = property $
  do SomeVector v <- forAll $ genSomeVector genOrdering
     toList (fmap (viewFin natValue) (indicesOf v)) === [0..(natValue (length v) - 1)]

prop_imapConst :: Property
prop_imapConst = property $
  do f <- forAll $ HG.element orderingEndomorphisms
     SomeVector v <- forAll $ genSomeVector genOrdering
     imap (const f) v === fmap f v

prop_ifoldMapConst :: Property
prop_ifoldMapConst = property $
  do f <- forAll $ HG.element orderingToStringFuns
     SomeVector v <- forAll $ genSomeVector genOrdering
     ifoldMap (const f) v === foldMap f v

prop_imapConstIndicesOf :: Property
prop_imapConstIndicesOf = property $
  do SomeVector v <- forAll $ genSomeVector genOrdering
     imap const v === indicesOf v

prop_imapElemAt :: Property
prop_imapElemAt = property $
  do SomeVector v <- forAll $ genSomeVector genOrdering
     imap (\i _ -> viewFin (\x -> elemAt x v) i) v === v

prop_OrdEqVectorIndex :: Property
prop_OrdEqVectorIndex = property $
  do i <- forAll $ genFin (knownNat @10)
     j <- forAll $ genFin (knownNat @10)
     (i == j) === (compare i j == EQ)

-- We use @Ordering@ just because it's simple
vecTests :: IO TestTree
vecTests = testGroup "Vector" <$> return
  [ testPropertyNamed "reverse100" "prop_reverse100" prop_reverse100
  , testPropertyNamed "reverseSingleton" "prop_reverseSingleton" prop_reverseSingleton

  , testPropertyNamed "split-join" "prop_splitJoin" prop_splitJoin

  -- @cons@ is the same for vectors or lists
  , testPropertyNamed "cons" "prop_cons" prop_cons

  -- @snoc@ is like appending to a list
  , testPropertyNamed "snoc" "prop_snoc" prop_snoc

  -- @snoc@ and @unsnoc@ are inverses
  , testPropertyNamed "snoc/unsnoc" "prop_snocUnsnoc" prop_snocUnsnoc

  -- @generate@ is like mapping a function over indices
  , testPropertyNamed "generate" "prop_generate" prop_generate

  -- @unfold@ works like @unfold@ on lists
  , testPropertyNamed "unfold" "prop_unfold" prop_unfold

  -- Converting to and from assignments preserves size and last element
  , testPropertyNamed "to-from-assignment" "prop_toFromAssignment" prop_toFromAssignment

  -- 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.
  , testPropertyNamed "fmap-id" "prop_fmapId" prop_fmapId

  , testPropertyNamed "fmap-compose" "prop_fmapCompose" prop_fmapCompose

  , testPropertyNamed "iterateN-range" "prop_iterateNRange" prop_iterateNRange

  , testPropertyNamed "indicesOf-range" "prop_indicesOfRange" prop_indicesOfRange

  , testPropertyNamed "imap-const" "prop_imapConst" prop_imapConst

  , testPropertyNamed "ifoldMap-const" "prop_ifoldMapConst" prop_ifoldMapConst

  , testPropertyNamed "imap-const-indicesOf" "prop_imapConstIndicesOf" prop_imapConstIndicesOf

  , testPropertyNamed "imap-elemAt" "prop_imapElemAt" prop_imapElemAt

  , testPropertyNamed "Ord-Eq-VectorIndex" "prop_OrdEqVectorIndex" prop_OrdEqVectorIndex

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