BitVector datatype, parameterized by width.

Construct a bit vector with a particular width, 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.

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

The zero bitvector with width 0.

Bitwise and.

Bitwise or.

Bitwise xor.

Bitwise complement (flip every bit).

Bitwise shift. Uses an arithmetic right shift.

Left shift.

Right arithmetic shift.

Right logical shift.

Bitwise rotate.

Get the width of a BitVector.

Test if a particular bit is set.

Get the number of 1 bits in a BitVector.

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

Bitwise add.

Bitwise multiply.

Bitwise division (unsigned). Rounds to zero.

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

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

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

Bitwise absolute value.

Bitwise negation.

Get the sign bit as a BitVector.

Signed less than.

Unsigned less than.

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.

Infix bvConcat.

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 with an explicit NatRepr.

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.

Unconstrained variant of bvExtract with an explicit NatRepr argument.

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

Unconstrained variant of bvZext with an explicit NatRepr argument.

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

Unconstrained variant of bvSext with an explicit NatRepr argument.

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

Signed interpretation of a bit vector as an Integer.

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.