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


-- | 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 <a>True</a> if a computation caused unsigned overflow.
ofUnsigned :: Overflow a -> Bool

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

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

-- | Left shift by positive <a>Natural</a>.
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 <a>BV</a> type and various
--   associated operations. A <tt><a>BV</a> w</tt> is a newtype around an
--   <a>Integer</a>, so operations that require the width take an explicit
--   <tt><a>NatRepr</a> w</tt> argument. We explicitly do not allow widths
--   that cannot be represented as an <a>Int</a>, as we appeal to the
--   underlying <a>Num</a> and <a>Bits</a> instances on <a>Integer</a> for
--   the implementation of many of the same operations (which, in turn,
--   require those widths to be <a>Int</a>s).
--   
--   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 <a>SignedBV</a> or
--   <a>UnsignedBV</a>.
--   
--   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 <a>Integer</a> representation from a <a>BV</a>. We
--   guarantee that <tt>(\(BV.BV x) -&gt; x) == BV.asUnsigned</tt>.
pattern BV :: Integer -> BV w

-- | A runtime presentation of a type-level <a>Nat</a>.
--   
--   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 <a>NatRepr</a> argument. The input
--   <a>Integer</a>, 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
--   <a>Int</a>.
--   
--   <pre>
--   &gt;&gt;&gt; mkBV (knownNat @4) 10
--   BV 10
--   
--   &gt;&gt;&gt; mkBV (knownNat @2) 10
--   BV 2
--   
--   &gt;&gt;&gt; mkBV (knownNat @4) (-2)
--   BV 14
--   </pre>
mkBV :: NatRepr w -> Integer -> BV w

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

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

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

-- | <tt>signedClamp w i</tt> rounds <tt>i</tt> to the nearest value
--   between <tt>-2^(w-1)</tt> and <tt>2^(w-1) - 1</tt> (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 <a>BV</a> from a <a>Bool</a>.
bool :: Bool -> BV 1

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

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

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

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

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

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

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

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

-- | Construct a <a>BV</a> 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 <a>BV</a> along with its
--   width.
--   
--   <pre>
--   &gt;&gt;&gt; case bitsBE [True, False] of p -&gt; (fstPair p, sndPair p)
--   (2,BV 2)
--   </pre>
bitsBE :: [Bool] -> Pair NatRepr BV

-- | Construct a <a>BV</a> 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 <a>BV</a> along
--   with its width.
--   
--   <pre>
--   &gt;&gt;&gt; case bitsLE [True, False] of p -&gt; (fstPair p, sndPair p)
--   (2,BV 1)
--   </pre>
bitsLE :: [Bool] -> Pair NatRepr BV

-- | Construct a <a>BV</a> 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).
--   
--   <pre>
--   &gt;&gt;&gt; case bytesBE [0, 1, 1] of p -&gt; (fstPair p, sndPair p)
--   (24,BV 257)
--   </pre>
bytesBE :: [Word8] -> Pair NatRepr BV

-- | Construct a <a>BV</a> 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).
--   
--   <pre>
--   &gt;&gt;&gt; case bytesLE [0, 1, 1] of p -&gt; (fstPair p, sndPair p)
--   (24,BV 65792)
--   </pre>
bytesLE :: [Word8] -> Pair NatRepr BV

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

-- | Construct a <a>BV</a> from a little-endian bytestring.
--   
--   <pre>
--   &gt;&gt;&gt; case bytestringLE (BS.pack [0, 1, 1]) of p -&gt; (fstPair p, sndPair p)
--   (24,BV 65792)
--   </pre>
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).
--   
--   <pre>
--   &gt;&gt;&gt; asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
--   [False,True,True,False,True]
--   </pre>
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).
--   
--   <pre>
--   &gt;&gt;&gt; asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
--   [True,False,True,True,False]
--   </pre>
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 <a>Nothing</a> if the width is not a multiple of 8.
--   
--   <pre>
--   &gt;&gt;&gt; asBytesBE (knownNat @32) (mkBV knownNat 0xaabbccdd)
--   Just [170,187,204,221]
--   </pre>
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 <a>Nothing</a> if the width is not a multiple of 8.
--   
--   <pre>
--   &gt;&gt;&gt; asBytesLE (knownNat @32) (mkBV knownNat 0xaabbccdd)
--   Just [221,204,187,170]
--   </pre>
asBytesLE :: NatRepr w -> BV w -> Maybe [Word8]

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

-- | <a>asBytesLE</a>, 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 <a>Natural</a>.
shl :: NatRepr w -> BV w -> Natural -> BV w

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

-- | Right arithmetic shift by positive <a>Natural</a>.
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 <a>BV</a> that has a particular bit set, and is 0 everywhere else.
bit :: (ix + 1) <= w => NatRepr w -> NatRepr ix -> BV w

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

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

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

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

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

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

-- | Like <a>complementBit</a>, but without the requirement that the index
--   bit refers to an actual bit in the input <a>BV</a>. 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 <a>testBit</a>, but takes a <a>Natural</a> for the bit index. If
--   the index is out of bounds, return <a>False</a>.
testBit' :: Natural -> BV w -> Bool

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

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

-- | Count leading zeros in a <a>BV</a>.
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

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

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

-- | <a>sdiv</a> and <a>smod</a> 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 <a>BV</a>.
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.
--   
--   <pre>
--   &gt;&gt;&gt; concat knownNat (mkBV (knownNat @3) 0b001) (mkBV (knownNat @2) 0b10)
--   BV 6
--   
--   &gt;&gt;&gt; :type it
--   it :: BV 5
--   </pre>
concat :: NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')

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

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

-- | Zero-extend a bitvector to one of strictly greater width.
--   
--   <pre>
--   &gt;&gt;&gt; zext (knownNat @8) (mkBV (knownNat @4) 0b1101)
--   BV 13
--   
--   &gt;&gt;&gt; :type it
--   it :: BV 8
--   </pre>
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 <a>trunc</a>, but allows the input width to be greater than or
--   equal to the output width, in which case it just performs a zero
--   extension.

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

-- | Resizes a bitvector. If <tt>w' &gt; w</tt>, perform a zero extension.
zresize :: NatRepr w' -> BV w -> BV w'

-- | Resizes a bitvector. If <tt>w' &gt; w</tt>, 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. <tt>succUnsigned w (maxUnsigned w)</tt> returns
--   <a>Nothing</a>.
succUnsigned :: NatRepr w -> BV w -> Maybe (BV w)

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

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

-- | Signed predecessor. <tt>predSigned w (minSigned w)</tt> returns
--   <a>Nothing</a>.
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 <a>uniformM</a>).
uniformM :: StatefulGen g m => NatRepr w -> g -> m (BV w)

-- | Generates a bitvector uniformly distributed over the provided range
--   (interpreted as a range of <i>unsigned</i> bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   <a>uniformRM</a>).
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 <i>signed</i> bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   <a>uniformRM</a>).
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 <a>BV</a> type,
--   <a>SignedBV</a>, with instances not provided by <a>BV</a>.
module Data.BitVector.Sized.Signed

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

-- | Convenience wrapper for <a>mkBV</a>.
mkSignedBV :: NatRepr w -> Integer -> 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 GHC.TypeNats.<= w) => GHC.Classes.Ord (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => Data.Bits.Bits (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => Data.Bits.FiniteBits (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => GHC.Num.Num (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => GHC.Enum.Enum (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => GHC.Ix.Ix (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= 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 GHC.TypeNats.<= w) => System.Random.Internal.UniformRange (Data.BitVector.Sized.Signed.SignedBV w)
instance (GHC.TypeNats.KnownNat w, 1 GHC.TypeNats.<= w) => System.Random.Random (Data.BitVector.Sized.Signed.SignedBV w)


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

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

-- | Convenience wrapper for <a>mkBV</a>.
mkUnsignedBV :: NatRepr w -> Integer -> 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 => Data.Bits.Bits (Data.BitVector.Sized.Unsigned.UnsignedBV w)
instance GHC.TypeNats.KnownNat w => Data.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)
