{-# language DataKinds #-}
{-# language MagicHash #-}
{-# language TypeOperators #-}

module Data.Bytes.Indexed
  ( ByteArrayN
  , append
  , length
  , length#
  ) where

import Prelude hiding (length)

import Data.Primitive (ByteArray(ByteArray))
import Data.Bytes.Types (ByteArrayN(ByteArrayN))
import GHC.TypeNats (type (+))
import Arithmetic.Types (Nat, Nat#)

import qualified Data.Primitive as PM
import qualified Arithmetic.Unsafe as Unsafe
import qualified GHC.Exts as Exts

append :: ByteArrayN m -> ByteArrayN n -> ByteArrayN (m + n)
{-# inline append #-}
append :: forall (m :: Nat) (n :: Nat).
ByteArrayN m -> ByteArrayN n -> ByteArrayN (m + n)
append (ByteArrayN ByteArray
x) (ByteArrayN ByteArray
y) = ByteArray -> ByteArrayN (m + n)
forall (n :: Nat). ByteArray -> ByteArrayN n
ByteArrayN (ByteArray
x ByteArray -> ByteArray -> ByteArray
forall a. Semigroup a => a -> a -> a
<> ByteArray
y)

-- | Recover a witness of the length.
length :: ByteArrayN n -> Nat n
{-# inline length #-}
length :: forall (n :: Nat). ByteArrayN n -> Nat n
length (ByteArrayN ByteArray
x) = Int -> Nat n
forall (n :: Nat). Int -> Nat n
Unsafe.Nat (ByteArray -> Int
PM.sizeofByteArray ByteArray
x)

-- | Recover an unboxed witness of the length.
length# :: ByteArrayN n -> Nat# n
{-# inline length# #-}
length# :: forall (n :: Nat). ByteArrayN n -> Nat# n
length# (ByteArrayN (ByteArray ByteArray#
x)) = Int# -> Nat# n
forall (a :: Nat). Int# -> Nat# a
Unsafe.Nat# (ByteArray# -> Int#
Exts.sizeofByteArray# ByteArray#
x)