-- 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.6

-- | 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 :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Natural -> Overflow (BV w)

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

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

-- | Bitvector multiply.
mulOf :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w -> Overflow (BV w)
instance GHC.Internal.Base.Applicative Data.BitVector.Sized.Overflow.Overflow
instance GHC.Classes.Eq a => GHC.Classes.Eq (Data.BitVector.Sized.Overflow.Overflow a)
instance GHC.Classes.Eq Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Classes.Eq Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Internal.Data.Foldable.Foldable Data.BitVector.Sized.Overflow.Overflow
instance GHC.Internal.Base.Functor Data.BitVector.Sized.Overflow.Overflow
instance GHC.Internal.Base.Monad Data.BitVector.Sized.Overflow.Overflow
instance GHC.Internal.Base.Monoid Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Internal.Base.Monoid Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Internal.Base.Semigroup Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Internal.Base.Semigroup Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Internal.Show.Show a => GHC.Internal.Show.Show (Data.BitVector.Sized.Overflow.Overflow a)
instance GHC.Internal.Show.Show Data.BitVector.Sized.Overflow.SignedOverflow
instance GHC.Internal.Show.Show Data.BitVector.Sized.Overflow.UnsignedOverflow
instance GHC.Internal.Data.Traversable.Traversable Data.BitVector.Sized.Overflow.Overflow

-- | 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)

-- | 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 :: forall (w :: Nat). NatRepr w -> Integer -> BV w

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

-- | Like mkBV, but returns Nothing if signed input integer
--   cannot be represented in w bits.
mkBVSigned :: forall (w :: Natural). 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 :: forall (w :: Nat). 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 :: forall (w :: Natural). 1 <= w => NatRepr w -> Integer -> BV w

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

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

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

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

-- | The zero bitvector of any width.
zero :: forall (w :: Nat). NatRepr w -> BV w

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

-- | The bitvector whose value is its own width, of any width.
width :: forall (w :: Nat). 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 :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> Integer

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

-- | Unsigned interpretation of a bitvector as a Natural.
asNatural :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]

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

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

-- | Bitwise and.
and :: forall (w :: Nat). BV w -> BV w -> BV w

-- | Bitwise or.
or :: forall (w :: Nat). BV w -> BV w -> BV w

-- | Bitwise xor.
xor :: forall (w :: Nat). BV w -> BV w -> BV w

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

-- | Left shift by positive Natural.
shl :: forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w

-- | Right logical shift by positive Natural.
lshr :: forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w

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

-- | Bitwise rotate left.
rotateL :: forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w

-- | Bitwise rotate right.
rotateR :: forall (w :: Nat). NatRepr w -> BV w -> Natural -> BV w

-- | The BV that has a particular bit set, and is 0 everywhere else.
bit :: forall (ix :: Natural) (w :: Natural). (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' :: forall (w :: Nat). NatRepr w -> Natural -> BV w

-- | setBit bv ix is the same as or bv (bit knownNat ix).
setBit :: forall (ix :: Natural) (w :: Natural). (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' :: forall (w :: Nat). NatRepr w -> Natural -> BV w -> BV w

-- | clearBit w bv ix is the same as and bv (complement (bit w
--   ix)).
clearBit :: forall (ix :: Natural) (w :: Natural). (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' :: forall (w :: Nat). NatRepr w -> Natural -> BV w -> BV w

-- | complementBit bv ix is the same as xor bv (bit knownNat
--   ix).
complementBit :: forall (ix :: Natural) (w :: Natural). (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' :: forall (w :: Nat). NatRepr w -> Natural -> BV w -> BV w

-- | Test if a particular bit is set.
testBit :: forall (ix :: Natural) (w :: Natural). (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' :: forall (w :: Nat). Natural -> BV w -> Bool

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

-- | Count trailing zeros in a BV.
ctz :: forall (w :: Nat). NatRepr w -> BV w -> BV w

-- | Count leading zeros in a BV.
clz :: forall (w :: Nat). NatRepr w -> BV w -> BV w

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

-- | Bitvector add.
add :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector subtract.
sub :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w

-- | Bitvector multiply.
mul :: forall (w :: Nat). NatRepr w -> BV w -> BV w -> BV w

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

-- | Bitvector division (signed). Rounds to zero. Division by zero yields a
--   runtime error.
squot :: forall (w :: Natural). 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 :: forall (w :: Natural). 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 :: forall (w :: Nat). BV w -> BV w -> BV w

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

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

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

-- | sdiv and smod returned as a pair.
sdivMod :: forall (w :: Natural). 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 :: forall (w :: Natural). 1 <= w => NatRepr w -> BV w -> BV w

-- | 2's complement bitvector negation.
negate :: forall (w :: Nat). NatRepr w -> BV w -> BV w

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

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

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

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

-- | Unsigned less than.
ult :: forall (w :: Nat). BV w -> BV w -> Bool

-- | Unsigned less than or equal.
ule :: forall (w :: Nat). BV w -> BV w -> Bool

-- | Unsigned minimum of two bitvectors.
umin :: forall (w :: Nat). BV w -> BV w -> BV w

-- | Unsigned maximum of two bitvectors.
umax :: forall (w :: Nat). BV w -> BV w -> BV w

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

-- | Signed maximum of two bitvectors.
smax :: forall (w :: Natural). 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 :: forall (w :: Nat) (w' :: Nat). 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 :: forall (ix :: Natural) (w' :: Natural) (w :: Natural). (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' :: forall (w' :: Nat) (w :: Nat). 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 :: forall (w :: Natural) (w' :: Natural). (w + 1) <= w' => NatRepr w' -> BV w -> BV w'

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

-- | Truncate a bitvector to one of strictly smaller width.
trunc :: forall (w' :: Natural) (w :: Natural). (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' :: forall (w' :: Nat) (w :: Nat). NatRepr w' -> BV w -> BV w'

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

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

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

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

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

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

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

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

-- | List of all signed bitvectors from a lower to an upper bound,
--   inclusive.
enumFromToSigned :: forall (w :: Natural). 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 :: forall g m (w :: Nat). 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 :: forall g m (w :: Nat). 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 :: forall g m (w :: Natural). (StatefulGen g m, 1 <= w) => NatRepr w -> (BV w, BV w) -> g -> m (BV w)

-- | Pretty print in hex
ppHex :: forall (w :: Nat). NatRepr w -> BV w -> String

-- | Pretty print in binary
ppBin :: forall (w :: Nat). NatRepr w -> BV w -> String

-- | Pretty print in octal
ppOct :: forall (w :: Nat). NatRepr w -> BV w -> String

-- | Pretty print in decimal
ppDec :: forall (w :: Nat). 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 :: Nat)
SignedBV :: BV w -> SignedBV (w :: Nat)
[asBV] :: SignedBV (w :: Nat) -> BV w

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

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