Copyright | (c) Galois Inc. 2018 |
---|---|
License | BSD-3 |
Maintainer | benselfridge@galois.com |
Stability | experimental |
Portability | portable |
Safe Haskell | None |
Language | Haskell2010 |
Synopsis
- data Chunk (w :: Nat) :: * where
- chunk :: KnownNat w => Int -> Chunk w
- data BitLayout (t :: Nat) (s :: Nat) :: *
- empty :: KnownNat t => BitLayout t 0
- singleChunk :: (KnownNat w, KnownNat w') => Int -> BitLayout w w'
- (<:) :: Chunk r -> BitLayout t s -> BitLayout t (r + s)
- inject :: BitLayout t s -> BitVector t -> BitVector s -> BitVector t
- extract :: BitLayout t s -> BitVector t -> BitVector s
- layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s)
- layoutsLens :: forall ws. List (BitLayout 32) ws -> Simple Lens (BitVector 32) (List BitVector ws)
- bitLayoutAssignmentList :: BitLayout t s -> [Int]
Chunk
data Chunk (w :: Nat) :: * where Source #
Chunk
type, parameterized by chunk width. The internal Int
is the
position of the least significant bit of the chunk, and the type-level nat w
is
the width of the chunk.
>>>
chunk 2 :: Chunk 5
Chunk 5 2
Intuitively, the above chunk index captures the notion of embedding a
BitVector
5
(bit vector of width 5) into a larger BitVector
at index 2,
preserving the order of the input bits. So an 5-bit input like 10011
would map
to some larger bit vector containing the input starting at position 2, like
000001001100
.
Instances
ShowF Chunk Source # | |
Show (Chunk w) Source # | |
Pretty (Chunk w) Source # | |
Defined in Data.BitVector.Sized.BitLayout pPrintPrec :: PrettyLevel -> Rational -> Chunk w -> Doc # pPrintList :: PrettyLevel -> [Chunk w] -> Doc # | |
Pretty (Some Chunk) Source # | |
Defined in Data.BitVector.Sized.BitLayout pPrintPrec :: PrettyLevel -> Rational -> Some Chunk -> Doc # pPrintList :: PrettyLevel -> [Some Chunk] -> Doc # |
chunk :: KnownNat w => Int -> Chunk w Source #
Construct a Chunk
in a context where the chunk width is known at compile time.
BitLayout
data BitLayout (t :: Nat) (s :: Nat) :: * Source #
BitLayout type, parameterized by target width and source width. t
is the
target width, s
is the source width. s
should always be less than or equal to
t
.
To construct a BitLayout
, use the empty
constructor and the <:
operator,
like so:
>>>
empty :: BitLayout 32 0
BitLayout 32 0 (fromList [])>>>
let layout = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)
>>>
layout
BitLayout 32 12 (fromList [Chunk 5 7,Chunk 7 25])>>>
:type it
it :: BitLayout 32 12
In the above example bitLayout
defines a chunk-by-chunk mapping from a bit
vector of width 12 to one of width 32. We imagine the input vector of width 12
listed like so:
0bAXXXXXBCXXXD |-----||---| 7 5
Here, bits A
, B
, C
, and D
are just labeled as such to illustrate their
place after the mapping. The BitLayout 32 12
defined above as the layout
variable would map that 12-bit vector to the following 32-bit vector:
(Bit 25) (Bit 5) | | | | v v 0bAXXXXXB0000000000000CXXXD0000000 |-----| |---| 7 5
To use a BitLayout
to achieve a bidirectional mapping like the one described
above, you can either use the Lens
interface or the functions inject
and
extract
, which give an explicit setter and getter, respectively.
Example use of inject
/extract
:
>>>
let bl = (chunk 25 :: Chunk 7) <: (chunk 7 :: Chunk 5) <: (empty :: BitLayout 32 0)
>>>
let sVec = bitVector 0b111111100001 :: BitVector 12
>>>
sVec
0xfe1>>>
inject bl (bitVector 0) (bitVector 0b111111100001)
0xfe000080>>>
extract bl $ inject bl (bitVector 0) (bitVector 0b111111100001)
0xfe1
Instances
Show (BitLayout t s) Source # | |
Pretty (BitLayout t s) Source # | |
Defined in Data.BitVector.Sized.BitLayout pPrintPrec :: PrettyLevel -> Rational -> BitLayout t s -> Doc # pPrint :: BitLayout t s -> Doc # pPrintList :: PrettyLevel -> [BitLayout t s] -> Doc # |
singleChunk :: (KnownNat w, KnownNat w') => Int -> BitLayout w w' Source #
Construct a BitLayout
with one chunk.
:: BitLayout t s | The layout |
-> BitVector t | The larger vector to inject into |
-> BitVector s | The smaller vector to be injected |
-> BitVector t |
Use a BitLayout
to inject a smaller vector into a larger one.
Use a BitLayout
to extract a smaller vector from a larger one.
Lenses
layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s) Source #
Lens for a BitLayout
.
layoutsLens :: forall ws. List (BitLayout 32) ws -> Simple Lens (BitVector 32) (List BitVector ws) Source #
Utilities
bitLayoutAssignmentList :: BitLayout t s -> [Int] Source #
From a BitLayout
, get a list representing the position of each bit from the
source to the target. The list
[3,4,5,10,11,12,13]
means that bit 0 of the source is placed in bit 3 of the target, bit 1 of the source is placed in bit 4 of the target, etc.