-- | '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 { forall (len :: Natural) s. PokeKnownLen len s -> Poke s
unPokeKnownLen :: P.Poke s }

mappend' :: PokeKnownLen n s -> PokeKnownLen m s -> PokeKnownLen (n+m) s
mappend' :: forall (n :: Natural) s (m :: Natural).
PokeKnownLen n s -> PokeKnownLen m s -> PokeKnownLen (n + m) s
mappend' (PokeKnownLen Poke s
l) (PokeKnownLen Poke s
r) = Poke s -> PokeKnownLen (n + m) s
forall (len :: Natural) s. Poke s -> PokeKnownLen len s
PokeKnownLen (Poke s
l Poke s -> Poke s -> Poke s
forall a. Semigroup a => a -> a -> a
<> Poke s
r)

mempty' :: PokeKnownLen 0 s
mempty' :: forall s. PokeKnownLen 0 s
mempty' = Poke s -> PokeKnownLen 0 s
forall (len :: Natural) s. Poke s -> PokeKnownLen len s
PokeKnownLen Poke s
forall a. Monoid a => a
mempty

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

prim :: Prim' a => a -> PokeKnownLen (SizeOf a) s
prim :: forall a s. Prim' a => a -> PokeKnownLen (SizeOf a) s
prim = Poke s -> PokeKnownLen (SizeOf a) s
forall (len :: Natural) s. Poke s -> PokeKnownLen len s
PokeKnownLen (Poke s -> PokeKnownLen (SizeOf a) s)
-> (a -> Poke s) -> a -> PokeKnownLen (SizeOf a) s
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Poke s
forall a s. Prim' a => a -> Poke s
P.prim