Copyright | (c) Benjamin Selfridge 2018 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
This module defines a width-parameterized BitVector
type and various associated
operations that assume a 2's complement representation.
- data BitVector (w :: Nat) :: * where
- bitVector :: KnownNat w => Integer -> BitVector w
- bvAnd :: BitVector w -> BitVector w -> BitVector w
- bvOr :: BitVector w -> BitVector w -> BitVector w
- bvXor :: BitVector w -> BitVector w -> BitVector w
- bvComplement :: BitVector w -> BitVector w
- bvShift :: BitVector w -> Int -> BitVector w
- bvShiftL :: BitVector w -> Int -> BitVector w
- bvShiftRA :: BitVector w -> Int -> BitVector w
- bvShiftRL :: BitVector w -> Int -> BitVector w
- bvRotate :: BitVector w -> Int -> BitVector w
- bvWidth :: BitVector w -> Int
- bvTestBit :: BitVector w -> Int -> Bool
- bvPopCount :: BitVector w -> Int
- bvTruncBits :: BitVector w -> Int -> BitVector w
- bvAdd :: BitVector w -> BitVector w -> BitVector w
- bvMul :: BitVector w -> BitVector w -> BitVector w
- bvDivU :: BitVector w -> BitVector w -> BitVector w
- bvDivS :: BitVector w -> BitVector w -> BitVector w
- bvAbs :: BitVector w -> BitVector w
- bvNegate :: BitVector w -> BitVector w
- bvSignum :: BitVector w -> BitVector w
- bvLTS :: BitVector w -> BitVector w -> Bool
- bvLTU :: BitVector w -> BitVector w -> Bool
- bvConcat :: BitVector v -> BitVector w -> BitVector (v + w)
- (<:>) :: BitVector v -> BitVector w -> BitVector (v + w)
- bvExtract :: forall w w'. KnownNat w' => Int -> BitVector w -> BitVector w'
- bvExtractWithRepr :: NatRepr w' -> Int -> BitVector w -> BitVector w'
- bvZext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- bvZextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- bvSext :: forall w w'. KnownNat w' => BitVector w -> BitVector w'
- bvSextWithRepr :: NatRepr w' -> BitVector w -> BitVector w'
- bvMulFU :: BitVector w -> BitVector w' -> BitVector (w + w')
- bvMulFS :: BitVector w -> BitVector w' -> BitVector (w + w')
- bvMulFSU :: BitVector w -> BitVector w' -> BitVector (w + w')
- bvIntegerU :: BitVector w -> Integer
- bvIntegerS :: BitVector w -> Integer
BitVector type
data BitVector (w :: Nat) :: * where Source #
BitVector datatype, parameterized by width.
TestEquality Nat BitVector Source # | |
EqF Nat BitVector Source # | |
ShowF Nat BitVector Source # | |
KnownNat w => Bounded (BitVector w) Source # | |
KnownNat w => Enum (BitVector w) Source # | |
Eq (BitVector w) Source # | |
KnownNat w => Num (BitVector w) Source # | |
Ord (BitVector w) Source # | |
KnownNat w => Read (BitVector w) Source # | |
Show (BitVector w) Source # | |
KnownNat w => Arbitrary (BitVector w) Source # | |
KnownNat w => Bits (BitVector w) Source # | |
KnownNat w => FiniteBits (BitVector w) Source # | |
Pretty (BitVector w) Source # | |
KnownNat w => Random (BitVector w) Source # | |
bitVector :: KnownNat w => Integer -> BitVector w Source #
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>>>
:type it
it :: BitVector 4
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.
bvComplement :: BitVector w -> BitVector w Source #
Bitwise complement (flip every bit).
bvTruncBits :: BitVector w -> Int -> BitVector w Source #
Truncate a bit vector to a particular width given at runtime, while keeping the type-level width constant.
Arithmetic operations (width-preserving)
Variable-width operations
These are functions that involve bit vectors of different lengths.
bvConcat :: BitVector v -> BitVector w -> BitVector (v + w) Source #
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.
bvExtract :: forall w w'. KnownNat w' => Int -> BitVector w -> BitVector w' Source #
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.
bvZext :: forall w w'. KnownNat w' => BitVector w -> BitVector w' Source #
Zero-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.
bvSext :: forall w w'. KnownNat w' => BitVector w -> BitVector w' Source #
Sign-extend a vector to one of greater length. If given an input of greater length than the output type, this performs a truncation.
bvMulFU :: BitVector w -> BitVector w' -> BitVector (w + w') Source #
Fully multiply two bit vectors as unsigned integers, returning a bit vector whose length is equal to the sum of the inputs.
bvMulFS :: BitVector w -> BitVector w' -> BitVector (w + w') Source #
Fully multiply two bit vectors as signed integers, returning a bit vector whose length is equal to the sum of the inputs.
bvMulFSU :: BitVector w -> BitVector w' -> BitVector (w + w') Source #
Fully multiply two bit vectors, treating the first as a signed integer and the second as an unsigned integer, returning a bit vector whose length is equal to the sum of the inputs.
Conversions to Integer
bvIntegerU :: BitVector w -> Integer Source #
Unsigned interpretation of a bit vector as a (positive) Integer.
bvIntegerS :: BitVector w -> Integer Source #
Signed interpretation of a bit vector as an Integer.