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

-- | 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 :: forall (w :: Nat). 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 :: forall (w :: Nat). 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 :: forall (w :: Natural). 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 :: forall (w :: Nat). 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 :: 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 <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 :: 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).
--   
--   <pre>
--   &gt;&gt;&gt; asBitsBE (knownNat @5) (mkBV knownNat 0b1101)
--   [False,True,True,False,True]
--   </pre>
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).
--   
--   <pre>
--   &gt;&gt;&gt; asBitsLE (knownNat @5) (mkBV knownNat 0b1101)
--   [True,False,True,True,False]
--   </pre>
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 <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 :: 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 <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 :: forall (w :: Nat). NatRepr w -> BV w -> Maybe [Word8]

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

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

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

-- | Right arithmetic shift by positive <a>Natural</a>.
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 <a>BV</a> 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 <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' :: forall (w :: Nat). NatRepr w -> Natural -> BV w

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

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

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

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

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

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

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

-- | <a>sdiv</a> and <a>smod</a> 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 <a>BV</a>.
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.
--   
--   <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 :: 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.
--   
--   <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 :: forall (ix :: Natural) (w' :: Natural) (w :: Natural). (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' :: forall (w' :: Nat) (w :: Nat). 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 :: 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 <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' :: forall (w' :: Nat) (w :: Nat). NatRepr w' -> BV w -> BV w'

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

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

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

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

-- | Signed predecessor. <tt>predSigned w (minSigned w)</tt> returns
--   <a>Nothing</a>.
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 <a>uniformM</a>).
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 <i>unsigned</i> bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   <a>uniformRM</a>).
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 <i>signed</i> bitvectors), which is
--   interpreted as inclusive in the lower and upper bound. (See
--   <a>uniformRM</a>).
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 <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 :: Nat)
SignedBV :: BV w -> SignedBV (w :: Nat)
[asBV] :: SignedBV (w :: Nat) -> BV w

-- | Convenience wrapper for <a>mkBV</a>.
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 <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 :: Nat)
UnsignedBV :: BV w -> UnsignedBV (w :: Nat)
[asBV] :: UnsignedBV (w :: Nat) -> BV w

-- | Convenience wrapper for <a>mkBV</a>.
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)
