Data.BitVector.Sized.BitLayout

This module defines a BitLayout datatype which encodes a chunk-to-chunk mapping (no overlaps) from a smaller bit vector into a larger one. BitLayouts are especially useful for defining the encoding and decoding of opcodes/operands in an instruction.

Chunk

data Chunk (w :: Nat) :: * where

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.

Multiple Chunks comprise a BitLayout; see below.

Constructors

Chunk :: NatRepr w -> Int -> Chunk w

Instances

ShowF Nat Chunk

Methods

withShow :: p f -> q tp -> (Show (f tp) -> a) -> a

showF :: f tp -> String

showsF :: f tp -> String -> String

Show (Chunk w)

Methods

showsPrec :: Int -> Chunk w -> ShowS

show :: Chunk w -> String

showList :: [Chunk w] -> ShowS

Pretty (Chunk w)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Chunk w -> Doc

pPrint :: Chunk w -> Doc

pPrintList :: PrettyLevel -> [Chunk w] -> Doc

Pretty (Some Nat Chunk)

Methods

pPrintPrec :: PrettyLevel -> Rational -> Some Nat Chunk -> Doc

pPrint :: Some Nat Chunk -> Doc

pPrintList :: PrettyLevel -> [Some Nat Chunk] -> Doc

chunk :: KnownNat w => Int -> Chunk w

Construct a Chunk in a context where the chunk width is known at compile time.

BitLayout

data BitLayout (t :: Nat) (s :: Nat) :: *

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)

Methods

showsPrec :: Int -> BitLayout t s -> ShowS

show :: BitLayout t s -> String

showList :: [BitLayout t s] -> ShowS

Pretty (BitLayout t s)

Methods

pPrintPrec :: PrettyLevel -> Rational -> BitLayout t s -> Doc

pPrint :: BitLayout t s -> Doc

pPrintList :: PrettyLevel -> [BitLayout t s] -> Doc

empty :: KnownNat t => BitLayout t 0

Construct an empty BitLayout.

(<:) infixr 6

Arguments

:: Chunk r

chunk to add

-> BitLayout t s

layout we are adding the chunk to

-> BitLayout t (r + s)

Add a Chunk to a BitLayout. If the Chunk does not fit, either because the resulting BitLayout would be too long or because it would overlap with a Chunk that is already in the BitLayout, we throw an error.

inject

Arguments

:: 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.

extract

Arguments

:: BitLayout t s

The layout

-> BitVector t

The larger vector to extract from

-> BitVector s

Use a BitLayout to extract a smaller vector from a larger one.

Lens

layoutLens :: BitLayout t s -> Simple Lens (BitVector t) (BitVector s)

Lens for bit layout.