{-# LANGUAGE ImportQualifiedPost #-}
{-# LANGUAGE BlockArguments, 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 (
allocateDs, D, AllocateInfo(..), DListFromMiddle, DefaultDynamicLengths,
Group, group, allocateDs', unsafeFreeDs, lookup,
updateDs,
W.Write(..), W.WriteListToMiddle,
W.WriteListUpdateDynamicLengths, W.UpdateDynamicLength,
W.WriteSources(..), W.WriteSourcesArg(..),
W.WriteSourcesToMiddle,
Copy(..), CopyListToMiddle,
BindingAndArrayElem, W.BindingAndArrayElemImage,
W.BindingAndArrayElemImageWithImmutableSampler,
W.BindingAndArrayElemBuffer, W.BindingAndArrayElemBufferView
) where
import Prelude hiding (lookup)
import Foreign.Storable.PeekPoke
import Data.Default
import Data.TypeLevel.Maybe qualified as TMaybe
import Data.TypeLevel.Tuple.Uncurry
import Data.TypeLevel.Tuple.Index qualified as TIndex
import qualified Data.HeteroParList as HeteroParList
import Data.HeteroParList (pattern (:**))
import Gpu.Vulkan.DescriptorSet.Type
import qualified Gpu.Vulkan.Device.Type as Device
import qualified Gpu.Vulkan.DescriptorPool.Type as Descriptor.Pool
import qualified Gpu.Vulkan.DescriptorSetLayout.Type as Layout
import qualified Gpu.Vulkan.DescriptorSetLayout.Middle as Layout.M
import qualified Gpu.Vulkan.DescriptorSet.Write as W
import qualified Gpu.Vulkan.DescriptorSet.Middle as M
import Gpu.Vulkan.DescriptorSet.Copy
import Gpu.Vulkan.Object.Base qualified as KObj
import Control.Concurrent.STM
import Control.Concurrent.STM.TSem
import Data.Map qualified as Map
import Data.IORef.ToolsYj
import Data.TypeLevel.Tuple.MapIndex qualified
import Control.Monad
import Debug
layoutToMiddle :: U2 Layout.D slbts -> Layout.M.D
layoutToMiddle :: forall (slbts :: (*, [BindingType])). U2 D slbts -> D
layoutToMiddle (U2 (Layout.D D
l)) = D
l
data AllocateInfo mn sp slbtss = AllocateInfo {
forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> M mn
allocateInfoNext :: TMaybe.M mn,
forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> P sp
allocateInfoDescriptorPool :: Descriptor.Pool.P sp,
forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> PL (U2 D) slbtss
allocateInfoSetLayouts :: HeteroParList.PL (U2 Layout.D) slbtss }
deriving instance (Show (TMaybe.M n), Show (HeteroParList.PL (U2 Layout.D) slbtss)) =>
Show (AllocateInfo n sp slbtss)
allocateInfoToMiddle :: AllocateInfo n sp slbtss -> M.AllocateInfo n
allocateInfoToMiddle :: forall (n :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo n sp slbtss -> AllocateInfo n
allocateInfoToMiddle AllocateInfo {
allocateInfoNext :: forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> M mn
allocateInfoNext = M n
mnxt,
allocateInfoDescriptorPool :: forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> P sp
allocateInfoDescriptorPool = Descriptor.Pool.P D
dp,
allocateInfoSetLayouts :: forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> PL (U2 D) slbtss
allocateInfoSetLayouts = PL (U2 D) slbtss
dscsls
} = M.AllocateInfo {
allocateInfoNext :: M n
M.allocateInfoNext = M n
mnxt,
allocateInfoDescriptorPool :: D
M.allocateInfoDescriptorPool = D
dp,
allocateInfoSetLayouts :: [D]
M.allocateInfoSetLayouts =
(forall (slbts :: (*, [BindingType])). U2 D slbts -> D)
-> PL (U2 D) slbtss -> [D]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
HeteroParList.toList U2 D s -> D
forall (slbts :: (*, [BindingType])). U2 D slbts -> D
layoutToMiddle PL (U2 D) slbtss
dscsls }
class DListFromMiddle slbtss where
dListFromMiddle :: [M.D] -> IO (HeteroParList.PL (D s) slbtss)
instance DListFromMiddle '[] where
dListFromMiddle :: forall s. [D] -> IO (PL (D s) '[])
dListFromMiddle = \case [] -> PL (D s) '[] -> IO (PL (D s) '[])
forall a. a -> IO a
forall (f :: * -> *) a. Applicative f => a -> f a
pure PL (D s) '[]
forall {k} (t :: k -> *). PL t '[]
HeteroParList.Nil; [D]
_ -> String -> IO (PL (D s) '[])
forall a. HasCallStack => String -> a
error String
"bad"
instance (
DefaultDynamicLengths slbts,
DListFromMiddle slbtss ) =>
DListFromMiddle (slbts ': slbtss) where
dListFromMiddle :: forall s. [D] -> IO (PL (D s) (slbts : slbtss))
dListFromMiddle = \case
(D
d : [D]
ds) -> D s slbts -> PL (D s) slbtss -> PL (D s) (slbts : slbtss)
forall {k} (t :: k -> *) (s :: k) (ss1 :: [k]).
t s -> PL t ss1 -> PL t (s : ss1)
(:**)
(D s slbts -> PL (D s) slbtss -> PL (D s) (slbts : slbtss))
-> IO (D s slbts)
-> IO (PL (D s) slbtss -> PL (D s) (slbts : slbtss))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> ((IORef (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts)))
-> D -> D s slbts
forall s (slbts :: (*, [BindingType])).
IORef (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts)))
-> D -> D s slbts
`D` D
d) (IORef
(PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts)))
-> D s slbts)
-> IO
(IORef
(PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts))))
-> IO (D s slbts)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IO
(IORef
(PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 slbts))))
forall a. Default a => IO (IORef a)
newDefaultIORef)
IO (PL (D s) slbtss -> PL (D s) (slbts : slbtss))
-> IO (PL (D s) slbtss) -> IO (PL (D s) (slbts : slbtss))
forall a b. IO (a -> b) -> IO a -> IO b
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> forall (slbtss :: [(*, [BindingType])]) s.
DListFromMiddle slbtss =>
[D] -> IO (PL (D s) slbtss)
dListFromMiddle @slbtss [D]
ds
[D]
_ -> String -> IO (PL (D s) (slbts : slbtss))
forall a. HasCallStack => String -> a
error String
"bad"
type DefaultDynamicLengths slbts = Default
(HeteroParList.PL
(HeteroParList.PL KObj.Length)
(Layout.BindingTypeListBufferOnlyDynamics (TIndex.I1_2 slbts)))
allocateDs :: (WithPoked (TMaybe.M mn), DListFromMiddle slbtss) =>
Device.D sd -> AllocateInfo mn sp slbtss ->
(forall s . HeteroParList.PL (D s) slbtss -> IO a) -> IO a
allocateDs :: forall (mn :: Maybe (*)) (slbtss :: [(*, [BindingType])]) sd sp a.
(WithPoked (M mn), DListFromMiddle slbtss) =>
D sd
-> AllocateInfo mn sp slbtss
-> (forall s. PL (D s) slbtss -> IO a)
-> IO a
allocateDs (Device.D D
dvc) AllocateInfo mn sp slbtss
ai forall s. PL (D s) slbtss -> IO a
f = do
dsm <- D -> AllocateInfo mn -> IO [D]
forall (mn :: Maybe (*)).
WithPoked (M mn) =>
D -> AllocateInfo mn -> IO [D]
M.allocateDs D
dvc (AllocateInfo mn sp slbtss -> AllocateInfo mn
forall (n :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo n sp slbtss -> AllocateInfo n
allocateInfoToMiddle AllocateInfo mn sp slbtss
ai)
ds <- dListFromMiddle dsm
f ds <* M.freeDs dvc
((\(Descriptor.Pool.P D
p) -> D
p) $ allocateInfoDescriptorPool ai)
dsm
data Group sd s k sp slbtss = Group (Device.D sd) TSem
(TVar (Map.Map k (Descriptor.Pool.P sp, HeteroParList.PL (D s) slbtss)))
group :: Device.D sd -> (forall s . Group sd s k sp slbtss -> IO a) -> IO a
group :: forall sd k sp (slbtss :: [(*, [BindingType])]) a.
D sd -> (forall s. Group sd s k sp slbtss -> IO a) -> IO a
group dv :: D sd
dv@(Device.D D
mdvc) forall s. Group sd s k sp slbtss -> IO a
f = do
(sem, dsss) <- STM (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
-> IO (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
forall a. STM a -> IO a
atomically (STM (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
-> IO (TSem, TVar (Map k (P sp, PL (D Any) slbtss))))
-> STM (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
-> IO (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
forall a b. (a -> b) -> a -> b
$ (,) (TSem
-> TVar (Map k (P sp, PL (D Any) slbtss))
-> (TSem, TVar (Map k (P sp, PL (D Any) slbtss))))
-> STM TSem
-> STM
(TVar (Map k (P sp, PL (D Any) slbtss))
-> (TSem, TVar (Map k (P sp, PL (D Any) slbtss))))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Integer -> STM TSem
newTSem Integer
1 STM
(TVar (Map k (P sp, PL (D Any) slbtss))
-> (TSem, TVar (Map k (P sp, PL (D Any) slbtss))))
-> STM (TVar (Map k (P sp, PL (D Any) slbtss)))
-> STM (TSem, TVar (Map k (P sp, PL (D Any) slbtss)))
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 (P sp, PL (D Any) slbtss)
-> STM (TVar (Map k (P sp, PL (D Any) slbtss)))
forall a. a -> STM (TVar a)
newTVar Map k (P sp, PL (D Any) slbtss)
forall k a. Map k a
Map.empty
rtn <- f $ Group dv sem dsss
((\(Descriptor.Pool.P D
dsp, PL (D Any) slbtss
dss) -> D -> D -> [D] -> IO ()
M.freeDs D
mdvc D
dsp ([D] -> IO ()) -> [D] -> IO ()
forall a b. (a -> b) -> a -> b
$ PL (D Any) slbtss -> [D]
forall s (slbtss :: [(*, [BindingType])]). PL (D s) slbtss -> [D]
dListToMiddle PL (D Any) slbtss
dss) `mapM_`) =<<
(Map.elems <$> atomically (readTVar dsss))
pure rtn
allocateDs' :: (Ord k, WithPoked (TMaybe.M mn), DListFromMiddle slbtss) =>
Group sd sg k sp slbtss -> k -> AllocateInfo mn sp slbtss ->
IO (Either String (HeteroParList.PL (D sg) slbtss))
allocateDs' :: forall k (mn :: Maybe (*)) (slbtss :: [(*, [BindingType])]) sd sg
sp.
(Ord k, WithPoked (M mn), DListFromMiddle slbtss) =>
Group sd sg k sp slbtss
-> k
-> AllocateInfo mn sp slbtss
-> IO (Either String (PL (D sg) slbtss))
allocateDs' (Group (Device.D D
dvc) TSem
sem TVar (Map k (P sp, PL (D sg) slbtss))
mp) k
k AllocateInfo mn sp slbtss
ai = do
ok <- STM Bool -> IO Bool
forall a. STM a -> IO a
atomically do
mx <- (k
-> Map k (P sp, PL (D sg) slbtss) -> Maybe (P sp, PL (D sg) slbtss)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k) (Map k (P sp, PL (D sg) slbtss) -> Maybe (P sp, PL (D sg) slbtss))
-> STM (Map k (P sp, PL (D sg) slbtss))
-> STM (Maybe (P sp, PL (D sg) slbtss))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (P sp, PL (D sg) slbtss))
-> STM (Map k (P sp, PL (D sg) slbtss))
forall a. TVar a -> STM a
readTVar TVar (Map k (P sp, PL (D sg) slbtss))
mp
case mx of
Maybe (P sp, PL (D sg) slbtss)
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 (P sp, PL (D sg) slbtss)
_ -> Bool -> STM Bool
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Bool
False
if ok
then do dsm <- M.allocateDs dvc (allocateInfoToMiddle ai)
ds <- dListFromMiddle dsm
atomically do
modifyTVar mp (Map.insert k (sp, ds))
signalTSem sem
pure $ Right ds
else pure . Left
$ "Gpu.Vulkan.DescriptorSet.allocateDs': The key already exist"
where sp :: P sp
sp = AllocateInfo mn sp slbtss -> P sp
forall (mn :: Maybe (*)) sp (slbtss :: [(*, [BindingType])]).
AllocateInfo mn sp slbtss -> P sp
allocateInfoDescriptorPool AllocateInfo mn sp slbtss
ai
unsafeFreeDs :: Ord k => Group sd sg k sp slbtss -> k -> IO (Either String ())
unsafeFreeDs :: forall k sd sg sp (slbtss :: [(*, [BindingType])]).
Ord k =>
Group sd sg k sp slbtss -> k -> IO (Either String ())
unsafeFreeDs (Group (Device.D D
mdvc) TSem
sem TVar (Map k (P sp, PL (D sg) slbtss))
mp) k
k = do
md <- STM (Maybe (P sp, PL (D sg) slbtss))
-> IO (Maybe (P sp, PL (D sg) slbtss))
forall a. STM a -> IO a
atomically do
mx <- k
-> Map k (P sp, PL (D sg) slbtss) -> Maybe (P sp, PL (D sg) slbtss)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k (Map k (P sp, PL (D sg) slbtss) -> Maybe (P sp, PL (D sg) slbtss))
-> STM (Map k (P sp, PL (D sg) slbtss))
-> STM (Maybe (P sp, PL (D sg) slbtss))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (P sp, PL (D sg) slbtss))
-> STM (Map k (P sp, PL (D sg) slbtss))
forall a. TVar a -> STM a
readTVar TVar (Map k (P sp, PL (D sg) slbtss))
mp
case mx of
Maybe (P sp, PL (D sg) slbtss)
Nothing -> Maybe (P sp, PL (D sg) slbtss)
-> STM (Maybe (P sp, PL (D sg) slbtss))
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (P sp, PL (D sg) slbtss)
forall a. Maybe a
Nothing
Just (P sp, PL (D sg) slbtss)
_ -> TSem -> STM ()
waitTSem TSem
sem STM ()
-> STM (Maybe (P sp, PL (D sg) slbtss))
-> STM (Maybe (P sp, PL (D sg) slbtss))
forall a b. STM a -> STM b -> STM b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Maybe (P sp, PL (D sg) slbtss)
-> STM (Maybe (P sp, PL (D sg) slbtss))
forall a. a -> STM a
forall (f :: * -> *) a. Applicative f => a -> f a
pure Maybe (P sp, PL (D sg) slbtss)
mx
case md of
Maybe (P sp, PL (D sg) slbtss)
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.DescriptorSet.unsafeFreeDs"
Just (Descriptor.Pool.P D
p, PL (D sg) slbtss
ds) -> do
D -> D -> [D] -> IO ()
M.freeDs D
mdvc D
p (PL (D sg) slbtss -> [D]
forall s (slbtss :: [(*, [BindingType])]). PL (D s) slbtss -> [D]
dListToMiddle PL (D sg) slbtss
ds)
STM (Either String ()) -> IO (Either String ())
forall a. STM a -> IO a
atomically do
TVar (Map k (P sp, PL (D sg) slbtss))
-> (Map k (P sp, PL (D sg) slbtss)
-> Map k (P sp, PL (D sg) slbtss))
-> STM ()
forall a. TVar a -> (a -> a) -> STM ()
modifyTVar TVar (Map k (P sp, PL (D sg) slbtss))
mp (k
-> Map k (P sp, PL (D sg) slbtss) -> Map k (P sp, PL (D sg) slbtss)
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 s k sp slbtss -> k -> IO (Maybe (HeteroParList.PL (D s) slbtss))
lookup :: forall k sd s sp (slbtss :: [(*, [BindingType])]).
Ord k =>
Group sd s k sp slbtss -> k -> IO (Maybe (PL (D s) slbtss))
lookup (Group D sd
_ TSem
_sem TVar (Map k (P sp, PL (D s) slbtss))
mp) k
k = STM (Maybe (PL (D s) slbtss)) -> IO (Maybe (PL (D s) slbtss))
forall a. STM a -> IO a
atomically (STM (Maybe (PL (D s) slbtss)) -> IO (Maybe (PL (D s) slbtss)))
-> STM (Maybe (PL (D s) slbtss)) -> IO (Maybe (PL (D s) slbtss))
forall a b. (a -> b) -> a -> b
$ ((P sp, PL (D s) slbtss) -> PL (D s) slbtss
forall a b. (a, b) -> b
snd ((P sp, PL (D s) slbtss) -> PL (D s) slbtss)
-> Maybe (P sp, PL (D s) slbtss) -> Maybe (PL (D s) slbtss)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$>) (Maybe (P sp, PL (D s) slbtss) -> Maybe (PL (D s) slbtss))
-> (Map k (P sp, PL (D s) slbtss) -> Maybe (P sp, PL (D s) slbtss))
-> Map k (P sp, PL (D s) slbtss)
-> Maybe (PL (D s) slbtss)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. k -> Map k (P sp, PL (D s) slbtss) -> Maybe (P sp, PL (D s) slbtss)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup k
k (Map k (P sp, PL (D s) slbtss) -> Maybe (PL (D s) slbtss))
-> STM (Map k (P sp, PL (D s) slbtss))
-> STM (Maybe (PL (D s) slbtss))
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> TVar (Map k (P sp, PL (D s) slbtss))
-> STM (Map k (P sp, PL (D s) slbtss))
forall a. TVar a -> STM a
readTVar TVar (Map k (P sp, PL (D s) slbtss))
mp
dListToMiddle :: HeteroParList.PL (D s) slbtss -> [M.D]
dListToMiddle :: forall s (slbtss :: [(*, [BindingType])]). PL (D s) slbtss -> [D]
dListToMiddle = (forall (s :: (*, [BindingType])). D s s -> D)
-> PL (D s) slbtss -> [D]
forall k (t :: k -> *) a (ss :: [k]).
(forall (s :: k). t s -> a) -> PL t ss -> [a]
HeteroParList.toList \(D IORef (PL2 Length (BindingTypeListBufferOnlyDynamics (I1_2 s)))
_ D
md) -> D
md
updateDs :: (
Show (HeteroParList.PL M.Write (Data.TypeLevel.Tuple.MapIndex.M0_5 writeArgs)),
W.WriteListToMiddle writeArgs,
W.WriteListUpdateDynamicLengths writeArgs,
CopyListToMiddle copyArgs) =>
Device.D sd ->
HeteroParList.PL (U5 W.Write) writeArgs ->
HeteroParList.PL (U8 Copy) copyArgs -> IO ()
updateDs :: forall (writeArgs :: [(Maybe (*), *, (*, [BindingType]),
WriteSourcesArg, Nat)])
(copyArgs :: [(Maybe (*), *, (*, [BindingType]), Nat, *,
(*, [BindingType]), Nat, BindingType)])
sd.
(Show (PL Write (M0_5 writeArgs)), WriteListToMiddle writeArgs,
WriteListUpdateDynamicLengths writeArgs,
CopyListToMiddle copyArgs) =>
D sd -> PL (U5 Write) writeArgs -> PL (U8 Copy) copyArgs -> IO ()
updateDs (Device.D D
dvc) PL (U5 Write) writeArgs
ws PL (U8 Copy) copyArgs
cs = Bool -> IO () -> IO ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when Bool
debug (PL Write (M0_5 writeArgs) -> IO ()
forall a. Show a => a -> IO ()
print PL Write (M0_5 writeArgs)
ws') 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) writeArgs -> IO ()
forall (wargs :: [(Maybe (*), *, (*, [BindingType]),
WriteSourcesArg, Nat)]).
WriteListUpdateDynamicLengths wargs =>
PL (U5 Write) wargs -> IO ()
W.writeListUpdateDynamicLength PL (U5 Write) writeArgs
ws IO () -> IO () -> IO ()
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> D -> PL Write (M0_5 writeArgs) -> PL Copy (M0_8 copyArgs) -> IO ()
forall (ws :: [Maybe (*)]) (cs :: [Maybe (*)]).
(WriteListToCore ws, CopyListToCore cs) =>
D -> PL Write ws -> PL Copy cs -> IO ()
M.updateDs D
dvc PL Write (M0_5 writeArgs)
ws' PL Copy (M0_8 copyArgs)
cs'
where ws' :: PL Write (M0_5 writeArgs)
ws' = PL (U5 Write) writeArgs -> PL Write (M0_5 writeArgs)
forall (wargs :: [(Maybe (*), *, (*, [BindingType]),
WriteSourcesArg, Nat)]).
WriteListToMiddle wargs =>
PL (U5 Write) wargs -> PL Write (M0_5 wargs)
W.writeListToMiddle PL (U5 Write) writeArgs
ws; cs' :: PL Copy (M0_8 copyArgs)
cs' = PL (U8 Copy) copyArgs -> PL Copy (M0_8 copyArgs)
forall (cargs :: [(Maybe (*), *, (*, [BindingType]), Nat, *,
(*, [BindingType]), Nat, BindingType)]).
CopyListToMiddle cargs =>
PL (U8 Copy) cargs -> PL Copy (M0_8 cargs)
copyListToMiddle PL (U8 Copy) copyArgs
cs