module Binrep.Example.FileTable where

import Binrep
import Refined hiding ( Weaken )
import Refined.Unsafe
import Binrep.Type.Common ( Endianness(..) )
import Binrep.Type.Int
import Binrep.Type.LenPfx
import FlatParse.Basic qualified as FP
import Data.ByteString qualified as B
import Strongweak
import Strongweak.Generic
--import Data.Map ( Map )
import GHC.Generics ( Generic )
import GHC.Exts
import Data.Vector.Sized qualified as V
import Data.Word

type BS = B.ByteString

-- We're unable to put one invariant in the types: an entry can't be placed past
-- the maximum offset. Validating that requires quite a lot of work: we have to
-- do much of the layouting work, which will be repeated for serializing. This
-- is a downside of phase separation, it crops up every now and then.
--
-- The BLen instance will similarly be a bit complex, but it could probably be
-- implemented with similar code to strengthening.
newtype Table s a = Table { forall (s :: Strength) a.
Table s a -> SW s (LenPfx 'I1 'LE (Entry s a))
unTable :: SW s (LenPfx 'I1 'LE (Entry s a)) }

instance (Put a, BLen a) => Put (Table 'Strong a) where put :: Table 'Strong a -> Builder
put = forall a. (Put a, BLen a) => Table 'Strong a -> Builder
putFileTable

putFileTable :: (Put a, BLen a) => Table 'Strong a -> Builder
putFileTable :: forall a. (Put a, BLen a) => Table 'Strong a -> Builder
putFileTable (Table a :: SW 'Strong (LenPfx 'I1 'LE (Entry 'Strong a))
a@(LenPfx Vector n (Entry 'Strong a)
es)) =
    let es' :: Vector n (Int, Word8 -> Builder, BS)
es' = forall a b (n :: Nat). (a -> b) -> Vector n a -> Vector n b
V.map forall a.
(Put a, BLen a) =>
Entry 'Strong a -> (Int, Word8 -> Builder, BS)
prepEntry Vector n (Entry 'Strong a)
es
        osBase :: Int
osBase = forall a (n :: Nat). Num a => Vector n a -> a
V.sum forall a b. (a -> b) -> a -> b
$ forall a b (n :: Nat). (a -> b) -> Vector n a -> Vector n b
V.map (\(Int
l, Word8 -> Builder
_, BS
_) -> Int
l) Vector n (Int, Word8 -> Builder, BS)
es'
    in  case forall a b (n :: Nat). (a -> b -> a) -> a -> Vector n b -> a
V.foldl (Word8, Builder, Builder)
-> (Int, Word8 -> Builder, BS) -> (Word8, Builder, Builder)
go ((forall a b. (Integral a, Num b) => a -> b
fromIntegral Int
osBase) forall a. Num a => a -> a -> a
- Word8
1, forall a. Monoid a => a
mempty, forall a. Monoid a => a
mempty) Vector n (Int, Word8 -> Builder, BS)
es' of
          (Word8
_, Builder
bh, Builder
bd) -> forall a. Put a => a -> Builder
put (forall (size :: ISize) (end :: Endianness) a.
Num (IRep 'U size) =>
LenPfx size end a -> I 'U size end
lenPfxSize SW 'Strong (LenPfx 'I1 'LE (Entry 'Strong a))
a) forall a. Semigroup a => a -> a -> a
<> Builder
bh forall a. Semigroup a => a -> a -> a
<> Builder
bd
  where
    go :: (Word8, Builder, Builder) -> (BLenT, Word8 -> Builder, BS) -> (Word8, Builder, Builder)
    go :: (Word8, Builder, Builder)
-> (Int, Word8 -> Builder, BS) -> (Word8, Builder, Builder)
go (Word8
os, Builder
bh, Builder
bd) (Int
_, Word8 -> Builder
eh, BS
ed) = (Word8
osforall a. Num a => a -> a -> a
+forall a b. (Integral a, Num b) => a -> b
fromIntegral (BS -> Int
B.length BS
ed), Builder
bhforall a. Semigroup a => a -> a -> a
<>Word8 -> Builder
eh Word8
os, Builder
bdforall a. Semigroup a => a -> a -> a
<>forall a. Put a => a -> Builder
put BS
ed)

prepEntry :: (Put a, BLen a) => Entry 'Strong a -> (BLenT, Word8 -> Builder, BS)
prepEntry :: forall a.
(Put a, BLen a) =>
Entry 'Strong a -> (Int, Word8 -> Builder, BS)
prepEntry (Entry a
nm SW 'Strong (Refined (SizeLessThan (IMax 'U 'I1)) BS)
bs) = (Int
l, Word8 -> Builder
b, BS
bs')
  where
    bs' :: BS
bs' = forall {k} (p :: k) x. Refined p x -> x
unrefine SW 'Strong (Refined (SizeLessThan (IMax 'U 'I1)) BS)
bs
    b :: Word8 -> Builder
b Word8
os =
        forall a. Put a => a -> Builder
put a
nm forall a. Semigroup a => a -> a -> a
<> forall a. Put a => a -> Builder
put Word8
os forall a. Semigroup a => a -> a -> a
<> forall a. Put a => a -> Builder
put (forall a b. (Integral a, Num b) => a -> b
fromIntegral (BS -> Int
B.length BS
bs') :: Word8)
    l :: Int
l = forall a. BLen a => a -> Int
blen a
nm forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ Int
1 forall a. Num a => a -> a -> a
+ forall a. BLen a => a -> Int
blen BS
bs'

instance Get a => Get (Table 'Strong a) where get :: Getter (Table 'Strong a)
get = forall a. Get a => Getter (Table 'Strong a)
getFileTable

getFileTable :: Get a => Getter (Table 'Strong a)
getFileTable :: forall a. Get a => Getter (Table 'Strong a)
getFileTable = forall e a. (Addr# -> Parser e a) -> Parser e a
FP.withAddr# forall a b. (a -> b) -> a -> b
$ \Addr#
addr# -> forall (s :: Strength) a.
SW s (LenPfx 'I1 'LE (Entry s a)) -> Table s a
Table forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall (size :: ISize) (end :: Endianness) a itype irep.
(itype ~ I 'U size end, irep ~ IRep 'U size, Get itype,
 Integral irep, KnownNat (MaxBound irep)) =>
Getter a -> Getter (LenPfx size end a)
getLenPfx (forall r a. GetWith r a => r -> Getter a
getWith Addr#
addr#)

{-
This is certainly a weird type.

  * Can use regular strongweak generics
  * Has no 'Get' instance
  * Has a 'GetWith Addr#' instance
  * Has no 'Put' instance
  * Has no 'PutWith' instance

You can't serialize an 'Entry' by itself, because it serializes to two
artifacts, a header entry and the associated data. Now I see why Kaitai Struct
was having trouble with serializing this sort of type.
-}
data Entry s a = Entry
  { forall (s :: Strength) a. Entry s a -> a
entryName :: a
  , forall (s :: Strength) a.
Entry s a -> SW s (Refined (SizeLessThan (IMax 'U 'I1)) BS)
entryData :: SW s (Refined (SizeLessThan (IMax 'U 'I1)) BS)
  } deriving stock (forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (s :: Strength) a x. Rep (Entry s a) x -> Entry s a
forall (s :: Strength) a x. Entry s a -> Rep (Entry s a) x
$cto :: forall (s :: Strength) a x. Rep (Entry s a) x -> Entry s a
$cfrom :: forall (s :: Strength) a x. Entry s a -> Rep (Entry s a) x
Generic)
deriving stock instance Show a => Show (Entry 'Weak   a)
deriving stock instance Eq   a => Eq   (Entry 'Weak   a)
deriving stock instance Show a => Show (Entry 'Strong a)
deriving stock instance Eq   a => Eq   (Entry 'Strong a)
instance Weaken (Entry 'Strong a) where
    type Weak (Entry 'Strong a) = Entry 'Weak a
    weaken :: Entry 'Strong a -> Weak (Entry 'Strong a)
weaken = forall s w.
(Generic s, Generic w, GWeaken (Rep s) (Rep w)) =>
s -> w
weakenGeneric
instance Strengthen (Entry 'Strong a) where
    strengthen :: Weak (Entry 'Strong a)
-> Validation (NonEmpty StrengthenFail) (Entry 'Strong a)
strengthen = forall w s.
(Generic w, Generic s, GStrengthenD (Rep w) (Rep s)) =>
w -> Validation (NonEmpty StrengthenFail) s
strengthenGeneric

instance Get a => GetWith Addr# (Entry 'Strong a) where getWith :: Addr# -> Getter (Entry 'Strong a)
getWith = forall a. Get a => Addr# -> Getter (Entry 'Strong a)
getEntry

getEntry :: Get a => Addr# -> Getter (Entry 'Strong a)
getEntry :: forall a. Get a => Addr# -> Getter (Entry 'Strong a)
getEntry Addr#
addr# = do
    a
name <- forall a. Get a => Getter a
get
    BS
dat  <- forall e a. (Word8'# -> Parser e a) -> Parser e a
FP.withAnyWord8# forall a b. (a -> b) -> a -> b
$ \Word8'#
offset# -> forall e a. (Word8'# -> Parser e a) -> Parser e a
FP.withAnyWord8# forall a b. (a -> b) -> a -> b
$ \Word8'#
len# ->
        forall e. Addr# -> Int# -> Int# -> Parser e BS
FP.takeBsOffAddr# Addr#
addr# (Word8'# -> Int#
w8i# Word8'#
offset#) (Word8'# -> Int#
w8i# Word8'#
len#)
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall (s :: Strength) a.
a -> SW s (Refined (SizeLessThan (IMax 'U 'I1)) BS) -> Entry s a
Entry a
name (forall {k} x (p :: k). x -> Refined p x
reallyUnsafeRefine BS
dat)

w8i# :: Word8# -> Int#
w8i# :: Word8'# -> Int#
w8i# Word8'#
w# = Word# -> Int#
word2Int# (Word8'# -> Word#
word8ToWord# Word8'#
w#)

exBs :: BS
exBs :: BS
exBs = [Word8] -> BS
B.pack
  [ Word8
0x02
  , Word8
0x30, Word8
0x31, Word8
0x32, Word8
0x00
  , Word8
12 -- <- offset!!
  , Word8
0x01
  , Word8
0x39, Word8
0x38, Word8
0x00
  , Word8
13
  , Word8
0x01
  , Word8
0xFF
  , Word8
0xF0
  ]