Data.BitVector.Sized.Internal

This module defines a width-parameterized BitVector type and various associated operations that assume a 2's complement representation. This module exports more of the internals of the type as well as several functions that operate on explicit NatReprs instead of requiring a KnownNat constraint.

BitVector type

data BitVector (w :: Nat) :: * where

BitVector datatype, parameterized by width.

Constructors

BV :: NatRepr w -> Integer -> BitVector w

Instances

TestEquality Nat BitVector

Methods

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

EqF Nat BitVector

Methods

eqF :: f a -> f a -> Bool

ShowF Nat BitVector

Methods

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

showF :: f tp -> String

showsF :: f tp -> String -> String

KnownNat w => Bounded (BitVector w)

Methods

minBound :: BitVector w

maxBound :: BitVector w

KnownNat w => Enum (BitVector w)

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)

Methods

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

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

KnownNat w => Num (BitVector w)

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

Show (BitVector w)

Methods

showsPrec :: Int -> BitVector w -> ShowS

show :: BitVector w -> String

showList :: [BitVector w] -> ShowS

KnownNat w => Bits (BitVector w)

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)

Methods

finiteBitSize :: BitVector w -> Int

countLeadingZeros :: BitVector w -> Int

countTrailingZeros :: BitVector w -> Int

bv :: KnownNat w => Integer -> BitVector w

Construct a bit vector in a context where the width is inferrable from the type context. The Integer 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.

>>> bv 0xA :: BitVector 4
0xa<4>
>>> bv 0xA :: BitVector 3
0x2<3>
>>> bv (-1) :: BitVector 8
0xff<8>
>>> bv (-1) :: BitVector 32
0xffffffff<32>

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.

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.

Arithmetic operations (width-preserving)

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

Bitwise add.

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

Bitwise multiply.

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.

Bitwise operations (variable width)

These are functions that involve bit vectors of different lengths.

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

Concatenate two bit vectors.

>>> (bv 0xAA :: BitVector 8) `bvConcat` (bv 0xBCDEF0 :: BitVector 24)
0xaabcdef0<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.

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 (bv 0xAABCDEF0 :: BitVector 32) :: BitVector 8
0xcd<8>

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.

bvExtractWithRepr :: 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.

bvZextWithRepr :: 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.

bvSextWithRepr :: 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.