{-# LANGUAGE UndecidableInstances #-}

{- | Magic numbers (also just magic): short constant bytestrings usually
     found at the top of a file, included as a safety check for parsing.

TODO rename: MagicBytes -> MagicVals, and have ByteVal be a "consumer" of
MagicVals where each value must be a byte. (It's conceivable that we have
another consumer which makes each value into a non-empty list of bytes, LE/BE.)

TODO unassociated type fams bad (maybe). turn into class -- and turn the reifier
into a default method! (TODO think about this)

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

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
$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, Typeable (Magic a)
Typeable (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))
-> (forall (c :: * -> *).
    (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 :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (Magic a)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    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 :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> Magic a -> m (Magic a))
-> Data (Magic a)
Magic a -> DataType
Magic a -> Constr
(forall b. Data b => b -> b) -> Magic a -> Magic a
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 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 -> 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 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 :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> Magic a -> m (Magic a)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> Magic a -> m (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)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (Magic a))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (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
[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
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
(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
/= :: 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)

-- | Assumes magic values are individual bytes.
type instance CBLen (Magic a) = Length (MagicVals a)

-- | Assumes magic values are individual bytes.
deriving anyclass instance KnownNat (Length (MagicVals a)) => BLen (Magic a)

-- | Forces magic values to be individual bytes.
instance (bs ~ MagicVals a, ByteVals bs) => Put (Magic a) where
    put :: Magic a -> Builder
put Magic a
Magic = forall (ns :: [Natural]). ByteVals ns => Builder
byteVals @bs

-- | Forces magic values to be individual bytes.
--
-- TODO improve show - maybe hexbytestring goes here? lol
instance (bs ~ MagicVals a, ByteVals bs) => Get (Magic a) where
    get :: Getter (Magic a)
get = do
        let expected :: ByteString
expected = Builder -> ByteString
Mason.toStrictByteString (Builder -> ByteString) -> Builder -> ByteString
forall a b. (a -> b) -> a -> b
$ forall (ns :: [Natural]). ByteVals ns => Builder
byteVals @bs
        ByteString
actual <- Int -> Parser String ByteString
forall e. Int -> Parser e ByteString
FP.takeBs (Int -> Parser String ByteString)
-> Int -> Parser String ByteString
forall a b. (a -> b) -> a -> b
$ ByteString -> Int
B.length ByteString
expected
        if   ByteString
actual ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
expected
        then Magic a -> Getter (Magic a)
forall (m :: * -> *) a. Monad m => a -> m a
return Magic a
forall k (a :: k). Magic a
Magic
        else String -> Getter (Magic a)
forall e a. e -> Parser e a
FP.err (String -> Getter (Magic a)) -> String -> Getter (Magic a)
forall a b. (a -> b) -> a -> b
$ String
"bad magic: expected "String -> ShowS
forall a. Semigroup a => a -> a -> a
<>ByteString -> String
forall a. Show a => a -> String
show ByteString
expectedString -> ShowS
forall a. Semigroup a => a -> a -> a
<>String
", got "String -> ShowS
forall a. Semigroup a => a -> a -> a
<>ByteString -> String
forall a. Show a => a -> String
show ByteString
actual

{-
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.
-}

type family MagicVals (a :: k) :: [Natural]
type instance MagicVals (a :: Symbol)    = SymbolUnicodeCodepoints a
type instance MagicVals (a :: [Natural]) = a

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)