Data.BitVector.Sized

This module defines a width-parameterized BitVector type and various associated operations that assume a 2's complement representation.

BitVector type

data BitVector (w :: Nat) :: *

BitVector datatype, parameterized by width.

Instances

TestEquality BitVector

Defined in Data.BitVector.Sized.Internal

Methods

testEquality :: BitVector a -> BitVector b -> Maybe (a :~: b)

EqF BitVector

Defined in Data.BitVector.Sized.Internal

Methods

eqF :: BitVector a -> BitVector a -> Bool

OrdF BitVector

Defined in Data.BitVector.Sized.Internal

Methods

compareF :: BitVector x -> BitVector y -> OrderingF x y

leqF :: BitVector x -> BitVector y -> Bool

ltF :: BitVector x -> BitVector y -> Bool

geqF :: BitVector x -> BitVector y -> Bool

gtF :: BitVector x -> BitVector y -> Bool

ShowF BitVector

Defined in Data.BitVector.Sized.Internal

Methods

withShow :: p BitVector -> q tp -> (Show (BitVector tp) -> a) -> a

showF :: BitVector tp -> String

showsPrecF :: Int -> BitVector tp -> String -> String

KnownNat w => Bounded (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

minBound :: BitVector w

maxBound :: BitVector w

KnownNat w => Enum (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

succ :: BitVector w -> BitVector w

pred :: BitVector w -> BitVector w

toEnum :: Int -> BitVector w

fromEnum :: BitVector w -> Int

enumFrom :: BitVector w -> [BitVector w]

enumFromThen :: BitVector w -> BitVector w -> [BitVector w]

enumFromTo :: BitVector w -> BitVector w -> [BitVector w]

enumFromThenTo :: BitVector w -> BitVector w -> BitVector w -> [BitVector w]

Eq (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

(==) :: BitVector w -> BitVector w -> Bool

(/=) :: BitVector w -> BitVector w -> Bool

KnownNat w => Num (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

(+) :: BitVector w -> BitVector w -> BitVector w

(-) :: BitVector w -> BitVector w -> BitVector w

(*) :: BitVector w -> BitVector w -> BitVector w

negate :: BitVector w -> BitVector w

abs :: BitVector w -> BitVector w

signum :: BitVector w -> BitVector w

fromInteger :: Integer -> BitVector w

Ord (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

compare :: BitVector w -> BitVector w -> Ordering

(<) :: BitVector w -> BitVector w -> Bool

(<=) :: BitVector w -> BitVector w -> Bool

(>) :: BitVector w -> BitVector w -> Bool

(>=) :: BitVector w -> BitVector w -> Bool

max :: BitVector w -> BitVector w -> BitVector w

min :: BitVector w -> BitVector w -> BitVector w

KnownNat w => Read (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

readsPrec :: Int -> ReadS (BitVector w)

readList :: ReadS [BitVector w]

readPrec :: ReadPrec (BitVector w)

readListPrec :: ReadPrec [BitVector w]

Show (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

showsPrec :: Int -> BitVector w -> ShowS

show :: BitVector w -> String

showList :: [BitVector w] -> ShowS

KnownNat w => Ix (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

range :: (BitVector w, BitVector w) -> [BitVector w]

index :: (BitVector w, BitVector w) -> BitVector w -> Int

unsafeIndex :: (BitVector w, BitVector w) -> BitVector w -> Int

inRange :: (BitVector w, BitVector w) -> BitVector w -> Bool

rangeSize :: (BitVector w, BitVector w) -> Int

unsafeRangeSize :: (BitVector w, BitVector w) -> Int

KnownNat w => Arbitrary (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

arbitrary :: Gen (BitVector w)

shrink :: BitVector w -> [BitVector w]

KnownNat w => Bits (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

(.&.) :: BitVector w -> BitVector w -> BitVector w

(.|.) :: BitVector w -> BitVector w -> BitVector w

xor :: BitVector w -> BitVector w -> BitVector w

complement :: BitVector w -> BitVector w

shift :: BitVector w -> Int -> BitVector w

rotate :: BitVector w -> Int -> BitVector w

zeroBits :: BitVector w

bit :: Int -> BitVector w

setBit :: BitVector w -> Int -> BitVector w

clearBit :: BitVector w -> Int -> BitVector w

complementBit :: BitVector w -> Int -> BitVector w

testBit :: BitVector w -> Int -> Bool

bitSizeMaybe :: BitVector w -> Maybe Int

bitSize :: BitVector w -> Int

isSigned :: BitVector w -> Bool

shiftL :: BitVector w -> Int -> BitVector w

unsafeShiftL :: BitVector w -> Int -> BitVector w

shiftR :: BitVector w -> Int -> BitVector w

unsafeShiftR :: BitVector w -> Int -> BitVector w

rotateL :: BitVector w -> Int -> BitVector w

rotateR :: BitVector w -> Int -> BitVector w

popCount :: BitVector w -> Int

KnownNat w => FiniteBits (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

finiteBitSize :: BitVector w -> Int

countLeadingZeros :: BitVector w -> Int

countTrailingZeros :: BitVector w -> Int

Pretty (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

pPrintPrec :: PrettyLevel -> Rational -> BitVector w -> Doc

pPrint :: BitVector w -> Doc

pPrintList :: PrettyLevel -> [BitVector w] -> Doc

KnownNat w => Random (BitVector w)

Defined in Data.BitVector.Sized.Internal

Methods

randomR :: RandomGen g => (BitVector w, BitVector w) -> g -> (BitVector w, g)

random :: RandomGen g => g -> (BitVector w, g)

randomRs :: RandomGen g => (BitVector w, BitVector w) -> g -> [BitVector w]

randoms :: RandomGen g => g -> [BitVector w]

randomRIO :: (BitVector w, BitVector w) -> IO (BitVector w)

randomIO :: IO (BitVector w)

pattern BitVector :: NatRepr w -> Integer -> BitVector w

BitVector can be treated as a constructor for pattern matching, but to build one you must use the smart constructor bitVector.

bitVector :: (Integral a, KnownNat w) => a -> BitVector w

Construct a bit vector with a particular width, where the width is inferrable from the type context. The input (an unbounded data type, hence with an infinite-width bit representation), whether positive or negative, is silently truncated to fit into the number of bits demanded by the return type.

>>> bitVector 0xA :: BitVector 4
0xa
>>> bitVector 0xA :: BitVector 2
0x2

bitVector' :: Integral a => NatRepr w -> a -> BitVector w

Like bitVector, but with an explict NatRepr.

bv0 :: BitVector 0

The zero bitvector with width 0.

Bitwise operations (width-preserving)

These are alternative versions of some of the Bits functions where we do not need to know the width at compile time. They are all width-preserving.

bvAnd :: BitVector w -> BitVector w -> BitVector w

Bitwise and.

bvOr :: BitVector w -> BitVector w -> BitVector w

Bitwise or.

bvXor :: BitVector w -> BitVector w -> BitVector w

Bitwise xor.

bvComplement :: BitVector w -> BitVector w

Bitwise complement (flip every bit).

bvShift :: BitVector w -> Int -> BitVector w

Bitwise shift. Uses an arithmetic right shift.

bvShiftL :: BitVector w -> Int -> BitVector w

Left shift.

bvShiftRA :: BitVector w -> Int -> BitVector w

Right arithmetic shift.

bvShiftRL :: BitVector w -> Int -> BitVector w

Right logical shift.

bvRotate :: BitVector w -> Int -> BitVector w

Bitwise rotate.

bvWidth :: BitVector w -> Int

Get the width of a BitVector.

bvTestBit :: BitVector w -> Int -> Bool

Test if a particular bit is set.

bvPopCount :: BitVector w -> Int

Get the number of 1 bits in a BitVector.

bvTruncBits :: BitVector w -> Int -> BitVector w

Truncate a bit vector to a particular width given at runtime, while keeping the type-level width constant.

Arithmetic operations (width-preserving)

bvAdd :: BitVector w -> BitVector w -> BitVector w

Bitwise add.

bvMul :: BitVector w -> BitVector w -> BitVector w

Bitwise multiply.

bvQuotU :: BitVector w -> BitVector w -> BitVector w

Bitwise division (unsigned). Rounds to zero.

bvQuotS :: BitVector w -> BitVector w -> BitVector w

Bitwise division (signed). Rounds to zero (not negative infinity).

bvRemU :: BitVector w -> BitVector w -> BitVector w

Bitwise remainder after division (unsigned), when rounded to zero.

bvRemS :: BitVector w -> BitVector w -> BitVector w

Bitwise remainder after division (signed), when rounded to zero (not negative infinity).

bvAbs :: BitVector w -> BitVector w

Bitwise absolute value.

bvNegate :: BitVector w -> BitVector w

Bitwise negation.

bvSignum :: BitVector w -> BitVector w

Get the sign bit as a BitVector.

bvLTS :: BitVector w -> BitVector w -> Bool

Signed less than.

bvLTU :: BitVector w -> BitVector w -> Bool

Unsigned less than.

Variable-width operations

These are functions that involve bit vectors of different lengths.

bvConcat :: BitVector v -> BitVector w -> BitVector (v + w)

Concatenate two bit vectors.

>>> (0xAA :: BitVector 8) `bvConcat` (0xBCDEF0 :: BitVector 24)
0xaabcdef0
>>> :type it
it :: BitVector 32

Note that the first argument gets placed in the higher-order bits. The above example should be illustrative enough.

(<:>) :: BitVector v -> BitVector w -> BitVector (v + w) infixl 6

Infix bvConcat.

bvConcatMany :: KnownNat w' => [BitVector w] -> BitVector w'

Concatenate a list of BitVectors into a BitVector of arbitrary width. The ordering is little endian:

>>> bvConcatMany [0xAA :: BitVector 8, 0xBB] :: BitVector 16
0xbbaa
>>> bvConcatMany [0xAA :: BitVector 8, 0xBB, 0xCC] :: BitVector 16
0xbbaa

If the sum of the widths of the input BitVectors exceeds the output width, we ignore the tail end of the list.

bvConcatMany' :: NatRepr w' -> [BitVector w] -> BitVector w'

bvConcatMany with an explicit NatRepr.

bvExtract :: forall w w'. KnownNat w' => Int -> BitVector w -> BitVector w'

Slice out a smaller bit vector from a larger one. The lowest significant bit is given explicitly as an argument of type Int, and the length of the slice is inferred from a type-level context.

>>> bvExtract 12 (0xAABCDEF0 :: BitVector 32) :: BitVector 8
0xcd

Note that bvExtract does not do any bounds checking whatsoever; if you try and extract bits that aren't present in the input, you will get 0's.

bvExtract' :: NatRepr w' -> Int -> BitVector w -> BitVector w'

Unconstrained variant of bvExtract with an explicit NatRepr argument.

bvZext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'

Zero-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.

bvZext' :: NatRepr w' -> BitVector w -> BitVector w'

Unconstrained variant of bvZext with an explicit NatRepr argument.

bvSext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'

Sign-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.

bvSext' :: NatRepr w' -> BitVector w -> BitVector w'

Unconstrained variant of bvSext with an explicit NatRepr argument.

Conversions to Integer

bvIntegerU :: BitVector w -> Integer

Unsigned interpretation of a bit vector as a (positive) Integer.

bvIntegerS :: BitVector w -> Integer

Signed interpretation of a bit vector as an Integer.

Byte decomposition

bvGetBytesU :: Int -> BitVector w -> [BitVector 8]

Given a BitVector of arbitrary length, decompose it into a list of bytes. Uses an unsigned interpretation of the input vector, so if you ask for more bytes that the BitVector contains, you get zeros. The result is little-endian, so the first element of the list will be the least significant byte of the input vector.