{-# LANGUAGE UndecidableInstances #-} -- for weirder type families

{- | Magic numbers (also just magic): short constant bytestrings usually
     found at the top of a file, often used as an early sanity check.

There are two main flavors of magics:

  * "random" bytes e.g. Zstandard: @28 B5 2F FD@
  * printable ASCII bytes e.g. Ogg: @4F 67 67 53@ -> OggS

For bytewise magics, use type-level 'Natural' lists.
For ASCII magics, use 'Symbol's (type-level strings).

Previously, I squashed these into a representationally-safe type. Now the check
only occurs during reification. So you are able to define invalid magics now
(bytes over 255, non-ASCII characters), and potentially use them, but you'll get
a clear type error like "no instance for ByteVal 256" when attempting to reify.

String magics are restricted to ASCII, and will type error during reification
otherwise. If you really want UTF-8, please read 'Binrep.Type.Magic.UTF8'.
-}

module Binrep.Type.Magic where

import Binrep
import FlatParse.Basic qualified as FP
import Util.TypeNats ( natValInt )

import GHC.TypeLits

import GHC.Generics ( Generic )
import Data.Data ( Data )

import Strongweak

import Bytezap.Struct.TypeLits.Bytes ( ReifyBytesW64(reifyBytesW64) )
import Bytezap.Parser.Struct.TypeLits.Bytes
  ( ParseReifyBytesW64(parseReifyBytesW64) )
import Bytezap.Parser.Struct qualified as BZ
import Data.ByteString.Internal qualified as B
import GHC.Exts ( Int(I#), plusAddr#, Ptr(Ptr) )
import Foreign.Marshal.Utils ( copyBytes )

-- | A singleton data type representing a "magic number" via a phantom type.
--
-- The phantom type variable unambiguously defines a constant bytestring.
-- A handful of types are supported for using magics conveniently, e.g. for pure
-- ASCII magics, you may use a 'Symbol' type-level string.
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)

-- | Weaken a @'Magic' a@ to the unit.
instance Weaken (Magic a) where
    type Weak (Magic a) = ()
    weaken :: Magic a -> Weak (Magic a)
weaken Magic a
Magic = ()

-- | Strengthen the unit to some @'Magic' a@.
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

-- | The byte length of a magic is known at compile time.
instance IsCBLen (Magic a) where type CBLen (Magic a) = Length (MagicBytes a)

-- | The byte length of a magic is obtained via reifying.
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]) s. ReifyBytesW64 ns => Poke s
reifyBytesW64 @bs

deriving via (ViaPutC (Magic a)) instance
  (bs ~ MagicBytes a, ReifyBytesW64 bs, KnownNat (Length bs)) => Put (Magic a)

{- this works, but is ugly.
* we have to duplicate our error wrapping because errors use parser internals
* we throw the magic into the error, so we need the serializer constraints too
I mean, it's fine. It's correct. It's as fast as possible. But it looks bad :<
-}
instance
  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs
  , ReifyBytesW64 bs, KnownNat (Length bs)
  ) => GetC (Magic a) where
    getC :: GetterC (Magic a)
getC = ParserT# PureMode E (Magic a) -> GetterC (Magic a)
forall (st :: ZeroBitType) e a. ParserT# st e a -> ParserT st e a
BZ.ParserT (ParserT# PureMode E (Magic a) -> GetterC (Magic a))
-> ParserT# PureMode E (Magic a) -> GetterC (Magic a)
forall a b. (a -> b) -> a -> b
$ \ForeignPtrContents
fpc Addr#
base Int#
os# PureMode
st0 ->
        case ParserT PureMode E () -> ParserT# PureMode E ()
forall (st :: ZeroBitType) e a. ParserT st e a -> ParserT# st e a
BZ.runParserT# (forall (ns :: [Natural]) (st :: ZeroBitType) e.
ParseReifyBytesW64 ns =>
ParserT st e ()
parseReifyBytesW64 @bs) ForeignPtrContents
fpc Addr#
base Int#
os# PureMode
st0 of
          BZ.OK#   PureMode
st1 () -> PureMode -> Magic a -> Res# PureMode E (Magic a)
forall (st :: ZeroBitType) a e. st -> a -> Res# st e a
BZ.OK#  PureMode
st1 Magic a
forall k (a :: k). Magic a
Magic
          BZ.Fail# PureMode
st1    ->
            let bsActual :: ByteString
bsActual = Int -> (Ptr Word8 -> IO ()) -> ByteString
B.unsafeCreate Int
len (\Ptr Word8
buf -> Ptr Word8 -> Ptr Word8 -> Int -> IO ()
forall a. Ptr a -> Ptr a -> Int -> IO ()
copyBytes Ptr Word8
buf (Addr# -> Ptr Word8
forall a. Addr# -> Ptr a
Ptr (Addr#
base Addr# -> Int# -> Addr#
`plusAddr#` Int#
os#)) Int
len)
                eb :: EBase
eb = ByteString -> ByteString -> EBase
EExpected ByteString
bsExpected ByteString
bsActual
            in  PureMode -> E -> Res# PureMode E (Magic a)
forall (st :: ZeroBitType) e a. st -> e -> Res# st e a
BZ.Err# PureMode
st1 (Int -> EMiddle -> E
E (Int# -> Int
I# Int#
os#) (EMiddle -> E) -> EMiddle -> E
forall a b. (a -> b) -> a -> b
$ EBase -> EMiddle
EBase EBase
eb)
          BZ.Err#  PureMode
st1 E
e  ->
            let bsActual :: ByteString
bsActual = Int -> (Ptr Word8 -> IO ()) -> ByteString
B.unsafeCreate Int
len (\Ptr Word8
buf -> Ptr Word8 -> Ptr Word8 -> Int -> IO ()
forall a. Ptr a -> Ptr a -> Int -> IO ()
copyBytes Ptr Word8
buf (Addr# -> Ptr Word8
forall a. Addr# -> Ptr a
Ptr (Addr#
base Addr# -> Int# -> Addr#
`plusAddr#` Int#
os#)) Int
len)
                eb :: EBase
eb = ByteString -> ByteString -> EBase
EExpected ByteString
bsExpected ByteString
bsActual
            in  PureMode -> E -> Res# PureMode E (Magic a)
forall (st :: ZeroBitType) e a. st -> e -> Res# st e a
BZ.Err# PureMode
st1 (Int -> EMiddle -> E
E (Int# -> Int
I# Int#
os#) (EMiddle -> E) -> EMiddle -> E
forall a b. (a -> b) -> a -> b
$ E -> EBase -> EMiddle
EAnd E
e EBase
eb)
      where
        len :: Int
len = forall (n :: Natural). KnownNat n => Int
natValInt @(Length bs)
        bsExpected :: ByteString
bsExpected = Magic a -> ByteString
forall a. (PutC a, KnownNat (CBLen a)) => a -> ByteString
runPutC (Magic a
forall k (a :: k). Magic a
Magic :: Magic a)

deriving via ViaGetC (Magic a) instance
  ( bs ~ MagicBytes a, ParseReifyBytesW64 bs
  , ReifyBytesW64 bs, KnownNat (Length bs)
  ) => Get (Magic a)

-- TODO might wanna move this
-- | The length of a type-level list.
type family Length (a :: [k]) :: Natural where
    Length '[]       = 0
    Length (a ': as) = 1 + Length as

{-
I do lots of functions on lists, because they're structurally simple. But you
can't pass type-level functions as arguments between type families. singletons
solves a related (?) problem using defunctionalization, where you manually write
out the function applications or something. Essentially, you can't do this:

    type family Map (f :: x -> y) (a :: [x]) :: [y] where
        Map _ '[]       = '[]
        Map f (a ': as) = f a ': Map f as

So you have to write that out for every concrete function over lists.

TODO wellll we depend on defun-core now so may as well use that LOL
-}

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)

--------------------------------------------------------------------------------

-- | Types which define a magic value.
class Magical (a :: k) where
    -- | How to turn the type into a list of bytes.
    type MagicBytes a :: [Natural]

-- | Type-level naturals go as-is. (Make sure you don't go over 255, though!)
instance Magical (ns :: [Natural]) where type MagicBytes ns = ns

-- | Type-level symbols are turned into their Unicode codepoints - but
--   multibyte characters aren't handled, so they'll simply be overlarge bytes,
--   which will fail further down.
instance Magical (sym :: Symbol) where
    type MagicBytes sym = SymbolUnicodeCodepoints sym