module Ivory.Language.BitData.Array where
import Ivory.Language.Bits
import Ivory.Language.Proxy
import Ivory.Language.BitData.Bits
import Ivory.Language.BitData.BitData
import GHC.TypeLits(Nat)
type family ArraySize (n :: Nat) (a :: *) :: Nat
data BitArray (n :: Nat) a = BitArray { unArray :: Bits (ArraySize n a) }
bitLength :: forall a n. ANat n => BitArray n a -> Int
bitLength _ = fromIntegral (fromTypeNat (aNat :: NatType n))
instance (ANat n,
ANat (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,
ANat n,
ANat (BitSize a),
ANat (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 (fromTypeNat (aNat :: NatType n)) :: Int
elemSize = fromIntegral (fromTypeNat (aNat :: NatType (BitSize a))) :: Int
field = BitDataField (i * elemSize) elemSize ixname
ixname = "[" ++ show i ++ "]"
bitIx :: forall a n.
(BitData a,
ANat n,
ANat (BitSize a),
ANat (ArraySize n a))
=> Int -> BitDataField (BitArray n a) a
bitIx i = BitDataField (i * elemSize) elemSize ixname
where
ixname = "[" ++ show i ++ "]"
elemSize = fromIntegral (fromTypeNat (aNat :: NatType (BitSize a))) :: Int