    {-# 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", 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
    $cshowsPrec :: forall a. Int -> BitIndex a -> ShowS
    showsPrec :: Int -> BitIndex a -> ShowS
    $cshow :: forall a. BitIndex a -> String
    show :: BitIndex a -> String
    $cshowList :: forall a. [BitIndex a] -> ShowS
    showList :: [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 = 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 -> GenT Identity (BitIndex a)
    forall a b. (a -> b) -> GenT Identity a -> GenT Identity b
    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 -> GenT Identity (BitIndex a)
    forall a. a -> GenT Identity 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 :: forall a. (Bits a, Show a) => 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
      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
    n a -> a -> a
    forall a. Bits a => a -> a -> a
    .&. a
    n; rhs = a
    n;
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      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
    n a -> a -> a
    forall a. Bits a => a -> a -> a
    .|. a
    n; rhs = a
    n;
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      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 -> a
    forall a. Bits a => a -> a
    complement (a -> a
    forall a. Bits a => a -> a
    complement a
    n); rhs = a
    n;
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }

      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      n <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      (BitIndex i) :: BitIndex a <- forAll genBitIndex
      let lhs = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    setBit a
    n Int
    i; 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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      n <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      (BitIndex i) :: BitIndex a <- forAll genBitIndex
      let lhs = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    clearBit a
    n Int
    i; 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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      n <- Gen a -> PropertyT IO a
    forall (m :: * -> *) a.
    (Monad m, Show a, HasCallStack) =>
    Gen a -> PropertyT m a
    forAll Gen a
    gen
      (BitIndex i) :: BitIndex a <- forAll genBitIndex
      let lhs = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    complementBit a
    n Int
    i; 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 = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      (BitIndex 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
    forall a. Bits a => a
    zeroBits :: a
      let lhs = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    clearBit a
    z Int
    i; rhs = a
    z
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      (BitIndex 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
    forall a. Bits a => a
    zeroBits :: a
      let lhs = a -> Int -> a
    forall a. Bits a => a -> Int -> a
    setBit a
    z Int
    i; rhs = Int -> a
    forall a. Bits a => Int -> a
    bit Int
    i;
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    PropertyT IO () -> Property
    property (PropertyT IO () -> Property) -> PropertyT IO () -> Property
    forall a b. (a -> b) -> a -> b
    $ do
      (BitIndex 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
    forall a. Bits a => a
    zeroBits :: a
      let lhs = a -> Int -> Bool
    forall a. Bits a => a -> Int -> Bool
    testBit a
    z Int
    i; rhs = Bool
    False;
      let ctx = LawContext -> Context
    contextualise (LawContext -> Context) -> LawContext -> Context
    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 = 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
            }
      heqCtx lhs rhs 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
    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
            { 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 :: forall a. (FiniteBits a, Show a) => 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
            { 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 :: forall a. (FiniteBits a, Show a) => 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
            { 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