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

module Gpu.Vulkan.Buffer.Internal (

	-- * CREATE

	create, B, CreateInfo(..),

	-- ** Buffer Group

	Group, group, create', unsafeDestroy, lookup,

	-- * BINDED

	getMemoryRequirements, Binded, lengthBinded,
	IndexedForList(..), indexedListToMiddles, indexedListToMiddle,

	-- * COPY

	MakeCopies(..), CopyInfo,

	-- * IMAGE COPY

	ImageCopy(..), ImageCopyListToMiddle(..),

	-- * MEMORY BARRIER

	MemoryBarrier(..), MemoryBarrierListToMiddle(..),
	MemoryBarrier2(..), MemoryBarrier2ListToMiddle(..),

	-- * UNSAFE

	unsafeToBinded
	
	) where

import Prelude hiding (lookup)
import GHC.TypeLits
import Foreign.Storable.PeekPoke
import Control.Exception
import Gpu.Vulkan.Object qualified as VObj
import Data.Kind
import Data.TypeLevel.Tuple.Uncurry
import Data.TypeLevel.Tuple.MapIndex qualified as TMapIndex
import Data.TypeLevel.Maybe qualified as TMaybe
import Data.TypeLevel.ParMaybe qualified as TPMaybe
import Data.HeteroParList qualified as HeteroParList
import Data.HeteroParList (pattern (:**))
import Data.Word

import Gpu.Vulkan.Enum hiding (ObjectType)
import Gpu.Vulkan.Buffer.Enum

import qualified Gpu.Vulkan.Middle as C
import qualified Gpu.Vulkan.AllocationCallbacks as AllocationCallbacks
import qualified Gpu.Vulkan.AllocationCallbacks.Type as AllocationCallbacks
import qualified Gpu.Vulkan.Device.Type as Device
import qualified Gpu.Vulkan.Device.Middle as Device.M
import qualified Gpu.Vulkan.Memory as Memory
import qualified Gpu.Vulkan.Buffer.Middle as M
import qualified Gpu.Vulkan.Buffer.Middle as C
import qualified Gpu.Vulkan.QueueFamily as QueueFamily
import qualified Gpu.Vulkan.Image as Image.M

import Gpu.Vulkan.Buffer.Type

import Control.Concurrent.STM
import Control.Concurrent.STM.TSem
import Data.Map qualified as Map

import qualified Gpu.Vulkan.Pipeline as Pipeline

data CreateInfo mn objs = CreateInfo {
	forall (mn :: Maybe (*)) (objs :: [O]). CreateInfo mn objs -> M mn
createInfoNext :: TMaybe.M mn,
	forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> CreateFlags
createInfoFlags :: CreateFlags,
	forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> PL Length objs
createInfoLengths :: HeteroParList.PL VObj.Length objs,
	forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> UsageFlags
createInfoUsage :: UsageFlags,
	forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> SharingMode
createInfoSharingMode :: SharingMode,
	forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> [Index]
createInfoQueueFamilyIndices :: [QueueFamily.Index] }

deriving instance
	(Show (TMaybe.M n), Show (HeteroParList.PL VObj.Length objs)) =>
	Show (CreateInfo n objs)

createInfoToMiddle :: VObj.SizeAlignmentList objs =>
	CreateInfo n objs -> M.CreateInfo n
createInfoToMiddle :: forall (objs :: [O]) (n :: Maybe (*)).
SizeAlignmentList objs =>
CreateInfo n objs -> CreateInfo n
createInfoToMiddle CreateInfo {
	createInfoNext :: forall (mn :: Maybe (*)) (objs :: [O]). CreateInfo mn objs -> M mn
createInfoNext = M n
mnxt,
	createInfoFlags :: forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> CreateFlags
createInfoFlags = CreateFlags
flgs,
	createInfoLengths :: forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> PL Length objs
createInfoLengths = PL Length objs
lns,
	createInfoUsage :: forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> UsageFlags
createInfoUsage = UsageFlags
usg,
	createInfoSharingMode :: forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> SharingMode
createInfoSharingMode = SharingMode
smd,
	createInfoQueueFamilyIndices :: forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> [Index]
createInfoQueueFamilyIndices = [Index]
qfis } = M.CreateInfo {
	createInfoNext :: M n
M.createInfoNext = M n
mnxt,
	createInfoFlags :: CreateFlags
M.createInfoFlags = CreateFlags
flgs,
	createInfoSize :: Size
M.createInfoSize = PL Length objs -> Size
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> Size
VObj.wholeSize PL Length objs
lns,
	createInfoUsage :: UsageFlags
M.createInfoUsage = UsageFlags
usg,
	createInfoSharingMode :: SharingMode
M.createInfoSharingMode = SharingMode
smd,
	createInfoQueueFamilyIndices :: [Index]
M.createInfoQueueFamilyIndices = [Index]
qfis }

create :: (
	WithPoked (TMaybe.M mn),
	VObj.SizeAlignmentList objs, AllocationCallbacks.ToMiddle ma ) =>
	Device.D sd -> CreateInfo mn objs ->
	TPMaybe.M (U2 AllocationCallbacks.A) ma ->
	(forall sb . B sb nm objs -> IO a) -> IO a
create :: forall (mn :: Maybe (*)) (objs :: [O]) (ma :: Maybe (*, *)) sd
       (nm :: Symbol) a.
(WithPoked (M mn), SizeAlignmentList objs, ToMiddle ma) =>
D sd
-> CreateInfo mn objs
-> M (U2 A) ma
-> (forall sb. B sb nm objs -> IO a)
-> IO a
create (Device.D D
dvc) CreateInfo mn objs
ci (M (U2 A) ma -> M A (Snd ma)
forall (msa :: Maybe (*, *)).
ToMiddle msa =>
M (U2 A) msa -> M A (Snd msa)
AllocationCallbacks.toMiddle -> M A (Snd ma)
mac) forall sb. B sb nm objs -> IO a
f = IO B -> (B -> IO ()) -> (B -> IO a) -> IO a
forall a b c. IO a -> (a -> IO b) -> (a -> IO c) -> IO c
bracket
	(D -> CreateInfo mn -> M A (Snd ma) -> IO B
forall (mn :: Maybe (*)) (mc :: Maybe (*)).
WithPoked (M mn) =>
D -> CreateInfo mn -> M A mc -> IO B
M.create D
dvc (CreateInfo mn objs -> CreateInfo mn
forall (objs :: [O]) (n :: Maybe (*)).
SizeAlignmentList objs =>
CreateInfo n objs -> CreateInfo n
createInfoToMiddle CreateInfo mn objs
ci) M A (Snd ma)
mac) (\B
b -> D -> B -> M A (Snd ma) -> IO ()
forall (md :: Maybe (*)). D -> B -> M A md -> IO ()
M.destroy D
dvc B
b M A (Snd ma)
mac)
	(B Any nm objs -> IO a
forall sb. B sb nm objs -> IO a
f (B Any nm objs -> IO a) -> (B -> B Any nm objs) -> B -> IO a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PL Length objs -> B -> B Any nm objs
forall s (nm :: Symbol) (objs :: [O]).
PL Length objs -> B -> B s nm objs
B (CreateInfo mn objs -> PL Length objs
forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> PL Length objs
createInfoLengths CreateInfo mn objs
ci))

data Group sd ma s k nm objs = Group (Device.D sd)
	(TPMaybe.M (U2 AllocationCallbacks.A) ma)
	TSem (TVar (Map.Map k (B s nm objs)))

group :: AllocationCallbacks.ToMiddle md =>
	Device.D sd -> TPMaybe.M (U2 AllocationCallbacks.A) md ->
	(forall s . Group sd md s k nm objs -> IO a) -> IO a
group :: forall (md :: Maybe (*, *)) sd k (nm :: Symbol) (objs :: [O]) a.
ToMiddle md =>
D sd
-> M (U2 A) md
-> (forall s. Group sd md s k nm objs -> IO a)
-> IO a
group dvc :: D sd
dvc@(Device.D D
mdvc) mac :: M (U2 A) md
mac@(M (U2 A) md -> M A (Snd md)
forall (msa :: Maybe (*, *)).
ToMiddle msa =>
M (U2 A) msa -> M A (Snd msa)
AllocationCallbacks.toMiddle -> M A (Snd md)
mmac) forall s. Group sd md s k nm objs -> IO a
f = do
	(sem, m) <- STM (TSem, TVar (Map k (B Any nm objs)))
-> IO (TSem, TVar (Map k (B Any nm objs)))
forall a. STM a -> IO a
atomically (STM (TSem, TVar (Map k (B Any nm objs)))
 -> IO (TSem, TVar (Map k (B Any nm objs))))
-> STM (TSem, TVar (Map k (B Any nm objs)))
-> IO (TSem, TVar (Map k (B Any nm objs)))
forall a b. (a -> b) -> a -> b
$ (,) (TSem
 -> TVar (Map k (B Any nm objs))
 -> (TSem, TVar (Map k (B Any nm objs))))
-> STM TSem
-> STM
     (TVar (Map k (B Any nm objs))
      -> (TSem, TVar (Map k (B Any nm objs))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> STM TSem
newTSem Integer
1 STM
  (TVar (Map k (B Any nm objs))
   -> (TSem, TVar (Map k (B Any nm objs))))
-> STM (TVar (Map k (B Any nm objs)))
-> STM (TSem, TVar (Map k (B Any nm objs)))
forall a b. STM (a -> b) -> STM a -> STM b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Map k (B Any nm objs) -> STM (TVar (Map k (B Any nm objs)))
forall a. a -> STM (TVar a)
newTVar Map k (B Any nm objs)
forall k a. Map k a
Map.empty
	rtn <- f $ Group dvc mac sem m
	((\(B PL Length objs
_ B
mb) -> D -> B -> M A (Snd md) -> IO ()
forall (md :: Maybe (*)). D -> B -> M A md -> IO ()
M.destroy D
mdvc B
mb M A (Snd md)
mmac) `mapM_`)
		=<< atomically (readTVar m)
	pure rtn

create' :: (
	Ord k, WithPoked (TMaybe.M mn),
	VObj.SizeAlignmentList objs, AllocationCallbacks.ToMiddle ma ) =>
	Group sd ma sg k nm objs -> k -> CreateInfo mn objs ->
	IO (Either String (B sg nm objs))
create' :: forall k (mn :: Maybe (*)) (objs :: [O]) (ma :: Maybe (*, *)) sd sg
       (nm :: Symbol).
(Ord k, WithPoked (M mn), SizeAlignmentList objs, ToMiddle ma) =>
Group sd ma sg k nm objs
-> k -> CreateInfo mn objs -> IO (Either String (B sg nm objs))
create' (Group (Device.D D
dvc)
	(M (U2 A) ma -> M A (Snd ma)
forall (msa :: Maybe (*, *)).
ToMiddle msa =>
M (U2 A) msa -> M A (Snd msa)
AllocationCallbacks.toMiddle -> M A (Snd ma)
mac) TSem
sem TVar (Map k (B sg nm objs))
bs) k
k CreateInfo mn objs
ci = do
	ok <- STM Bool -> IO Bool
forall a. STM a -> IO a
atomically do
		mx <- (k -> Map k (B sg nm objs) -> Maybe (B sg nm objs)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k) (Map k (B sg nm objs) -> Maybe (B sg nm objs))
-> STM (Map k (B sg nm objs)) -> STM (Maybe (B sg nm objs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (B sg nm objs)) -> STM (Map k (B sg nm objs))
forall a. TVar a -> STM a
readTVar TVar (Map k (B sg nm objs))
bs
		case mx of
			Maybe (B sg nm objs)
Nothing -> TSem -> STM ()
waitTSem TSem
sem STM () -> STM Bool -> STM Bool
forall a b. STM a -> STM b -> STM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Bool -> STM Bool
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
True
			Just B sg nm objs
_ -> Bool -> STM Bool
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
	if ok
	then do	b <- M.create dvc (createInfoToMiddle ci) mac
		let b' = PL Length objs -> B -> B sg nm objs
forall s (nm :: Symbol) (objs :: [O]).
PL Length objs -> B -> B s nm objs
B (CreateInfo mn objs -> PL Length objs
forall (mn :: Maybe (*)) (objs :: [O]).
CreateInfo mn objs -> PL Length objs
createInfoLengths CreateInfo mn objs
ci) B
b
		atomically $ modifyTVar bs (Map.insert k b') >> signalTSem sem
		pure $ Right b'
	else pure . Left $ "Gpu.Vulkan.Buffer.create': The key already exist"

unsafeDestroy :: (Ord k, AllocationCallbacks.ToMiddle ma) =>
	Group sd ma sg k nm objs -> k -> IO (Either String ())
unsafeDestroy :: forall k (ma :: Maybe (*, *)) sd sg (nm :: Symbol) (objs :: [O]).
(Ord k, ToMiddle ma) =>
Group sd ma sg k nm objs -> k -> IO (Either String ())
unsafeDestroy (Group (Device.D D
mdvc)
	(M (U2 A) ma -> M A (Snd ma)
forall (msa :: Maybe (*, *)).
ToMiddle msa =>
M (U2 A) msa -> M A (Snd msa)
AllocationCallbacks.toMiddle -> M A (Snd ma)
ma) TSem
sem TVar (Map k (B sg nm objs))
bs) k
k = do
	mb <- STM (Maybe (B sg nm objs)) -> IO (Maybe (B sg nm objs))
forall a. STM a -> IO a
atomically do
		mx <- k -> Map k (B sg nm objs) -> Maybe (B sg nm objs)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k (Map k (B sg nm objs) -> Maybe (B sg nm objs))
-> STM (Map k (B sg nm objs)) -> STM (Maybe (B sg nm objs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (B sg nm objs)) -> STM (Map k (B sg nm objs))
forall a. TVar a -> STM a
readTVar TVar (Map k (B sg nm objs))
bs
		case mx of
			Maybe (B sg nm objs)
Nothing -> Maybe (B sg nm objs) -> STM (Maybe (B sg nm objs))
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (B sg nm objs)
forall a. Maybe a
Nothing
			Just B sg nm objs
_ -> TSem -> STM ()
waitTSem TSem
sem STM () -> STM (Maybe (B sg nm objs)) -> STM (Maybe (B sg nm objs))
forall a b. STM a -> STM b -> STM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (B sg nm objs) -> STM (Maybe (B sg nm objs))
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (B sg nm objs)
mx
	case mb of
		Maybe (B sg nm objs)
Nothing -> Either String () -> IO (Either String ())
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String () -> IO (Either String ()))
-> Either String () -> IO (Either String ())
forall a b. (a -> b) -> a -> b
$ String -> Either String ()
forall a b. a -> Either a b
Left String
"Gpu.Vulkan.Buffer.unsafeDestroy: No such key"
		Just (B PL Length objs
_ B
b) -> do
			D -> B -> M A (Snd ma) -> IO ()
forall (md :: Maybe (*)). D -> B -> M A md -> IO ()
M.destroy D
mdvc B
b M A (Snd ma)
ma
			STM (Either String ()) -> IO (Either String ())
forall a. STM a -> IO a
atomically do
				TVar (Map k (B sg nm objs))
-> (Map k (B sg nm objs) -> Map k (B sg nm objs)) -> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar (Map k (B sg nm objs))
bs (k -> Map k (B sg nm objs) -> Map k (B sg nm objs)
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete k
k)
				TSem -> STM ()
signalTSem TSem
sem
				Either String () -> STM (Either String ())
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Either String () -> STM (Either String ()))
-> Either String () -> STM (Either String ())
forall a b. (a -> b) -> a -> b
$ () -> Either String ()
forall a b. b -> Either a b
Right ()

lookup :: Ord k => Group sd md sg k nm objs -> k -> IO (Maybe (B sg nm objs))
lookup :: forall k sd (md :: Maybe (*, *)) sg (nm :: Symbol) (objs :: [O]).
Ord k =>
Group sd md sg k nm objs -> k -> IO (Maybe (B sg nm objs))
lookup (Group D sd
_ M (U2 A) md
_ TSem
_sem TVar (Map k (B sg nm objs))
bs) k
k = STM (Maybe (B sg nm objs)) -> IO (Maybe (B sg nm objs))
forall a. STM a -> IO a
atomically (STM (Maybe (B sg nm objs)) -> IO (Maybe (B sg nm objs)))
-> STM (Maybe (B sg nm objs)) -> IO (Maybe (B sg nm objs))
forall a b. (a -> b) -> a -> b
$ k -> Map k (B sg nm objs) -> Maybe (B sg nm objs)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k (Map k (B sg nm objs) -> Maybe (B sg nm objs))
-> STM (Map k (B sg nm objs)) -> STM (Maybe (B sg nm objs))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (B sg nm objs)) -> STM (Map k (B sg nm objs))
forall a. TVar a -> STM a
readTVar TVar (Map k (B sg nm objs))
bs

getMemoryRequirements :: Device.D sd -> B sb nm objs -> IO Memory.Requirements
getMemoryRequirements :: forall sd sb (nm :: Symbol) (objs :: [O]).
D sd -> B sb nm objs -> IO Requirements
getMemoryRequirements (Device.D D
dvc) (B PL Length objs
_ B
b) = D -> B -> IO Requirements
M.getMemoryRequirements D
dvc B
b

data IndexedForList sm sb nm t onm = forall objs .
	VObj.OffsetOfList t onm objs => IndexedForList (Binded sm sb nm objs)

indexedListToOffset :: forall sm sb nm v onm a . IndexedForList sm sb nm v onm ->
	(forall vs . (Binded sm sb nm vs, Device.M.Size) -> a) -> a
indexedListToOffset :: forall {k} sm sb (nm :: Symbol) (v :: k) (onm :: Symbol) a.
IndexedForList sm sb nm v onm
-> (forall (vs :: [O]). (Binded sm sb nm vs, Size) -> a) -> a
indexedListToOffset (IndexedForList b :: Binded sm sb nm objs
b@(Binded PL Length objs
lns B
_)) forall (vs :: [O]). (Binded sm sb nm vs, Size) -> a
f =
	(Binded sm sb nm objs, Size) -> a
forall (vs :: [O]). (Binded sm sb nm vs, Size) -> a
f (Binded sm sb nm objs
b, (Size, Size) -> Size
forall a b. (a, b) -> a
fst ((Size, Size) -> Size) -> (Size, Size) -> Size
forall a b. (a -> b) -> a -> b
$ forall (v :: k) (onm :: Symbol) (vs :: [O]).
OffsetOfList v onm vs =>
PL Length vs -> (Size, Size)
forall {k} (v :: k) (onm :: Symbol) (vs :: [O]).
OffsetOfList v onm vs =>
PL Length vs -> (Size, Size)
VObj.offsetOfList @v @onm PL Length objs
lns)

indexedListToMiddle :: IndexedForList sm sb nm v onm -> (M.B, Device.M.Size)
indexedListToMiddle :: forall {k} sm sb (nm :: Symbol) (v :: k) (onm :: Symbol).
IndexedForList sm sb nm v onm -> (B, Size)
indexedListToMiddle IndexedForList sm sb nm v onm
il = IndexedForList sm sb nm v onm
-> (forall (vs :: [O]). (Binded sm sb nm vs, Size) -> (B, Size))
-> (B, Size)
forall {k} sm sb (nm :: Symbol) (v :: k) (onm :: Symbol) a.
IndexedForList sm sb nm v onm
-> (forall (vs :: [O]). (Binded sm sb nm vs, Size) -> a) -> a
indexedListToOffset IndexedForList sm sb nm v onm
il \(Binded PL Length vs
_ B
b, Size
sz) -> (B
b, Size
sz)

indexedListToMiddles ::
	HeteroParList.PL (U5 IndexedForList) smsbvs -> [(M.B, Device.M.Size)]
indexedListToMiddles :: forall {k3} (smsbvs :: [(*, *, Symbol, k3, Symbol)]).
PL (U5 IndexedForList) smsbvs -> [(B, Size)]
indexedListToMiddles PL (U5 IndexedForList) smsbvs
HeteroParList.Nil = []
indexedListToMiddles (U5 IndexedForList s1 s2 s3 s4 s5
il :** PL (U5 IndexedForList) ss1
ils) =
	IndexedForList s1 s2 s3 s4 s5 -> (B, Size)
forall {k} sm sb (nm :: Symbol) (v :: k) (onm :: Symbol).
IndexedForList sm sb nm v onm -> (B, Size)
indexedListToMiddle IndexedForList s1 s2 s3 s4 s5
il (B, Size) -> [(B, Size)] -> [(B, Size)]
forall a. a -> [a] -> [a]
: PL (U5 IndexedForList) ss1 -> [(B, Size)]
forall {k3} (smsbvs :: [(*, *, Symbol, k3, Symbol)]).
PL (U5 IndexedForList) smsbvs -> [(B, Size)]
indexedListToMiddles PL (U5 IndexedForList) ss1
ils

class CopyPrefix (area :: [VObj.O]) (src :: [VObj.O]) (dst :: [VObj.O]) where
	copyCheckLengthPrefix ::
		HeteroParList.PL VObj.Length src ->
		HeteroParList.PL VObj.Length dst -> Bool
	copySizePrefix :: Word64 -> HeteroParList.PL VObj.Length src -> Word64

instance CopyPrefix '[] src dst where
	copyCheckLengthPrefix :: PL Length src -> PL Length dst -> Bool
copyCheckLengthPrefix PL Length src
_ PL Length dst
_ = Bool
True
	copySizePrefix :: Word64 -> PL Length src -> Word64
copySizePrefix Word64
sz PL Length src
_ = Word64
sz

instance (
	VObj.SizeAlignment a,
	CopyPrefix as ss ds ) =>
	CopyPrefix (a ': as) (a ': ss) (a ': ds) where
	copyCheckLengthPrefix :: PL Length (a : ss) -> PL Length (a : ds) -> Bool
copyCheckLengthPrefix (Length s
s :** PL Length ss1
ss) (Length s
d :** PL Length ss1
ds) =
		Length s
s Length s -> Length s -> Bool
forall a. Eq a => a -> a -> Bool
== Length s
Length s
d Bool -> Bool -> Bool
&& forall (area :: [O]) (src :: [O]) (dst :: [O]).
CopyPrefix area src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLengthPrefix @as PL Length ss1
ss PL Length ss1
ds
	copySizePrefix :: Word64 -> PL Length (a : ss) -> Word64
copySizePrefix Word64
sz (Length s
ln :** PL Length ss1
lns) = forall (area :: [O]) (src :: [O]) (dst :: [O]).
CopyPrefix area src dst =>
Word64 -> PL Length src -> Word64
copySizePrefix @as @ss @ds
		(((Word64
sz Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
VObj.size Length s
ln))
		PL Length ss
PL Length ss1
lns
		where algn :: Word64
algn = Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Word64) -> Size -> Word64
forall a b. (a -> b) -> a -> b
$ forall (obj :: O). SizeAlignment obj => Size
VObj.alignment @a

class CopyInfo (area :: [VObj.O]) (is :: Nat) (id :: Nat) (src :: [VObj.O]) (dst :: [VObj.O]) where
	copyCheckLength ::
		HeteroParList.PL VObj.Length src ->
		HeteroParList.PL VObj.Length dst -> Bool
	copySrcOffset :: Word64 -> HeteroParList.PL VObj.Length src -> Word64
	copyDstOffset :: Word64 -> HeteroParList.PL VObj.Length dst -> Word64
	copySize :: HeteroParList.PL VObj.Length src -> Word64

type OT o = VObj.TypeOf o

instance (
	Sizable (VObj.TypeOf a),
	CopyPrefix (a ': as) (a ': ss) (a ': ds) ) => CopyInfo (a ': as) 0 0 (a ': ss) (a ': ds) where
	copyCheckLength :: PL Length (a : ss) -> PL Length (a : ds) -> Bool
copyCheckLength = forall (area :: [O]) (src :: [O]) (dst :: [O]).
CopyPrefix area src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLengthPrefix @(a ': as) @(a ': ss) @(a ': ds)
	copySrcOffset :: Word64 -> PL Length (a : ss) -> Word64
copySrcOffset Word64
ost PL Length (a : ss)
_ = ((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn
		where algn :: Word64
algn = Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ forall a. Sizable a => Int
alignment' @(OT a)
	copyDstOffset :: Word64 -> PL Length (a : ds) -> Word64
copyDstOffset Word64
ost PL Length (a : ds)
_ = ((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn
		where algn :: Word64
algn = Int -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Word64) -> Int -> Word64
forall a b. (a -> b) -> a -> b
$ forall a. Sizable a => Int
alignment' @(OT a)
	copySize :: PL Length (a : ss) -> Word64
copySize = forall (area :: [O]) (src :: [O]) (dst :: [O]).
CopyPrefix area src dst =>
Word64 -> PL Length src -> Word64
copySizePrefix @(a ': as) @(a ': ss) @(a ': ds) Word64
0

instance {-# OVERLAPPABLE #-}
	(VObj.SizeAlignment a, CopyInfo (a ': as) 0 (id - 1) (a ': ss) ds) =>
	CopyInfo (a ': as) 0 id (a ': ss) (a ': ds) where
	copyCheckLength :: PL Length (a : ss) -> PL Length (a : ds) -> Bool
copyCheckLength PL Length (a : ss)
ss (Length s
_ :** PL Length ss1
ds) =
		forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLength @(a ': as) @0 @(id - 1) @(a ': ss) @ds PL Length (a : ss)
ss PL Length ds
PL Length ss1
ds
	copySrcOffset :: Word64 -> PL Length (a : ss) -> Word64
copySrcOffset Word64
ost PL Length (a : ss)
lns = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length src -> Word64
copySrcOffset @(a ': as) @0 @(id - 1) @(a ': ss) @ds Word64
ost PL Length (a : ss)
lns
	copyDstOffset :: Word64 -> PL Length (a : ds) -> Word64
copyDstOffset Word64
ost (Length s
ln :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length dst -> Word64
copyDstOffset @(a ': as) @0 @(id - 1) @(a ': ss)
		(((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
VObj.size Length s
ln))
		PL Length ss1
lns
		where algn :: Word64
algn = Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Word64) -> Size -> Word64
forall a b. (a -> b) -> a -> b
$ forall (obj :: O). SizeAlignment obj => Size
VObj.alignment @a
	copySize :: PL Length (a : ss) -> Word64
copySize = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> Word64
copySize @(a ': as) @0 @(id - 1) @(a ': ss) @ds

instance {-# OVERLAPPABLE #-}
	(VObj.SizeAlignment d, CopyInfo (a ': as) 0 id (a ': ss) ds) =>
	CopyInfo (a ': as) 0 id (a ': ss) (d ': ds) where
	copyCheckLength :: PL Length (a : ss) -> PL Length (d : ds) -> Bool
copyCheckLength PL Length (a : ss)
ss (Length s
_ :** PL Length ss1
ds) =
		forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLength @(a ': as) @0 @id @(a ': ss) @ds PL Length (a : ss)
ss PL Length ds
PL Length ss1
ds
	copySrcOffset :: Word64 -> PL Length (a : ss) -> Word64
copySrcOffset Word64
ost PL Length (a : ss)
lns = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length src -> Word64
copySrcOffset @(a ': as) @0 @id @(a ': ss) @ds Word64
ost PL Length (a : ss)
lns
	copyDstOffset :: Word64 -> PL Length (d : ds) -> Word64
copyDstOffset Word64
ost (Length s
ln :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length dst -> Word64
copyDstOffset @(a ': as) @0 @id @(a ': ss)
		(((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
VObj.size Length s
ln))
		PL Length ss1
lns
		where algn :: Word64
algn = Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Word64) -> Size -> Word64
forall a b. (a -> b) -> a -> b
$ forall (obj :: O). SizeAlignment obj => Size
VObj.alignment @d
	copySize :: PL Length (a : ss) -> Word64
copySize = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> Word64
copySize @(a ': as) @0 @id @(a ': ss) @ds

instance {-# OVERLAPPABLE #-}
	(VObj.SizeAlignment a, CopyInfo (a ': as) (is - 1) id ss ds) =>
	CopyInfo (a ': as) is id (a ': ss) ds where
	copyCheckLength :: PL Length (a : ss) -> PL Length ds -> Bool
copyCheckLength (Length s
_ :** PL Length ss1
ss) PL Length ds
ds = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLength @(a ': as) @(is - 1) @id @ss @ds PL Length ss
PL Length ss1
ss PL Length ds
ds
	copySrcOffset :: Word64 -> PL Length (a : ss) -> Word64
copySrcOffset Word64
ost (Length s
ln :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length src -> Word64
copySrcOffset @(a ': as) @(is - 1) @id @ss @ds
		(((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
VObj.size Length s
ln))
		PL Length ss
PL Length ss1
lns
		where algn :: Word64
algn = Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Size -> Word64) -> Size -> Word64
forall a b. (a -> b) -> a -> b
$ forall (obj :: O). SizeAlignment obj => Size
VObj.alignment @a
	copyDstOffset :: Word64 -> PL Length ds -> Word64
copyDstOffset Word64
ost PL Length ds
lns = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length dst -> Word64
copyDstOffset @(a ': as) @(is - 1) @id @ss Word64
ost PL Length ds
lns
	copySize :: PL Length (a : ss) -> Word64
copySize (Length s
_ :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> Word64
copySize @(a ': as) @(is - 1) @id @ss @ds PL Length ss
PL Length ss1
lns

instance {-# OVERLAPPABLE #-}
	(VObj.SizeAlignment s,
	CopyInfo as is id ss ds) =>
	CopyInfo as is id (s ': ss) ds where
	copyCheckLength :: PL Length (s : ss) -> PL Length ds -> Bool
copyCheckLength (Length s
_ :** PL Length ss1
ss) PL Length ds
ds = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLength @as @is @id PL Length ss1
ss PL Length ds
ds
	copySrcOffset :: Word64 -> PL Length (s : ss) -> Word64
copySrcOffset Word64
ost (Length s
ln :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length src -> Word64
copySrcOffset @as @is @id @ss @ds
		(((Word64
ost Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
- Word64
1) Word64 -> Word64 -> Word64
forall a. Integral a => a -> a -> a
`div` Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Word64
1) Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
* Word64
algn Word64 -> Word64 -> Word64
forall a. Num a => a -> a -> a
+ Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
VObj.size Length s
ln))
		PL Length ss
PL Length ss1
lns
		where algn :: Word64
algn = Size -> Word64
forall a b. (Integral a, Num b) => a -> b
fromIntegral (forall (obj :: O). SizeAlignment obj => Size
VObj.alignment @s)
	copyDstOffset :: Word64 -> PL Length ds -> Word64
copyDstOffset Word64
ost PL Length ds
lns = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length dst -> Word64
copyDstOffset @as @is @id @ss Word64
ost PL Length ds
lns
	copySize :: PL Length (s : ss) -> Word64
copySize (Length s
_ :** PL Length ss1
lns) = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> Word64
copySize @as @is @id @ss @ds PL Length ss
PL Length ss1
lns

makeCopy :: forall (as :: [VObj.O]) is id ss ds . CopyInfo as is id ss ds =>
	HeteroParList.PL VObj.Length ss -> HeteroParList.PL VObj.Length ds -> C.Copy
makeCopy :: forall (as :: [O]) (is :: Nat) (id :: Nat) (ss :: [O]) (ds :: [O]).
CopyInfo as is id ss ds =>
PL Length ss -> PL Length ds -> Copy
makeCopy PL Length ss
src PL Length ds
dst
	| forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> PL Length dst -> Bool
copyCheckLength @as @is @id PL Length ss
src PL Length ds
dst = C.Copy {
		copySrcOffset :: Word64
C.copySrcOffset = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length src -> Word64
copySrcOffset @as @is @id @ss @ds Word64
0 PL Length ss
src,
		copyDstOffset :: Word64
C.copyDstOffset = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
Word64 -> PL Length dst -> Word64
copyDstOffset @as @is @id @ss @ds Word64
0 PL Length ds
dst,
		copySize :: Word64
C.copySize = forall (area :: [O]) (is :: Nat) (id :: Nat) (src :: [O])
       (dst :: [O]).
CopyInfo area is id src dst =>
PL Length src -> Word64
copySize @as @is @id @ss @ds PL Length ss
src }
	| Bool
otherwise = String -> Copy
forall a. HasCallStack => String -> a
error String
"List lengths are different"

class MakeCopies (cpss :: [([VObj.O], Nat, Nat)]) (ss :: [VObj.O]) (ds :: [VObj.O]) where
	makeCopies ::
		HeteroParList.PL VObj.Length ss ->
		HeteroParList.PL VObj.Length ds -> [C.Copy]

instance MakeCopies '[] ss ds where makeCopies :: PL Length ss -> PL Length ds -> [Copy]
makeCopies PL Length ss
_ PL Length ds
_ = []

instance (CopyInfo as is id ss ds, MakeCopies ass ss ds) =>
	MakeCopies ('(as, is, id) ': ass) ss ds where
	makeCopies :: PL Length ss -> PL Length ds -> [Copy]
makeCopies PL Length ss
src PL Length ds
dst = forall (as :: [O]) (is :: Nat) (id :: Nat) (ss :: [O]) (ds :: [O]).
CopyInfo as is id ss ds =>
PL Length ss -> PL Length ds -> Copy
makeCopy @as @is @id PL Length ss
src PL Length ds
dst Copy -> [Copy] -> [Copy]
forall a. a -> [a] -> [a]
: forall (cpss :: [([O], Nat, Nat)]) (ss :: [O]) (ds :: [O]).
MakeCopies cpss ss ds =>
PL Length ss -> PL Length ds -> [Copy]
makeCopies @ass PL Length ss
src PL Length ds
dst

{-
offsetSize :: forall v vs . (
	VObj.OffsetRange v vs, VObj.SizeAlignment v,
	VObj.LengthOf v vs ) =>
	HeteroParList.PL VObj.Length vs ->
	Device.M.Size -> (Device.M.Size, Device.M.Size)
offsetSize lns _ = (VObj.offsetNew @v lns, sizeNew @v lns)

sizeNew :: forall v vs . (
	VObj.SizeAlignment v, VObj.LengthOf v vs ) =>
	HeteroParList.PL VObj.Length vs -> Device.M.Size
sizeNew = fromIntegral . VObj.size . VObj.objectLengthOf @v
-}

data MemoryBarrier mn sm sb nm obj = forall objs . (
	VObj.OffsetRange obj objs 0, VObj.LengthOf obj objs ) =>
	MemoryBarrier {
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> M mn
memoryBarrierNext :: TMaybe.M mn,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> AccessFlags
memoryBarrierSrcAccessMask :: AccessFlags,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> AccessFlags
memoryBarrierDstAccessMask :: AccessFlags,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> Index
memoryBarrierSrcQueueFamilyIndex :: QueueFamily.Index,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> Index
memoryBarrierDstQueueFamilyIndex :: QueueFamily.Index,
		()
memoryBarrierBuffer :: Binded sm sb nm objs }

memoryBarrierToMiddle :: forall n sm sb nm obj .
	MemoryBarrier n sm sb nm obj -> M.MemoryBarrier n
memoryBarrierToMiddle :: forall (n :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier n sm sb nm obj -> MemoryBarrier n
memoryBarrierToMiddle MemoryBarrier {
	memoryBarrierNext :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> M mn
memoryBarrierNext = M n
mnxt,
	memoryBarrierSrcAccessMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> AccessFlags
memoryBarrierSrcAccessMask = AccessFlags
sam, memoryBarrierDstAccessMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> AccessFlags
memoryBarrierDstAccessMask = AccessFlags
dam,
	memoryBarrierSrcQueueFamilyIndex :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> Index
memoryBarrierSrcQueueFamilyIndex = Index
sqfi,
	memoryBarrierDstQueueFamilyIndex :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier mn sm sb nm obj -> Index
memoryBarrierDstQueueFamilyIndex = Index
dqfi,
	memoryBarrierBuffer :: ()
memoryBarrierBuffer = Binded PL Length objs
lns B
b } = M.MemoryBarrier {
	memoryBarrierNext :: M n
M.memoryBarrierNext = M n
mnxt,
	memoryBarrierSrcAccessMask :: AccessFlags
M.memoryBarrierSrcAccessMask = AccessFlags
sam,
	memoryBarrierDstAccessMask :: AccessFlags
M.memoryBarrierDstAccessMask = AccessFlags
dam,
	memoryBarrierSrcQueueFamilyIndex :: Index
M.memoryBarrierSrcQueueFamilyIndex = Index
sqfi,
	memoryBarrierDstQueueFamilyIndex :: Index
M.memoryBarrierDstQueueFamilyIndex = Index
dqfi,
	memoryBarrierBuffer :: B
M.memoryBarrierBuffer = B
b,
	memoryBarrierOffset :: Size
M.memoryBarrierOffset = Size
ost,
	memoryBarrierSize :: Size
M.memoryBarrierSize = Size
sz }
	where (Size
ost, Size
sz) = forall (obj :: O) (objs :: [O]) (i :: Nat).
OffsetRange obj objs i =>
Size -> PL Length objs -> (Size, Size)
VObj.offsetRange @obj @_ @0 Size
0 PL Length objs
lns

class MemoryBarrierListToMiddle nsmsbnmobjs where
	memoryBarrierListToMiddle ::
		HeteroParList.PL (U5 MemoryBarrier) nsmsbnmobjs ->
		HeteroParList.PL M.MemoryBarrier (TMapIndex.M0_5 nsmsbnmobjs)

instance MemoryBarrierListToMiddle '[] where
	memoryBarrierListToMiddle :: PL (U5 MemoryBarrier) '[] -> PL MemoryBarrier (M0_5 '[])
memoryBarrierListToMiddle PL (U5 MemoryBarrier) '[]
HeteroParList.Nil = PL MemoryBarrier '[]
PL MemoryBarrier (M0_5 '[])
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance MemoryBarrierListToMiddle nsmsbnmobjs =>
	MemoryBarrierListToMiddle ('(mn, sm, sb, nm, obj) ': nsmsbnmobjs) where
	memoryBarrierListToMiddle :: PL (U5 MemoryBarrier) ('(mn, sm, sb, nm, obj) : nsmsbnmobjs)
-> PL MemoryBarrier (M0_5 ('(mn, sm, sb, nm, obj) : nsmsbnmobjs))
memoryBarrierListToMiddle (U5 MemoryBarrier s1 s2 s3 s4 s5
mb :** PL (U5 MemoryBarrier) ss1
mbs) =
		MemoryBarrier s1 s2 s3 s4 s5 -> MemoryBarrier s1
forall (n :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier n sm sb nm obj -> MemoryBarrier n
memoryBarrierToMiddle MemoryBarrier s1 s2 s3 s4 s5
mb MemoryBarrier s1
-> PL MemoryBarrier (M0_5 nsmsbnmobjs)
-> PL MemoryBarrier (s1 : M0_5 nsmsbnmobjs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (U5 MemoryBarrier) ss1 -> PL MemoryBarrier (M0_5 ss1)
forall (nsmsbnmobjs :: [(Maybe (*), *, *, Symbol, O)]).
MemoryBarrierListToMiddle nsmsbnmobjs =>
PL (U5 MemoryBarrier) nsmsbnmobjs
-> PL MemoryBarrier (M0_5 nsmsbnmobjs)
memoryBarrierListToMiddle PL (U5 MemoryBarrier) ss1
mbs

data MemoryBarrier2 mn sm sb nm obj = forall objs . (
	VObj.OffsetRange obj objs 0, VObj.LengthOf obj objs ) =>
	MemoryBarrier2 {
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> M mn
memoryBarrier2Next :: TMaybe.M mn,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> StageFlags2
memoryBarrier2SrcStageMask :: Pipeline.StageFlags2,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> AccessFlags2
memoryBarrier2SrcAccessMask :: AccessFlags2,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> StageFlags2
memoryBarrier2DstStageMask :: Pipeline.StageFlags2,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> AccessFlags2
memoryBarrier2DstAccessMask :: AccessFlags2,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> Index
memoryBarrier2SrcQueueFamilyIndex :: QueueFamily.Index,
		forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> Index
memoryBarrier2DstQueueFamilyIndex :: QueueFamily.Index,
		()
memoryBarrier2Buffer :: Binded sm sb nm objs }

memoryBarrier2ToMiddle :: forall mn sm sb nm obj .
	MemoryBarrier2 mn sm sb nm obj -> M.MemoryBarrier2 mn
memoryBarrier2ToMiddle :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> MemoryBarrier2 mn
memoryBarrier2ToMiddle MemoryBarrier2 {
	memoryBarrier2Next :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> M mn
memoryBarrier2Next = M mn
mnxt,
	memoryBarrier2SrcStageMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> StageFlags2
memoryBarrier2SrcStageMask = StageFlags2
ssm, memoryBarrier2SrcAccessMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> AccessFlags2
memoryBarrier2SrcAccessMask = AccessFlags2
sam,
	memoryBarrier2DstStageMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> StageFlags2
memoryBarrier2DstStageMask = StageFlags2
dsm, memoryBarrier2DstAccessMask :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> AccessFlags2
memoryBarrier2DstAccessMask = AccessFlags2
dam,
	memoryBarrier2SrcQueueFamilyIndex :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> Index
memoryBarrier2SrcQueueFamilyIndex = Index
sqfi,
	memoryBarrier2DstQueueFamilyIndex :: forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> Index
memoryBarrier2DstQueueFamilyIndex = Index
dqfi,
	memoryBarrier2Buffer :: ()
memoryBarrier2Buffer = Binded PL Length objs
lns B
b } = M.MemoryBarrier2 {
	memoryBarrier2Next :: M mn
M.memoryBarrier2Next = M mn
mnxt,
	memoryBarrier2SrcStageMask :: StageFlags2
M.memoryBarrier2SrcStageMask = StageFlags2
ssm, memoryBarrier2SrcAccessMask :: AccessFlags2
M.memoryBarrier2SrcAccessMask = AccessFlags2
sam,
	memoryBarrier2DstStageMask :: StageFlags2
M.memoryBarrier2DstStageMask = StageFlags2
dsm, memoryBarrier2DstAccessMask :: AccessFlags2
M.memoryBarrier2DstAccessMask = AccessFlags2
dam,
	memoryBarrier2SrcQueueFamilyIndex :: Index
M.memoryBarrier2SrcQueueFamilyIndex = Index
sqfi,
	memoryBarrier2DstQueueFamilyIndex :: Index
M.memoryBarrier2DstQueueFamilyIndex = Index
dqfi,
	memoryBarrier2Buffer :: B
M.memoryBarrier2Buffer = B
b,
	memoryBarrier2Offset :: Size
M.memoryBarrier2Offset = Size
ost, memoryBarrier2Size :: Size
M.memoryBarrier2Size = Size
sz }
	where (Size
ost, Size
sz) = forall (obj :: O) (objs :: [O]) (i :: Nat).
OffsetRange obj objs i =>
Size -> PL Length objs -> (Size, Size)
VObj.offsetRange @obj @_ @0 Size
0 PL Length objs
lns

class MemoryBarrier2ListToMiddle nsmsbnmobjs where
	memoryBarrier2ListToMiddle ::
		HeteroParList.PL (U5 MemoryBarrier2) nsmsbnmobjs ->
		HeteroParList.PL M.MemoryBarrier2 (TMapIndex.M0_5 nsmsbnmobjs)

instance MemoryBarrier2ListToMiddle '[] where
	memoryBarrier2ListToMiddle :: PL (U5 MemoryBarrier2) '[] -> PL MemoryBarrier2 (M0_5 '[])
memoryBarrier2ListToMiddle PL (U5 MemoryBarrier2) '[]
HeteroParList.Nil = PL MemoryBarrier2 '[]
PL MemoryBarrier2 (M0_5 '[])
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance MemoryBarrier2ListToMiddle nsmsbnmobjs =>
	MemoryBarrier2ListToMiddle ('(mn, sm, sb, nm, obj) ': nsmsbnmobjs) where
	memoryBarrier2ListToMiddle :: PL (U5 MemoryBarrier2) ('(mn, sm, sb, nm, obj) : nsmsbnmobjs)
-> PL MemoryBarrier2 (M0_5 ('(mn, sm, sb, nm, obj) : nsmsbnmobjs))
memoryBarrier2ListToMiddle (U5 MemoryBarrier2 s1 s2 s3 s4 s5
mb :** PL (U5 MemoryBarrier2) ss1
mbs) =
		MemoryBarrier2 s1 s2 s3 s4 s5 -> MemoryBarrier2 s1
forall (mn :: Maybe (*)) sm sb (nm :: Symbol) (obj :: O).
MemoryBarrier2 mn sm sb nm obj -> MemoryBarrier2 mn
memoryBarrier2ToMiddle MemoryBarrier2 s1 s2 s3 s4 s5
mb MemoryBarrier2 s1
-> PL MemoryBarrier2 (M0_5 nsmsbnmobjs)
-> PL MemoryBarrier2 (s1 : M0_5 nsmsbnmobjs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL (U5 MemoryBarrier2) ss1 -> PL MemoryBarrier2 (M0_5 ss1)
forall (nsmsbnmobjs :: [(Maybe (*), *, *, Symbol, O)]).
MemoryBarrier2ListToMiddle nsmsbnmobjs =>
PL (U5 MemoryBarrier2) nsmsbnmobjs
-> PL MemoryBarrier2 (M0_5 nsmsbnmobjs)
memoryBarrier2ListToMiddle PL (U5 MemoryBarrier2) ss1
mbs

data ImageCopy img inm = ImageCopy {
	forall {k} {k} (img :: k) (inm :: k).
ImageCopy img inm -> SubresourceLayers
imageCopyImageSubresource :: Image.M.SubresourceLayers,
	forall {k} {k} (img :: k) (inm :: k). ImageCopy img inm -> Offset3d
imageCopyImageOffset :: C.Offset3d,
	forall {k} {k} (img :: k) (inm :: k). ImageCopy img inm -> Extent3d
imageCopyImageExtent :: C.Extent3d }
	deriving Int -> ImageCopy img inm -> ShowS
[ImageCopy img inm] -> ShowS
ImageCopy img inm -> String
(Int -> ImageCopy img inm -> ShowS)
-> (ImageCopy img inm -> String)
-> ([ImageCopy img inm] -> ShowS)
-> Show (ImageCopy img inm)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (img :: k) k (inm :: k). Int -> ImageCopy img inm -> ShowS
forall k (img :: k) k (inm :: k). [ImageCopy img inm] -> ShowS
forall k (img :: k) k (inm :: k). ImageCopy img inm -> String
$cshowsPrec :: forall k (img :: k) k (inm :: k). Int -> ImageCopy img inm -> ShowS
showsPrec :: Int -> ImageCopy img inm -> ShowS
$cshow :: forall k (img :: k) k (inm :: k). ImageCopy img inm -> String
show :: ImageCopy img inm -> String
$cshowList :: forall k (img :: k) k (inm :: k). [ImageCopy img inm] -> ShowS
showList :: [ImageCopy img inm] -> ShowS
Show

class ImageCopyListToMiddle algn objs (img :: Type) (inms :: [Symbol]) where
	imageCopyListToMiddle ::
		Binded sm sb nm objs ->
		HeteroParList.PL (ImageCopy img) inms ->
		[M.ImageCopy]

instance ImageCopyListToMiddle algn objs img '[] where
	imageCopyListToMiddle :: forall sm sb (nm :: Symbol).
Binded sm sb nm objs -> PL (ImageCopy img) '[] -> [ImageCopy]
imageCopyListToMiddle Binded sm sb nm objs
_ PL (ImageCopy img) '[]
HeteroParList.Nil = []

instance (
	VObj.OffsetRange (VObj.Image algn img nm) objs 0,
	VObj.LengthOf (VObj.Image algn img nm) objs,
	ImageCopyListToMiddle algn objs img nms ) =>
	ImageCopyListToMiddle algn objs img (nm ': nms) where
	imageCopyListToMiddle :: forall sm sb (nm :: Symbol).
Binded sm sb nm objs
-> PL (ImageCopy img) (nm : nms) -> [ImageCopy]
imageCopyListToMiddle Binded sm sb nm objs
bf (ImageCopy img s
ic :** PL (ImageCopy img) ss1
ics) =
		forall (algn :: Nat) img (inm :: Symbol) sm sb (nm :: Symbol)
       (obj :: O) (objs :: [O]).
(obj ~ Image algn img inm, OffsetRange obj objs 0,
 LengthOf obj objs) =>
Binded sm sb nm objs -> ImageCopy img inm -> ImageCopy
imageCopyToMiddle @algn @_ @nm Binded sm sb nm objs
bf (ImageCopy img nm
ImageCopy img s
ic :: ImageCopy img nm) ImageCopy -> [ImageCopy] -> [ImageCopy]
forall a. a -> [a] -> [a]
:
		forall (algn :: Nat) (objs :: [O]) img (inms :: [Symbol]) sm sb
       (nm :: Symbol).
ImageCopyListToMiddle algn objs img inms =>
Binded sm sb nm objs -> PL (ImageCopy img) inms -> [ImageCopy]
forall {k} (algn :: k) (objs :: [O]) img (inms :: [Symbol]) sm sb
       (nm :: Symbol).
ImageCopyListToMiddle algn objs img inms =>
Binded sm sb nm objs -> PL (ImageCopy img) inms -> [ImageCopy]
imageCopyListToMiddle @algn Binded sm sb nm objs
bf PL (ImageCopy img) ss1
ics

imageCopyToMiddle :: forall algn img inm sm sb nm obj objs . (
	obj ~ VObj.Image algn img inm,
	VObj.OffsetRange obj objs 0, VObj.LengthOf obj objs ) =>
	Binded sm sb nm objs -> ImageCopy img inm -> M.ImageCopy
imageCopyToMiddle :: forall (algn :: Nat) img (inm :: Symbol) sm sb (nm :: Symbol)
       (obj :: O) (objs :: [O]).
(obj ~ Image algn img inm, OffsetRange obj objs 0,
 LengthOf obj objs) =>
Binded sm sb nm objs -> ImageCopy img inm -> ImageCopy
imageCopyToMiddle (Binded PL Length objs
lns B
_) ImageCopy {
	imageCopyImageSubresource :: forall {k} {k} (img :: k) (inm :: k).
ImageCopy img inm -> SubresourceLayers
imageCopyImageSubresource = SubresourceLayers
isr,
	imageCopyImageOffset :: forall {k} {k} (img :: k) (inm :: k). ImageCopy img inm -> Offset3d
imageCopyImageOffset = Offset3d
iost,
	imageCopyImageExtent :: forall {k} {k} (img :: k) (inm :: k). ImageCopy img inm -> Extent3d
imageCopyImageExtent = Extent3d
iext } = M.ImageCopy {
	imageCopyBufferOffset :: Size
M.imageCopyBufferOffset = Size
ost,
	imageCopyBufferRowLength :: Word32
M.imageCopyBufferRowLength = Size -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
r,
	imageCopyBufferImageHeight :: Word32
M.imageCopyBufferImageHeight = Size -> Word32
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
h,
	imageCopyImageSubresource :: SubresourceLayers
M.imageCopyImageSubresource = SubresourceLayers
isr,
	imageCopyImageOffset :: Offset3d
M.imageCopyImageOffset = Offset3d
iost,
	imageCopyImageExtent :: Extent3d
M.imageCopyImageExtent = Extent3d
iext }
	where
	(Size
ost, Size
_) = forall (obj :: O) (objs :: [O]) (i :: Nat).
OffsetRange obj objs i =>
Size -> PL Length objs -> (Size, Size)
VObj.offsetRange @(VObj.Image algn img inm) @_ @0 Size
0 PL Length objs
lns
	VObj.LengthImage Size
r Size
_w Size
h Size
_d Size
_lc = forall (obj :: O) (objs :: [O]).
LengthOf obj objs =>
PL Length objs -> Length obj
VObj.lengthOf @obj PL Length objs
lns