{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE ScopedTypeVariables, RankNTypes, TypeApplications #-}
{-# LANGUAGE GADTs, TypeFamilies #-}
{-# LANGUAGE DataKinds, ConstraintKinds #-}
{-# LANGUAGE KindSignatures, TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses, AllowAmbiguousTypes #-}
{-# LANGUAGE FlexibleContexts, FlexibleInstances, UndecidableInstances #-}
{-# LANGUAGE PatternSynonyms, ViewPatterns #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# OPTIONS_GHC -Wall -fno-warn-tabs #-}

module Gpu.Vulkan.DescriptorSet.Write (

	-- * WRITE

	-- ** Types

	Write(..), WriteSources(..), WriteSourcesArg(..),

	-- ** WriteListToMiddle

	WriteListToMiddle(..), WriteSourcesToMiddle,
	BindingAndArrayElemImage, BindingAndArrayElemImageWithImmutableSampler,
	BindingAndArrayElemBuffer, BindingAndArrayElemBufferView,

	-- ** WriteListUpdateDynamicLengths

	WriteListUpdateDynamicLengths(..),
	WriteSourcesUpdateDynamicLengths, UpdateDynamicLength

	) where

import GHC.TypeLits
import Foreign.Storable.PeekPoke
import Data.TypeLevel.Tuple.Index qualified as TIndex
import Data.TypeLevel.Tuple.MapIndex qualified as TMapIndex
import Data.TypeLevel.Maybe qualified as TMaybe
import Data.TypeLevel.Tuple.Uncurry
import qualified Data.HeteroParList as HeteroParList
import Data.HeteroParList (pattern (:**))

import Gpu.Vulkan.DescriptorSet.Type

import qualified Gpu.Vulkan.Descriptor.Enum as Descriptor
import qualified Gpu.Vulkan.DescriptorSet.Middle as M

import Gpu.Vulkan.DescriptorSet.Write.Sources

-- * WRITE

data Write mn sds slbts wsarg (i :: Nat) = Write {
	forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> M mn
writeNext :: TMaybe.M mn,
	forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> D sds slbts
writeDstSet :: D sds slbts,
	forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> Type
writeDescriptorType :: Descriptor.Type,
	forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> WriteSources wsarg
writeSources :: WriteSources wsarg }

-- ** WriteListToMiddle

class M.WriteListToCore (TMapIndex.M0_5 wargs) => WriteListToMiddle wargs where
	writeListToMiddle ::
		HeteroParList.PL (U5 Write) wargs ->
		HeteroParList.PL M.Write (TMapIndex.M0_5 wargs)

instance WriteListToMiddle '[] where
	writeListToMiddle :: PL (U5 Write) '[] -> PL Write (M0_5 '[])
writeListToMiddle PL (U5 Write) '[]
HeteroParList.Nil = PL Write '[]
PL Write (M0_5 '[])
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance (
	WithPoked (TMaybe.M mn),
	WriteSourcesToMiddle (TIndex.I1_2 slbts) wsarg i,
	WriteListToMiddle wargs ) =>
	WriteListToMiddle ('(mn, sds, slbts, wsarg, i) ': wargs) where
	writeListToMiddle :: PL (U5 Write) ('(mn, sds, slbts, wsarg, i) : wargs)
-> PL Write (M0_5 ('(mn, sds, slbts, wsarg, i) : wargs))
writeListToMiddle (U5 Write s1 s2 s3 s4 s5
w :** PL (U5 Write) ss1
ws) =
		Write s1 s2 s3 s4 s5 -> Write s1
forall (mn :: Maybe (*)) s (slbts :: (*, [BindingType]))
       (wsa :: WriteSourcesArg) (i :: Nat).
WriteSourcesToMiddle (I1_2 slbts) wsa i =>
Write mn s slbts wsa i -> Write mn
writeToMiddle Write s1 s2 s3 s4 s5
w Write s1 -> PL Write (M0_5 wargs) -> PL Write (s1 : M0_5 wargs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (U5 Write) ss1 -> PL Write (M0_5 ss1)
forall (wargs :: [(Maybe (*), *, (*, [BindingType]),
                   WriteSourcesArg, Nat)]).
WriteListToMiddle wargs =>
PL (U5 Write) wargs -> PL Write (M0_5 wargs)
writeListToMiddle PL (U5 Write) ss1
ws

writeToMiddle :: forall mn s slbts wsa i .
	WriteSourcesToMiddle (TIndex.I1_2 slbts) wsa i =>
	Write mn s slbts wsa i -> M.Write mn
writeToMiddle :: forall (mn :: Maybe (*)) s (slbts :: (*, [BindingType]))
       (wsa :: WriteSourcesArg) (i :: Nat).
WriteSourcesToMiddle (I1_2 slbts) wsa i =>
Write mn s slbts wsa i -> Write mn
writeToMiddle Write {
	writeNext :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> M mn
writeNext = M mn
mnxt,
	writeDstSet :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> D sds slbts
writeDstSet = D IORef (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts)))
_ D
ds,
	writeDescriptorType :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> Type
writeDescriptorType = Type
dt,
	writeSources :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> WriteSources wsarg
writeSources = WriteSources wsa
srcs } = M.Write {
		writeNext :: M mn
M.writeNext = M mn
mnxt,
		writeDstSet :: D
M.writeDstSet = D
ds,
		writeDstBinding :: Word32
M.writeDstBinding = Word32
bdg, writeDstArrayElement :: Word32
M.writeDstArrayElement = Word32
ae,
		writeDescriptorType :: Type
M.writeDescriptorType = Type
dt,
		writeSources :: WriteSources
M.writeSources = WriteSources
srcs' }
	where ((Word32
bdg, Word32
ae), WriteSources
srcs') =
		forall (lbts :: [BindingType]) (wsarg :: WriteSourcesArg)
       (i :: Nat).
WriteSourcesToMiddle lbts wsarg i =>
WriteSources wsarg -> ((Word32, Word32), WriteSources)
writeSourcesToMiddle @(TIndex.I1_2 slbts) @_ @i WriteSources wsa
srcs

-- ** WriteListUpdateDynamicLengths

class WriteListUpdateDynamicLengths wargs where
	writeListUpdateDynamicLength ::
		HeteroParList.PL (U5 Write) wargs -> IO ()

instance WriteListUpdateDynamicLengths '[] where
	writeListUpdateDynamicLength :: PL (U5 Write) '[] -> IO ()
writeListUpdateDynamicLength PL (U5 Write) '[]
HeteroParList.Nil = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

instance (
	WriteSourcesUpdateDynamicLengths bts wsarg,
	WriteListUpdateDynamicLengths wargs ) =>
	WriteListUpdateDynamicLengths
		('(mn, sds, '(sl, bts), wsarg, i) ': wargs) where
	writeListUpdateDynamicLength :: PL (U5 Write) ('(mn, sds, '(sl, bts), wsarg, i) : wargs) -> IO ()
writeListUpdateDynamicLength (U5 Write s1 s2 s3 s4 s5
w :** PL (U5 Write) ss1
ws) =
		Write s1 s2 '(sl, bts) s4 s5 -> IO ()
forall (bts :: [BindingType]) (wsarg :: WriteSourcesArg)
       (n :: Maybe (*)) s sl (i :: Nat).
WriteSourcesUpdateDynamicLengths bts wsarg =>
Write n s '(sl, bts) wsarg i -> IO ()
writeUpdateDynamicLength Write s1 s2 s3 s4 s5
Write s1 s2 '(sl, bts) s4 s5
w IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> PL (U5 Write) ss1 -> IO ()
forall (wargs :: [(Maybe (*), *, (*, [BindingType]),
                   WriteSourcesArg, Nat)]).
WriteListUpdateDynamicLengths wargs =>
PL (U5 Write) wargs -> IO ()
writeListUpdateDynamicLength PL (U5 Write) ss1
ws

writeUpdateDynamicLength ::
	WriteSourcesUpdateDynamicLengths bts wsarg =>
	Write n s '(sl, bts) wsarg i -> IO ()
writeUpdateDynamicLength :: forall (bts :: [BindingType]) (wsarg :: WriteSourcesArg)
       (n :: Maybe (*)) s sl (i :: Nat).
WriteSourcesUpdateDynamicLengths bts wsarg =>
Write n s '(sl, bts) wsarg i -> IO ()
writeUpdateDynamicLength Write { writeDstSet :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> D sds slbts
writeDstSet = D s '(sl, bts)
ds, writeSources :: forall (mn :: Maybe (*)) sds (slbts :: (*, [BindingType]))
       (wsarg :: WriteSourcesArg) (i :: Nat).
Write mn sds slbts wsarg i -> WriteSources wsarg
writeSources = WriteSources wsarg
ws } =
	D s '(sl, bts) -> WriteSources wsarg -> IO ()
forall (lbts :: [BindingType]) (wsarg :: WriteSourcesArg) sds sl.
WriteSourcesUpdateDynamicLengths lbts wsarg =>
D sds '(sl, lbts) -> WriteSources wsarg -> IO ()
forall sds sl. D sds '(sl, bts) -> WriteSources wsarg -> IO ()
writeSourcesUpdateDynamicLength D s '(sl, bts)
ds WriteSources wsarg
ws