{-# LANGUAGE UndecidableInstances #-} -- for tons of stuff
{-# LANGUAGE PatternSynonyms #-} -- TODO wip
{-# LANGUAGE OverloadedStrings #-} -- for easy error building

{- | 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:

  * byte magics e.g. Zstandard: @28 B5 2F FD@
  * printable magics e.g. Ogg: @4F 67 67 53@ -> @OggS@ (in ASCII)

For byte magics, use type-level 'Natural' lists e.g. @'Magic' \@'[0xFF, 0x01]@
For printable (UTF-8) magics, use 'Symbol's e.g. @'Magic' \@"hello"@.
-}

module Binrep.Type.Magic
  ( Magic(Magic)
  , Magical(type MagicBytes)
  , type Length
  ) where

import Data.Type.Symbol.Utf8 ( type SymbolToUtf8 )

import GHC.TypeLits ( type Natural, type Symbol, type KnownNat, type (+) )

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

import Binrep
import Bytezap.Struct.TypeLits.Bytes ( ReifyBytesW64(reifyBytesW64) )
import Bytezap.Parser.Struct.TypeLits.Bytes
  ( ParseReifyBytesW64(parseReifyBytesW64) )
import Bytezap.Parser.Struct qualified as BZ
import GHC.Exts ( Int(I#) )
import FlatParse.Basic qualified as FP
import Data.Text.Builder.Linear qualified as TBL

{- | A unit data type representing a "magic number" via a phantom type.

The phantom type unambiguously defines a bytestring at compile time. This
depends on the type's kind. See 'MagicBytes' for details.

This is defined using GADT syntax to permit labelling the phantom type kind as
/inferred/, which effectively means hidden (not available for visible type
applications). That kind is always evident from the type, so it's just nicer.
-}
data Magic a where Magic :: forall {k} (a :: k). Magic a
    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)

-- | The byte length of a magic is known at compile time.
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)

-- | Efficiently serialize a @'Magic' a@.
instance (bs ~ MagicBytes a, ReifyBytesW64 bs) => PutC (Magic a) where
    putC :: Magic a -> PutterC
putC Magic a
Magic = forall (bs :: [Natural]) s. ReifyBytesW64 bs => Poke s
reifyBytesW64 @bs

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

-- | Efficiently parse a @'Magic' a@. Serialization constraints are included as
--   we emit the expected bytestring in errors.
instance (bs ~ MagicBytes a, ParseReifyBytesW64 0 bs) => GetC (Magic a) where
    getC :: GetterC (Magic a)
getC = ParserT# PureMode (ParseError Int Builder) (Magic a)
-> GetterC (Magic a)
forall (st :: ZeroBitType) e a. ParserT# st e a -> ParserT st e a
BZ.ParserT (ParserT# PureMode (ParseError Int Builder) (Magic a)
 -> GetterC (Magic a))
-> ParserT# PureMode (ParseError Int Builder) (Magic a)
-> GetterC (Magic a)
forall a b. (a -> b) -> a -> b
$ \ForeignPtrContents
fpc Addr#
base# Int#
os# PureMode
st0 ->
        case ParserT PureMode (Int, Word8) ()
-> ParserT# PureMode (Int, Word8) ()
forall (st :: ZeroBitType) e a. ParserT st e a -> ParserT# st e a
BZ.runParserT# (forall (idx :: Natural) (bs :: [Natural]) (st :: ZeroBitType).
ParseReifyBytesW64 idx bs =>
ParserT st (Int, Word8) ()
parseReifyBytesW64 @0 @bs) ForeignPtrContents
fpc Addr#
base# Int#
os# PureMode
st0 of
          BZ.OK#   PureMode
st1 ()             -> PureMode
-> Magic a -> Res# PureMode (ParseError Int Builder) (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.Err#  PureMode
st1 (Int
pos, Word8
bActual) -> PureMode
-> ParseError Int Builder
-> Res# PureMode (ParseError Int Builder) (Magic a)
forall (st :: ZeroBitType) e a. st -> e -> Res# st e a
BZ.Err#  PureMode
st1 ([Builder] -> Int -> ParseError Int Builder
forall text pos. [text] -> pos -> ParseError pos text
parseError1
            [Builder
"TODO magic parse error: "Builder -> Builder -> Builder
forall a. Semigroup a => a -> a -> a
<>Word8 -> Builder
forall a. (Integral a, FiniteBits a) => a -> Builder
TBL.fromDec Word8
bActual]
            (Int
pos Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int# -> Int
I# Int#
os#))
          BZ.Fail# PureMode
st1                -> PureMode -> Res# PureMode (ParseError Int Builder) (Magic a)
forall (st :: ZeroBitType) e a. st -> Res# st e a
BZ.Fail# PureMode
st1 -- shouldn't occur

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

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

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

-- | Type-level symbols are converted to UTF-8.
instance Magical (sym :: Symbol) where type MagicBytes sym = SymbolToUtf8 sym

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