{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE AllowAmbiguousTypes #-}
module Binrep.Type.Magic where
import Binrep
import Binrep.Type.Byte
import GHC.TypeLits
import Data.ByteString qualified as B
import FlatParse.Basic qualified as FP
import GHC.Generics ( Generic )
import Data.Data ( Data )
import Mason.Builder qualified as Mason
import Strongweak
data Magic (a :: k) = Magic
deriving stock (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
$cto :: forall k (a :: k) x. Rep (Magic a) x -> Magic a
$cfrom :: forall k (a :: k) x. Magic a -> Rep (Magic a) x
Generic, Magic a -> DataType
Magic a -> Constr
forall a.
Typeable a
-> (forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
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 :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall {k} {a :: k}. (Typeable a, Typeable k) => Typeable (Magic a)
forall k (a :: k). (Typeable a, Typeable k) => Magic a -> DataType
forall k (a :: k). (Typeable a, Typeable k) => Magic a -> Constr
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 :: * -> *).
(Typeable a, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall k (a :: k) (m :: * -> *).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall k (a :: k) (c :: * -> *).
(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 :: * -> *).
(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 :: * -> *) (c :: * -> *).
(Typeable a, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
forall k (a :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable a, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
gmapMo :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
$cgmapMo :: forall k (a :: k) (m :: * -> *).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapMp :: forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
$cgmapMp :: forall k (a :: k) (m :: * -> *).
(Typeable a, Typeable k, MonadPlus m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapM :: forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
$cgmapM :: forall k (a :: k) (m :: * -> *).
(Typeable a, Typeable k, Monad m) =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
gmapQi :: forall u. Int -> (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
gmapQ :: forall u. (forall d. Data d => d -> u) -> Magic a -> [u]
$cgmapQ :: forall k (a :: k) u.
(Typeable a, Typeable k) =>
(forall d. Data d => d -> u) -> Magic a -> [u]
gmapQr :: 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
gmapQl :: forall r r'.
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
$cgmapQl :: forall k (a :: k) r r'.
(Typeable a, Typeable k) =>
(r -> r' -> r)
-> r -> (forall d. Data d => d -> r') -> Magic a -> r
gmapT :: (forall b. Data b => b -> b) -> Magic a -> Magic a
$cgmapT :: forall k (a :: k).
(Typeable a, Typeable k) =>
(forall b. Data b => b -> b) -> Magic a -> Magic a
dataCast2 :: forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
$cdataCast2 :: forall k (a :: k) (t :: * -> * -> *) (c :: * -> *).
(Typeable a, Typeable k, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (Magic a))
dataCast1 :: forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
$cdataCast1 :: forall k (a :: k) (t :: * -> *) (c :: * -> *).
(Typeable a, Typeable k, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
dataTypeOf :: Magic a -> DataType
$cdataTypeOf :: forall k (a :: k). (Typeable a, Typeable k) => Magic a -> DataType
toConstr :: Magic a -> Constr
$ctoConstr :: forall k (a :: k). (Typeable a, Typeable k) => Magic a -> Constr
gunfold :: forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
$cgunfold :: forall k (a :: k) (c :: * -> *).
(Typeable a, Typeable k) =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (Magic a)
gfoldl :: forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> Magic a -> c (Magic a)
$cgfoldl :: forall k (a :: k) (c :: * -> *).
(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)
Data, Int -> Magic a -> ShowS
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
showList :: [Magic a] -> ShowS
$cshowList :: forall k (a :: k). [Magic a] -> ShowS
show :: Magic a -> String
$cshow :: forall k (a :: k). Magic a -> String
showsPrec :: Int -> Magic a -> ShowS
$cshowsPrec :: forall k (a :: k). Int -> Magic a -> ShowS
Show, Magic a -> Magic a -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
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
$c== :: forall k (a :: k). Magic a -> Magic a -> Bool
Eq)
instance Weaken (Magic a) where
type Weak (Magic a) = ()
weaken :: Magic a -> Weak (Magic a)
weaken Magic a
_ = ()
instance Strengthen (Magic a) where
strengthen :: Weak (Magic a) -> Validation (NonEmpty StrengthenFail) (Magic a)
strengthen Weak (Magic a)
_ = forall (f :: * -> *) a. Applicative f => a -> f a
pure forall k (a :: k). Magic a
Magic
instance (KnownNat (Length (MagicBytes a))) => BLen (Magic a) where
type CBLen (Magic a) = Length (MagicBytes a)
instance (bs ~ MagicBytes a, ReifyBytes bs) => Put (Magic a) where
put :: Magic a -> Builder
put Magic a
Magic = forall (ns :: [Natural]). ReifyBytes ns => Builder
reifyBytes @bs
instance (bs ~ MagicBytes a, ReifyBytes bs) => Get (Magic a) where
get :: Getter (Magic a)
get = do
let expected :: ByteString
expected = Builder -> ByteString
Mason.toStrictByteString forall a b. (a -> b) -> a -> b
$ forall (ns :: [Natural]). ReifyBytes ns => Builder
reifyBytes @bs
ByteString
actual <- forall e. Int -> Parser e ByteString
FP.takeBs forall a b. (a -> b) -> a -> b
$ ByteString -> Int
B.length ByteString
expected
if ByteString
actual forall a. Eq a => a -> a -> Bool
== ByteString
expected
then forall (m :: * -> *) a. Monad m => a -> m a
return forall k (a :: k). Magic a
Magic
else forall a. EBase -> Getter a
eBase forall a b. (a -> b) -> a -> b
$ ByteString -> ByteString -> EBase
EExpected ByteString
expected ByteString
actual
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