-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/

-- | a bitvector datatype that is parameterized by the vector width
--   
--   This module defines a width-parameterized bitvector type and various
--   associated operations.
@package bv-sized
@version 1.0.5

-- | This module provides alternative definitions of certain bitvector
--   functions that might produce signed or unsigned overflow. Instead of
--   producing a pure value, these versions produce the same value along
--   with overflow flags. We only provide definitions for operators that
--   might actually overflow.
module Data.BitVector.Sized.Overflow

-- | A value annotated with overflow information.
data Overflow a
Overflow :: UnsignedOverflow -> SignedOverflow -> a -> Overflow a

-- | Datatype representing the possibility of unsigned overflow.
data UnsignedOverflow
UnsignedOverflow :: UnsignedOverflow
NoUnsignedOverflow :: UnsignedOverflow

-- | Datatype representing the possibility of signed overflow.
data SignedOverflow
SignedOverflow :: SignedOverflow
NoSignedOverflow :: SignedOverflow

-- | Return True if a computation caused unsigned overflow.
ofUnsigned :: Overflow a -> Bool

-- | Return True if a computation caused signed overflow.
ofSigned :: Overflow a -> Bool

-- | Return the result of a computation.
ofResult :: Overflow a -> a

-- | Left shift by positive Natural.
shlOf :: 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w)

-- | Bitvector add.
addOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector subtract.
subOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector multiply.
mulOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector division (signed). Rounds to zero. Division by zero yields a
--   runtime error.
squotOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector remainder after division (signed), when rounded to zero.
--   Division by zero yields a runtime error.
sremOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector division (signed). Rounds to zero. Division by zero yields a
--   runtime error.
sdivOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)

-- | Bitvector remainder after division (signed), when rounded to zero.
--   Division by zero yields a runtime error.
smodOf :: 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
instance GHC.Classes.Eq Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Show.Show Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Classes.Eq Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Show.Show Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.BitVector.Sized.Overflow.Overflow a)
instance GHC.Show.Show a => GHC.Show.Show (Data.BitVector.Sized.Overflow.Overflow a)
instance Data.Foldable.Foldable Data.BitVector.Sized.Overflow.Overflow
instance Data.Traversable.Traversable Data.BitVector.Sized.Overflow.Overflow
instance GHC.Base.Functor Data.BitVector.Sized.Overflow.Overflow
instance GHC.Base.Applicative Data.BitVector.Sized.Overflow.Overflow
instance GHC.Base.Monad Data.BitVector.Sized.Overflow.Overflow
instance GHC.Base.Semigroup Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Base.Monoid Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Base.Semigroup Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Base.Monoid Data.BitVector.Sized.Overflow.UnsignedOverflow

-- | This module defines a width-parameterized BV type and various
--   associated operations. A BV w is a newtype around an
--   Integer, so operations that require the width take an explicit
--   NatRepr w argument. We explicitly do not allow widths
--   that cannot be represented as an Int, as we appeal to the
--   underlying Num and Bits instances on Integer for
--   the implementation of many of the same operations (which, in turn,
--   require those widths to be Ints).
--   
--   We omit all typeclass instances that require compile-time knowledge of
--   bitvector width, or force a signed or unsigned intepretation. Those
--   instances can be recovered via the use of SignedBV or
--   UnsignedBV.
--   
--   This module should be imported qualified, as many of the names clash
--   with those in Prelude or other base packages.
module Data.BitVector.Sized

-- | Bitvector datatype, parameterized by width.
data BV (w :: Nat) :: Type

-- | Get the underlying Integer representation from a BV. We
--   guarantee that (\(BV.BV x) -> x) == BV.asUnsigned.
pattern BV :: Integer -> BV w

-- | A runtime presentation of a type-level Nat.
--   
--   This can be used for performing dynamic checks on a type-level natural
--   numbers.
data () => NatRepr (n :: Nat)

-- | This generates a NatRepr from a type-level context.
knownNat :: forall (n :: Nat). KnownNat n => NatRepr n

-- | Construct a bitvector with a particular width, where the width is
--   provided as an explicit NatRepr argument. The input
--   Integer, whether positive or negative, is silently truncated to
--   fit into the number of bits demanded by the return type. The width
--   cannot be arbitrarily large; it must be representable as an
--   Int.
--   
--   
--   >>> mkBV (knownNat @4) 10
--   BV 10
--   
--   >>> mkBV (knownNat @2) 10
--   BV 2
--   
--   >>> mkBV (knownNat @4) (-2)
--   BV 14
--   
mkBV :: NatRepr w -> Integer -> BV w

-- | Like mkBV, but returns Nothing if unsigned input integer
--   cannot be represented in w bits.
mkBVUnsigned :: NatRepr w -> Integer -> Maybe (BV w)

-- | Like mkBV, but returns Nothing if signed input integer
--   cannot be represented in w bits.
mkBVSigned :: 1 <= w => NatRepr w -> Integer -> Maybe (BV w)

-- | unsignedClamp w i rounds i to the nearest value
--   between 0 and 2^w - 1 (inclusive).
unsignedClamp :: NatRepr w -> Integer -> BV w

-- | signedClamp w i rounds i to the nearest value
--   between -2^(w-1) and 2^(w-1) - 1 (inclusive).
signedClamp :: 1 <= w => NatRepr w -> Integer -> BV w

-- | The minimum unsigned value for bitvector with given width (always 0).
minUnsigned :: NatRepr w -> BV w

-- | The maximum unsigned value for bitvector with given width.
maxUnsigned :: NatRepr w -> BV w

-- | The minimum value for bitvector in two's complement with given width.
minSigned :: 1 <= w => NatRepr w -> BV w

-- | The maximum value for bitvector in two's complement with given width.
maxSigned :: 1 <= w => NatRepr w -> BV w

-- | The zero bitvector of any width.
zero :: NatRepr w -> BV w

-- | The bitvector with value 1, of any positive width.
one :: 1 <= w => NatRepr w -> BV w

-- | The bitvector whose value is its own width, of any width.
width :: NatRepr w -> BV w

-- | Construct a BV from a Bool.
bool :: Bool -> BV 1

-- | Construct a BV from a Word8.
word8 :: Word8 -> BV 8

-- | Construct a BV from a Word16.
word16 :: Word16 -> BV 16

-- | Construct a BV from a Word32.
word32 :: Word32 -> BV 32

-- | Construct a BV from a Word64.
word64 :: Word64 -> BV 64

-- | Construct a BV from an Int8.
int8 :: Int8 -> BV 8

-- | Construct a BV from an Int16.
int16 :: Int16 -> BV 16

-- | Construct a BV from an Int32.
int32 :: Int32 -> BV 32

-- | Construct a BV from an Int64.
int64 :: Int64 -> BV 64

-- | Construct a BV from a list of bits, in big endian order (bits
--   with lower value index in the list are mapped to higher order bits in
--   the output bitvector). Return the resulting BV along with its
--   width.
--   
--   
--   >>> case bitsBE [True, False] of p -> (fstPair p, sndPair p)
--   (2,BV 2)
--   
bitsBE :: [Bool] -> Pair NatRepr BV

-- | Construct a BV from a list of bits, in little endian order
--   (bits with lower value index in the list are mapped to lower order
--   bits in the output bitvector). Return the resulting BV along
--   with its width.
--   
--   
--   >>> case bitsLE [True, False] of p -> (fstPair p, sndPair p)
--   (2,BV 1)
--   
bitsLE :: [Bool] -> Pair NatRepr BV

-- | Construct a BV from a list of bytes, in big endian order (bytes
--   with lower value index in the list are mapped to higher order bytes in
--   the output bitvector).
--   
--   
--   >>> case bytesBE [0, 1, 1] of p -> (fstPair p, sndPair p)
--   (24,BV 257)
--   
bytesBE :: [Word8] -> Pair NatRepr BV

-- | Construct a BV from a list of bytes, in little endian order
--   (bytes with lower value index in the list are mapped to lower order
--   bytes in the output bitvector).
--   
--   
--   >>> case bytesLE [0, 1, 1] of p -> (fstPair p, sndPair p)
--   (24,BV 65792)
--   
bytesLE :: [Word8] -> Pair NatRepr BV

-- | Construct a BV from a big-endian bytestring.
--   
--   
--   >>> case bytestringBE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
--   (24,BV 257)
--   
bytestringBE :: ByteString -> Pair NatRepr BV

-- | Construct a BV from a little-endian bytestring.
--   
--   
--   >>> case bytestringLE (BS.pack [0, 1, 1]) of p -> (fstPair p, sndPair p)
--   (24,BV 65792)
--   
bytestringLE :: ByteString -> Pair NatRepr BV

-- | Signed interpretation of a bitvector as an Integer.
asSigned :: 1 <= w => NatRepr w -> BV w -> Integer

-- | Unsigned interpretation of a bitvector as a positive Integer.
asUnsigned :: BV w -> Integer

-- | Unsigned interpretation of a bitvector as a Natural.
asNatural :: BV w -> Natural

-- | Convert a bitvector to a list of bits, in big endian order (higher
--   order bits in the bitvector are mapped to lower indices in the output
--   list).
--   
--   
--   >>> asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
--   [False,True,True,False,True]
--   
asBitsBE :: NatRepr w -> BV w -> [Bool]

-- | Convert a bitvector to a list of bits, in little endian order (lower
--   order bits in the bitvector are mapped to lower indices in the output
--   list).
--   
--   
--   >>> asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
--   [True,False,True,True,False]
--   
asBitsLE :: NatRepr w -> BV w -> [Bool]

-- | Convert a bitvector to a list of bytes, in big endian order (higher
--   order bytes in the bitvector are mapped to lower indices in the output
--   list). Return Nothing if the width is not a multiple of 8.
--   
--   
--   >>> asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
--   Just [170,187,204,221]
--   
asBytesBE :: NatRepr w -> BV w -> Maybe [Word8]

-- | Convert a bitvector to a list of bytes, in little endian order (lower
--   order bytes in the bitvector are mapped to lower indices in the output
--   list). Return Nothing if the width is not a multiple of 8.
--   
--   
--   >>> asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
--   Just [221,204,187,170]
--   
asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]

-- | asBytesBE, but for bytestrings.
asBytestringBE :: NatRepr w -> BV w -> Maybe ByteString

-- | asBytesLE, but for bytestrings.
asBytestringLE :: NatRepr w -> BV w -> Maybe ByteString

-- | Bitwise and.
and :: BV w -> BV w -> BV w

-- | Bitwise or.
or :: BV w -> BV w -> BV w

-- | Bitwise xor.
xor :: BV w -> BV w -> BV w

-- | Bitwise complement (flip every bit).
complement :: NatRepr w -> BV w -> BV w

-- | Left shift by positive Natural.
shl :: NatRepr w -> BV w -> Natural -> BV w

-- | Right logical shift by positive Natural.
lshr :: NatRepr w -> BV w -> Natural -> BV w

-- | Right arithmetic shift by positive Natural.
ashr :: 1 <= w => NatRepr w -> BV w -> Natural -> BV w

-- | Bitwise rotate left.
rotateL :: NatRepr w -> BV w -> Natural -> BV w

-- | Bitwise rotate right.
rotateR :: NatRepr w -> BV w -> Natural -> BV w

-- | The BV that has a particular bit set, and is 0 everywhere else.
bit :: (ix + 1) <= w => NatRepr w -> NatRepr ix -> BV w

-- | Like bit, but without the requirement that the index bit refers
--   to an actual bit in the output BV. If it is out of range, just
--   silently return the zero bitvector.
bit' :: NatRepr w -> Natural -> BV w

-- | setBit bv ix is the same as or bv (bit knownNat ix).
setBit :: (ix + 1) <= w => NatRepr ix -> BV w -> BV w

-- | Like setBit, but without the requirement that the index bit
--   refers to an actual bit in the input BV. If it is out of range,
--   just silently return the original input.
setBit' :: NatRepr w -> Natural -> BV w -> BV w

-- | clearBit w bv ix is the same as and bv (complement (bit w
--   ix)).
clearBit :: (ix + 1) <= w => NatRepr w -> NatRepr ix -> BV w -> BV w

-- | Like clearBit, but without the requirement that the index bit
--   refers to an actual bit in the input BV. If it is out of range,
--   just silently return the original input.
clearBit' :: NatRepr w -> Natural -> BV w -> BV w

-- | complementBit bv ix is the same as xor bv (bit knownNat
--   ix).
complementBit :: (ix + 1) <= w => NatRepr ix -> BV w -> BV w

-- | Like complementBit, but without the requirement that the index
--   bit refers to an actual bit in the input BV. If it is out of
--   range, just silently return the original input.
complementBit' :: NatRepr w -> Natural -> BV w -> BV w

-- | Test if a particular bit is set.
testBit :: (ix + 1) <= w => NatRepr ix -> BV w -> Bool

-- | Like testBit, but takes a Natural for the bit index. If
--   the index is out of bounds, return False.
testBit' :: Natural -> BV w -> Bool

-- | Get the number of 1 bits in a BV.
popCount :: BV w -> BV w

-- | Count trailing zeros in a BV.
ctz :: NatRepr w -> BV w -> BV w

-- | Count leading zeros in a BV.
clz :: NatRepr w -> BV w -> BV w

-- | Truncate a bitvector to a particular width given at runtime, while
--   keeping the type-level width constant.
truncBits :: Natural -> BV w -> BV w

-- | Bitvector add.
add :: NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector subtract.
sub :: NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector multiply.
mul :: NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector division (unsigned). Rounds to zero. Division by zero yields
--   a runtime error.
uquot :: BV w -> BV w -> BV w

-- | Bitvector division (signed). Rounds to zero. Division by zero yields a
--   runtime error.
squot :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector division (signed). Rounds to negative infinity. Division by
--   zero yields a runtime error.
sdiv :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector remainder after division (unsigned), when rounded to zero.
--   Division by zero yields a runtime error.
urem :: BV w -> BV w -> BV w

-- | Bitvector remainder after division (signed), when rounded to zero.
--   Division by zero yields a runtime error.
srem :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector remainder after division (signed), when rounded to negative
--   infinity. Division by zero yields a runtime error.
smod :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | uquot and urem returned as a pair.
uquotRem :: BV w -> BV w -> (BV w, BV w)

-- | squot and srem returned as a pair.
squotRem :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)

-- | sdiv and smod returned as a pair.
sdivMod :: 1 <= w => NatRepr w -> BV w -> BV w -> (BV w, BV w)

-- | Bitvector absolute value. Returns the 2's complement magnitude of the
--   bitvector.
abs :: 1 <= w => NatRepr w -> BV w -> BV w

-- | 2's complement bitvector negation.
negate :: NatRepr w -> BV w -> BV w

-- | Get the sign bit as a BV.
signBit :: 1 <= w => NatRepr w -> BV w -> BV w

-- | Return 1 if positive, -1 if negative, and 0 if 0.
signum :: 1 <= w => NatRepr w -> BV w -> BV w

-- | Signed less than.
slt :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool

-- | Signed less than or equal.
sle :: 1 <= w => NatRepr w -> BV w -> BV w -> Bool

-- | Unsigned less than.
ult :: BV w -> BV w -> Bool

-- | Unsigned less than or equal.
ule :: BV w -> BV w -> Bool

-- | Unsigned minimum of two bitvectors.
umin :: BV w -> BV w -> BV w

-- | Unsigned maximum of two bitvectors.
umax :: BV w -> BV w -> BV w

-- | Signed minimum of two bitvectors.
smin :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | Signed maximum of two bitvectors.
smax :: 1 <= w => NatRepr w -> BV w -> BV w -> BV w

-- | Concatenate two bitvectors. The first argument gets placed in the
--   higher order bits.
--   
--   
--   >>> concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
--   BV 6
--   
--   >>> :type it
--   it :: BV 5
--   
concat :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')

-- | Slice out a smaller bitvector from a larger one.
--   
--   
--   >>> select (knownNat @4) (knownNat @1) (mkBV (knownNat @12) 0b110010100110)
--   BV 3
--   
--   >>> :type it
--   it :: BV 4
--   
select :: (ix + w') <= w => NatRepr ix -> NatRepr w' -> BV w -> BV w'

-- | Like select, but takes a Natural as the index to start
--   selecting from. Neither the index nor the output width is checked to
--   ensure the resulting BV lies entirely within the bounds of the
--   original bitvector. Any bits "selected" from beyond the bounds of the
--   input bitvector will be 0.
--   
--   
--   >>> select' (knownNat @4) 9 (mkBV (knownNat @12) 0b110010100110)
--   BV 6
--   
--   >>> :type it
--   it :: BV 4
--   
select' :: Natural -> NatRepr w' -> BV w -> BV w'

-- | Zero-extend a bitvector to one of strictly greater width.
--   
--   
--   >>> zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
--   BV 13
--   
--   >>> :type it
--   it :: BV 8
--   
zext :: (w + 1) <= w' => NatRepr w' -> BV w -> BV w'

-- | Sign-extend a bitvector to one of strictly greater width.
sext :: (1 <= w, (w + 1) <= w') => NatRepr w -> NatRepr w' -> BV w -> BV w'

-- | Truncate a bitvector to one of strictly smaller width.
trunc :: (w' + 1) <= w => NatRepr w' -> BV w -> BV w'

-- | Like trunc, but allows the input width to be greater than or
--   equal to the output width, in which case it just performs a zero
--   extension.

-- | Deprecated: Use zresize instead
trunc' :: NatRepr w' -> BV w -> BV w'

-- | Resizes a bitvector. If w' > w, perform a zero extension.
zresize :: NatRepr w' -> BV w -> BV w'

-- | Resizes a bitvector. If w' > w, perform a signed
--   extension.
sresize :: 1 <= w => NatRepr w -> NatRepr w' -> BV w -> BV w'

-- | Wide multiply of two bitvectors.
mulWide :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')

-- | Unsigned successor. succUnsigned w (maxUnsigned w) returns
--   Nothing.
succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)

-- | Signed successor. succSigned w (maxSigned w) returns
--   Nothing.
succSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)

-- | Unsigned predecessor. predUnsigned w zero returns
--   Nothing.
predUnsigned :: NatRepr w -> BV w -> Maybe (BV w)

-- | Signed predecessor. predSigned w (minSigned w) returns
--   Nothing.
predSigned :: 1 <= w => NatRepr w -> BV w -> Maybe (BV w)

-- | List of all unsigned bitvectors from a lower to an upper bound,
--   inclusive.
enumFromToUnsigned :: BV w -> BV w -> [BV w]

-- | List of all signed bitvectors from a lower to an upper bound,
--   inclusive.
enumFromToSigned :: 1 <= w => NatRepr w -> BV w -> BV w -> [BV w]

-- | Generates a bitvector uniformly distributed over all possible values
--   for a given width. (See uniformM).
uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)

-- | Generates a bitvector uniformly distributed over the provided range
--   (interpreted as a range of unsigned bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   uniformRM).
uUniformRM :: StatefulGen g m => (BV w, BV w) -> g -> m (BV w)

-- | Generates a bitvector uniformly distributed over the provided range
--   (interpreted as a range of signed bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   uniformRM).
sUniformRM :: (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)

-- | Pretty print in hex
ppHex :: NatRepr w -> BV w -> String

-- | Pretty print in binary
ppBin :: NatRepr w -> BV w -> String

-- | Pretty print in octal
ppOct :: NatRepr w -> BV w -> String

-- | Pretty print in decimal
ppDec :: NatRepr w -> BV w -> String

-- | This module defines a wrapper around the BV type,
--   SignedBV, with instances not provided by BV.
module Data.BitVector.Sized.Signed

-- | Signed bit vector.
newtype SignedBV w
SignedBV :: BV w -> SignedBV w
[asBV] :: SignedBV w -> BV w

-- | Convenience wrapper for mkBV.
mkSignedBV :: NatRepr w -> Integer -> SignedBV w
instance Control.DeepSeq.NFData (Data.BitVector.Sized.Signed.SignedBV w)
instance Language.Haskell.TH.Syntax.Lift (Data.BitVector.Sized.Signed.SignedBV w)
instance GHC.Classes.Eq (Data.BitVector.Sized.Signed.SignedBV w)
instance GHC.Read.Read (Data.BitVector.Sized.Signed.SignedBV w)
instance GHC.Show.Show (Data.BitVector.Sized.Signed.SignedBV w)
instance GHC.Generics.Generic (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Classes.Ord (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Bits.Bits (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Bits.FiniteBits (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Num.Num (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Enum.Enum (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Ix.Ix (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => GHC.Enum.Bounded (Data.BitVector.Sized.Signed.SignedBV w)
instance GHC.TypeNats.KnownNat w => System.Random.Internal.Uniform (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => System.Random.Internal.UniformRange (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 Data.Type.Ord.<= w) => System.Random.Random (Data.BitVector.Sized.Signed.SignedBV w)
instance Data.Hashable.Class.Hashable (Data.BitVector.Sized.Signed.SignedBV w)

-- | This module defines a wrapper around the BV type,
--   UnsignedBV, with instances not provided by BV.
module Data.BitVector.Sized.Unsigned

-- | Signed bit vector.
newtype UnsignedBV w
UnsignedBV :: BV w -> UnsignedBV w
[asBV] :: UnsignedBV w -> BV w

-- | Convenience wrapper for mkBV.
mkUnsignedBV :: NatRepr w -> Integer -> UnsignedBV w
instance Control.DeepSeq.NFData (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance Language.Haskell.TH.Syntax.Lift (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.Classes.Ord (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.Classes.Eq (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.Read.Read (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.Show.Show (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.Generics.Generic (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Bits.Bits (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Bits.FiniteBits (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Num.Num (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Enum.Enum (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Ix.Ix (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => GHC.Enum.Bounded (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => System.Random.Internal.Uniform (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance System.Random.Internal.UniformRange (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => System.Random.Random (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance Data.Hashable.Class.Hashable (Data.BitVector.Sized.Unsigned.UnsignedBV w)
