-- TODO cleanup proxy usage (can we be faster via unboxed @Proxy#@ s ?)

{-# 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 )

-- | Holy shit - no need to do a smart constructor, it's simply impossible to
--   instantiate invalid values of this type!
data LenPfx (size :: ISize) (end :: Endianness) a =
    forall n. (KnownNat n, n <= IMax 'U size) => LenPfx { ()
unLenPfx :: Vector n a }

-- uhhhhhhhhhh i dunno. TODO
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

-- TODO
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
        -- TODO we actually know that @n <= MaxBound irep@ before doing this
        -- because @len <= maxBound (_ :: irep)@ but that's hard to prove to
        -- GHC without lots of refactoring. This is good enough.
        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