module Ivory.BitData.Array where
import GHC.TypeLits
import Ivory.Language
import Ivory.BitData.Bits
import Ivory.BitData.BitData
type family ArraySize (n :: Nat) (a :: *) :: Nat
data BitArray (n :: Nat) a = BitArray { unArray :: Bits (ArraySize n a) }
bitLength :: forall a n. SingI n => BitArray n a -> Int
bitLength _ = fromIntegral (fromSing (sing :: Sing n))
instance (SingI n,
SingI (ArraySize n a),
BitData a,
IvoryRep (BitRep (ArraySize n a)))
=> BitData (BitArray n a) where
type BitType (BitArray n a) = Bits (ArraySize n a)
toBits = unArray
fromBits = BitArray
(#!) :: forall a n.
(BitData a,
SingI n,
SingI (BitSize a),
SingI (ArraySize n a),
BitCast (BitRep (ArraySize n a)) (BitDataRep a),
IvoryRep (BitRep (ArraySize n a)))
=> BitArray n a -> Int -> a
BitArray bits #! i =
if (i < 0) || (i >= n')
then error "bit array index out of bounds"
else bits #. field
where
n' = fromIntegral (fromSing (sing :: Sing n)) :: Int
elemSize = fromIntegral (fromSing (sing :: Sing (BitSize a))) :: Int
field = BitDataField (i * elemSize) elemSize
bitIx :: forall a n.
(BitData a,
SingI n,
SingI (BitSize a),
SingI (ArraySize n a))
=> Int -> BitDataField (BitArray n a) a
bitIx i = BitDataField (i * elemSize) elemSize
where
elemSize = fromIntegral (fromSing (sing :: Sing (BitSize a))) :: Int