{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE UndecidableInstances #-}
module Binrep.Type.LenPfx where
import Binrep
import Strongweak
import Data.Either.Validation
import Binrep.Type.Vector ( getVector )
import Binrep.Type.Common ( Endianness )
import Binrep.Type.Int
import Binrep.Util ( natVal'' )
import Data.Vector.Sized ( Vector )
import Data.Vector.Sized qualified as V
import GHC.TypeNats
import GHC.TypeLits ( OrderingI(..) )
import Data.Proxy ( Proxy(..) )
import GHC.Generics
import Data.Typeable ( Typeable )
data LenPfx (size :: ISize) (end :: Endianness) a =
forall n. (KnownNat n, n <= IMax 'U size) => LenPfx { ()
unLenPfx :: Vector n a }
instance Generic (LenPfx size end a) where
type Rep (LenPfx size end a) = Rec0 (LenPfx size end a)
from :: forall x. LenPfx size end a -> Rep (LenPfx size end a) x
from = forall k i c (p :: k). c -> K1 i c p
K1
to :: forall x. Rep (LenPfx size end a) x -> LenPfx size end a
to = forall k i c (p :: k). K1 i c p -> c
unK1
instance Eq a => Eq (LenPfx size end a) where
(LenPfx Vector n a
a) == :: LenPfx size end a -> LenPfx size end a -> Bool
== (LenPfx Vector n a
b) = forall a (n :: Nat) (m :: Nat).
(Eq a, KnownNat n, KnownNat m) =>
Vector n a -> Vector m a -> Bool
vsEq Vector n a
a Vector n a
b
instance Show a => Show (LenPfx size end a) where
show :: LenPfx size end a -> String
show (LenPfx Vector n a
a) = String
"LenPfx ("forall a. Semigroup a => a -> a -> a
<>forall a. Show a => a -> String
show Vector n a
aforall a. Semigroup a => a -> a -> a
<>String
")"
vsEq :: forall a n m. (Eq a, KnownNat n, KnownNat m) => Vector n a -> Vector m a -> Bool
vsEq :: forall a (n :: Nat) (m :: Nat).
(Eq a, KnownNat n, KnownNat m) =>
Vector n a -> Vector m a -> Bool
vsEq Vector n a
vn Vector m a
vm =
if forall (a :: Nat). KnownNat a => Nat
natVal'' @n forall a. Eq a => a -> a -> Bool
== forall (a :: Nat). KnownNat a => Nat
natVal'' @m
then forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector n a
vn forall a. Eq a => a -> a -> Bool
== forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector m a
vm
else Bool
False
instance Weaken (LenPfx size end a) where
type Weak (LenPfx size end a) = [a]
weaken :: LenPfx size end a -> Weak (LenPfx size end a)
weaken (LenPfx Vector n a
v) = forall (n :: Nat) a. Vector n a -> [a]
V.toList Vector n a
v
instance (KnownNat (MaxBound (IRep 'U size)), Show a, Typeable a, Typeable size, Typeable end)
=> Strengthen (LenPfx size end a) where
strengthen :: Weak (LenPfx size end a)
-> Validation (NonEmpty StrengthenFail) (LenPfx size end a)
strengthen Weak (LenPfx size end a)
l = case forall (size :: ISize) (end :: Endianness) a irep.
(irep ~ IRep 'U size, KnownNat (MaxBound irep)) =>
[a] -> Maybe (LenPfx size end a)
lenPfxFromList Weak (LenPfx size end a)
l of
Maybe (LenPfx size end a)
Nothing -> forall s w.
(Typeable w, Show w, Typeable s) =>
w -> String -> Validation (NonEmpty StrengthenFail) s
strengthenFailBase Weak (LenPfx size end a)
l String
"TODO doesn't fit"
Just LenPfx size end a
v -> forall e a. a -> Validation e a
Success LenPfx size end a
v
asLenPfx
:: forall size end n a irep
. (irep ~ IRep 'U size, KnownNat n, KnownNat (MaxBound irep))
=> Vector n a -> Maybe (LenPfx size end a)
asLenPfx :: forall (size :: ISize) (end :: Endianness) (n :: Nat) a irep.
(irep ~ IRep 'U size, KnownNat n, KnownNat (MaxBound irep)) =>
Vector n a -> Maybe (LenPfx size end a)
asLenPfx Vector n a
v =
case forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxBound (IRep 'U size))) of
OrderingI n (MaxBound irep)
LTI -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (size :: ISize) (end :: Endianness) a (n :: Nat).
(KnownNat n, n <= IMax 'U size) =>
Vector n a -> LenPfx size end a
LenPfx Vector n a
v
OrderingI n (MaxBound irep)
EQI -> forall a. a -> Maybe a
Just forall a b. (a -> b) -> a -> b
$ forall (size :: ISize) (end :: Endianness) a (n :: Nat).
(KnownNat n, n <= IMax 'U size) =>
Vector n a -> LenPfx size end a
LenPfx Vector n a
v
OrderingI n (MaxBound irep)
GTI -> forall a. Maybe a
Nothing
lenPfxFromList
:: forall size end a irep
. (irep ~ IRep 'U size, KnownNat (MaxBound irep))
=> [a] -> Maybe (LenPfx size end a)
lenPfxFromList :: forall (size :: ISize) (end :: Endianness) a irep.
(irep ~ IRep 'U size, KnownNat (MaxBound irep)) =>
[a] -> Maybe (LenPfx size end a)
lenPfxFromList [a]
l = forall a r.
[a] -> (forall (n :: Nat). KnownNat n => Vector n a -> r) -> r
V.withSizedList [a]
l forall (size :: ISize) (end :: Endianness) (n :: Nat) a irep.
(irep ~ IRep 'U size, KnownNat n, KnownNat (MaxBound irep)) =>
Vector n a -> Maybe (LenPfx size end a)
asLenPfx
instance (BLen a, itype ~ I 'U size end, KnownNat (CBLen itype))
=> BLen (LenPfx size end a) where
blen :: LenPfx size end a -> Int
blen (LenPfx Vector n a
v) = forall a (n :: Nat). (n ~ CBLen a, KnownNat n) => Int
cblen @itype forall a. Num a => a -> a -> a
+ forall a. BLen a => a -> Int
blen Vector n a
v
instance (itype ~ I 'U size end, irep ~ IRep 'U size, Put a, Put itype, Num irep)
=> Put (LenPfx size end a) where
put :: LenPfx size end a -> Builder
put (LenPfx Vector n a
v) = forall a. Put a => a -> Builder
put @itype (forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) x. KnownNat n => Vector n x -> Nat
vnatVal Vector n a
v)) forall a. Semigroup a => a -> a -> a
<> forall a. Put a => a -> Builder
put Vector n a
v
where
vnatVal :: forall n x. KnownNat n => Vector n x -> Natural
vnatVal :: forall (n :: Nat) x. KnownNat n => Vector n x -> Nat
vnatVal Vector n x
_ = forall (a :: Nat). KnownNat a => Nat
natVal'' @n
lenPfxSize :: Num (IRep 'U size) => LenPfx size end a -> I 'U size end
lenPfxSize :: forall (size :: ISize) (end :: Endianness) a.
Num (IRep 'U size) =>
LenPfx size end a -> I 'U size end
lenPfxSize (LenPfx Vector n a
v) = forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (n :: Nat) x. KnownNat n => Vector n x -> Nat
vnatVal Vector n a
v)
where
vnatVal :: forall n x. KnownNat n => Vector n x -> Natural
vnatVal :: forall (n :: Nat) x. KnownNat n => Vector n x -> Nat
vnatVal Vector n x
_ = forall (a :: Nat). KnownNat a => Nat
natVal'' @n
instance (itype ~ I 'U size end, irep ~ IRep 'U size, Get itype, Integral irep, Get a, KnownNat (MaxBound irep))
=> Get (LenPfx size end a) where
get :: Getter (LenPfx size end a)
get = forall (size :: ISize) (end :: Endianness) a itype irep.
(itype ~ I 'U size end, irep ~ IRep 'U size, Get itype,
Integral irep, KnownNat (MaxBound irep)) =>
Getter a -> Getter (LenPfx size end a)
getLenPfx forall a. Get a => Getter a
get
getLenPfx
:: forall size end a itype irep
. (itype ~ I 'U size end, irep ~ IRep 'U size, Get itype, Integral irep, KnownNat (MaxBound irep))
=> Getter a -> Getter (LenPfx size end a)
getLenPfx :: forall (size :: ISize) (end :: Endianness) a itype irep.
(itype ~ I 'U size end, irep ~ IRep 'U size, Get itype,
Integral irep, KnownNat (MaxBound irep)) =>
Getter a -> Getter (LenPfx size end a)
getLenPfx Getter a
g = do
itype
len <- forall a. Get a => Getter a
get @itype
case Nat -> SomeNat
someNatVal (forall a b. (Integral a, Num b) => a -> b
fromIntegral itype
len) of
SomeNat (Proxy n
Proxy :: Proxy n) -> do
Vector n a
x <- forall (n :: Nat) a. KnownNat n => Getter a -> Getter (Vector n a)
getVector @n Getter a
g
case forall (a :: Nat) (b :: Nat) (proxy1 :: Nat -> *)
(proxy2 :: Nat -> *).
(KnownNat a, KnownNat b) =>
proxy1 a -> proxy2 b -> OrderingI a b
cmpNat (forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxBound irep)) of
OrderingI n (MaxBound irep)
GTI -> forall a. HasCallStack => String -> a
error String
"impossible"
OrderingI n (MaxBound irep)
LTI -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (size :: ISize) (end :: Endianness) a (n :: Nat).
(KnownNat n, n <= IMax 'U size) =>
Vector n a -> LenPfx size end a
LenPfx Vector n a
x
OrderingI n (MaxBound irep)
EQI -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (size :: ISize) (end :: Endianness) a (n :: Nat).
(KnownNat n, n <= IMax 'U size) =>
Vector n a -> LenPfx size end a
LenPfx Vector n a
x