{-# LANGUAGE ScopedTypeVariables #-}
module Hedgehog.Classes.Bits (bitsLaws) where
import Data.Bits
import Hedgehog
import Hedgehog.Classes.Common
import qualified Hedgehog.Gen as Gen
import qualified Hedgehog.Range as Range
bitsLaws :: (FiniteBits a, Show a) => Gen a -> Laws
bitsLaws :: Gen a -> Laws
bitsLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Bits"
[ (String
"Conjunction Idempotence", Gen a -> Property
forall a. (Bits a, Show a) => Gen a -> Property
bitsConjunctionIdempotence Gen a
gen)
, (String
"Disjunction Idempotence", Gen a -> Property
forall a. (Bits a, Show a) => Gen a -> Property
bitsDisjunctionIdempotence Gen a
gen)
, (String
"Double Complement", Gen a -> Property
forall a. (Bits a, Show a) => Gen a -> Property
bitsDoubleComplement Gen a
gen)
, (String
"Set Bit", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetBit Gen a
gen)
, (String
"Clear Bit", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearBit Gen a
gen)
, (String
"Complement Bit", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsComplementBit Gen a
gen)
, (String
"Clear Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearZero Gen a
gen)
, (String
"Set Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetZero Gen a
gen)
, (String
"Test Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsTestZero Gen a
gen)
, (String
"Pop Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsPopZero Gen a
gen)
, (String
"Count Leading Zeros of Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountLeadingZeros Gen a
gen)
, (String
"Count Trailing Zeros of Zero", Gen a -> Property
forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountTrailingZeros Gen a
gen)
]
newtype BitIndex a = BitIndex Int
deriving (Int -> BitIndex a -> ShowS
[BitIndex a] -> ShowS
BitIndex a -> String
(Int -> BitIndex a -> ShowS)
-> (BitIndex a -> String)
-> ([BitIndex a] -> ShowS)
-> Show (BitIndex a)
forall a. Int -> BitIndex a -> ShowS
forall a. [BitIndex a] -> ShowS
forall a. BitIndex a -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [BitIndex a] -> ShowS
$cshowList :: forall a. [BitIndex a] -> ShowS
show :: BitIndex a -> String
$cshow :: forall a. BitIndex a -> String
showsPrec :: Int -> BitIndex a -> ShowS
$cshowsPrec :: forall a. Int -> BitIndex a -> ShowS
Show)
genBitIndex :: forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex :: Gen (BitIndex a)
genBitIndex = let n :: Int
n = a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (a
forall a. HasCallStack => a
undefined :: a) in if Int
n Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
0
then (Int -> BitIndex a) -> GenT Identity Int -> Gen (BitIndex a)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Int -> BitIndex a
forall a. Int -> BitIndex a
BitIndex (Range Int -> GenT Identity Int
forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral (Range Int -> GenT Identity Int) -> Range Int -> GenT Identity Int
forall a b. (a -> b) -> a -> b
$ Int -> Int -> Range Int
forall a. Integral a => a -> a -> Range a
Range.linear Int
0 (Int
n Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1))
else BitIndex a -> Gen (BitIndex a)
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> BitIndex a
forall a. Int -> BitIndex a
BitIndex Int
0)
bitsConjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
bitsConjunctionIdempotence :: Gen a -> Property
bitsConjunctionIdempotence Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a
n a -> a -> a
forall a. Bits a => a -> a -> a
.&. a
n; rhs :: a
rhs = a
n;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Conjunction Idempotence"
, lawContextLawBody :: String
lawContextLawBody = String
"n .&. n" String -> ShowS
`congruency` String
"n"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n;
in [String] -> String
lawWhere [ String
"n .&. n" String -> ShowS
`congruency` String
"n, where", String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN ]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsDisjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
bitsDisjunctionIdempotence :: Gen a -> Property
bitsDisjunctionIdempotence Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a
n a -> a -> a
forall a. Bits a => a -> a -> a
.|. a
n; rhs :: a
rhs = a
n;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Disjunction Idempotence"
, lawContextLawBody :: String
lawContextLawBody = String
"n .|. n" String -> ShowS
`congruency` String
"n"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n
in [String] -> String
lawWhere [ String
"n .|. n" String -> ShowS
`congruency` String
"n, where", String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN ]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsDoubleComplement :: forall a. (Bits a, Show a) => Gen a -> Property
bitsDoubleComplement :: Gen a -> Property
bitsDoubleComplement Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
let lhs :: a
lhs = a -> a
forall a. Bits a => a -> a
complement (a -> a
forall a. Bits a => a -> a
complement a
n); rhs :: a
rhs = a
n;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Double Complement"
, lawContextLawBody :: String
lawContextLawBody = String
"complement . complement" String -> ShowS
`congruency` String
"id"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n
in [String] -> String
lawWhere [ String
"complement . complement $ n" String -> ShowS
`congruency` String
"id n, where", String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN ]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsSetBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetBit :: Gen a -> Property
bitsSetBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let lhs :: a
lhs = a -> Int -> a
forall a. Bits a => a -> Int -> a
setBit a
n Int
i; rhs :: a
rhs = a
n a -> a -> a
forall a. Bits a => a -> a -> a
.|. Int -> a
forall a. Bits a => Int -> a
bit Int
i;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Set Bit"
, lawContextLawBody :: String
lawContextLawBody = String
"setBit n i" String -> ShowS
`congruency` String
"n .|. bit i"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"setBit n i" String -> ShowS
`congruency` String
"n .|. bit i, where"
, String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsClearBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearBit :: Gen a -> Property
bitsClearBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let lhs :: a
lhs = a -> Int -> a
forall a. Bits a => a -> Int -> a
clearBit a
n Int
i; rhs :: a
rhs = a
n a -> a -> a
forall a. Bits a => a -> a -> a
.&. a -> a
forall a. Bits a => a -> a
complement (Int -> a
forall a. Bits a => Int -> a
bit Int
i)
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Clear Bit"
, lawContextLawBody :: String
lawContextLawBody = String
"clearBit n i" String -> ShowS
`congruency` String
"n .&. complement (bit i)"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"clearBit n i" String -> ShowS
`congruency` String
"n .&. complement (bit i), where"
, String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsComplementBit :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsComplementBit :: Gen a -> Property
bitsComplementBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
a
n <- Gen a -> PropertyT IO a
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let lhs :: a
lhs = a -> Int -> a
forall a. Bits a => a -> Int -> a
complementBit a
n Int
i; rhs :: a
rhs = a -> a -> a
forall a. Bits a => a -> a -> a
xor a
n (Int -> a
forall a. Bits a => Int -> a
bit Int
i);
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Complement Bit"
, lawContextLawBody :: String
lawContextLawBody = String
"complement n i" String -> ShowS
`congruency` String
"xor n (bit i)"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showN :: String
showN = a -> String
forall a. Show a => a -> String
show a
n
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"complement n i" String -> ShowS
`congruency` String
"xor n (bit i), where"
, String
"n = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showN
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsClearZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearZero :: Gen a -> Property
bitsClearZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let lhs :: a
lhs = a -> Int -> a
forall a. Bits a => a -> Int -> a
clearBit a
z Int
i; rhs :: a
rhs = a
z
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Clear Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"clearBit zeroBits i" String -> ShowS
`congruency` String
"zeroBits"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"clearBit zeroBits i" String -> ShowS
`congruency` String
"zeroBits, where"
, String
"zerBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsSetZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetZero :: Gen a -> Property
bitsSetZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let lhs :: a
lhs = a -> Int -> a
forall a. Bits a => a -> Int -> a
setBit a
z Int
i; rhs :: a
rhs = Int -> a
forall a. Bits a => Int -> a
bit Int
i;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Set Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"setBit zeroBits i" String -> ShowS
`congruency` String
"zeroBits"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"setBit zeroBits i" String -> ShowS
`congruency` String
"zeroBits, where"
, String
"zeroBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = a -> a -> String
forall a. Show a => a -> a -> String
reduced a
lhs a
rhs
}
a -> a -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx a
lhs a
rhs Context
ctx
bitsTestZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsTestZero :: Gen a -> Property
bitsTestZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
(BitIndex Int
i) :: BitIndex a <- Gen (BitIndex a) -> PropertyT IO (BitIndex a)
forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen (BitIndex a)
forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let lhs :: Bool
lhs = a -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit a
z Int
i; rhs :: Bool
rhs = Bool
False;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Test Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"testBit zeroBits i" String -> ShowS
`congruency` String
"False"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
showI :: String
showI = Int -> String
forall a. Show a => a -> String
show Int
i
in [String] -> String
lawWhere
[ String
"testBit zeroBits i" String -> ShowS
`congruency` String
"False, where"
, String
"zeroBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
, String
"i = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showI
]
, lawContextReduced :: String
lawContextReduced = Bool -> Bool -> String
forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs
}
Bool -> Bool -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Bool
lhs Bool
rhs Context
ctx
bitsPopZero :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsPopZero :: Gen a -> Property
bitsPopZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let lhs :: Int
lhs = a -> Int
forall a. Bits a => a -> Int
popCount a
z; rhs :: Int
rhs = Int
0;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Pop Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"popCount zeroBits" String -> ShowS
`congruency` String
"0"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
in [String] -> String
lawWhere
[ String
"popCount zeroBits" String -> ShowS
`congruency` String
"0, where"
, String
"zeroBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
]
, lawContextReduced :: String
lawContextReduced = Int -> Int -> String
forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs
}
Int -> Int -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Int
lhs Int
rhs Context
ctx
bitsCountLeadingZeros :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountLeadingZeros :: Gen a -> Property
bitsCountLeadingZeros Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let f :: Int
f = a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (a
forall a. HasCallStack => a
undefined :: a)
let lhs :: Int
lhs = a -> Int
forall b. FiniteBits b => b -> Int
countLeadingZeros a
z; rhs :: Int
rhs = Int
f;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Count Leading Zeros of Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"countLeadingZeros zeroBits" String -> ShowS
`congruency` String
"finiteBitSize (undefined :: a)"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
showF :: String
showF = Int -> String
forall a. Show a => a -> String
show Int
f
in [String] -> String
lawWhere
[ String
"countLeadingZeros zeroBits" String -> ShowS
`congruency` String
"finiteBitSize (undefined :: a), where"
, String
"zeroBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
, String
"finiteBitSize = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showF
]
, lawContextReduced :: String
lawContextReduced = Int -> Int -> String
forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs
}
Int -> Int -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Int
lhs Int
rhs Context
ctx
bitsCountTrailingZeros :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountTrailingZeros :: Gen a -> Property
bitsCountTrailingZeros Gen a
_ = HasCallStack => PropertyT IO () -> Property
PropertyT IO () -> Property
property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
forall a b. (a -> b) -> a -> b
$ do
let z :: a
z = a
forall a. Bits a => a
zeroBits :: a
let f :: Int
f = a -> Int
forall b. FiniteBits b => b -> Int
finiteBitSize (a
forall a. HasCallStack => a
undefined :: a)
let lhs :: Int
lhs = a -> Int
forall b. FiniteBits b => b -> Int
countTrailingZeros a
z; rhs :: Int
rhs = Int
f;
let ctx :: Context
ctx = LawContext -> Context
contextualise (LawContext -> Context) -> LawContext -> Context
forall a b. (a -> b) -> a -> b
$ LawContext :: String -> String -> String -> String -> String -> LawContext
LawContext
{ lawContextLawName :: String
lawContextLawName = String
"Count Trailing Zeros of Zero"
, lawContextLawBody :: String
lawContextLawBody = String
"countTrailingZeros zeroBits" String -> ShowS
`congruency` String
"finiteBitSize (undefined :: a)"
, lawContextTcName :: String
lawContextTcName = String
"Bits"
, lawContextTcProp :: String
lawContextTcProp =
let showZ :: String
showZ = a -> String
forall a. Show a => a -> String
show a
z
showF :: String
showF = Int -> String
forall a. Show a => a -> String
show Int
f
in [String] -> String
lawWhere
[ String
"countTrailingZeros zeroBits" String -> ShowS
`congruency` String
"finiteBitSize (undefined :: a), where"
, String
"zeroBits = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showZ
, String
"finiteBitSize = " String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
showF
]
, lawContextReduced :: String
lawContextReduced = Int -> Int -> String
forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs
}
Int -> Int -> Context -> PropertyT IO ()
forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Int
lhs Int
rhs Context
ctx