{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
import Hedgehog
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
import Test.DocTest
import Numeric.Sized.WordOfSize
import Numeric.Sized.IntOfSize
import Control.Monad
import Data.Data
default ()
binaryProp
:: forall a.
Integral a
=> (forall t. Integral t => t -> t -> t)
-> Integer
-> Integer
-> (Integer -> Integer -> Bool)
-> Property
binaryProp op lb ub cond = property $ do
x <- forAll (Gen.integral (Range.linear lb ub))
y <- forAll (Gen.integral (Range.linear lb ub))
guard (cond x y)
let zb = op x y
let zt = op (fromInteger x :: a) (fromInteger y)
zb === toInteger zt
ordProps
:: forall a.
(Ord a, Show a, Typeable a)
=> Gen IO a
-> Property
ordProps xs = property $ do
x <- forAll xs
info "reflexive"
x === x
info "irreflexive"
assert (not (x < x))
y <- forAll xs
info "Ord functions behave same as default implementations"
case compare x y of
LT -> do
assert (x < y)
assert (x /= y)
assert (not (x == y))
assert (x <= y)
assert (not (x >= y))
info "antisymmetric"
assert (y > x)
info "irreflexive"
assert (not (x > y))
info "transitive"
z <- forAll xs
when (z > y) (assert (z > x))
EQ -> do
assert (x == y)
assert (not (x /= y))
assert (not (x < y))
assert (not (x > y))
assert (x <= y)
assert (x >= y)
info "symmetric"
assert (y == x)
info "transitive"
z <- forAll xs
assert $ (x == z) == (y == z)
GT -> do
assert (x > y)
assert (x /= y)
assert (not (x == y))
assert (x >= y)
assert (not (x <= y))
info "irreflexive"
assert (not (x < y))
info "antisymmetric"
assert (y < x)
info "transitive"
z <- forAll xs
when (z < y) (assert (z < x))
holdsForLength :: Foldable f => (a -> Bool) -> f a -> Int
holdsForLength p = flip (foldr f id ) 0 where
f e a i | p e = a (i + 1)
| otherwise = i
enumProps
:: forall a.
(Enum a, Show a, Typeable a, Ord a)
=> (Int -> Bool) -> Gen IO Int -> Gen IO a -> Property
enumProps p ig eg = property $ do
x <- forAll ig
info "from . to"
(fromEnum . toEnum @a) x === x
info "to . from"
n <- forAll eg
(toEnum . fromEnum) n === n
info "[n..]"
let lhs1 = take 100 $ map fromEnum [n..]
rhs1 = take 100 $ [fromEnum n..]
len1 = min (holdsForLength p lhs1) (holdsForLength p rhs1)
take len1 lhs1 === take len1 rhs1
info "[n,m..]"
m <- forAll eg
let lhs2 = take 100 $ map fromEnum [n,m..]
rhs2 = take 100 $ [fromEnum n, fromEnum m..]
len2 = min (holdsForLength p lhs2) (holdsForLength p rhs2)
take len2 lhs2 === take len2 rhs2
when (m >= n) $ do
info "[n..m]"
map fromEnum [n..m] === [fromEnum n..fromEnum m]
l <- forAll eg
when (((l > n) == (n > m)) && (l /= n)) $ do
info "[l,n..m]"
map fromEnum [l,n..m] === [fromEnum l, fromEnum n..fromEnum m]
prop_Word3Add :: Property
prop_Word3Add = binaryProp @(WordOfSize 3) (+) 0 7 (\x y -> x + y <= 7)
prop_Word3Mul :: Property
prop_Word3Mul = binaryProp @(WordOfSize 3) (*) 0 7 (\x y -> x * y <= 7)
prop_Word3Sub :: Property
prop_Word3Sub = withDiscards 1000 $ binaryProp @(WordOfSize 3) (-) 0 7 (>=)
prop_Word3Rem :: Property
prop_Word3Rem = binaryProp @(WordOfSize 3) rem 0 7 (\_ y -> y > 0)
prop_Word3Quot :: Property
prop_Word3Quot = binaryProp @(WordOfSize 3) quot 0 7 (\_ y -> y > 0)
prop_Word3Ord :: Property
prop_Word3Ord = ordProps (Gen.integral (Range.linear @(WordOfSize 3) 0 7))
prop_Word3Enum :: Property
prop_Word3Enum =
enumProps
(inBounds 0 7)
(Gen.integral (Range.linear 0 7))
(Gen.integral (Range.linear @(WordOfSize 3) 0 7))
inBounds :: Ord a => a -> a -> a -> Bool
inBounds lb ub x = x >= lb && x <= ub
prop_Int3Add :: Property
prop_Int3Add =
withDiscards 1000 $
binaryProp
@(IntOfSize 3)
(+)
(-4)
3
(\x y ->
inBounds (-4) 3 (x + y))
prop_Int3Mul :: Property
prop_Int3Mul =
withDiscards 1000 $
binaryProp
@(IntOfSize 3)
(*)
(-4)
3
(\x y ->
inBounds (-4) 3 (x * y))
prop_Int3Sub :: Property
prop_Int3Sub = binaryProp @(IntOfSize 3) (-) (-4) 3 (\x y -> inBounds (-4) 3 (x - y))
prop_Int3Rem :: Property
prop_Int3Rem = binaryProp @(IntOfSize 3) rem (-4) 3 (\_ y -> y /= 0)
prop_Int3Quot :: Property
prop_Int3Quot = binaryProp @(IntOfSize 3) quot (-4) 3 (\x y -> y /= 0 && inBounds (-4) 3 (quot x y))
prop_Int3Ord :: Property
prop_Int3Ord = ordProps (Gen.integral (Range.linear @(IntOfSize 3) (-3) 4))
prop_Int3Enum :: Property
prop_Int3Enum =
enumProps
(inBounds (-4) 3)
(Gen.integral (Range.linear (-4) 3))
(Gen.integral (Range.linear @(IntOfSize 3) (-4) 3))
main :: IO Bool
main = do
doctest ["-isrc","src/"]
$$(checkConcurrent)