{-# LANGUAGE UndecidableInstances #-}
module Binrep.Type.Magic where
import Binrep
import Bytezap.Struct.TypeLits ( ReifyBytesW64(reifyBytesW64) )
import FlatParse.Basic qualified as FP
import Data.ByteString qualified as B
import Util.TypeNats ( natValInt )
import GHC.TypeLits
import GHC.Generics ( Generic )
import Data.Data ( Data )
import Strongweak
data Magic (a :: k) = Magic deriving stock ((forall x. Magic a -> Rep (Magic a) x)
-> (forall x. Rep (Magic a) x -> Magic a) -> Generic (Magic a)
forall x. Rep (Magic a) x -> Magic a
forall x. Magic a -> Rep (Magic a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (a :: k) x. Rep (Magic a) x -> Magic a
forall k (a :: k) x. Magic a -> Rep (Magic a) x
$cfrom :: forall k (a :: k) x. Magic a -> Rep (Magic a) x
from :: forall x. Magic a -> Rep (Magic a) x
$cto :: forall k (a :: k) x. Rep (Magic a) x -> Magic a
to :: forall x. Rep (Magic a) x -> Magic a
Generic, Typeable (Magic a)
Typeable (Magic a) =>
(forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a))
-> (forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a))
-> (Magic a -> Constr)
-> (Magic a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a)))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a)))
-> ((forall b. Data b => b -> b) -> Magic a -> Magic a)
-> (forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r)
-> (forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r)
-> (forall u. (forall d. Data d => d -> u) -> Magic a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> Magic a -> u)
-> (forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> Data (Magic a)
Magic a -> Constr
Magic a -> DataType
(forall b. Data b => b -> b) -> Magic a -> Magic a
forall a.
Typeable a =>
(forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> Magic a -> u
forall u. (forall d. Data d => d -> u) -> Magic a -> [u]
forall k (a :: k). (Typeable a, Typeable k) => Typeable (Magic a)
forall k (a :: k). (Typeable a, Typeable k) => Magic a -> Constr
forall k (a :: k). (Typeable a, Typeable k) => Magic a -> DataType
forall k (a :: k).
(Typeable a, Typeable k) =>
(forall b. Data b => b -> b) -> Magic a -> Magic a
forall k (a :: k) u.
(Typeable a, Typeable k) =>
Int -> (forall d. Data d => d -> u) -> Magic a -> u
forall k (a :: k) u.
(Typeable a, Typeable k) =>
(forall d. Data d => d -> u) -> Magic a -> [u]
forall k (a :: k) r r'.
(Typeable a, Typeable k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
forall k (a :: k) r r'.
(Typeable a, Typeable k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
forall k (a :: k) (m :: Type -> Type).
(Typeable a, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall k (a :: k) (m :: Type -> Type).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall k (a :: k) (c :: Type -> Type).
(Typeable a, Typeable k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
forall k (a :: k) (c :: Type -> Type).
(Typeable a, Typeable k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
forall k (a :: k) (t :: Type -> Type) (c :: Type -> Type).
(Typeable a, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
forall k (a :: k) (t :: Type -> Type -> Type) (c :: Type -> Type).
(Typeable a, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
$cgfoldl :: forall k (a :: k) (c :: Type -> Type).
(Typeable a, Typeable k) =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
gfoldl :: forall (c :: Type -> Type).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
$cgunfold :: forall k (a :: k) (c :: Type -> Type).
(Typeable a, Typeable k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
gunfold :: forall (c :: Type -> Type).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
$ctoConstr :: forall k (a :: k). (Typeable a, Typeable k) => Magic a -> Constr
toConstr :: Magic a -> Constr
$cdataTypeOf :: forall k (a :: k). (Typeable a, Typeable k) => Magic a -> DataType
dataTypeOf :: Magic a -> DataType
$cdataCast1 :: forall k (a :: k) (t :: Type -> Type) (c :: Type -> Type).
(Typeable a, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
dataCast1 :: forall (t :: Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
$cdataCast2 :: forall k (a :: k) (t :: Type -> Type -> Type) (c :: Type -> Type).
(Typeable a, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
dataCast2 :: forall (t :: Type -> Type -> Type) (c :: Type -> Type).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
$cgmapT :: forall k (a :: k).
(Typeable a, Typeable k) =>
(forall b. Data b => b -> b) -> Magic a -> Magic a
gmapT :: (forall b. Data b => b -> b) -> Magic a -> Magic a
$cgmapQl :: forall k (a :: k) r r'.
(Typeable a, Typeable k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
$cgmapQr :: forall k (a :: k) r r'.
(Typeable a, Typeable k) =>
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
gmapQr :: forall r r'.
(r' -> r -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
$cgmapQ :: forall k (a :: k) u.
(Typeable a, Typeable k) =>
(forall d. Data d => d -> u) -> Magic a -> [u]
gmapQ :: forall u. (forall d. Data d => d -> u) -> Magic a -> [u]
$cgmapQi :: forall k (a :: k) u.
(Typeable a, Typeable k) =>
Int -> (forall d. Data d => d -> u) -> Magic a -> u
gmapQi :: forall u. Int -> (forall d. Data d => d -> u) -> Magic a -> u
$cgmapM :: forall k (a :: k) (m :: Type -> Type).
(Typeable a, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapM :: forall (m :: Type -> Type).
Monad m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
$cgmapMp :: forall k (a :: k) (m :: Type -> Type).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapMp :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
$cgmapMo :: forall k (a :: k) (m :: Type -> Type).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapMo :: forall (m :: Type -> Type).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
Data, Int -> Magic a -> ShowS
[Magic a] -> ShowS
Magic a -> String
(Int -> Magic a -> ShowS)
-> (Magic a -> String) -> ([Magic a] -> ShowS) -> Show (Magic a)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (a :: k). Int -> Magic a -> ShowS
forall k (a :: k). [Magic a] -> ShowS
forall k (a :: k). Magic a -> String
$cshowsPrec :: forall k (a :: k). Int -> Magic a -> ShowS
showsPrec :: Int -> Magic a -> ShowS
$cshow :: forall k (a :: k). Magic a -> String
show :: Magic a -> String
$cshowList :: forall k (a :: k). [Magic a] -> ShowS
showList :: [Magic a] -> ShowS
Show, Magic a -> Magic a -> Bool
(Magic a -> Magic a -> Bool)
-> (Magic a -> Magic a -> Bool) -> Eq (Magic a)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (a :: k). Magic a -> Magic a -> Bool
$c== :: forall k (a :: k). Magic a -> Magic a -> Bool
== :: Magic a -> Magic a -> Bool
$c/= :: forall k (a :: k). Magic a -> Magic a -> Bool
/= :: Magic a -> Magic a -> Bool
Eq)
instance Weaken (Magic a) where
type Weak (Magic a) = ()
weaken :: Magic a -> Weak (Magic a)
weaken Magic a
Magic = ()
instance Strengthen (Magic a) where strengthen :: Weak (Magic a) -> Result (Magic a)
strengthen () = Magic a -> Result (Magic a)
forall a. a -> Validation Fails a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Magic a
forall k (a :: k). Magic a
Magic
instance IsCBLen (Magic a) where type CBLen (Magic a) = Length (MagicBytes a)
deriving via ViaCBLen (Magic a) instance
KnownNat (Length (MagicBytes a)) => BLen (Magic a)
instance (bs ~ MagicBytes a, ReifyBytesW64 bs) => PutC (Magic a) where
putC :: Magic a -> PutterC
putC Magic a
Magic = forall (ns :: [Natural]) n. ReifyBytesW64 ns => Poke n
reifyBytesW64 @bs
deriving via (ViaPutC (Magic a)) instance
(bs ~ MagicBytes a, ReifyBytesW64 bs, KnownNat (Length bs)) => Put (Magic a)
instance (bs ~ MagicBytes a, ReifyBytesW64 bs, KnownNat (Length bs))
=> Get (Magic a) where
get :: Getter (Magic a)
get = do
ByteString
actual <- Int -> ParserT PureMode E ByteString
forall (st :: ZeroBitType) e. Int -> ParserT st e ByteString
FP.take (forall (n :: Natural). KnownNat n => Int
natValInt @(Length bs))
if ByteString
actual ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
expected
then Magic a -> Getter (Magic a)
forall a. a -> ParserT PureMode E a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure Magic a
magic
else EBase -> Getter (Magic a)
forall a. EBase -> Getter a
eBase (EBase -> Getter (Magic a)) -> EBase -> Getter (Magic a)
forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString -> EBase
EExpected ByteString
expected (ByteString -> ByteString
B.copy ByteString
actual)
where
expected :: ByteString
expected = Magic a -> ByteString
forall a. (BLen a, Put a) => a -> ByteString
runPut Magic a
magic
magic :: Magic a
magic = Magic a
forall k (a :: k). Magic a
Magic :: Magic a
type family Length (a :: [k]) :: Natural where
Length '[] = 0
Length (a ': as) = 1 + Length as
type family SymbolUnicodeCodepoints (a :: Symbol) :: [Natural] where
SymbolUnicodeCodepoints a = CharListUnicodeCodepoints (SymbolAsCharList a)
type family CharListUnicodeCodepoints (a :: [Char]) :: [Natural] where
CharListUnicodeCodepoints '[] = '[]
CharListUnicodeCodepoints (c ': cs) = CharToNat c ': CharListUnicodeCodepoints cs
type family SymbolAsCharList (a :: Symbol) :: [Char] where
SymbolAsCharList a = SymbolAsCharList' (UnconsSymbol a)
type family SymbolAsCharList' (a :: Maybe (Char, Symbol)) :: [Char] where
SymbolAsCharList' 'Nothing = '[]
SymbolAsCharList' ('Just '(c, s)) = c ': SymbolAsCharList' (UnconsSymbol s)
class Magical (a :: k) where
type MagicBytes a :: [Natural]
instance Magical (ns :: [Natural]) where type MagicBytes ns = ns
instance Magical (sym :: Symbol) where
type MagicBytes sym = SymbolUnicodeCodepoints sym