-- | Constant-size data.

{-# LANGUAGE UndecidableInstances #-} -- for PredicateName
{-# LANGUAGE OverloadedStrings #-} -- for refine error builder

module Binrep.Type.Sized where

import Binrep
import FlatParse.Basic qualified as FP

import Rerefined.Predicate.Common
import Rerefined.Refine
import TypeLevelShow.Natural
import TypeLevelShow.Utils
import Data.Text.Builder.Linear qualified as TBL

import GHC.TypeNats
import Util.TypeNats ( natValInt )

-- | Essentially runtime reflection of a 'BLen' type to 'CBLen'.
data Size (n :: Natural)

instance Predicate (Size n) where
    type PredicateName d (Size n) = ShowParen (d > 9)
        ("Size " ++ ShowNatDec n)

type Sized n = Refined (Size n)

instance (KnownPredicateName (Size n), BLen a, KnownNat n)
  => Refine (Size n) a where
    validate :: Proxy# (Size n) -> a -> Maybe RefineFailure
validate Proxy# (Size n)
p a
a = Proxy# (Size n) -> Bool -> Builder -> Maybe RefineFailure
forall {k} (p :: k).
(Predicate p, KnownPredicateName p) =>
Proxy# p -> Bool -> Builder -> Maybe RefineFailure
validateBool Proxy# (Size n)
p (Int
len Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
n) (Builder -> Maybe RefineFailure) -> Builder -> Maybe RefineFailure
forall a b. (a -> b) -> a -> b
$
        Builder
"not correctly sized: "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Int -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec Int
lenBuilder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Builder
" /= "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Int -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec Int
n
      where
        n :: Int
n = forall (n :: Natural). 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) a. Refined p a -> a
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) a. Refined p a -> a
unrefine

instance (Get a, KnownNat n) => Get (Sized n a) where
    get :: Getter (Sized n a)
get = do
        a
a <- Int
-> ParserT PureMode (ParseError Pos Builder) a
-> ParserT PureMode (ParseError Pos Builder) a
forall (st :: ZeroBitType) e a.
Int -> ParserT st e a -> ParserT st e a
FP.isolate (forall (n :: Natural). KnownNat n => Int
natValInt @n) ParserT PureMode (ParseError Pos Builder) a
forall a. Get a => Getter a
get
        Sized n a -> Getter (Sized n a)
forall a. a -> ParserT PureMode (ParseError Pos Builder) 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} a (p :: k). a -> Refined p a
unsafeRefine a
a
        -- ^ REFINE SAFETY: 'FP.isolate' consumes precisely the number of bytes
        -- requested when it succeeds