Data.BitVector.Sized.Lens

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
>>> printBV $ bv ^. bvViewL v
0b100:[3]
>>> printBV $ bv & bvViewL v .~ BV.mkBV knownNat 0b101
0b1110:[4]

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:

>>> :t opcode
opcode :: BVView 32 '[6, 5, 4, 3, 2, 1, 0]
>>> :t rd
rd :: BVView 32 '[11, 10, 9, 8, 7]
>>> :t imm
imm
:: BVView
     32
     '[31, 19, 18, 17, 16, 15, 14, 13, 12, 20, 30, 29, 28, 27, 26, 25,
       24, 23, 22, 21]

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

>>> v = bvView @32 @('[5] ++ Slice 3 4)
<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 @(Slice 30 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)

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.

BVIx

data BVIx w ix

Index of a single bit of a BV.

Instances

TestEquality (BVIx w :: Nat -> Type)

Defined in Data.BitVector.Sized.Lens

Methods

testEquality :: forall (a :: k) (b :: k). BVIx w a -> BVIx w b -> Maybe (a :~: b)

OrdF (BVIx w :: Nat -> Type)

Defined in Data.BitVector.Sized.Lens

Methods

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)

Defined in Data.BitVector.Sized.Lens

Methods

withShow :: forall p q (tp :: k) a. p (BVIx w) -> q tp -> (Show (BVIx w tp) => a) -> a

showF :: forall (tp :: k). BVIx w tp -> String

showsPrecF :: forall (tp :: k). Int -> BVIx w tp -> String -> String

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

Defined in Data.BitVector.Sized.Lens

Methods

knownRepr :: BVIx w ix

Show (BVIx w ix)

Defined in Data.BitVector.Sized.Lens

Methods

showsPrec :: Int -> BVIx w ix -> ShowS

show :: BVIx w ix -> String

showList :: [BVIx w ix] -> ShowS

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

Construct a BVIx when the index is known at compile time.

>>> bvIx @32 @7
BVIx 7
>>> :type it
it :: BVIx 7

bvIxL :: KnownNat w => BVIx w ix -> Lens' (BV w) (BV 1)

Get a lens from a BVIx.

BVView

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

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

Instances

ShowF (BVView w :: [Nat] -> Type)

Defined in Data.BitVector.Sized.Lens

Methods

withShow :: forall p q (tp :: k) a. p (BVView w) -> q tp -> (Show (BVView w tp) => a) -> a

showF :: forall (tp :: k). BVView w tp -> String

showsPrecF :: forall (tp :: k). Int -> BVView w tp -> String -> String

(ValidView ixs, KnownRepr (List (BVIx w)) ixs) => KnownRepr (BVView w :: [Nat] -> Type) (ixs :: [Nat])

Defined in Data.BitVector.Sized.Lens

Methods

knownRepr :: BVView w ixs

Show (BVView w pr)

Defined in Data.BitVector.Sized.Lens

Methods

showsPrec :: Int -> BVView w pr -> ShowS

show :: BVView w pr -> String

showList :: [BVView w pr] -> ShowS

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

Construct a BVView when the width and indices are known at compile time.

>>> bvView @32 @(Slice 9 3)
BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil)
>>> :type it
it :: BVView 32 '[11, 10, 9]
>>> bvView @32 @'[5, 7, 5]
<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]

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

Get a lens from a BVView.

BVViews

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

A list of BVViews where each BVView is disjoint from the others. This is basically a decomposition of a bitvector into disjoint fields.

Instances

ShowF (BVViews w :: [[Nat]] -> Type)

Defined in Data.BitVector.Sized.Lens

Methods

withShow :: forall p q (tp :: k) a. p (BVViews w) -> q tp -> (Show (BVViews w tp) => a) -> a

showF :: forall (tp :: k). BVViews w tp -> String

showsPrecF :: forall (tp :: k). Int -> BVViews w tp -> String -> String

(ValidViews l, KnownRepr (List (BVView w)) l) => KnownRepr (BVViews w :: [[Nat]] -> Type) (l :: [[Nat]])

Defined in Data.BitVector.Sized.Lens

Methods

knownRepr :: BVViews w l

Show (BVViews w ixss)

Defined in Data.BitVector.Sized.Lens

Methods

showsPrec :: Int -> BVViews w ixss -> ShowS

show :: BVViews w ixss -> String

showList :: [BVViews w ixss] -> ShowS

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

Construct a BVViews when the type is fully known at compile time.

>>> bvViews @32 @'[Slice 9 3, Slice' 14 2]
BVViews (BVView (BVIx 11 :< BVIx 10 :< BVIx 9 :< Nil) :< BVView (BVIx 14 :< BVIx 15 :< Nil) :< Nil)
>>> :type it
it :: BVViews 32 '[ '[11, 10, 9], '[14, 15]]
>>> bvViews @32 @'[Slice 0 3, Slice 2 2]
<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]

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

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 (as :: [k]) ++ (bs :: [k]) :: [k] where ...

Type-level list append.

Equations

'[] ++ bs = bs

(a ': as) ++ bs = a ': (as ++ bs)

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

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.

>>> :kind! Slice 7 4
Slice 7 4 :: [Nat]
= '[10, 9, 8, 7]
>>> v = bvView @8 @(Slice 4 2)
>>> printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b01
0b1011100:[8]

Equations

Slice i 0 = '[]

Slice i w = ((i + w) - 1) ': Slice i (w - 1)

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

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.

>>> :kind! Slice' 7 4
Slice' 7 4 :: [Nat]
= '[7, 8, 9, 10]
>>> v = bvView @8 @(Slice' 4 2)
>>> printBV $ BV.mkBV knownNat 0b01101100 & bvViewL v .~ BV.mkBV knownNat 0b10
0b1011100:[8]

Equations

Slice' i 0 = '[]

Slice' i w = i ': Slice' (i + 1) (w - 1)

type family Length (l :: [k]) :: Nat where ...

Type-level list length.

Equations

Length '[] = 0

Length (_ ': ks) = 1 + Length ks

type family Lengths (kss :: [[k]]) :: [Nat] where ...

Length mapped over a list to produce a list of lengths.

Equations

Lengths '[] = '[]

Lengths (ks ': kss) = Length ks ': Lengths kss