-- | 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

instance KnownNat n => BLen (Sized n a) where type CBLen (Sized n a) = n

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

instance Put a => Put (Sized n a) where
    put :: Sized n a -> Builder
put = forall a. Put a => a -> Builder
put forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 <- forall e a. BLenT -> Parser e a -> Parser e a
FP.isolate (forall a b. (Integral a, Num b) => a -> b
fromIntegral BLenT
n) forall a. Get a => Getter a
get
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine a
a
      where
        n :: BLenT
n = forall (n :: Nat). KnownNat n => BLenT
typeNatToBLen @n