-- | Constant-size data.

{-# LANGUAGE OverloadedStrings #-}

module Binrep.Type.Sized where

import Binrep
import FlatParse.Basic qualified as FP

import Binrep.Util ( tshow )

import Refined
import Refined.Unsafe
import Data.Typeable ( typeRep )

import GHC.TypeNats
import Util.TypeNats ( natValInt )

-- | Essentially runtime reflection of a 'BLen' type to 'CBLen'.
data Size (n :: Natural)
type Sized n = Refined (Size 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
     | Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
n
        = TypeRep -> Text -> Maybe RefineException
throwRefineOtherException (Proxy (Size n) -> TypeRep
forall {k} (proxy :: k -> Type) (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
<>Int -> Text
forall a. Show a => a -> Text
tshow Int
lenText -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>Text
" /= "Text -> Text -> Text
forall a. Semigroup a => a -> a -> a
<>Int -> Text
forall a. Show a => a -> Text
tshow Int
n
     | Bool
otherwise = Maybe RefineException
success
      where
        n :: Int
n = forall (n :: Nat). KnownNat n => Int
natValInt @n
        len :: Int
len = a -> Int
forall a. BLen a => a -> Int
blen a
a

instance IsCBLen (Sized n a) where type CBLen (Sized n a) = n
deriving via ViaCBLen (Sized n a) instance KnownNat n => BLen (Sized n a)

instance PutC a => PutC (Sized n a) where
    putC :: Sized n a -> PutterC
putC = a -> PutterC
forall a. PutC a => a -> PutterC
putC (a -> PutterC) -> (Sized n a -> a) -> Sized n a -> PutterC
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sized n a -> a
forall {k} (p :: k) x. Refined p x -> x
unrefine

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

instance (Get a, KnownNat n) => Get (Sized n a) where
    get :: Getter (Sized n a)
get = do
        a
a <- Int -> ParserT PureMode E a -> ParserT PureMode E a
forall (st :: ZeroBitType) e a.
Int -> ParserT st e a -> ParserT st e a
FP.isolate (forall (n :: Nat). KnownNat n => Int
natValInt @n) ParserT PureMode E a
forall a. Get a => Getter a
get
        Sized n a -> Getter (Sized n a)
forall a. a -> ParserT PureMode E a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (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
        -- ^ REFINE SAFETY: 'FP.isolate' consumes precisely the number of bytes
        -- requested when it succeeds