bv-sized-0.4.0: a BitVector datatype that is parameterized by the vector width

Copyright(c) Benjamin Selfridge 2018
Galois Inc.
Safe HaskellNone




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.



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.

Multiple Chunks comprise a BitLayout; see below.


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


ShowF Nat Chunk Source # 


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

showF :: f tp -> String #

showsF :: f tp -> String -> String #

Show (Chunk w) Source # 


showsPrec :: Int -> Chunk w -> ShowS #

show :: Chunk w -> String #

showList :: [Chunk w] -> ShowS #

Pretty (Chunk w) Source # 
Pretty (Some Nat Chunk) Source # 

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

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


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:

     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
  |-----|             |---|
     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
>>> inject bl (bitVector 0) (bitVector 0b111111100001)
>>> extract bl $ inject bl (bitVector 0) (bitVector 0b111111100001)


empty :: KnownNat t => BitLayout t 0 Source #

Construct an empty BitLayout.

(<:) infixr 6 Source #


:: 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 Source #


:: 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 Source #


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


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

Lens for bit layout.