Copyright | (c) Benjamin Selfridge 2018 Galois Inc. |
---|---|
License | BSD3 |
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
- data BitVector (w :: Nat) :: * where
- bv :: 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
- bvRotate :: BitVector w -> Int -> BitVector w
- bvWidth :: BitVector w -> Int
- bvTestBit :: BitVector w -> Int -> Bool
- bvPopCount :: BitVector w -> Int
- bvAdd :: BitVector w -> BitVector w -> BitVector w
- bvMul :: BitVector w -> BitVector w -> BitVector w
- bvAbs :: BitVector w -> BitVector w
- bvNegate :: BitVector w -> BitVector w
- bvSignum :: BitVector w -> BitVector w
- 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'
- 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 # | |
Show (BitVector w) Source # | |
KnownNat w => Bits (BitVector w) Source # | |
KnownNat w => FiniteBits (BitVector w) Source # | |
bv :: KnownNat w => Integer -> BitVector w Source #
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.
bvComplement :: BitVector w -> BitVector w Source #
Bitwise complement (flip every bit).
Arithmetic operations (width-preserving)
Bitwise operations (variable width)
These are functions that involve bit vectors of different lengths.
bvConcat :: BitVector v -> BitVector w -> BitVector (v + w) Source #
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.
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 (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.
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.
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.