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

module Gpu.Vulkan.Object (

	-- * OBJECT

	O(..),

	-- ** Synonyms

	Static, Dynamic,

	-- *** static

	Atom, List, Image,
	AtomNoName, ListNoName, ImageNoName,
	AtomMaybeName, ListMaybeName, ImageMaybeName,

	-- *** dynamic

	DynAtomNew, DynList, DynImage,
	DynAtomNoName, DynListNoName, DynImageNoName,
	DynAtomMaybeName, DynListMaybeName, DynImageMaybeName,

	-- ** Type Of Object

	TypeOf,

	-- * OBJECT LENGTH

	Length,

	-- ** Synonyms

	pattern LengthAtom,
	pattern LengthList,
	pattern LengthImage,
	lengthImageRow, lengthImageWidth, lengthImageHeight, lengthImageDepth,
	lengthImageLayerCount,

	pattern LengthDynAtom,
	pattern LengthDynList,
	pattern LengthDynImage,

	pattern LengthList',

	-- ** Find Length

	LengthOf(..),

	-- * ONLY DYNAMIC LENGTHS

	OnlyDynamicLengths(..),

	-- * STORE

	Store(..),

	-- * SIZE, ALIGNMENT AND OFFSET

	-- ** Whole Size

	wholeSize, WholeAlign(..),

	-- ** Offset Range

	offsetRange, offsetSize, OffsetRange,

	-- ** Offset Of List

	offsetOfList, OffsetOfList(..),

	-- ** Size AlignmentList

	SizeAlignmentList(..), SizeAlignment(..),

	) where

import Prelude hiding (length)

import GHC.TypeLits (Symbol)
import GHC.TypeNats
import Foreign.Ptr
import Data.Proxy
import Data.HeteroParList qualified as HeteroParList
import Data.HeteroParList (pattern (:**))

import Data.Maybe
import Data.Word

import Foreign.Storable (Storable)
import Gpu.Vulkan.Object.Base qualified as K
import Gpu.Vulkan.Device.Middle.Internal qualified as Device.M

-- OBJECT

data O = Static_ K.O | Dynamic Nat K.O

type Static algn mnm ot v = 'Static_ ('K.O algn mnm ot v)
type Dynamic n algn mnm ot v = 'Dynamic n ('K.O algn mnm ot v)

type Atom algn v nm = AtomMaybeName algn v ('Just nm)
type List algn v nm = ListMaybeName algn v ('Just nm)
type Image algn v nm = ImageMaybeName algn v ('Just nm)

type AtomNoName algn v = AtomMaybeName algn v 'Nothing
type ListNoName algn v = ListMaybeName algn v 'Nothing
type ImageNoName algn v = ImageMaybeName algn v 'Nothing

type AtomMaybeName algn v mnm = Static_ (K.AtomMaybeName algn v mnm)
type ListMaybeName algn v mnm = Static_ (K.ListMaybeName algn v mnm)
type ImageMaybeName algn v mnm = Static_ (K.ImageMaybeName algn v mnm)

type DynAtomNew n algn v nm = 'Dynamic n (K.AtomNew algn v nm)
type DynList n algn v nm = 'Dynamic n (K.List algn v nm)
type DynImage n algn v nm = 'Dynamic n (K.Image algn v nm)

type DynAtomNoName n algn v = 'Dynamic n (K.AtomNoName algn v)
type DynListNoName n algn v = 'Dynamic n (K.ListNoName algn v)
type DynImageNoName n algn v = 'Dynamic n (K.ImageNoName algn v)

type DynAtomMaybeName n algn v mnm = 'Dynamic n (K.AtomMaybeName algn v mnm)
type DynListMaybeName n algn v mnm = 'Dynamic n (K.ListMaybeName algn v mnm)
type DynImageMaybeName n algn v mnm = 'Dynamic n (K.ImageMaybeName algn v mnm)

type family TypeOf obj where
	TypeOf (Static_ kobj) = K.TypeOf kobj
	TypeOf ('Dynamic n kobj) = K.TypeOf kobj

-- OBJECT LENGTH

data Length obj where
	LengthStatic :: K.Length kobj -> Length ('Static_ kobj)
	LengthDynamic ::
		K.Length kobj -> Length ('Dynamic n kobj)

deriving instance Eq (Length obj)
deriving instance Show (Length obj)

pattern LengthAtom :: Length ('Static_ (K.AtomMaybeName algn v mnm))
pattern $mLengthAtom :: forall {r} {algn :: Alignment} {v} {mnm :: Maybe Symbol}.
Length ('Static_ (AtomMaybeName algn v mnm))
-> ((# #) -> r) -> ((# #) -> r) -> r
$bLengthAtom :: forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (AtomMaybeName algn v mnm))
LengthAtom <- LengthStatic K.LengthAtom where
	LengthAtom = Length (AtomMaybeName algn v mnm)
-> Length ('Static_ (AtomMaybeName algn v mnm))
forall (kobj :: O). Length kobj -> Length ('Static_ kobj)
LengthStatic Length (AtomMaybeName algn v mnm)
forall (algn :: Alignment) t (nm :: Maybe Symbol).
Length ('O algn nm 'AtomT t)
K.LengthAtom

{-# COMPLETE LengthList #-}
{-# COMPLETE LengthList' #-}

pattern LengthList :: Device.M.Size ->
	Length ('Static_ (K.ListMaybeName algn v mnm))
pattern $mLengthList :: forall {r} {algn :: Alignment} {v} {mnm :: Maybe Symbol}.
Length ('Static_ (ListMaybeName algn v mnm))
-> (Size -> r) -> ((# #) -> r) -> r
$bLengthList :: forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Size -> Length ('Static_ (ListMaybeName algn v mnm))
LengthList n <- LengthStatic (K.LengthList n) where
	LengthList Size
n = Length (ListMaybeName algn v mnm)
-> Length ('Static_ (ListMaybeName algn v mnm))
forall (kobj :: O). Length kobj -> Length ('Static_ kobj)
LengthStatic (Size -> Length (ListMaybeName algn v mnm)
forall (algn :: Alignment) (mnm :: Maybe Symbol) t.
Size -> Length ('O algn mnm 'ListT t)
K.LengthList Size
n)

pattern LengthList' :: Word64 -> Length ('Static_ (K.ListMaybeName algn v nm))
pattern $mLengthList' :: forall {r} {algn :: Alignment} {v} {nm :: Maybe Symbol}.
Length ('Static_ (ListMaybeName algn v nm))
-> (Word64 -> r) -> ((# #) -> r) -> r
$bLengthList' :: forall (algn :: Alignment) v (nm :: Maybe Symbol).
Word64 -> Length ('Static_ (ListMaybeName algn v nm))
LengthList' n <- LengthStatic (K.LengthList (Device.M.Size n)) where
	LengthList' Word64
n = Length (ListMaybeName algn v nm)
-> Length ('Static_ (ListMaybeName algn v nm))
forall (kobj :: O). Length kobj -> Length ('Static_ kobj)
LengthStatic (Size -> Length (ListMaybeName algn v nm)
forall (algn :: Alignment) (mnm :: Maybe Symbol) t.
Size -> Length ('O algn mnm 'ListT t)
K.LengthList (Word64 -> Size
Device.M.Size Word64
n))

{-# COMPLETE LengthImage #-}

pattern LengthImage ::
	Device.M.Size -> Device.M.Size -> Device.M.Size -> Device.M.Size -> Device.M.Size ->
	Length ('Static_ (K.ImageMaybeName algn v mnm))
pattern $mLengthImage :: forall {r} {algn :: Alignment} {v} {mnm :: Maybe Symbol}.
Length ('Static_ (ImageMaybeName algn v mnm))
-> (Size -> Size -> Size -> Size -> Size -> r) -> ((# #) -> r) -> r
$bLengthImage :: forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Size
-> Size
-> Size
-> Size
-> Size
-> Length ('Static_ (ImageMaybeName algn v mnm))
LengthImage {
	forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (ImageMaybeName algn v mnm)) -> Size
lengthImageRow, forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (ImageMaybeName algn v mnm)) -> Size
lengthImageWidth,
	forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (ImageMaybeName algn v mnm)) -> Size
lengthImageHeight, forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (ImageMaybeName algn v mnm)) -> Size
lengthImageDepth, forall (algn :: Alignment) v (mnm :: Maybe Symbol).
Length ('Static_ (ImageMaybeName algn v mnm)) -> Size
lengthImageLayerCount } = LengthStatic (K.LengthImage
		lengthImageRow lengthImageWidth
		lengthImageHeight lengthImageDepth lengthImageLayerCount)

pattern LengthDynAtom :: Length ('Dynamic n (K.Atom algn v nm))
pattern $mLengthDynAtom :: forall {r} {n :: Alignment} {algn :: Alignment} {v}
       {nm :: Maybe Symbol}.
Length ('Dynamic n (Atom algn v nm))
-> ((# #) -> r) -> ((# #) -> r) -> r
$bLengthDynAtom :: forall (n :: Alignment) (algn :: Alignment) v (nm :: Maybe Symbol).
Length ('Dynamic n (Atom algn v nm))
LengthDynAtom <- LengthDynamic K.LengthAtom where
	LengthDynAtom = Length (Atom algn v nm) -> Length ('Dynamic n (Atom algn v nm))
forall (kobj :: O) (n :: Alignment).
Length kobj -> Length ('Dynamic n kobj)
LengthDynamic Length (Atom algn v nm)
forall (algn :: Alignment) t (nm :: Maybe Symbol).
Length ('O algn nm 'AtomT t)
K.LengthAtom

pattern LengthDynList :: Device.M.Size -> Length ('Dynamic n (K.List algn v nm))
pattern $mLengthDynList :: forall {r} {n :: Alignment} {algn :: Alignment} {v} {nm :: Symbol}.
Length ('Dynamic n (List algn v nm))
-> (Size -> r) -> ((# #) -> r) -> r
$bLengthDynList :: forall (n :: Alignment) (algn :: Alignment) v (nm :: Symbol).
Size -> Length ('Dynamic n (List algn v nm))
LengthDynList n <- LengthDynamic (K.LengthList n) where
	LengthDynList Size
n = Length (List algn v nm) -> Length ('Dynamic n (List algn v nm))
forall (kobj :: O) (n :: Alignment).
Length kobj -> Length ('Dynamic n kobj)
LengthDynamic (Size -> Length (List algn v nm)
forall (algn :: Alignment) (mnm :: Maybe Symbol) t.
Size -> Length ('O algn mnm 'ListT t)
K.LengthList Size
n)

pattern LengthDynImage ::
	Device.M.Size -> Device.M.Size -> Device.M.Size -> Device.M.Size -> Device.M.Size -> Length ('Dynamic n (K.Image algn v nm))
pattern $mLengthDynImage :: forall {r} {n :: Alignment} {algn :: Alignment} {v} {nm :: Symbol}.
Length ('Dynamic n (Image algn v nm))
-> (Size -> Size -> Size -> Size -> Size -> r) -> ((# #) -> r) -> r
$bLengthDynImage :: forall (n :: Alignment) (algn :: Alignment) v (nm :: Symbol).
Size
-> Size
-> Size
-> Size
-> Size
-> Length ('Dynamic n (Image algn v nm))
LengthDynImage kr kw kh kd klc <- (LengthDynamic (K.LengthImage kr kw kh kd klc))
	where LengthDynImage Size
kr Size
kw Size
kh Size
kd Size
klc = Length (Image algn v nm) -> Length ('Dynamic n (Image algn v nm))
forall (kobj :: O) (n :: Alignment).
Length kobj -> Length ('Dynamic n kobj)
LengthDynamic (Size -> Size -> Size -> Size -> Size -> Length (Image algn v nm)
forall (algn :: Alignment) (mnm :: Maybe Symbol) t.
Size
-> Size -> Size -> Size -> Size -> Length ('O algn mnm 'ImageT t)
K.LengthImage Size
kr Size
kw Size
kh Size
kd Size
klc)

class LengthOf (obj :: O) (objs :: [O]) where
	lengthOf :: HeteroParList.PL Length objs -> Length obj

instance LengthOf obj (obj ': objs) where lengthOf :: PL Length (obj : objs) -> Length obj
lengthOf (Length s
ln :** PL Length ss1
_) = Length obj
Length s
ln

instance {-# OVERLAPPABLE #-} LengthOf obj objs =>
	LengthOf obj (obj' ': objs) where
	lengthOf :: PL Length (obj' : objs) -> Length obj
lengthOf (Length s
_ :** PL Length ss1
lns) = forall (obj :: O) (objs :: [O]).
LengthOf obj objs =>
PL Length objs -> Length obj
lengthOf @obj PL Length ss1
lns

-- ONLY DYNAMIC LENGTH

class OnlyDynamicLengths (objs :: [O]) where
	type OnlyDynamics objs :: [K.O]
	onlyDynamicLength ::
		HeteroParList.PL Length objs ->
		HeteroParList.PL K.Length (OnlyDynamics objs)

instance OnlyDynamicLengths '[] where
	type OnlyDynamics '[] = '[]
	onlyDynamicLength :: PL Length '[] -> PL Length (OnlyDynamics '[])
onlyDynamicLength PL Length '[]
HeteroParList.Nil = PL Length '[]
PL Length (OnlyDynamics '[])
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance OnlyDynamicLengths objs => OnlyDynamicLengths ('Static_ _o ': objs) where
	type OnlyDynamics ('Static_ _o ': objs) = OnlyDynamics objs
	onlyDynamicLength :: PL Length ('Static_ _o : objs)
-> PL Length (OnlyDynamics ('Static_ _o : objs))
onlyDynamicLength (LengthStatic Length kobj
_ :** PL Length ss1
lns) = PL Length ss1 -> PL Length (OnlyDynamics ss1)
forall (objs :: [O]).
OnlyDynamicLengths objs =>
PL Length objs -> PL Length (OnlyDynamics objs)
onlyDynamicLength PL Length ss1
lns

instance OnlyDynamicLengths objs => OnlyDynamicLengths ('Dynamic _n o ': objs) where
	type OnlyDynamics ('Dynamic _n o ': objs) = o ': OnlyDynamics objs
	onlyDynamicLength :: PL Length ('Dynamic _n o : objs)
-> PL Length (OnlyDynamics ('Dynamic _n o : objs))
onlyDynamicLength (LengthDynamic Length kobj
ln :** PL Length ss1
lns) =
		Length kobj
ln Length kobj
-> PL Length (OnlyDynamics objs)
-> PL Length (kobj : OnlyDynamics objs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:** PL Length ss1 -> PL Length (OnlyDynamics ss1)
forall (objs :: [O]).
OnlyDynamicLengths objs =>
PL Length objs -> PL Length (OnlyDynamics objs)
onlyDynamicLength PL Length ss1
lns

-- STORE

class Store v obj where
	store :: Ptr (TypeOf obj) -> Length obj -> v -> IO ()
	load :: Ptr (TypeOf obj) -> Length obj -> IO v
	length :: v -> Length obj

instance K.Store v bobj => Store v (Static_ bobj) where
	store :: Ptr (TypeOf ('Static_ bobj))
-> Length ('Static_ bobj) -> v -> IO ()
store Ptr (TypeOf ('Static_ bobj))
p (LengthStatic Length kobj
kln) = Ptr (TypeOf kobj) -> Length kobj -> v -> IO ()
forall v (obj :: O).
Store v obj =>
Ptr (TypeOf obj) -> Length obj -> v -> IO ()
K.store Ptr (TypeOf kobj)
Ptr (TypeOf ('Static_ bobj))
p Length kobj
kln
	load :: Ptr (TypeOf ('Static_ bobj)) -> Length ('Static_ bobj) -> IO v
load Ptr (TypeOf ('Static_ bobj))
p (LengthStatic Length kobj
kln) = Ptr (TypeOf kobj) -> Length kobj -> IO v
forall v (obj :: O).
Store v obj =>
Ptr (TypeOf obj) -> Length obj -> IO v
K.load Ptr (TypeOf kobj)
Ptr (TypeOf ('Static_ bobj))
p Length kobj
kln
	length :: v -> Length ('Static_ bobj)
length = Length bobj -> Length ('Static_ bobj)
forall (kobj :: O). Length kobj -> Length ('Static_ kobj)
LengthStatic (Length bobj -> Length ('Static_ bobj))
-> (v -> Length bobj) -> v -> Length ('Static_ bobj)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Length bobj
forall v (obj :: O). Store v obj => v -> Length obj
K.length

instance (KnownNat n, K.Store v bobj) => Store [Maybe v] ('Dynamic n bobj) where
	store :: Ptr (TypeOf ('Dynamic n bobj))
-> Length ('Dynamic n bobj) -> [Maybe v] -> IO ()
store Ptr (TypeOf ('Dynamic n bobj))
p0 (LengthDynamic Length kobj
kln) =
		Ptr (TypeOf bobj) -> Alignment -> [Maybe v] -> IO ()
go Ptr (TypeOf bobj)
Ptr (TypeOf ('Dynamic n bobj))
p0 (Proxy n -> Alignment
forall (n :: Alignment) (proxy :: Alignment -> *).
KnownNat n =>
proxy n -> Alignment
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
		where
		go :: Ptr (TypeOf bobj) -> Alignment -> [Maybe v] -> IO ()
go Ptr (TypeOf bobj)
_ Alignment
_ [] = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
		go Ptr (TypeOf bobj)
_ Alignment
n [Maybe v]
_ | Alignment
n Alignment -> Alignment -> Bool
forall a. Ord a => a -> a -> Bool
< Alignment
1 = () -> IO ()
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
		go Ptr (TypeOf bobj)
p Alignment
n (Just v
x : [Maybe v]
xs) = do
			Ptr (TypeOf kobj) -> Length kobj -> v -> IO ()
forall v (obj :: O).
Store v obj =>
Ptr (TypeOf obj) -> Length obj -> v -> IO ()
K.store Ptr (TypeOf bobj)
Ptr (TypeOf kobj)
p Length kobj
kln v
x IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Ptr (TypeOf bobj) -> Alignment -> [Maybe v] -> IO ()
go (Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
forall (kobj :: O).
SizeAlignment kobj =>
Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
nextObject Ptr (TypeOf bobj)
Ptr (TypeOf kobj)
p Length kobj
kln) (Alignment
n Alignment -> Alignment -> Alignment
forall a. Num a => a -> a -> a
- Alignment
1) [Maybe v]
xs
		go Ptr (TypeOf bobj)
p Alignment
n (Maybe v
Nothing : [Maybe v]
xs) = do
			Ptr (TypeOf bobj) -> Alignment -> [Maybe v] -> IO ()
go (Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
forall (kobj :: O).
SizeAlignment kobj =>
Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
nextObject Ptr (TypeOf bobj)
Ptr (TypeOf kobj)
p Length kobj
kln) (Alignment
n Alignment -> Alignment -> Alignment
forall a. Num a => a -> a -> a
- Alignment
1) [Maybe v]
xs
	load :: Ptr (TypeOf ('Dynamic n bobj))
-> Length ('Dynamic n bobj) -> IO [Maybe v]
load Ptr (TypeOf ('Dynamic n bobj))
p0 (LengthDynamic Length kobj
kln) = Ptr (TypeOf bobj) -> Alignment -> IO [Maybe v]
go Ptr (TypeOf bobj)
Ptr (TypeOf ('Dynamic n bobj))
p0 (Proxy n -> Alignment
forall (n :: Alignment) (proxy :: Alignment -> *).
KnownNat n =>
proxy n -> Alignment
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n))
		where
		go :: Ptr (TypeOf bobj) -> Alignment -> IO [Maybe v]
go Ptr (TypeOf bobj)
_ Alignment
n | Alignment
n Alignment -> Alignment -> Bool
forall a. Ord a => a -> a -> Bool
< Alignment
1 = [Maybe v] -> IO [Maybe v]
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure []
		go Ptr (TypeOf bobj)
p Alignment
n = (:) (Maybe v -> [Maybe v] -> [Maybe v])
-> IO (Maybe v) -> IO ([Maybe v] -> [Maybe v])
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (v -> Maybe v
forall a. a -> Maybe a
Just (v -> Maybe v) -> IO v -> IO (Maybe v)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Ptr (TypeOf kobj) -> Length kobj -> IO v
forall v (obj :: O).
Store v obj =>
Ptr (TypeOf obj) -> Length obj -> IO v
K.load Ptr (TypeOf bobj)
Ptr (TypeOf kobj)
p Length kobj
kln) IO ([Maybe v] -> [Maybe v]) -> IO [Maybe v] -> IO [Maybe v]
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Ptr (TypeOf bobj) -> Alignment -> IO [Maybe v]
go (Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
forall (kobj :: O).
SizeAlignment kobj =>
Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
nextObject Ptr (TypeOf bobj)
Ptr (TypeOf kobj)
p Length kobj
kln) (Alignment
n Alignment -> Alignment -> Alignment
forall a. Num a => a -> a -> a
- Alignment
1)
	length :: [Maybe v] -> Length ('Dynamic n bobj)
length = Length bobj -> Length ('Dynamic n bobj)
forall (kobj :: O) (n :: Alignment).
Length kobj -> Length ('Dynamic n kobj)
LengthDynamic (Length bobj -> Length ('Dynamic n bobj))
-> ([Maybe v] -> Length bobj)
-> [Maybe v]
-> Length ('Dynamic n bobj)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. v -> Length bobj
forall v (obj :: O). Store v obj => v -> Length obj
K.length (v -> Length bobj) -> ([Maybe v] -> v) -> [Maybe v] -> Length bobj
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Maybe v -> v
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe v -> v) -> ([Maybe v] -> Maybe v) -> [Maybe v] -> v
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Maybe v] -> Maybe v
forall a. HasCallStack => [a] -> a
head

nextObject :: forall kobj . K.SizeAlignment kobj =>
	Ptr (K.TypeOf kobj) -> K.Length kobj -> Ptr (K.TypeOf kobj)
nextObject :: forall (kobj :: O).
SizeAlignment kobj =>
Ptr (TypeOf kobj) -> Length kobj -> Ptr (TypeOf kobj)
nextObject Ptr (TypeOf kobj)
p Length kobj
ln = Ptr (TypeOf kobj)
p Ptr (TypeOf kobj) -> Int -> Ptr (TypeOf kobj)
forall a b. Ptr a -> Int -> Ptr b
`plusPtr` Size -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Size
n
	where
	n :: Size
n = ((Length kobj -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
K.size Length kobj
ln Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1) Size -> Size -> Size
forall a. Integral a => a -> a -> a
`div` Size
algn Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
algn
	algn :: Size
algn = forall (obj :: O). SizeAlignment obj => Size
K.alignment @kobj

-- SIZE, ALIGNMENT AND OFFSET

-- WholeSize

wholeSize :: SizeAlignmentList objs =>
	HeteroParList.PL Length objs -> Size
wholeSize :: forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> Size
wholeSize = Size -> PL SizeAlignmentOf objs -> Size
forall (objs :: [O]). Size -> PL SizeAlignmentOf objs -> Size
wholeSizeFromSzAlgns Size
0 (PL SizeAlignmentOf objs -> Size)
-> (PL Length objs -> PL SizeAlignmentOf objs)
-> PL Length objs
-> Size
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PL Length objs -> PL SizeAlignmentOf objs
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> PL SizeAlignmentOf objs
sizeAlignmentList

wholeSizeFromSzAlgns ::
	Size -> HeteroParList.PL SizeAlignmentOf objs -> Size
wholeSizeFromSzAlgns :: forall (objs :: [O]). Size -> PL SizeAlignmentOf objs -> Size
wholeSizeFromSzAlgns Size
sz0 PL SizeAlignmentOf objs
HeteroParList.Nil = Size
sz0
wholeSizeFromSzAlgns Size
sz0 (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
saoo) =
	Size -> PL SizeAlignmentOf ss1 -> Size
forall (objs :: [O]). Size -> PL SizeAlignmentOf objs -> Size
wholeSizeFromSzAlgns (Size -> Size -> Size
adjust Size
algn Size
sz0 Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf ss1
saoo

class WholeAlign (objs :: [O]) where wholeAlign :: Size

instance WholeAlign '[] where wholeAlign :: Size
wholeAlign = Size
1

instance (SizeAlignment obj, WholeAlign objs) =>
	WholeAlign (obj ': objs) where
	wholeAlign :: Size
wholeAlign = forall (obj :: O). SizeAlignment obj => Size
alignment @obj Size -> Size -> Size
forall a. Integral a => a -> a -> a
`lcm` forall (objs :: [O]). WholeAlign objs => Size
wholeAlign @objs

-- OffsetRange

offsetRange :: forall obj objs i . OffsetRange obj objs i => Device.M.Size ->
	HeteroParList.PL Length objs -> (Device.M.Size, Device.M.Size)
offsetRange :: forall (obj :: O) (objs :: [O]) (i :: Alignment).
OffsetRange obj objs i =>
Size -> PL Length objs -> (Size, Size)
offsetRange Size
ost0 PL Length objs
lns = forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetRangeFromSzAlgns' @obj @_ @i Size
ost0 (PL SizeAlignmentOf objs -> (Size, Size))
-> PL SizeAlignmentOf objs -> (Size, Size)
forall a b. (a -> b) -> a -> b
$ PL Length objs -> PL SizeAlignmentOf objs
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> PL SizeAlignmentOf objs
sizeAlignmentList PL Length objs
lns

offsetSize :: forall obj objs i . OffsetRange obj objs i => Device.M.Size ->
	HeteroParList.PL Length objs -> (Device.M.Size, Device.M.Size)
offsetSize :: forall (obj :: O) (objs :: [O]) (i :: Alignment).
OffsetRange obj objs i =>
Size -> PL Length objs -> (Size, Size)
offsetSize Size
ost0 PL Length objs
lns = forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetSizeFromSzAlgns' @obj @_ @i Size
ost0 (PL SizeAlignmentOf objs -> (Size, Size))
-> PL SizeAlignmentOf objs -> (Size, Size)
forall a b. (a -> b) -> a -> b
$ PL Length objs -> PL SizeAlignmentOf objs
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> PL SizeAlignmentOf objs
sizeAlignmentList PL Length objs
lns

class (SizeAlignmentList vs, HeteroParList.TypeIndex v vs) =>
	OffsetRange (v :: O) (vs :: [O]) (i :: Nat) where
	offsetRangeFromSzAlgns' ::
		Device.M.Size -> HeteroParList.PL SizeAlignmentOf vs ->
		(Device.M.Size, Device.M.Size)
	offsetSizeFromSzAlgns' ::
		Device.M.Size -> HeteroParList.PL SizeAlignmentOf vs ->
		(Device.M.Size, Device.M.Size)

instance (SizeAlignment v, SizeAlignmentList vs) =>
	OffsetRange v (v ': vs) 0 where
	offsetRangeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v : vs) -> (Size, Size)
offsetRangeFromSzAlgns' Size
ost (SizeAlignmentOf Size
_dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
_) =
		(Size -> Size -> Size
adjust Size
algn Size
ost, Size
sz)
	offsetSizeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v : vs) -> (Size, Size)
offsetSizeFromSzAlgns' Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
_) =
		(Size -> Size -> Size
adjust Size
algn Size
ost, Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz)

instance {-# OVERLAPPABLE #-}
	(SizeAlignment v, OffsetRange v vs (i - 1)) =>
	OffsetRange v (v ': vs) i where
	offsetRangeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v : vs) -> (Size, Size)
offsetRangeFromSzAlgns' Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
sas) =
		forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetRangeFromSzAlgns' @v @vs @(i - 1) (Size -> Size -> Size
adjust Size
algn Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf vs
PL SizeAlignmentOf ss1
sas
	offsetSizeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v : vs) -> (Size, Size)
offsetSizeFromSzAlgns' Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
sas) =
		forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetSizeFromSzAlgns' @v @vs @(i - 1) (Size -> Size -> Size
adjust Size
algn Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf vs
PL SizeAlignmentOf ss1
sas

instance {-# OVERLAPPABLE #-} (SizeAlignment v', OffsetRange v vs i) =>
	OffsetRange v (v' ': vs) i where
	offsetRangeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v' : vs) -> (Size, Size)
offsetRangeFromSzAlgns' Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
sas) =
		forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetRangeFromSzAlgns' @v @vs @i (Size -> Size -> Size
adjust Size
algn Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf vs
PL SizeAlignmentOf ss1
sas
	offsetSizeFromSzAlgns' :: Size -> PL SizeAlignmentOf (v' : vs) -> (Size, Size)
offsetSizeFromSzAlgns' Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
sas) =
		forall (v :: O) (vs :: [O]) (i :: Alignment).
OffsetRange v vs i =>
Size -> PL SizeAlignmentOf vs -> (Size, Size)
offsetSizeFromSzAlgns' @v @vs @i (Size -> Size -> Size
adjust Size
algn Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf vs
PL SizeAlignmentOf ss1
sas

-- OffsetOfList

offsetOfList :: forall v onm vs . OffsetOfList v onm vs =>
	HeteroParList.PL Length vs -> (Device.M.Size, Device.M.Size)
offsetOfList :: forall {k} (v :: k) (onm :: Symbol) (vs :: [O]).
OffsetOfList v onm vs =>
PL Length vs -> (Size, Size)
offsetOfList = forall (v :: k) (nm :: Symbol) (objs :: [O]).
OffsetOfList v nm objs =>
Size -> PL SizeAlignmentOf objs -> (Size, Size)
forall {k} (v :: k) (nm :: Symbol) (objs :: [O]).
OffsetOfList v nm objs =>
Size -> PL SizeAlignmentOf objs -> (Size, Size)
offsetRangeListFromSzAlgns @v @onm Size
0 (PL SizeAlignmentOf vs -> (Size, Size))
-> (PL Length vs -> PL SizeAlignmentOf vs)
-> PL Length vs
-> (Size, Size)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PL Length vs -> PL SizeAlignmentOf vs
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> PL SizeAlignmentOf objs
sizeAlignmentList

class SizeAlignmentList objs =>
	OffsetOfList v (nm :: Symbol) (objs :: [O]) where
	offsetRangeListFromSzAlgns ::
		Device.M.Size -> HeteroParList.PL SizeAlignmentOf objs ->
		(Device.M.Size, Device.M.Size)

instance (Storable v, KnownNat oalgn, SizeAlignmentList objs) =>
	OffsetOfList v nm (List oalgn v nm ': objs) where
	offsetRangeListFromSzAlgns :: Size -> PL SizeAlignmentOf (List oalgn v nm : objs) -> (Size, Size)
offsetRangeListFromSzAlgns Size
ost (SizeAlignmentOf Size
_ Size
sz Size
algn :** PL SizeAlignmentOf ss1
_) =
		(Size -> Size -> Size
adjust Size
algn Size
ost, Size
sz)

instance {-# OVERLAPPABLE #-} (SizeAlignment obj, OffsetOfList v nm objs) =>
	OffsetOfList v nm (obj ': objs) where
	offsetRangeListFromSzAlgns :: Size -> PL SizeAlignmentOf (obj : objs) -> (Size, Size)
offsetRangeListFromSzAlgns Size
ost (SizeAlignmentOf Size
dn Size
sz Size
algn :** PL SizeAlignmentOf ss1
sas) =
		forall (v :: k) (nm :: Symbol) (objs :: [O]).
OffsetOfList v nm objs =>
Size -> PL SizeAlignmentOf objs -> (Size, Size)
forall {k} (v :: k) (nm :: Symbol) (objs :: [O]).
OffsetOfList v nm objs =>
Size -> PL SizeAlignmentOf objs -> (Size, Size)
offsetRangeListFromSzAlgns
			@v @nm @objs (Size -> Size -> Size
adjust Size
algn Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
dn Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
sz) PL SizeAlignmentOf objs
PL SizeAlignmentOf ss1
sas

adjust :: Device.M.Size -> Device.M.Size -> Device.M.Size
adjust :: Size -> Size -> Size
adjust Size
algn Size
ost = ((Size
ost Size -> Size -> Size
forall a. Num a => a -> a -> a
- Size
1) Size -> Size -> Size
forall a. Integral a => a -> a -> a
`div` Size
algn Size -> Size -> Size
forall a. Num a => a -> a -> a
+ Size
1) Size -> Size -> Size
forall a. Num a => a -> a -> a
* Size
algn

-- SizeAlignmentList

data SizeAlignmentOf (obj :: O) = SizeAlignmentOf DynNum Size ObjAlignment
	deriving Int -> SizeAlignmentOf obj -> ShowS
[SizeAlignmentOf obj] -> ShowS
SizeAlignmentOf obj -> String
(Int -> SizeAlignmentOf obj -> ShowS)
-> (SizeAlignmentOf obj -> String)
-> ([SizeAlignmentOf obj] -> ShowS)
-> Show (SizeAlignmentOf obj)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (obj :: O). Int -> SizeAlignmentOf obj -> ShowS
forall (obj :: O). [SizeAlignmentOf obj] -> ShowS
forall (obj :: O). SizeAlignmentOf obj -> String
$cshowsPrec :: forall (obj :: O). Int -> SizeAlignmentOf obj -> ShowS
showsPrec :: Int -> SizeAlignmentOf obj -> ShowS
$cshow :: forall (obj :: O). SizeAlignmentOf obj -> String
show :: SizeAlignmentOf obj -> String
$cshowList :: forall (obj :: O). [SizeAlignmentOf obj] -> ShowS
showList :: [SizeAlignmentOf obj] -> ShowS
Show

type DynNum = Device.M.Size
type Size = Device.M.Size
type ObjAlignment = Device.M.Size

class SizeAlignmentList objs where
	sizeAlignmentListWholeAlignment :: ObjAlignment
	sizeAlignmentList :: HeteroParList.PL Length objs ->
		HeteroParList.PL SizeAlignmentOf objs

instance SizeAlignmentList '[] where
	sizeAlignmentListWholeAlignment :: Size
sizeAlignmentListWholeAlignment = Size
1
	sizeAlignmentList :: PL Length '[] -> PL SizeAlignmentOf '[]
sizeAlignmentList PL Length '[]
HeteroParList.Nil = PL SizeAlignmentOf '[]
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil

instance (SizeAlignment obj, SizeAlignmentList objs) =>
	SizeAlignmentList (obj ': objs) where
	sizeAlignmentListWholeAlignment :: Size
sizeAlignmentListWholeAlignment =
		forall (obj :: O). SizeAlignment obj => Size
alignment @obj Size -> Size -> Size
forall a. Integral a => a -> a -> a
`lcm` forall (objs :: [O]). SizeAlignmentList objs => Size
sizeAlignmentListWholeAlignment @objs
	sizeAlignmentList :: PL Length (obj : objs) -> PL SizeAlignmentOf (obj : objs)
sizeAlignmentList (Length s
ln :** PL Length ss1
lns) =
		Size -> Size -> Size -> SizeAlignmentOf obj
forall (obj :: O). Size -> Size -> Size -> SizeAlignmentOf obj
SizeAlignmentOf
			(forall (obj :: O). SizeAlignment obj => Size
dynNum @obj) (Length s -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
size Length s
ln) (forall (obj :: O). SizeAlignment obj => Size
alignment @obj) SizeAlignmentOf obj
-> PL SizeAlignmentOf objs -> PL SizeAlignmentOf (obj : objs)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
:**
		PL Length objs -> PL SizeAlignmentOf objs
forall (objs :: [O]).
SizeAlignmentList objs =>
PL Length objs -> PL SizeAlignmentOf objs
sizeAlignmentList PL Length objs
PL Length ss1
lns

-- SizeAlignment

class SizeAlignment obj where
	dynNum :: Device.M.Size
	size :: Length obj -> Device.M.Size
	alignment :: Device.M.Size

instance K.SizeAlignment kobj => SizeAlignment (Static_ kobj) where
	dynNum :: Size
dynNum = Size
1
	size :: Length ('Static_ kobj) -> Size
size (LengthStatic Length kobj
kln) = Length kobj -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
K.size Length kobj
kln
	alignment :: Size
alignment = forall (obj :: O). SizeAlignment obj => Size
K.alignment @kobj

instance (KnownNat n, K.SizeAlignment kobj) =>
	SizeAlignment ('Dynamic n kobj) where
	dynNum :: Size
dynNum = Alignment -> Size
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Alignment -> Size) -> Alignment -> Size
forall a b. (a -> b) -> a -> b
$ Proxy n -> Alignment
forall (n :: Alignment) (proxy :: Alignment -> *).
KnownNat n =>
proxy n -> Alignment
natVal (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)
	size :: Length ('Dynamic n kobj) -> Size
size (LengthDynamic Length kobj
kln) = Length kobj -> Size
forall (obj :: O). SizeAlignment obj => Length obj -> Size
K.size Length kobj
kln
	alignment :: Size
alignment = forall (obj :: O). SizeAlignment obj => Size
K.alignment @kobj