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

-- | Tests the following 'Bits' laws:
--
-- [__Conjunction Idempotence__]: @n '.&.' n@ ≡ @n@
-- [__Disjunction Idempotence__]: @n '.|.' n@ ≡ @n@
-- [__Double Complement__]: @'complement' '.' 'complement'@ ≡ @id@
-- [__Set Bit__]: @'setBit' n i ≡ n '.|.' 'bit' i@
-- [__Clear Bit__]: @'clearBit' n i@ ≡ @n '.&.' 'complement' ('bit' i)@
-- [__Complement Bit__]: @'complement' n i@ ≡ @'xor' n ('bit' i)@
-- [__Clear Zero__]: @'clearBit' 'zeroBits' i@ ≡ @'zeroBits'@
-- [__Set Zero__]: @'setBit' 'zeroBits' i@ ≡ @'zeroBits'@
-- [__Test Zero__]: @'testBit' 'zeroBits' i@ ≡ @'False'@
-- [__Pop Zero__]: @'popCount' 'zeroBits'@ ≡ @0@
-- [__Count Leading Zeros of Zero__]: @'countLeadingZeros' 'zeroBits'@ ≡ @'finiteBitSize' ('undefined' :: a)@
-- [__Count Trailing Zeros of Zero__]: @'countTrailingZeros' 'zeroBits'@ ≡ @'finiteBitSize' ('undefined' :: a)@
bitsLaws :: (FiniteBits a, Show a) => Gen a -> Laws
bitsLaws :: forall a. (FiniteBits a, Show a) => Gen a -> Laws
bitsLaws Gen a
gen = String -> [(String, Property)] -> Laws
Laws String
"Bits"
  [ (String
"Conjunction Idempotence", forall a. (Bits a, Show a) => Gen a -> Property
bitsConjunctionIdempotence Gen a
gen)
  , (String
"Disjunction Idempotence", forall a. (Bits a, Show a) => Gen a -> Property
bitsDisjunctionIdempotence Gen a
gen)
  , (String
"Double Complement", forall a. (Bits a, Show a) => Gen a -> Property
bitsDoubleComplement Gen a
gen) 
  , (String
"Set Bit", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetBit Gen a
gen) 
  , (String
"Clear Bit", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearBit Gen a
gen)
  , (String
"Complement Bit", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsComplementBit Gen a
gen)
  , (String
"Clear Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearZero Gen a
gen)
  , (String
"Set Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetZero Gen a
gen)
  , (String
"Test Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsTestZero Gen a
gen)
  , (String
"Pop Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsPopZero Gen a
gen)
  , (String
"Count Leading Zeros of Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountLeadingZeros Gen a
gen)
  , (String
"Count Trailing Zeros of Zero", forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountTrailingZeros Gen a
gen)
  ]

newtype BitIndex a = BitIndex Int
  deriving (Int -> BitIndex a -> ShowS
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 :: forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex = let n :: Int
n = forall b. FiniteBits b => b -> Int
finiteBitSize (forall a. HasCallStack => a
undefined :: a) in if Int
n forall a. Ord a => a -> a -> Bool
> Int
0
  then forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap forall a. Int -> BitIndex a
BitIndex (forall (m :: * -> *) a. (MonadGen m, Integral a) => Range a -> m a
Gen.integral forall a b. (a -> b) -> a -> b
$ forall a. Integral a => a -> a -> Range a
Range.linear Int
0 (Int
n forall a. Num a => a -> a -> a
- Int
1))
  else forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall a. Int -> BitIndex a
BitIndex Int
0)

bitsConjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
bitsConjunctionIdempotence :: forall a. (Bits a, Show a) => Gen a -> Property
bitsConjunctionIdempotence Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
n forall a. Bits a => a -> a -> a
.&. a
n; rhs :: a
rhs = a
n; 
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
n;
            in [String] -> String
lawWhere [ String
"n .&. n" String -> ShowS
`congruency` String
"n, where", String
"n = " forall a. [a] -> [a] -> [a]
++ String
showN ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  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 :: forall a. (Bits a, Show a) => Gen a -> Property
bitsDisjunctionIdempotence Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = a
n forall a. Bits a => a -> a -> a
.|. a
n; rhs :: a
rhs = a
n; 
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
n
            in [String] -> String
lawWhere [ String
"n .|. n" String -> ShowS
`congruency` String
"n, where", String
"n = " forall a. [a] -> [a] -> [a]
++ String
showN ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  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 :: forall a. (Bits a, Show a) => Gen a -> Property
bitsDoubleComplement Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  let lhs :: a
lhs = forall a. Bits a => a -> a
complement (forall a. Bits a => a -> a
complement a
n); rhs :: a
rhs = a
n;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = 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 = " forall a. [a] -> [a] -> [a]
++ String
showN ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let lhs :: a
lhs = forall a. Bits a => a -> Int -> a
setBit a
n Int
i; rhs :: a
rhs = a
n forall a. Bits a => a -> a -> a
.|. forall a. Bits a => Int -> a
bit Int
i;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
n
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showN
                 , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        } 
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let lhs :: a
lhs = forall a. Bits a => a -> Int -> a
clearBit a
n Int
i; rhs :: a
rhs = a
n forall a. Bits a => a -> a -> a
.&. forall a. Bits a => a -> a
complement (forall a. Bits a => Int -> a
bit Int
i)
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
n
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showN
                 , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsComplementBit Gen a
gen = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  a
n <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll Gen a
gen
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let lhs :: a
lhs = forall a. Bits a => a -> Int -> a
complementBit a
n Int
i; rhs :: a
rhs = forall a. Bits a => a -> a -> a
xor a
n (forall a. Bits a => Int -> a
bit Int
i);
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
n
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showN
                 , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        } 
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsClearZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let lhs :: a
lhs = forall a. Bits a => a -> Int -> a
clearBit a
z Int
i; rhs :: a
rhs = a
z
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showZ
                 , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
                 ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsSetZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let lhs :: a
lhs = forall a. Bits a => a -> Int -> a
setBit a
z Int
i; rhs :: a
rhs = forall a. Bits a => Int -> a
bit Int
i;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showZ
              , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced a
lhs a
rhs 
        }
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsTestZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  (BitIndex Int
i) :: BitIndex a <- forall (m :: * -> *) a.
(Monad m, Show a, HasCallStack) =>
Gen a -> PropertyT m a
forAll forall a. FiniteBits a => Gen (BitIndex a)
genBitIndex
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let lhs :: Bool
lhs = forall a. Bits a => a -> Int -> Bool
testBit a
z Int
i; rhs :: Bool
rhs = Bool
False;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
                showI :: String
showI = 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 = " forall a. [a] -> [a] -> [a]
++ String
showZ
              , String
"i = " forall a. [a] -> [a] -> [a]
++ String
showI
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Bool
lhs Bool
rhs 
        }
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsPopZero Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let lhs :: Int
lhs = forall a. Bits a => a -> Int
popCount a
z; rhs :: Int
rhs = Int
0;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
            in [String] -> String
lawWhere
              [ String
"popCount zeroBits" String -> ShowS
`congruency` String
"0, where"
              , String
"zeroBits = " forall a. [a] -> [a] -> [a]
++ String
showZ
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs 
        } 
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountLeadingZeros Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let f :: Int
f = forall b. FiniteBits b => b -> Int
finiteBitSize (forall a. HasCallStack => a
undefined :: a)
  let lhs :: Int
lhs = forall b. FiniteBits b => b -> Int
countLeadingZeros a
z; rhs :: Int
rhs = Int
f;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
                showF :: String
showF = 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 = " forall a. [a] -> [a] -> [a]
++ String
showZ
              , String
"finiteBitSize = " forall a. [a] -> [a] -> [a]
++ String
showF
              ]
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs 
        } 
  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 :: forall a. (FiniteBits a, Show a) => Gen a -> Property
bitsCountTrailingZeros Gen a
_ = HasCallStack => PropertyT IO () -> Property
property forall a b. (a -> b) -> a -> b
$ do
  let z :: a
z = forall a. Bits a => a
zeroBits :: a
  let f :: Int
f = forall b. FiniteBits b => b -> Int
finiteBitSize (forall a. HasCallStack => a
undefined :: a)
  let lhs :: Int
lhs = forall b. FiniteBits b => b -> Int
countTrailingZeros a
z; rhs :: Int
rhs = Int
f;
  let ctx :: Context
ctx = LawContext -> Context
contextualise forall a b. (a -> b) -> a -> b
$ 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 = forall a. Show a => a -> String
show a
z
                showF :: String
showF = 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 = " forall a. [a] -> [a] -> [a]
++ String
showZ
              , String
"finiteBitSize = " forall a. [a] -> [a] -> [a]
++ String
showF
              ]           
        , lawContextReduced :: String
lawContextReduced = forall a. Show a => a -> a -> String
reduced Int
lhs Int
rhs 
        }
  forall (m :: * -> *) a.
(MonadTest m, HasCallStack, Eq a, Show a) =>
a -> a -> Context -> m ()
heqCtx Int
lhs Int
rhs Context
ctx