{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE StandaloneKindSignatures #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | 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.
module Data.BitVector.Sized.Lens
  ( -- * BVIx
    BVIx
  , bvIx
  , bvIxL
    -- * BVView
  , BVView
  , bvView
  , bvViewL
    -- * BVViews
  , BVViews
  , bvViews
  , bvViewsL
  -- * Type families on lists
  -- | Various type families that are useful for constructing types when using
  -- this library.
  , type (++)
  , type Slice
  , type Slice'
  , type Length
  , type Lengths
  ) where

import           Data.BitVector.Sized ( BV, pattern BV )
import qualified Data.BitVector.Sized as BV
import Data.Parameterized.Classes
import           Data.Parameterized.List
import Data.Parameterized.NatRepr
import Data.Type.Bool
import Data.Type.Equality
import Control.Lens.Getter
import Control.Lens.Lens
import Control.Lens.Setter
import GHC.Exts (Constraint)
import GHC.TypeLits
import Prelude hiding (concat)

type ValidIx' :: Nat -> Nat -> Bool
type family ValidIx' w ix where
  ValidIx' w ix = If (ix + 1 <=? w) 'True
    (TypeError
     (('Text "Invalid index " ':<>: 'ShowType ix ':<>:
       'Text " into BV " ':<>: 'ShowType w) ':$$:
      ('Text "index must be strictly smaller than bitvector width")))

type ValidIx :: Nat -> Nat -> Constraint
class ix + 1 <= w => ValidIx w ix
instance (ValidIx' w ix ~ 'True, ix + 1 <= w) => ValidIx w ix

catLens :: forall w wh wl .
           NatRepr wh
        -> NatRepr wl
        -> Lens' (BV w) (BV wh)
        -> Lens' (BV w) (BV wl)
        -> Lens' (BV w) (BV (wh + wl))
catLens :: NatRepr wh
-> NatRepr wl
-> Lens' (BV w) (BV wh)
-> Lens' (BV w) (BV wl)
-> Lens' (BV w) (BV (wh + wl))
catLens NatRepr wh
wh NatRepr wl
wl Lens' (BV w) (BV wh)
hi Lens' (BV w) (BV wl)
lo = (BV w -> BV (wh + wl))
-> (BV w -> BV (wh + wl) -> BV w) -> Lens' (BV w) (BV (wh + wl))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens BV w -> BV (wh + wl)
g BV w -> BV (wh + wl) -> BV w
s
  where g :: BV w -> BV (wh + wl)
g BV w
bv = NatRepr wh -> NatRepr wl -> BV wh -> BV wl -> BV (wh + wl)
forall (w :: Nat) (w' :: Nat).
NatRepr w -> NatRepr w' -> BV w -> BV w' -> BV (w + w')
BV.concat NatRepr wh
wh NatRepr wl
wl (BV w
bv BV w -> Getting (BV wh) (BV w) (BV wh) -> BV wh
forall s a. s -> Getting a s a -> a
^. Getting (BV wh) (BV w) (BV wh)
Lens' (BV w) (BV wh)
hi) (BV w
bv BV w -> Getting (BV wl) (BV w) (BV wl) -> BV wl
forall s a. s -> Getting a s a -> a
^. Getting (BV wl) (BV w) (BV wl)
Lens' (BV w) (BV wl)
lo)
        s :: BV w -> BV (wh + wl) -> BV w
        s :: BV w -> BV (wh + wl) -> BV w
s BV w
bv BV (wh + wl)
bv'
          | LeqProof wl (wh + wl)
LeqProof <- NatRepr wh -> NatRepr wl -> LeqProof wl (wh + wl)
forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
f m -> g n -> LeqProof n (m + n)
addPrefixIsLeq NatRepr wh
wh NatRepr wl
wl
          , (wh + wl) :~: (wl + wh)
Refl <- NatRepr wh -> NatRepr wl -> (wh + wl) :~: (wl + wh)
forall (f :: Nat -> *) (m :: Nat) (g :: Nat -> *) (n :: Nat).
f m -> g n -> (m + n) :~: (n + m)
plusComm NatRepr wh
wh NatRepr wl
wl
          = let bvl :: BV wl
                bvl :: BV wl
bvl = NatRepr 0 -> NatRepr wl -> BV (wh + wl) -> BV wl
forall (ix :: Nat) (w' :: Nat) (w :: Nat).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
BV.select (KnownNat 0 => NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @0) NatRepr wl
wl BV (wh + wl)
bv'
                bvh :: BV wh
                bvh :: BV wh
bvh = NatRepr wl -> NatRepr wh -> BV (wh + wl) -> BV wh
forall (ix :: Nat) (w' :: Nat) (w :: Nat).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
BV.select NatRepr wl
wl NatRepr wh
wh BV (wh + wl)
bv'
            in BV w
bv BV w -> (BV w -> BV w) -> BV w
forall a b. a -> (a -> b) -> b
& (BV wh -> Identity (BV wh)) -> BV w -> Identity (BV w)
Lens' (BV w) (BV wh)
hi ((BV wh -> Identity (BV wh)) -> BV w -> Identity (BV w))
-> BV wh -> BV w -> BV w
forall s t a b. ASetter s t a b -> b -> s -> t
.~ BV wh
bvh BV w -> (BV w -> BV w) -> BV w
forall a b. a -> (a -> b) -> b
& (BV wl -> Identity (BV wl)) -> BV w -> Identity (BV w)
Lens' (BV w) (BV wl)
lo ((BV wl -> Identity (BV wl)) -> BV w -> Identity (BV w))
-> BV wl -> BV w -> BV w
forall s t a b. ASetter s t a b -> b -> s -> t
.~ BV wl
bvl

-- | Index of a single bit of a 'Data.BitVector.Sized.Internal.BV'.
data BVIx w ix where
  BVIx :: ValidIx w ix => NatRepr ix -> BVIx w ix

deriving instance Show (BVIx w ix)
instance ShowF (BVIx w)

instance TestEquality (BVIx w) where
  BVIx NatRepr a
ix testEquality :: BVIx w a -> BVIx w b -> Maybe (a :~: b)
`testEquality` BVIx NatRepr b
ix' = NatRepr a
ix NatRepr a -> NatRepr b -> Maybe (a :~: b)
forall k (f :: k -> *) (a :: k) (b :: k).
TestEquality f =>
f a -> f b -> Maybe (a :~: b)
`testEquality` NatRepr b
ix'

instance OrdF (BVIx w) where
  BVIx NatRepr x
ix compareF :: BVIx w x -> BVIx w y -> OrderingF x y
`compareF` BVIx NatRepr y
ix' = NatRepr x
ix NatRepr x -> NatRepr y -> OrderingF x y
forall k (ktp :: k -> *) (x :: k) (y :: k).
OrdF ktp =>
ktp x -> ktp y -> OrderingF x y
`compareF` NatRepr y
ix'

instance (KnownNat ix, ValidIx w ix) => KnownRepr (BVIx w) ix where
  knownRepr :: BVIx w ix
knownRepr = NatRepr ix -> BVIx w ix
forall (w :: Nat) (ix :: Nat).
ValidIx w ix =>
NatRepr ix -> BVIx w ix
BVIx NatRepr ix
forall (n :: Nat). KnownNat n => NatRepr n
knownNat

-- | Construct a 'BVIx' when the index is known at compile time.
--
-- >>> bvIx @32 @7
-- BVIx 7
-- >>> :type it
-- it :: BVIx 7
bvIx :: forall w ix . (KnownNat ix, ValidIx w ix) => BVIx w ix
bvIx :: BVIx w ix
bvIx = BVIx w ix
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Get a lens from a 'BVIx'.
bvIxL :: KnownNat w => BVIx w ix -> Lens' (BV w) (BV 1)
bvIxL :: BVIx w ix -> Lens' (BV w) (BV 1)
bvIxL (BVIx NatRepr ix
i) = NatRepr w -> NatRepr ix -> Lens' (BV w) (BV 1)
forall (w :: Nat) (ix :: Nat).
ValidIx w ix =>
NatRepr w -> NatRepr ix -> Lens' (BV w) (BV 1)
bit NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat NatRepr ix
i

-- | A lens into a single bit of a 'Data.BitVector.Sized.Internal.BV'.
bit :: ValidIx w ix => NatRepr w -> NatRepr ix -> Lens' (BV w) (BV 1)
bit :: NatRepr w -> NatRepr ix -> Lens' (BV w) (BV 1)
bit NatRepr w
w NatRepr ix
w' = (BV w -> BV 1) -> (BV w -> BV 1 -> BV w) -> Lens' (BV w) (BV 1)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (NatRepr ix -> NatRepr 1 -> BV w -> BV 1
forall (ix :: Nat) (w' :: Nat) (w :: Nat).
((ix + w') <= w) =>
NatRepr ix -> NatRepr w' -> BV w -> BV w'
BV.select NatRepr ix
w' NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat) BV w -> BV 1 -> BV w
s
  where s :: BV w -> BV 1 -> BV w
s BV w
bv (BV Integer
1) = NatRepr ix -> BV w -> BV w
forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr ix -> BV w -> BV w
BV.setBit NatRepr ix
w' BV w
bv
        s BV w
bv BV 1
_      = NatRepr w -> NatRepr ix -> BV w -> BV w
forall (ix :: Nat) (w :: Nat).
((ix + 1) <= w) =>
NatRepr w -> NatRepr ix -> BV w -> BV w
BV.clearBit NatRepr w
w NatRepr ix
w' BV w
bv

-- | Type-level list membership.
type family Elem (a :: k) (l :: [k]) :: Bool where
  Elem _ '[]    = 'False
  Elem a (k:ks) = a == k || Elem a ks

type family FindDuplicate (ks :: [k]) :: Maybe k where
  FindDuplicate '[] = 'Nothing
  FindDuplicate (k:ks) = If (Elem k ks) ('Just k) (FindDuplicate ks)

type family CheckFindDuplicateResult ixs mix where
  CheckFindDuplicateResult _ 'Nothing = 'True
  CheckFindDuplicateResult ixs ('Just ix) =
    TypeError (('Text "Invalid index list: " ':<>: 'ShowType ixs ':$$:
                'Text "(repeated index " ':<>: 'ShowType ix ':<>: 'Text ")"))

type family ValidView' ixs where
  ValidView' ixs = CheckFindDuplicateResult ixs (FindDuplicate ixs)

class ValidView' ixs ~ 'True => ValidView ixs
instance ValidView' ixs ~ 'True => ValidView ixs

-- | A list of 'BVIx' with no repeated elements. This essentially gives us a
-- reordering of some subset of the bits in a bitvector.
data BVView (w :: Nat) (ixs :: [Nat]) where
  BVView :: ValidView ixs => List (BVIx w) ixs -> BVView w ixs

listLength :: List f ixs -> NatRepr (Length ixs)
listLength :: List f ixs -> NatRepr (Length ixs)
listLength List f ixs
Nil = NatRepr (Length ixs)
forall (n :: Nat). KnownNat n => NatRepr n
knownNat
listLength (f tp
_ :< List f tps
rst) = NatRepr 1 -> NatRepr (Length tps) -> NatRepr (1 + Length tps)
forall (m :: Nat) (n :: Nat).
NatRepr m -> NatRepr n -> NatRepr (m + n)
addNat (KnownNat 1 => NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @1) (List f tps -> NatRepr (Length tps)
forall k (f :: k -> *) (ixs :: [k]).
List f ixs -> NatRepr (Length ixs)
listLength List f tps
rst)

deriving instance Show (BVView w pr)
instance ShowF (BVView w)

instance ( ValidView ixs
         , KnownRepr (List (BVIx w)) ixs
         ) => KnownRepr (BVView w) ixs where
  knownRepr :: BVView w ixs
knownRepr = List (BVIx w) ixs -> BVView w ixs
forall (ixs :: [Nat]) (w :: Nat).
ValidView ixs =>
List (BVIx w) ixs -> BVView w ixs
BVView List (BVIx w) ixs
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | 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]
bvView :: forall w ixs . (KnownRepr (BVView w) ixs, ValidView ixs) => BVView w ixs
bvView :: BVView w ixs
bvView = BVView w ixs
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | Get a lens from a 'BVView'.
bvViewL :: forall w ixs . KnownNat w => BVView w ixs -> Lens' (BV w) (BV (Length ixs))
bvViewL :: BVView w ixs -> Lens' (BV w) (BV (Length ixs))
bvViewL (BVView List (BVIx w) ixs
l) = List (BVIx w) ixs -> Lens' (BV w) (BV (Length ixs))
forall (ixs' :: [Nat]).
List (BVIx w) ixs' -> Lens' (BV w) (BV (Length ixs'))
go List (BVIx w) ixs
l
  where go :: List (BVIx w) ixs' -> Lens' (BV w) (BV (Length ixs'))
        go :: List (BVIx w) ixs' -> Lens' (BV w) (BV (Length ixs'))
go = \case
          List (BVIx w) ixs'
Nil -> (BV w -> BV 0)
-> (BV w -> BV 0 -> BV w) -> Lens (BV w) (BV w) (BV 0) (BV 0)
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (BV 0 -> BV w -> BV 0
forall a b. a -> b -> a
const (NatRepr 0 -> BV 0
forall (w :: Nat). NatRepr w -> BV w
BV.zero NatRepr 0
forall (n :: Nat). KnownNat n => NatRepr n
knownNat)) BV w -> BV 0 -> BV w
forall a b. a -> b -> a
const
          BVIx NatRepr tp
i :< List (BVIx w) tps
rst ->
            NatRepr 1
-> NatRepr (Length tps)
-> Lens' (BV w) (BV 1)
-> Lens' (BV w) (BV (Length tps))
-> Lens' (BV w) (BV (1 + Length tps))
forall (w :: Nat) (wh :: Nat) (wl :: Nat).
NatRepr wh
-> NatRepr wl
-> Lens' (BV w) (BV wh)
-> Lens' (BV w) (BV wl)
-> Lens' (BV w) (BV (wh + wl))
catLens NatRepr 1
forall (n :: Nat). KnownNat n => NatRepr n
knownNat (List (BVIx w) tps -> NatRepr (Length tps)
forall k (f :: k -> *) (ixs :: [k]).
List f ixs -> NatRepr (Length ixs)
listLength List (BVIx w) tps
rst) (NatRepr w -> NatRepr tp -> Lens' (BV w) (BV 1)
forall (w :: Nat) (ix :: Nat).
ValidIx w ix =>
NatRepr w -> NatRepr ix -> Lens' (BV w) (BV 1)
bit (KnownNat w => NatRepr w
forall (n :: Nat). KnownNat n => NatRepr n
knownNat @w) NatRepr tp
i) (List (BVIx w) tps -> Lens' (BV w) (BV (Length tps))
forall (ixs' :: [Nat]).
List (BVIx w) ixs' -> Lens' (BV w) (BV (Length ixs'))
go List (BVIx w) tps
rst)

-- | Computes the intersection of two lists. The lists are assumed to already
-- have no duplicates. If the first argument does have duplicates that survive
-- the intersection operation, the result will have the same duplicates as well.
type Intersection :: [k] -> [k] -> [k]
type family Intersection ks ks' where
  Intersection '[] _ = '[]
  Intersection (k:ks) ks' =
    If (Elem k ks') (k ': Intersection ks ks') (Intersection ks ks')

-- | Two lists are disjoint.
type Disjoint :: [k] -> [k] -> Bool
type Disjoint ks ks' = Intersection ks ks' == '[]

type FindIntersecting' :: [k] -> [[k]] -> Maybe [k]
type family FindIntersecting' ks kss where
  FindIntersecting' _ '[] = 'Nothing
  FindIntersecting' ks (ks' ': kss') =
    If (Disjoint ks ks') (FindIntersecting' ks kss') ('Just ks')

type MergeFstMaybe :: k -> Maybe k -> Maybe (k, k)
type family MergeFstMaybe k mk where
  MergeFstMaybe _ 'Nothing = 'Nothing
  MergeFstMaybe k ('Just k') = 'Just '(k, k')

type (<>) :: Maybe k -> Maybe k -> Maybe k
type family mk <> mk' where
  'Nothing <> mk' = mk'
  'Just k <> _ = 'Just k

type FindIntersecting :: [[k]] -> Maybe ([k],[k])
type family FindIntersecting kss where
  FindIntersecting '[] = 'Nothing
  FindIntersecting (ks ': kss) =
    MergeFstMaybe ks (FindIntersecting' ks kss) <>
    FindIntersecting kss

type family CheckFindIntersectingResult kss m where
  CheckFindIntersectingResult _ 'Nothing = 'True
  CheckFindIntersectingResult kss ('Just '(ks, ks')) =
    TypeError (('Text "Invalid index lists " ':<>: 'ShowType kss) ':$$:
               ('Text "Lists " ':<>: 'ShowType ks ':<>:
                'Text " and " ':<>: 'ShowType ks' ':<>: 'Text " are not disjoint") ':$$:
               ('Text "(their intersection is " ':<>: 'ShowType (Intersection ks ks') ':<>:
                'Text ")"))

type family ValidViews' kss where
  ValidViews' kss = CheckFindIntersectingResult kss (FindIntersecting kss)

class ValidViews' kss ~ 'True => ValidViews kss
instance (ValidViews' kss ~ 'True) => ValidViews kss

-- | A list of 'BVViews' where each 'BVView' is disjoint from the others. This
-- is basically a decomposition of a bitvector into disjoint fields.
data BVViews (w :: Nat) (ixss :: [[Nat]]) where
  BVViews :: ValidViews ixss => List (BVView w) ixss -> BVViews w ixss

deriving instance Show (BVViews w ixss)
instance ShowF (BVViews w)

instance ( ValidViews l
         , KnownRepr (List (BVView w)) l
         ) => KnownRepr (BVViews w) l where
  knownRepr :: BVViews w l
knownRepr = List (BVView w) l -> BVViews w l
forall (ixss :: [[Nat]]) (w :: Nat).
ValidViews ixss =>
List (BVView w) ixss -> BVViews w ixss
BVViews List (BVView w) l
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | 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]
bvViews :: forall w ixss . (KnownRepr (BVViews w) ixss, ValidViews ixss) => BVViews w ixss
bvViews :: BVViews w ixss
bvViews = BVViews w ixss
forall k (f :: k -> *) (ctx :: k). KnownRepr f ctx => f ctx
knownRepr

-- | 'Length' mapped over a list to produce a list of lengths.
type Lengths :: [[k]] -> [Nat]
type family Lengths (kss :: [[k]]) :: [Nat] where
  Lengths '[] = '[]
  Lengths (ks ': kss) = Length ks ': Lengths kss

-- | Get a lens from a 'BVViews'.
bvViewsL :: forall w ixss . KnownNat w
         => BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss))
bvViewsL :: BVViews w ixss -> Lens' (BV w) (List BV (Lengths ixss))
bvViewsL (BVViews List (BVView w) ixss
l) = (BV w -> List BV (Lengths ixss))
-> (BV w -> List BV (Lengths ixss) -> BV w)
-> Lens' (BV w) (List BV (Lengths ixss))
forall s a b t. (s -> a) -> (s -> b -> t) -> Lens s t a b
lens (List (BVView w) ixss -> BV w -> List BV (Lengths ixss)
forall (ixss' :: [[Nat]]).
List (BVView w) ixss' -> BV w -> List BV (Lengths ixss')
g List (BVView w) ixss
l) (List (BVView w) ixss -> BV w -> List BV (Lengths ixss) -> BV w
forall (ixss' :: [[Nat]]).
List (BVView w) ixss' -> BV w -> List BV (Lengths ixss') -> BV w
s List (BVView w) ixss
l)
  where g :: List (BVView w) ixss' -> BV w -> List BV (Lengths ixss')
        g :: List (BVView w) ixss' -> BV w -> List BV (Lengths ixss')
g List (BVView w) ixss'
Nil BV w
_ = List BV (Lengths ixss')
forall k (a :: k -> *). List a '[]
Nil
        g (BVView w tp
v :< List (BVView w) tps
vs) BV w
bv = BV w
bv BV w
-> Getting (BV (Length tp)) (BV w) (BV (Length tp))
-> BV (Length tp)
forall s a. s -> Getting a s a -> a
^. BVView w tp -> Lens' (BV w) (BV (Length tp))
forall (w :: Nat) (ixs :: [Nat]).
KnownNat w =>
BVView w ixs -> Lens' (BV w) (BV (Length ixs))
bvViewL BVView w tp
v BV (Length tp)
-> List BV (Lengths tps) -> List BV (Length tp : Lengths tps)
forall k (a :: k -> *) (tp :: k) (tps :: [k]).
a tp -> List a tps -> List a (tp : tps)
:< List (BVView w) tps -> BV w -> List BV (Lengths tps)
forall (ixss' :: [[Nat]]).
List (BVView w) ixss' -> BV w -> List BV (Lengths ixss')
g List (BVView w) tps
vs BV w
bv
        s :: List (BVView w) ixss' -> BV w -> List BV (Lengths ixss') -> BV w
        s :: List (BVView w) ixss' -> BV w -> List BV (Lengths ixss') -> BV w
s List (BVView w) ixss'
Nil BV w
bv List BV (Lengths ixss')
Nil = BV w
bv
        s (BVView w tp
v :< List (BVView w) tps
vs) BV w
bv (BV tp
bv' :< List BV tps
bvs') = List (BVView w) tps -> BV w -> List BV (Lengths tps) -> BV w
forall (ixss' :: [[Nat]]).
List (BVView w) ixss' -> BV w -> List BV (Lengths ixss') -> BV w
s List (BVView w) tps
vs BV w
bv List BV tps
List BV (Lengths tps)
bvs' BV w -> (BV w -> BV w) -> BV w
forall a b. a -> (a -> b) -> b
& BVView w tp -> Lens' (BV w) (BV (Length tp))
forall (w :: Nat) (ixs :: [Nat]).
KnownNat w =>
BVView w ixs -> Lens' (BV w) (BV (Length ixs))
bvViewL BVView w tp
v ((BV tp -> Identity (BV tp)) -> BV w -> Identity (BV w))
-> BV tp -> BV w -> BV w
forall s t a b. ASetter s t a b -> b -> s -> t
.~ BV tp
bv'

-- | Type-level list length.
type family Length (l :: [k]) :: Nat where
  Length '[] = 0
  Length (_:ks) = 1 + Length ks

-- | Type-level list append.
type family (++) (as :: [k]) (bs :: [k]) :: [k] where
  '[] ++ bs = bs
  (a ': as) ++ bs = a ': (as ++ bs)

-- | 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]
type family Slice (i :: Nat) (w :: Nat) :: [Nat] where
  Slice i 0 = '[]
  Slice i w = i + w - 1 ': Slice i (w-1)

-- | 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]
type family Slice' (i :: Nat) (w :: Nat) :: [Nat] where
  Slice' i 0 = '[]
  Slice' i w = i ': Slice' (i+1) (w-1)