{-# LANGUAGE UndecidableInstances #-} -- for @KnownNat (CBLen a)@ in head

module Binrep.Put.Struct where

import Bytezap.Struct qualified as Struct
import Bytezap.Struct.Generic qualified as Struct
import Control.Monad.ST ( RealWorld )
import Binrep.CBLen
import GHC.TypeLits ( KnownNat )
import GHC.Generics
import Data.ByteString qualified as B

import Binrep.Common.Via.Prim ( ViaPrim(..) )
import Raehik.Compat.Data.Primitive.Types ( Prim' )
import Data.Word
import Data.Int
import Binrep.Util.ByteOrder
import Raehik.Compat.Data.Primitive.Types.Endian ( ByteSwap )

import Binrep.Common.Class.TypeErrors ( ENoSum, ENoEmpty )
import GHC.TypeLits ( TypeError )
import Data.Void

import Generic.Type.Assert

import Binrep.Common.Via.Generically.NonSum

import Rerefined.Refine
import Rerefined.Predicate.Logical.And

type PutterC = Struct.Poke RealWorld

-- | constant size putter
class PutC a where putC :: a -> PutterC

runPutC :: forall a. (PutC a, KnownNat (CBLen a)) => a -> B.ByteString
runPutC :: forall a. (PutC a, KnownNat (CBLen a)) => a -> ByteString
runPutC = Int -> Poke RealWorld -> ByteString
Struct.unsafeRunPokeBS (forall a. KnownNat (CBLen a) => Int
forall {k} (a :: k). KnownNat (CBLen a) => Int
cblen @a) (Poke RealWorld -> ByteString)
-> (a -> Poke RealWorld) -> a -> ByteString
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Poke RealWorld
forall a. PutC a => a -> Poke RealWorld
putC

instance Struct.GPokeBase PutC where
    type GPokeBaseSt PutC   = RealWorld
    type GPokeBaseC  PutC a = PutC a
    gPokeBase :: forall a. GPokeBaseC PutC a => a -> Poke# (GPokeBaseSt PutC)
gPokeBase = Poke RealWorld -> Poke# RealWorld
forall s. Poke s -> Poke# s
Struct.unPoke (Poke RealWorld -> Poke# RealWorld)
-> (a -> Poke RealWorld) -> a -> Poke# RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Poke RealWorld
forall a. PutC a => a -> Poke RealWorld
putC
    type GPokeBaseLenTF PutC = CBLenSym

-- | Serialize a term of the struct-like type @a@ via its 'Generic' instance.
putGenericStruct
    :: forall a
    .  ( Generic a, Struct.GPoke PutC (Rep a)
       , GAssertNotVoid a, GAssertNotSum a
    ) => a -> PutterC
putGenericStruct :: forall a.
(Generic a, GPoke PutC (Rep a), GAssertNotVoid a,
 GAssertNotSum a) =>
a -> Poke RealWorld
putGenericStruct = Poke# RealWorld -> Poke RealWorld
forall s. Poke# s -> Poke s
Struct.Poke (Poke# RealWorld -> Poke RealWorld)
-> (a -> Poke# RealWorld) -> a -> Poke RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k1} (tag :: k) (f :: k1 -> Type) (p :: k1).
GPoke tag f =>
f p -> Poke# (GPokeBaseSt tag)
forall (tag :: Type -> Constraint) (f :: Type -> Type) p.
GPoke tag f =>
f p -> Poke# (GPokeBaseSt tag)
Struct.gPoke @PutC (Rep a Any -> Poke# RealWorld)
-> (a -> Rep a Any) -> a -> Poke# RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Rep a Any
forall x. a -> Rep a x
forall a x. Generic a => a -> Rep a x
from

instance
  ( Generic a, Struct.GPoke PutC (Rep a)
  , GAssertNotVoid a, GAssertNotSum a
  ) => PutC (Generically a) where
    putC :: Generically a -> Poke RealWorld
putC (Generically a
a) = a -> Poke RealWorld
forall a.
(Generic a, GPoke PutC (Rep a), GAssertNotVoid a,
 GAssertNotSum a) =>
a -> Poke RealWorld
putGenericStruct a
a

instance
  ( Generic a, Struct.GPoke PutC (Rep a)
  , GAssertNotVoid a, GAssertNotSum a
  ) => PutC (GenericallyNonSum a) where
    putC :: GenericallyNonSum a -> Poke RealWorld
putC = a -> Poke RealWorld
forall a.
(Generic a, GPoke PutC (Rep a), GAssertNotVoid a,
 GAssertNotSum a) =>
a -> Poke RealWorld
putGenericStruct (a -> Poke RealWorld)
-> (GenericallyNonSum a -> a)
-> GenericallyNonSum a
-> Poke RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. GenericallyNonSum a -> a
forall a. GenericallyNonSum a -> a
unGenericallyNonSum

instance PutC (Refined pr (Refined pl a))
  => PutC (Refined (pl `And` pr) a) where
    putC :: Refined (And pl pr) a -> Poke RealWorld
putC = Refined pr (Refined pl a) -> Poke RealWorld
forall a. PutC a => a -> Poke RealWorld
putC (Refined pr (Refined pl a) -> Poke RealWorld)
-> (Refined (And pl pr) a -> Refined pr (Refined pl a))
-> Refined (And pl pr) a
-> Poke RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (p :: k1). a -> Refined p a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine @_ @pr (Refined pl a -> Refined pr (Refined pl a))
-> (Refined (And pl pr) a -> Refined pl a)
-> Refined (And pl pr) a
-> Refined pr (Refined pl a)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a (p :: k). a -> Refined p a
forall {k} a (p :: k). a -> Refined p a
unsafeRefine @_ @pl (a -> Refined pl a)
-> (Refined (And pl pr) a -> a)
-> Refined (And pl pr) a
-> Refined pl a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Refined (And pl pr) a -> a
forall {k} (p :: k) a. Refined p a -> a
unrefine

instance Prim' a => PutC (ViaPrim a) where
    putC :: ViaPrim a -> Poke RealWorld
putC = a -> Poke RealWorld
forall a s. Prim' a => a -> Poke s
Struct.prim (a -> Poke RealWorld)
-> (ViaPrim a -> a) -> ViaPrim a -> Poke RealWorld
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ViaPrim a -> a
forall a. ViaPrim a -> a
unViaPrim
    {-# INLINE putC #-}

instance TypeError ENoEmpty => PutC Void where putC :: Void -> Poke RealWorld
putC = Void -> Poke RealWorld
forall a. HasCallStack => a
undefined
instance TypeError ENoSum => PutC (Either a b) where putC :: Either a b -> Poke RealWorld
putC = Either a b -> Poke RealWorld
forall a. HasCallStack => a
undefined

instance PutC PutterC where putC :: Poke RealWorld -> Poke RealWorld
putC = Poke RealWorld -> Poke RealWorld
forall a. a -> a
id

-- | Unit type serializes to nothing. How zen.
instance PutC () where
    {-# INLINE putC #-}
    putC :: () -> Poke RealWorld
putC () = Poke RealWorld
forall s. Poke s
Struct.emptyPoke

-- | Look weird? Yeah. But it's correct :)
instance (PutC l, KnownNat (CBLen l), PutC r) => PutC (l, r) where
    {-# INLINE putC #-}
    putC :: (l, r) -> Poke RealWorld
putC (l
l, r
r) = Poke RealWorld -> Int -> Poke RealWorld -> Poke RealWorld
forall s. Poke s -> Int -> Poke s -> Poke s
Struct.sequencePokes (l -> Poke RealWorld
forall a. PutC a => a -> Poke RealWorld
putC l
l) (forall a. KnownNat (CBLen a) => Int
forall {k} (a :: k). KnownNat (CBLen a) => Int
cblen @l) (r -> Poke RealWorld
forall a. PutC a => a -> Poke RealWorld
putC r
r)

-- | 8-bit (1-byte) words do not require byte order in order to precisely
--   define their representation.
deriving via ViaPrim Word8 instance PutC Word8

-- | 8-bit (1-byte) words do not require byte order in order to precisely
--   define their representation.
deriving via ViaPrim  Int8 instance PutC  Int8

-- | Byte order is irrelevant for 8-bit (1-byte) words.
deriving via Word8 instance PutC (ByteOrdered end Word8)

-- | Byte order is irrelevant for 8-bit (1-byte) words.
deriving via  Int8 instance PutC (ByteOrdered end  Int8)

-- ByteSwap is required on opposite endian platforms, but we're not checking
-- here, so make sure to keep it on both.
deriving via ViaPrim (ByteOrdered LittleEndian a)
    instance (Prim' a, ByteSwap a) => PutC (ByteOrdered LittleEndian a)
deriving via ViaPrim (ByteOrdered    BigEndian a)
    instance (Prim' a, ByteSwap a) => PutC (ByteOrdered    BigEndian a)