BitVector datatype, parameterized by width.

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>

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.

Infix bvConcat.

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.

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

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

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

Signed interpretation of a bit vector as an Integer.