KnownLen.hs

-- | 'P.Poke's with type-level poke length.
module Bytezap.Poke.KnownLen where

import Bytezap.Poke qualified as P
import GHC.TypeNats
import Data.ByteString qualified as BS
import GHC.Exts
import Util.TypeNats ( natValInt )

import Raehik.Compat.Data.Primitive.Types

newtype PokeKnownLen (len :: Natural) s =
    PokeKnownLen { unPokeKnownLen :: P.Poke s }

mappend' :: PokeKnownLen n s -> PokeKnownLen m s -> PokeKnownLen (n+m) s
mappend' (PokeKnownLen l) (PokeKnownLen r) = PokeKnownLen (l <> r)

mempty' :: PokeKnownLen 0 s
mempty' = PokeKnownLen mempty

runPokeKnownLenBS
    :: forall n. KnownNat n
    => PokeKnownLen n RealWorld
    -> BS.ByteString
runPokeKnownLenBS (PokeKnownLen p) = P.unsafeRunPokeBS (natValInt @n) p

prim :: Prim' a => a -> PokeKnownLen (SizeOf a) s
prim = PokeKnownLen . P.prim