1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
|
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# Language CPP #-}
module Test.Fin
( finTests
, genFin
)
where
import Numeric.Natural (Natural)
import Hedgehog
import qualified Hedgehog.Gen as HG
import Hedgehog.Range (linear)
import Test.Tasty (TestTree, testGroup)
import Test.Tasty.Hedgehog (testPropertyNamed)
import Test.Tasty.HUnit (assertBool, testCase)
import Data.Parameterized.NatRepr
import Data.Parameterized.Fin
import Data.Parameterized.Some (Some(Some))
#if __GLASGOW_HASKELL__ >= 806
import qualified Hedgehog.Classes as HC
#endif
genNatRepr :: (Monad m) => Natural -> GenT m (Some NatRepr)
genNatRepr bound =
do x0 <- HG.integral (linear 0 bound)
return (mkNatRepr x0)
genFin :: (1 <= n, Monad m) => NatRepr n -> GenT m (Fin n)
genFin n =
do Some x <- genNatRepr (natValue n - 1 :: Natural)
return $
case testLeq (incNat x) n of
Just LeqProof -> mkFin x
Nothing -> error "Impossible"
prop_count_true :: Property
prop_count_true = property $
do Some n <- forAll (genNatRepr 100)
finToNat (countFin n (\_ _ -> True)) === natValue n
prop_count_false :: Property
prop_count_false = property $
do Some n <- forAll (genNatRepr 100)
finToNat (countFin n (\_ _ -> False)) === 0
finTests :: IO TestTree
finTests =
testGroup "Fin" <$>
return
[ testCase "minBound <= maxBound (1)" $
assertBool
"minBound <= maxBound (1)"
((minBound :: Fin 1) <= (minBound :: Fin 1))
, testCase "minBound <= maxBound (2)" $
assertBool
"minBound <= maxBound (2)"
((minBound :: Fin 2) <= (minBound :: Fin 2))
, testPropertyNamed "count-true" "prop_count_true" prop_count_true
, testPropertyNamed "count-false" "prop_count_false" prop_count_false
#if __GLASGOW_HASKELL__ >= 806
, testCase "Eq-Fin-laws-1" $
assertBool "Eq-Fin-laws-1" =<<
HC.lawsCheck (HC.eqLaws (genFin (knownNat @1)))
, testCase "Ord-Fin-laws-1" $
assertBool "Ord-Fin-laws-1" =<<
HC.lawsCheck (HC.ordLaws (genFin (knownNat @1)))
, testCase "Eq-Fin-laws-10" $
assertBool "Eq-Fin-laws-10" =<<
HC.lawsCheck (HC.eqLaws (genFin (knownNat @10)))
, testCase "Ord-Fin-laws-10" $
assertBool "Ord-Fin-laws-10" =<<
HC.lawsCheck (HC.ordLaws (genFin (knownNat @10)))
#endif
]
|
