-- | Constant-size data.

{-# LANGUAGE OverloadedStrings #-}

module Binrep.Type.Sized 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

data Size (n :: Natural)

type Sized n a = Refined (Size n) a

type instance CBLen (Sized n a) = n

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

instance (BLen a, KnownNat n) => Predicate (Size n) a where
    validate :: Proxy (Size n) -> a -> Maybe RefineException
validate Proxy (Size n)
p a
a
     | BLenT
len BLenT -> BLenT -> Bool
forall a. Ord a => a -> a -> Bool
> BLenT
n
        = TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (Size n) -> TypeRep
forall {k} (proxy :: k -> *) (a :: k).
Typeable a =>
proxy a -> TypeRep
typeRep Proxy (Size n)
p) (Text -> Maybe RefineException) -> Text -> Maybe RefineException
forall a b. (a -> b) -> a -> b
$
            Text
"not correctly sized: "Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>BLenT -> Text
forall a. Show a => a -> Text
tshow BLenT
lenText -> 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

instance Put a => Put (Sized n a) where
    put :: Sized n a -> Builder
put = a -> Builder
forall a. Put a => a -> Builder
put (a -> Builder) -> (Sized n a -> a) -> Sized n a -> Builder
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized n a -> a
forall {k} (p :: k) x. Refined p x -> x
unrefine

-- TODO safety: isolate consumes all bytes if succeeds
instance (Get a, KnownNat n) => Get (Sized n a) where
    get :: Getter (Sized n a)
get = do
        a
a <- BLenT -> Parser String a -> Parser String a
forall e a. BLenT -> Parser e a -> Parser e a
FP.isolate (BLenT -> BLenT
forall a b. (Integral a, Num b) => a -> b
fromIntegral BLenT
n) Parser String a
forall a. Get a => Getter a
get
        Sized n a -> Getter (Sized n a)
forall (m :: * -> *) a. Monad m => a -> m a
return (Sized n a -> Getter (Sized n a))
-> Sized n a -> Getter (Sized n a)
forall a b. (a -> b) -> a -> b
$ a -> Sized 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