Safe Haskell | None |
---|---|

Language | Haskell2010 |

This module provides a convenient lens from a larger bitvector into a smaller one:

`>>>`

`v = bvView @4 @'[3, 0, 1]`

`v`

is the "view" into a `BV 4`

that you get by extracting the bits at
indices `3`

, `0`

, and `1`

(in order of most-significant to least-significant
bit). If

bv = 0bABCD

then the view `v`

defined above refers to the bits `0bADC`

, a bitvector of
width 3. We can see this by creating a concrete bitvector, and using the view
to get and set bits:

`>>>`

`bv = BV.mkBV (knownNat @4) 0b1100`

`>>>`

`printBV = putStrLn . BV.ppBin knownNat`

`>>>`

0b100:[3]`printBV $ bv ^. bvViewL v`

`>>>`

0b1110:[4]`printBV $ bv & bvViewL v .~ BV.mkBV knownNat 0b101`

This is very useful for defining sub-fields of an instruction word. Consider the encoding for the RISC-V instruction JAL:

[ imm[20] | imm[10:1] | imm[11] | imm[19:12] | rd[4:0] | opcode=1101111 ] 31 21 20 12 7 0

Notice how the 7-bit `opcode`

and 5-bit `rd`

are laid out consecutively in
the 32-bit instruction word, but the `imm`

field has its bits jumbled up
throughout the rest of the instruction. We can create a view of the three
fields like so:

`>>>`

`opcode = bvView @32 @(Slice 0 7)`

`>>>`

`rd = bvView :: BVView 32 (Slice 7 5)`

`>>>`

`imm = bvView :: BVView 32 ('[31] ++ Slice 12 8 ++ '[20] ++ Slice 21 10)`

The `Slice`

and `++`

operators are useful for shortening the above
definitions. Expanded out, the types of the above definitions are:

`>>>`

opcode :: BVView 32 '[6, 5, 4, 3, 2, 1, 0]`:t opcode`

`>>>`

rd :: BVView 32 '[11, 10, 9, 8, 7]`:t rd`

`>>>`

imm :: BVView 32 '[31, 19, 18, 17, 16, 15, 14, 13, 12, 20, 30, 29, 28, 27, 26, 25, 24, 23, 22, 21]`:t imm`

The type system prevents you from creating an invalid view (for instance, where a bit index is repeated or out of range):

`>>>`

<interactive>:37:5: error: • Invalid index list: '[5, 6, 5, 4, 3] (repeated index 5) • In the expression: bvView @32 @('[5] ++ Slice 3 4) In an equation for ‘v’: v = bvView @32 @('[5] ++ Slice 3 4)`v = bvView @32 @('[5] ++ Slice 3 4)`

`>>>`

<interactive>:1:5: error: • Invalid index 33 into BV 32 index must be strictly smaller than bitvector width • In the expression: bvView @32 @(Slice 30 4) In an equation for ‘v’: v = bvView @32 @(Slice 30 4) <interactive>:1:5: error: • Invalid index 32 into BV 32 index must be strictly smaller than bitvector width • In the expression: bvView @32 @(Slice 30 4) In an equation for ‘v’: v = bvView @32 @(Slice 30 4)`v = bvView @32 @(Slice 30 4)`

**WARNING**: Don't attempt to use this library unless all your type-level
indices are known at compile time. If you try abstracting over `BVView`

,
you're gonna have a bad time.

## Synopsis

- data BVIx w ix
- bvIx :: forall w ix. (KnownNat ix, ValidIx w ix) => BVIx w ix
- bvIxL :: KnownNat w => BVIx w ix -> Lens' (BV w) (BV 1)
- data BVView (w :: Nat) (ixs :: [Nat])
- bvView :: forall w ixs. (KnownRepr (BVView w) ixs, ValidView ixs) => BVView w ixs
- bvViewL :: forall w ixs. KnownNat w => BVView w ixs -> Lens' (BV w) (BV (Length ixs))
- data BVViews (w :: Nat) (ixss :: [[Nat]])
- bvViews :: forall w ixss. (KnownRepr (BVViews w) ixss, ValidViews ixss) => BVViews w ixss
- bvViewsL :: forall w ixss. KnownNat w => BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss))
- type family (as :: [k]) ++ (bs :: [k]) :: [k] where ...
- type family Slice (i :: Nat) (w :: Nat) :: [Nat] where ...
- type family Slice' (i :: Nat) (w :: Nat) :: [Nat] where ...
- type family Length (l :: [k]) :: Nat where ...
- type family Lengths (kss :: [[k]]) :: [Nat] where ...

# BVIx

Index of a single bit of a `BV`

.

#### Instances

TestEquality (BVIx w :: Nat -> Type) Source # | |

Defined in Data.BitVector.Sized.Lens | |

OrdF (BVIx w :: Nat -> Type) Source # | |

Defined in Data.BitVector.Sized.Lens compareF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> OrderingF x y # leqF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # ltF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # geqF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # gtF :: forall (x :: k) (y :: k). BVIx w x -> BVIx w y -> Bool # | |

ShowF (BVIx w :: Nat -> Type) Source # | |

(KnownNat ix, ValidIx w ix) => KnownRepr (BVIx w :: Nat -> Type) (ix :: Nat) Source # | |

Defined in Data.BitVector.Sized.Lens | |

Show (BVIx w ix) Source # | |

bvIx :: forall w ix. (KnownNat ix, ValidIx w ix) => BVIx w ix Source #

Construct a `BVIx`

when the index is known at compile time.

`>>>`

BVIx 7`bvIx @32 @7`

`>>>`

it :: BVIx 7`:type it`

# BVView

data BVView (w :: Nat) (ixs :: [Nat]) Source #

A list of `BVIx`

with no repeated elements. This essentially gives us a
reordering of some subset of the bits in a bitvector.

bvView :: forall w ixs. (KnownRepr (BVView w) ixs, ValidView ixs) => BVView w ixs Source #

Construct a `BVView`

when the width and indices are known at compile time.

`>>>`

BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil)`bvView @32 @(Slice 9 3)`

`>>>`

it :: BVView 32 '[11, 10, 9]`:type it`

`>>>`

<interactive>:19:1: error: • Invalid index list: '[5, 7, 5] (repeated index 5) • In the expression: bvView @32 @'[5, 7, 5] In an equation for ‘it’: it = bvView @32 @'[5, 7, 5]`bvView @32 @'[5, 7, 5]`

bvViewL :: forall w ixs. KnownNat w => BVView w ixs -> Lens' (BV w) (BV (Length ixs)) Source #

Get a lens from a `BVView`

.

# BVViews

data BVViews (w :: Nat) (ixss :: [[Nat]]) Source #

A list of `BVViews`

where each `BVView`

is disjoint from the others. This
is basically a decomposition of a bitvector into disjoint fields.

bvViews :: forall w ixss. (KnownRepr (BVViews w) ixss, ValidViews ixss) => BVViews w ixss Source #

Construct a `BVViews`

when the type is fully known at compile time.

`>>>`

BVViews (BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil) :< BVView (BVIx 14 :< BVIx 15 :< Nil) :< Nil)`bvViews @32 @'[Slice 9 3, Slice' 14 2]`

`>>>`

it :: BVViews 32 '[ '[11, 10, 9], '[14, 15]]`:type it`

`>>>`

<interactive>:3:1: error: • Invalid index lists '[ '[2, 1, 0], '[3, 2]] Lists '[2, 1, 0] and '[3, 2] are not disjoint (their intersection is '[2]) • In the expression: bvViews @32 @'[Slice 0 3, Slice 2 2] In an equation for ‘it’: it = bvViews @32 @'[Slice 0 3, Slice 2 2]`bvViews @32 @'[Slice 0 3, Slice 2 2]`

bvViewsL :: forall w ixss. KnownNat w => BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss)) Source #

Get a lens from a `BVViews`

.

# Type families on lists

Various type families that are useful for constructing types when using this library.

type family Slice (i :: Nat) (w :: Nat) :: [Nat] where ... Source #

A "slice" of a bitvector. The first argument is the index of the least significant bit of the slice, and the second argument is the width.

`>>>`

Slice 7 4 :: [Nat] = '[10, 9, 8, 7]`:kind! Slice 7 4`

`>>>`

`v = bvView @8 @(Slice 4 2)`

`>>>`

0b1011100:[8]`printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b01`

type family Slice' (i :: Nat) (w :: Nat) :: [Nat] where ... Source #

A "reversed slice" of a bitvector. The first argument is the index of the least significant bit of the slice, and the second argument is the width. The resulting slice reverses the order of the bits.

`>>>`

Slice' 7 4 :: [Nat] = '[7, 8, 9, 10]`:kind! Slice' 7 4`

`>>>`

`v = bvView @8 @(Slice' 4 2)`

`>>>`

0b1011100:[8]`printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b10`