{-# 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.Copy (

	-- * COPY

	Copy(..),

	-- ** CopyListToMiddle

	CopyListToMiddle(..),

	-- ** BindingAndArrayElem

	BindingAndArrayElem,

	-- ** BindingLength

	BindingLength

	) where

import Data.TypeLevel.List qualified as TList
import Gpu.Vulkan.DescriptorSet.BindingAndArrayElem
import Gpu.Vulkan.DescriptorSet.BindingAndArrayElem.Buffer

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

import Gpu.Vulkan.DescriptorSet.Type

import qualified Gpu.Vulkan.DescriptorSetLayout.Type as Lyt
import qualified Gpu.Vulkan.DescriptorSet.Middle as M

-- * COPY

data Copy mn sdss slbtss (is :: Nat) sdsd slbtsd (id :: Nat)
	(lbts :: Lyt.BindingType) = Copy {
	forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> M mn
copyNext :: TMaybe.M mn,
	forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> D sdss slbtss
copySrcSet :: D sdss slbtss, forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> D sdsd slbtsd
copyDstSet :: D sdsd slbtsd }

-- ** CopyListToMiddle

class M.CopyListToCore (TMapIndex.M0_8 cargs) =>
	CopyListToMiddle cargs where
	copyListToMiddle ::
		HeteroParList.PL (U8 Copy) cargs ->
		HeteroParList.PL M.Copy (TMapIndex.M0_8 cargs)

instance CopyListToMiddle '[] where
	copyListToMiddle :: PL (U8 Copy) '[] -> PL Copy (M0_8 '[])
copyListToMiddle PL (U8 Copy) '[]
HeteroParList.Nil = PL Copy '[]
PL Copy (M0_8 '[])
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance (
	WithPoked (TMaybe.M mn),
	BindingAndArrayElem (TIndex.I1_2 slbtss) lbts is,
	BindingAndArrayElem (TIndex.I1_2 slbtsd) lbts id,
	BindingLength lbts, CopyListToMiddle cargs ) =>
	CopyListToMiddle (
		'(mn, sdss, slbtss, is, sdsd, slbtsd, id, lbts) ': cargs) where
	copyListToMiddle :: PL
  (U8 Copy) ('(mn, sdss, slbtss, is, sdsd, slbtsd, id, lbts) : cargs)
-> PL
     Copy
     (M0_8 ('(mn, sdss, slbtss, is, sdsd, slbtsd, id, lbts) : cargs))
copyListToMiddle (U8 Copy s1 s2 s3 s4 s5 s6 s7 s8
c :** PL (U8 Copy) ss1
cs) = Copy s1 s2 s3 s4 s5 s6 s7 s8 -> Copy s1
forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
(BindingAndArrayElem (I1_2 slbtss) lbts is,
 BindingAndArrayElem (I1_2 slbtsd) lbts id, BindingLength lbts) =>
Copy mn sdss slbtss is sdsd slbtsd id lbts -> Copy mn
copyToMiddle Copy s1 s2 s3 s4 s5 s6 s7 s8
c Copy s1 -> PL Copy (M0_8 cargs) -> PL Copy (s1 : M0_8 cargs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (U8 Copy) ss1 -> PL Copy (M0_8 ss1)
forall (cargs :: [(Maybe (*), *, (*, [BindingType]), Nat, *,
                   (*, [BindingType]), Nat, BindingType)]).
CopyListToMiddle cargs =>
PL (U8 Copy) cargs -> PL Copy (M0_8 cargs)
copyListToMiddle PL (U8 Copy) ss1
cs

copyToMiddle :: forall mn sdss slbtss is sdsd slbtsd id lbts . (
	BindingAndArrayElem (TIndex.I1_2 slbtss) lbts is,
	BindingAndArrayElem (TIndex.I1_2 slbtsd) lbts id, BindingLength lbts ) =>
	Copy mn sdss slbtss is sdsd slbtsd id lbts -> M.Copy mn
copyToMiddle :: forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
(BindingAndArrayElem (I1_2 slbtss) lbts is,
 BindingAndArrayElem (I1_2 slbtsd) lbts id, BindingLength lbts) =>
Copy mn sdss slbtss is sdsd slbtsd id lbts -> Copy mn
copyToMiddle Copy {
	copyNext :: forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> M mn
copyNext = M mn
mnxt, copySrcSet :: forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> D sdss slbtss
copySrcSet = D IORef
  (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbtss)))
_ D
ss, copyDstSet :: forall (mn :: Maybe (*)) sdss (slbtss :: (*, [BindingType]))
       (is :: Nat) sdsd (slbtsd :: (*, [BindingType])) (id :: Nat)
       (lbts :: BindingType).
Copy mn sdss slbtss is sdsd slbtsd id lbts -> D sdsd slbtsd
copyDstSet = D IORef
  (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbtsd)))
_ D
sd } = let
	(Word32
bs, Word32
aes) = forall (lbts :: [BindingType]) (lbt :: BindingType) (i :: Nat) n.
(BindingAndArrayElem lbts lbt i, Integral n) =>
(n, n)
bindingAndArrayElem @(TIndex.I1_2 slbtss) @lbts @is
	(Word32
bd, Word32
aed) = forall (lbts :: [BindingType]) (lbt :: BindingType) (i :: Nat) n.
(BindingAndArrayElem lbts lbt i, Integral n) =>
(n, n)
bindingAndArrayElem @(TIndex.I1_2 slbtsd) @lbts @id
	cnt :: Word32
cnt = forall (bt :: BindingType) n. (BindingLength bt, Integral n) => n
bindingLength @lbts in
	M.Copy {
		copyNext :: M mn
M.copyNext = M mn
mnxt,
		copySrcSet :: D
M.copySrcSet = D
ss,
		copySrcBinding :: Word32
M.copySrcBinding = Word32
bs, copySrcArrayElement :: Word32
M.copySrcArrayElement = Word32
aes,
		copyDstSet :: D
M.copyDstSet = D
sd,
		copyDstBinding :: Word32
M.copyDstBinding = Word32
bd, copyDstArrayElement :: Word32
M.copyDstArrayElement = Word32
aed,
		copyDescriptorCount :: Word32
M.copyDescriptorCount = Word32
cnt }

-- ** BindingAndArrayElem

class BindingAndArrayElem
	(lbts :: [Lyt.BindingType])
	(lbt :: Lyt.BindingType) (i :: Nat) where
	bindingAndArrayElem :: Integral n => (n, n)

instance BindingAndArrayElemBuffer lbts objs i =>
	BindingAndArrayElem lbts (Lyt.Buffer objs) i where
	bindingAndArrayElem :: forall n. Integral n => (n, n)
bindingAndArrayElem = forall (lbts :: [BindingType]) (objs :: [O]) (i :: Nat) n.
(BindingAndArrayElemBuffer lbts objs i, Integral n) =>
n -> n -> (n, n)
bindingAndArrayElemBuffer @lbts @objs @i n
0 n
0

instance BindingAndArrayElemImage lbts iargs i =>
	BindingAndArrayElem lbts (Lyt.Image iargs) i where
	bindingAndArrayElem :: forall n. Integral n => (n, n)
bindingAndArrayElem = forall (lbts :: [BindingType]) (iargs :: [(Symbol, Format)])
       (i :: Nat) n.
(BindingAndArrayElemImage lbts iargs i, Integral n) =>
n -> n -> (n, n)
bindingAndArrayElemImage @lbts @iargs @i n
0 n
0

instance BindingAndArrayElemImageWithImmutableSampler lbts (TMapIndex.M0'1_3 iargs) i =>
	BindingAndArrayElem lbts (Lyt.ImageSampler iargs) i where
	bindingAndArrayElem :: forall n. Integral n => (n, n)
bindingAndArrayElem =
		forall (lbts :: [BindingType]) (iargs :: [(Symbol, Format)])
       (i :: Nat) n.
(BindingAndArrayElemImageWithImmutableSampler lbts iargs i,
 Integral n) =>
n -> n -> (n, n)
bindingAndArrayElemImageWithImmutableSampler @lbts @(TMapIndex.M0'1_3 iargs) @i n
0 n
0

instance BindingAndArrayElemBufferView lbts bvargs i =>
	BindingAndArrayElem lbts (Lyt.BufferView bvargs) i where
	bindingAndArrayElem :: forall n. Integral n => (n, n)
bindingAndArrayElem = forall (bt :: [BindingType]) (bvargs :: [(Symbol, *)]) (i :: Nat)
       n.
(BindingAndArrayElemBufferView bt bvargs i, Integral n) =>
n -> n -> (n, n)
bindingAndArrayElemBufferView @lbts @bvargs @i n
0 n
0

-- ** BindingLength

class BindingLength (bt :: Lyt.BindingType) where
	bindingLength :: Integral n => n

instance TList.Length objs => BindingLength (Lyt.Buffer objs) where
	bindingLength :: forall n. Integral n => n
bindingLength = forall k (as :: [k]) n. (Length as, Integral n) => n
TList.length @_ @objs

instance TList.Length iargs => BindingLength (Lyt.Image iargs) where
	bindingLength :: forall n. Integral n => n
bindingLength = forall k (as :: [k]) n. (Length as, Integral n) => n
TList.length @_ @iargs

instance TList.Length bvargs => BindingLength (Lyt.BufferView bvargs) where
	bindingLength :: forall n. Integral n => n
bindingLength = forall k (as :: [k]) n. (Length as, Integral n) => n
TList.length @_ @bvargs

instance TList.Length isargs => BindingLength (Lyt.ImageSampler isargs) where
	bindingLength :: forall n. Integral n => n
bindingLength = forall k (as :: [k]) n. (Length as, Integral n) => n
TList.length @_ @isargs