{-# LANGUAGE OverloadedStrings #-}

module Binrep.Type.NullPadded where

import Binrep
import Binrep.Util ( tshow )

import Refined
import Refined.Unsafe

import GHC.TypeNats
import Data.Typeable ( typeRep )
import FlatParse.Basic qualified as FP
import FlatParse.Basic ( Parser )
import Mason.Builder qualified as Mason
import Data.ByteString qualified as BS

data NullPad (n :: Natural)

type NullPadded n a = Refined (NullPad n) a

-- | The size of some null-padded data is known - at compile time!
type instance CBLen (NullPadded n a) = n

deriving anyclass instance KnownNat n => BLen (NullPadded n a)

instance (BLen a, KnownNat n) => Predicate (NullPad n) a where
    validate :: Proxy (NullPad n) -> a -> Maybe RefineException
validate Proxy (NullPad n)
p a
a
      | BLenT
len BLenT -> BLenT -> Bool
forall a. Ord a => a -> a -> Bool
> BLenT
n
          = TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (NullPad n) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (NullPad n)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$
                   Text
"too long: " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BLenT -> Text
forall a. Show a => a -> Text
tshow BLenT
len Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> Text
" > " Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<> BLenT -> Text
forall a. Show a => a -> Text
tshow BLenT
n
      | Bool
otherwise = Maybe RefineException
success
      where
        n :: BLenT
n = forall (n :: Nat). KnownNat n => BLenT
typeNatToBLen @n
        len :: BLenT
len = a -> BLenT
forall a. BLen a => a -> BLenT
blen a
a

-- TODO cleanup
instance (Put a, BLen a, KnownNat n) => Put (NullPadded n a) where
    put :: NullPadded n a -> Builder
put NullPadded n a
wrnpa =
        let npa :: a
npa = NullPadded n a -> a
forall {k} (p :: k) x. Refined p x -> x
unrefine NullPadded n a
wrnpa
            paddingLength :: BLenT
paddingLength = BLenT
n BLenT -> BLenT -> BLenT
forall a. Num a => a -> a -> a
- a -> BLenT
forall a. BLen a => a -> BLenT
blen a
npa
         in a -> Builder
forall a. Put a => a -> Builder
put a
npa Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<> ByteString -> Builder
forall s. Buildable s => ByteString -> BuilderFor s
Mason.byteString (BLenT -> Word8 -> ByteString
BS.replicate (BLenT -> BLenT
forall a b. (Integral a, Num b) => a -> b
fromIntegral BLenT
paddingLength) Word8
0x00)
      where
        n :: BLenT
n = forall (n :: Nat). KnownNat n => BLenT
typeNatToBLen @n

-- | Safety: we assert actual length is within expected length (in order to
--   calculate how much padding to parse).
--
-- Note that the consumer probably doesn't care about the content of the
-- padding, just that the data is chunked correctly. I figure we care about
-- correctness here, so it'd be nice to know about the padding well-formedness
-- (i.e. that it's all nulls).
--
-- TODO maybe better definition via isolate
instance (Get a, BLen a, KnownNat n) => Get (NullPadded n a) where
    get :: Getter (NullPadded n a)
get = do
        a
a <- Getter a
forall a. Get a => Getter a
get
        let len :: BLenT
len = a -> BLenT
forall a. BLen a => a -> BLenT
blen a
a
            nullStrLen :: BLenT
nullStrLen = BLenT
n BLenT -> BLenT -> BLenT
forall a. Num a => a -> a -> a
- BLenT
len
        if   BLenT
nullStrLen BLenT -> BLenT -> Bool
forall a. Ord a => a -> a -> Bool
< BLenT
0
        then String -> Getter (NullPadded n a)
forall e a. e -> Parser e a
FP.err (String -> Getter (NullPadded n a))
-> String -> Getter (NullPadded n a)
forall a b. (a -> b) -> a -> b
$ String
"too long: " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> BLenT -> String
forall a. Show a => a -> String
show BLenT
len String -> String -> String
forall a. Semigroup a => a -> a -> a
<> String
" > " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> BLenT -> String
forall a. Show a => a -> String
show BLenT
n
        else BLenT -> Parser String ()
getNNulls BLenT
nullStrLen Parser String ()
-> Getter (NullPadded n a) -> Getter (NullPadded n a)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> NullPadded n a -> Getter (NullPadded n a)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> NullPadded n a
forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine a
a)
      where
        n :: BLenT
n = forall (n :: Nat). KnownNat n => BLenT
typeNatToBLen @n

getNNulls :: BLenT -> Parser String ()
getNNulls :: BLenT -> Parser String ()
getNNulls = \case BLenT
0 -> () -> Parser String ()
forall (m :: * -> *) a. Monad m => a -> m a
return ()
                  BLenT
n -> Parser String Word8
forall e. Parser e Word8
FP.anyWord8 Parser String Word8
-> (Word8 -> Parser String ()) -> Parser String ()
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                         Word8
0x00    -> BLenT -> Parser String ()
getNNulls (BLenT -> Parser String ()) -> BLenT -> Parser String ()
forall a b. (a -> b) -> a -> b
$ BLenT
nBLenT -> BLenT -> BLenT
forall a. Num a => a -> a -> a
-BLenT
1
                         Word8
nonNull -> String -> Parser String ()
forall e a. e -> Parser e a
FP.err String
"TODO expected null, wasn't"