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