    {-# LANGUAGE CPP #-}
    {-# LANGUAGE DataKinds #-}
    {-# LANGUAGE DeriveAnyClass #-}
    {-# LANGUAGE DeriveGeneric #-}
    {-# LANGUAGE DeriveLift #-}
    {-# LANGUAGE GADTs #-}
    {-# LANGUAGE KindSignatures #-}
    {-# LANGUAGE PatternSynonyms #-}
    {-# LANGUAGE ScopedTypeVariables #-}
    {-# LANGUAGE TemplateHaskell #-}
    {-# LANGUAGE TypeOperators #-}
    {-# LANGUAGE TypeApplications #-}

    {-|
    Module      : Data.BitVector.Sized.Unsigned
    Copyright   : (c) Galois Inc. 2018
    License     : BSD-3
    Maintainer  : benselfridge@galois.com
    Stability   : experimental
    Portability : portable

    This module defines a wrapper around the 'BV' type, 'UnsignedBV', with
    instances not provided by 'BV'.
    -}

    module Data.BitVector.Sized.Unsigned
      ( UnsignedBV(..)
      , mkUnsignedBV
      ) where

    import Control.DeepSeq (NFData)
    import           Data.BitVector.Sized.Internal (BV(..), mkBV)
    import qualified Data.BitVector.Sized.Internal as BV
    import           Data.BitVector.Sized.Panic (panic)
    import           Data.Parameterized.Classes (Hashable(..))
    import           Data.Parameterized.NatRepr (NatRepr, knownNat, maxUnsigned, widthVal)

    import Data.Bits (Bits(..), FiniteBits(..))
    import Data.Ix (Ix(inRange, range, index))
    import GHC.Generics (Generic)
    import GHC.TypeLits (KnownNat)
    import Language.Haskell.TH.Lift (Lift)
    import Numeric.Natural (Natural)
    import System.Random
    import System.Random.Stateful

    -- | Signed bit vector.
    newtype UnsignedBV w = UnsignedBV { forall (w :: Natural). UnsignedBV w -> BV w
    asBV :: BV w }
      deriving ((forall x. UnsignedBV w -> Rep (UnsignedBV w) x)
    -> (forall x. Rep (UnsignedBV w) x -> UnsignedBV w)
    -> Generic (UnsignedBV w)
    forall (w :: Natural) x. Rep (UnsignedBV w) x -> UnsignedBV w
    forall (w :: Natural) x. UnsignedBV w -> Rep (UnsignedBV w) x
    forall x. Rep (UnsignedBV w) x -> UnsignedBV w
    forall x. UnsignedBV w -> Rep (UnsignedBV w) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall (w :: Natural) x. UnsignedBV w -> Rep (UnsignedBV w) x
    from :: forall x. UnsignedBV w -> Rep (UnsignedBV w) x
    $cto :: forall (w :: Natural) x. Rep (UnsignedBV w) x -> UnsignedBV w
    to :: forall x. Rep (UnsignedBV w) x -> UnsignedBV w
    Generic, Int -> UnsignedBV w -> ShowS
    [UnsignedBV w] -> ShowS
    UnsignedBV w -> String
    (Int -> UnsignedBV w -> ShowS)
    -> (UnsignedBV w -> String)
    -> ([UnsignedBV w] -> ShowS)
    -> Show (UnsignedBV w)
    forall (w :: Natural). Int -> UnsignedBV w -> ShowS
    forall (w :: Natural). [UnsignedBV w] -> ShowS
    forall (w :: Natural). UnsignedBV w -> String
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: forall (w :: Natural). Int -> UnsignedBV w -> ShowS
    showsPrec :: Int -> UnsignedBV w -> ShowS
    $cshow :: forall (w :: Natural). UnsignedBV w -> String
    show :: UnsignedBV w -> String
    $cshowList :: forall (w :: Natural). [UnsignedBV w] -> ShowS
    showList :: [UnsignedBV w] -> ShowS
    Show, ReadPrec [UnsignedBV w]
    ReadPrec (UnsignedBV w)
    Int -> ReadS (UnsignedBV w)
    ReadS [UnsignedBV w]
    (Int -> ReadS (UnsignedBV w))
    -> ReadS [UnsignedBV w]
    -> ReadPrec (UnsignedBV w)
    -> ReadPrec [UnsignedBV w]
    -> Read (UnsignedBV w)
    forall (w :: Natural). ReadPrec [UnsignedBV w]
    forall (w :: Natural). ReadPrec (UnsignedBV w)
    forall (w :: Natural). Int -> ReadS (UnsignedBV w)
    forall (w :: Natural). ReadS [UnsignedBV w]
    forall a.
    (Int -> ReadS a)
    -> ReadS [a] -> ReadPrec a -> ReadPrec [a] -> Read a
    $creadsPrec :: forall (w :: Natural). Int -> ReadS (UnsignedBV w)
    readsPrec :: Int -> ReadS (UnsignedBV w)
    $creadList :: forall (w :: Natural). ReadS [UnsignedBV w]
    readList :: ReadS [UnsignedBV w]
    $creadPrec :: forall (w :: Natural). ReadPrec (UnsignedBV w)
    readPrec :: ReadPrec (UnsignedBV w)
    $creadListPrec :: forall (w :: Natural). ReadPrec [UnsignedBV w]
    readListPrec :: ReadPrec [UnsignedBV w]
    Read, UnsignedBV w -> UnsignedBV w -> Bool
    (UnsignedBV w -> UnsignedBV w -> Bool)
    -> (UnsignedBV w -> UnsignedBV w -> Bool) -> Eq (UnsignedBV w)
    forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    == :: UnsignedBV w -> UnsignedBV w -> Bool
    $c/= :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    /= :: UnsignedBV w -> UnsignedBV w -> Bool
    Eq, Eq (UnsignedBV w)
    Eq (UnsignedBV w) =>
    (UnsignedBV w -> UnsignedBV w -> Ordering)
    -> (UnsignedBV w -> UnsignedBV w -> Bool)
    -> (UnsignedBV w -> UnsignedBV w -> Bool)
    -> (UnsignedBV w -> UnsignedBV w -> Bool)
    -> (UnsignedBV w -> UnsignedBV w -> Bool)
    -> (UnsignedBV w -> UnsignedBV w -> UnsignedBV w)
    -> (UnsignedBV w -> UnsignedBV w -> UnsignedBV w)
    -> Ord (UnsignedBV w)
    UnsignedBV w -> UnsignedBV w -> Bool
    UnsignedBV w -> UnsignedBV w -> Ordering
    UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural). Eq (UnsignedBV w)
    forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Ordering
    forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Ordering
    compare :: UnsignedBV w -> UnsignedBV w -> Ordering
    $c< :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    < :: UnsignedBV w -> UnsignedBV w -> Bool
    $c<= :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    <= :: UnsignedBV w -> UnsignedBV w -> Bool
    $c> :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    > :: UnsignedBV w -> UnsignedBV w -> Bool
    $c>= :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> Bool
    >= :: UnsignedBV w -> UnsignedBV w -> Bool
    $cmax :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    max :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    $cmin :: forall (w :: Natural). UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    min :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    Ord, (forall (m :: * -> *). Quote m => UnsignedBV w -> m Exp)
    -> (forall (m :: * -> *).
        Quote m =>
        UnsignedBV w -> Code m (UnsignedBV w))
    -> Lift (UnsignedBV w)
    forall (w :: Natural) (m :: * -> *).
    Quote m =>
    UnsignedBV w -> m Exp
    forall (w :: Natural) (m :: * -> *).
    Quote m =>
    UnsignedBV w -> Code m (UnsignedBV w)
    forall t.
    (forall (m :: * -> *). Quote m => t -> m Exp)
    -> (forall (m :: * -> *). Quote m => t -> Code m t) -> Lift t
    forall (m :: * -> *). Quote m => UnsignedBV w -> m Exp
    forall (m :: * -> *).
    Quote m =>
    UnsignedBV w -> Code m (UnsignedBV w)
    $clift :: forall (w :: Natural) (m :: * -> *).
    Quote m =>
    UnsignedBV w -> m Exp
    lift :: forall (m :: * -> *). Quote m => UnsignedBV w -> m Exp
    $cliftTyped :: forall (w :: Natural) (m :: * -> *).
    Quote m =>
    UnsignedBV w -> Code m (UnsignedBV w)
    liftTyped :: forall (m :: * -> *).
    Quote m =>
    UnsignedBV w -> Code m (UnsignedBV w)
    Lift, UnsignedBV w -> ()
    (UnsignedBV w -> ()) -> NFData (UnsignedBV w)
    forall (w :: Natural). UnsignedBV w -> ()
    forall a. (a -> ()) -> NFData a
    $crnf :: forall (w :: Natural). UnsignedBV w -> ()
    rnf :: UnsignedBV w -> ()
    NFData)

    -- | Convenience wrapper for 'BV.mkBV'.
    mkUnsignedBV :: NatRepr w -> Integer -> UnsignedBV w
    mkUnsignedBV :: forall (w :: Natural). NatRepr w -> Integer -> UnsignedBV w
    mkUnsignedBV NatRepr w
    w Integer
    x = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    BV.mkBV NatRepr w
    w Integer
    x)

    liftUnary :: (BV w -> BV w)
              -> UnsignedBV w
              -> UnsignedBV w
    liftUnary :: forall (w :: Natural).
    (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
    liftUnary BV w -> BV w
    op (UnsignedBV BV w
    bv) = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> BV w
    op BV w
    bv)

    liftBinary :: (BV w -> BV w -> BV w)
               -> UnsignedBV w
               -> UnsignedBV w
               -> UnsignedBV w
    liftBinary :: forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary BV w -> BV w -> BV w
    op (UnsignedBV BV w
    bv1) (UnsignedBV BV w
    bv2) = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> BV w -> BV w
    op BV w
    bv1 BV w
    bv2)

    liftBinaryInt :: (BV w -> Natural -> BV w)
                  -> UnsignedBV w
                  -> Int
                  -> UnsignedBV w
    liftBinaryInt :: forall (w :: Natural).
    (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    liftBinaryInt BV w -> Natural -> BV w
    op (UnsignedBV BV w
    bv) Int
    i = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> Natural -> BV w
    op BV w
    bv (Int -> Natural
    intToNatural Int
    i))

    intToNatural :: Int -> Natural
    intToNatural :: Int -> Natural
    intToNatural = Int -> Natural
    forall a b. (Integral a, Num b) => a -> b
    fromIntegral

    instance KnownNat w => Bits (UnsignedBV w) where
      .&. :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    (.&.)        = (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    BV.and
      .|. :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    (.|.)        = (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    BV.or
      xor :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    xor          = (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary BV w -> BV w -> BV w
    forall (w :: Natural). BV w -> BV w -> BV w
    BV.xor
      complement :: UnsignedBV w -> UnsignedBV w
    complement   = (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
    liftUnary (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.complement NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      shiftL :: UnsignedBV w -> Int -> UnsignedBV w
    shiftL       = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.shl NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      shiftR :: UnsignedBV w -> Int -> UnsignedBV w
    shiftR       = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.lshr NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      rotateL :: UnsignedBV w -> Int -> UnsignedBV w
    rotateL      = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.rotateL NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      rotateR :: UnsignedBV w -> Int -> UnsignedBV w
    rotateR      = (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> Natural -> BV w) -> UnsignedBV w -> Int -> UnsignedBV w
    liftBinaryInt (NatRepr w -> BV w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> Natural -> BV w
    BV.rotateR NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      bitSize :: UnsignedBV w -> Int
    bitSize UnsignedBV w
    _    = NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @w)
      bitSizeMaybe :: UnsignedBV w -> Maybe Int
    bitSizeMaybe UnsignedBV w
    _ = Int -> Maybe Int
    forall a. a -> Maybe a
    Just (NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @w))
      isSigned :: UnsignedBV w -> Bool
    isSigned     = Bool -> UnsignedBV w -> Bool
    forall a b. a -> b -> a
    const Bool
    False
      testBit :: UnsignedBV w -> Int -> Bool
    testBit (UnsignedBV BV w
    bv) Int
    ix = Natural -> BV w -> Bool
    forall (w :: Natural). Natural -> BV w -> Bool
    BV.testBit' (Int -> Natural
    intToNatural Int
    ix) BV w
    bv
      bit :: Int -> UnsignedBV w
    bit          = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w) -> (Int -> BV w) -> Int -> UnsignedBV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr w -> Natural -> BV w
    forall (w :: Natural). NatRepr w -> Natural -> BV w
    BV.bit' NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat (Natural -> BV w) -> (Int -> Natural) -> Int -> BV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Natural
    intToNatural
      popCount :: UnsignedBV w -> Int
    popCount (UnsignedBV BV w
    bv) = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> BV w
    forall (w :: Natural). BV w -> BV w
    BV.popCount BV w
    bv))

    instance KnownNat w => FiniteBits (UnsignedBV w) where
      finiteBitSize :: UnsignedBV w -> Int
    finiteBitSize UnsignedBV w
    _ = NatRepr w -> Int
    forall (n :: Natural). NatRepr n -> Int
    widthVal (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @w)
      countLeadingZeros :: UnsignedBV w -> Int
    countLeadingZeros  (UnsignedBV BV w
    bv) = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> Integer) -> BV w -> Integer
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.clz NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    bv
      countTrailingZeros :: UnsignedBV w -> Int
    countTrailingZeros (UnsignedBV BV w
    bv) = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (Integer -> Int) -> Integer -> Int
    forall a b. (a -> b) -> a -> b
    $ BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned (BV w -> Integer) -> BV w -> Integer
    forall a b. (a -> b) -> a -> b
    $ NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.ctz NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat BV w
    bv

    instance KnownNat w => Num (UnsignedBV w) where
      + :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    (+)         = (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    BV.add NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      * :: UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    (*)         = (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w -> BV w)
    -> UnsignedBV w -> UnsignedBV w -> UnsignedBV w
    liftBinary (NatRepr w -> BV w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w -> BV w
    BV.mul NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      abs :: UnsignedBV w -> UnsignedBV w
    abs         = UnsignedBV w -> UnsignedBV w
    forall a. a -> a
    id
      signum :: UnsignedBV w -> UnsignedBV w
    signum (UnsignedBV BV w
    bv) = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w) -> BV w -> UnsignedBV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> BV w
    forall (w :: Natural). Integer -> BV w
    BV.BV (Integer -> BV w) -> Integer -> BV w
    forall a b. (a -> b) -> a -> b
    $ Integer -> Integer
    forall a. Num a => a -> a
    signum (Integer -> Integer) -> Integer -> Integer
    forall a b. (a -> b) -> a -> b
    $ BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    bv
      fromInteger :: Integer -> UnsignedBV w
    fromInteger = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w)
    -> (Integer -> BV w) -> Integer -> UnsignedBV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat
      -- in this case, negate just means "additive inverse"
      negate :: UnsignedBV w -> UnsignedBV w
    negate      = (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
    forall (w :: Natural).
    (BV w -> BV w) -> UnsignedBV w -> UnsignedBV w
    liftUnary (NatRepr w -> BV w -> BV w
    forall (w :: Natural). NatRepr w -> BV w -> BV w
    BV.negate NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)

    instance KnownNat w => Enum (UnsignedBV w) where
      toEnum :: Int -> UnsignedBV w
    toEnum = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w) -> (Int -> BV w) -> Int -> UnsignedBV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat (Integer -> BV w) -> (Int -> Integer) -> Int -> BV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Integer
    checkInt
        where checkInt :: Int -> Integer
    checkInt Int
    i | Int
    0 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    i Bool -> Bool -> Bool
    && Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i Integer -> Integer -> Bool
    forall a. Ord a => a -> a -> Bool
    <= NatRepr w -> Integer
    forall (w :: Natural). NatRepr w -> Integer
    maxUnsigned (forall (n :: Natural). KnownNat n => NatRepr n
    knownNat @w) = Int -> Integer
    forall a. Integral a => a -> Integer
    toInteger Int
    i
                         | Bool
    otherwise = String -> [String] -> Integer
    forall a. String -> [String] -> a
    panic String
    "Data.BitVector.Sized.Unsigned"
                                       [String
    "toEnum: bad argument"]

      fromEnum :: UnsignedBV w -> Int
    fromEnum (UnsignedBV BV w
    bv) = Integer -> Int
    forall a. Num a => Integer -> a
    fromInteger (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    bv)

    instance KnownNat w => Ix (UnsignedBV w) where
      range :: (UnsignedBV w, UnsignedBV w) -> [UnsignedBV w]
    range (UnsignedBV BV w
    loBV, UnsignedBV BV w
    hiBV) =
        BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w)
    -> (Integer -> BV w) -> Integer -> UnsignedBV w
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NatRepr w -> Integer -> BV w
    forall (w :: Natural). NatRepr w -> Integer -> BV w
    mkBV NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat (Integer -> UnsignedBV w) -> [Integer] -> [UnsignedBV w]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$>
        [BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    loBV .. BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    hiBV]
      index :: (UnsignedBV w, UnsignedBV w) -> UnsignedBV w -> Int
    index (UnsignedBV BV w
    loBV, UnsignedBV BV w
    hiBV) (UnsignedBV BV w
    ixBV) =
        (Integer, Integer) -> Integer -> Int
    forall a. Ix a => (a, a) -> a -> Int
    index ( BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    loBV,
                BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    hiBV)
        (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    ixBV)
      inRange :: (UnsignedBV w, UnsignedBV w) -> UnsignedBV w -> Bool
    inRange (UnsignedBV BV w
    loBV, UnsignedBV BV w
    hiBV) (UnsignedBV BV w
    ixBV) =
        (Integer, Integer) -> Integer -> Bool
    forall a. Ix a => (a, a) -> a -> Bool
    inRange ( BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    loBV
                , BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    hiBV)
        (BV w -> Integer
    forall (w :: Natural). BV w -> Integer
    BV.asUnsigned BV w
    ixBV)

    instance KnownNat w => Bounded (UnsignedBV w) where
      minBound :: UnsignedBV w
    minBound = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.minUnsigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)
      maxBound :: UnsignedBV w
    maxBound = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (NatRepr w -> BV w
    forall (w :: Natural). NatRepr w -> BV w
    BV.maxUnsigned NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat)

    instance KnownNat w => Uniform (UnsignedBV w) where
      uniformM :: forall g (m :: * -> *). StatefulGen g m => g -> m (UnsignedBV w)
    uniformM g
    g = BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w) -> m (BV w) -> m (UnsignedBV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> NatRepr w -> g -> m (BV w)
    forall g (m :: * -> *) (w :: Natural).
    StatefulGen g m =>
    NatRepr w -> g -> m (BV w)
    BV.uniformM NatRepr w
    forall (n :: Natural). KnownNat n => NatRepr n
    knownNat g
    g

    instance UniformRange (UnsignedBV w) where
      uniformRM :: forall g (m :: * -> *).
    StatefulGen g m =>
    (UnsignedBV w, UnsignedBV w) -> g -> m (UnsignedBV w)
    uniformRM (UnsignedBV BV w
    lo, UnsignedBV BV w
    hi) g
    g =
        BV w -> UnsignedBV w
    forall (w :: Natural). BV w -> UnsignedBV w
    UnsignedBV (BV w -> UnsignedBV w) -> m (BV w) -> m (UnsignedBV w)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (BV w, BV w) -> g -> m (BV w)
    forall g (m :: * -> *) (w :: Natural).
    StatefulGen g m =>
    (BV w, BV w) -> g -> m (BV w)
    BV.uUniformRM (BV w
    lo, BV w
    hi) g
    g
    #if MIN_VERSION_random(1,3,0)
      isInRange (lo, hi) x =
        lo <= x && x <= hi
    #endif

    instance KnownNat w => Random (UnsignedBV w)

    instance Hashable (UnsignedBV w) where
      hashWithSalt :: Int -> UnsignedBV w -> Int
    hashWithSalt Int
    salt (UnsignedBV BV w
    b) = Int -> BV w -> Int
    forall a. Hashable a => Int -> a -> Int
    hashWithSalt Int
    salt BV w
    b