module Bind.Marshal.Action.Monad ( module Bind.Marshal.Action.Monad
, module Bind.Marshal.Action.Monad.Static
)
where
import Bind.Marshal.Prelude
import Bind.Marshal.Action.Base
import Bind.Marshal.Action.Static
import Bind.Marshal.Action.Dynamic
import Bind.Marshal.Action.Monad.Static
import Bind.Marshal.DataModel
import Bind.Marshal.StaticProperties
import qualified Control.Monad as BaseMonad
import Data.Strict.Either
import Data.Strict.Tuple
import Foreign.Ptr
import GHC.Exts
import System.IO
instance BufferDelegate bd => Return (DynAction Sealed Sealed Sealed bd tag) where
returnM v = SealedSealedAction (\ eval_cont -> eval_cont v)
instance BufferDelegate bd => BaseMonad.Monad (DynAction Sealed Sealed Sealed bd tag) where
return v = SealedSealedAction (\ eval_cont -> eval_cont v )
(>>=) (SealedSealedAction ma) fmb = SealedSealedAction
( \ eval_cont -> ma (\v -> case fmb v of
SealedSealedAction mb -> mb eval_cont
)
)
(>>) (SealedSealedAction ma) (SealedSealedAction mb)
= SealedSealedAction ( \ eval_cont -> ma (const $! mb eval_cont) )
returnM_v_bd :: a -> BDIter bd -> IO (a, BDIter bd)
returnM_v_bd a !bd_iter = returnM (a, bd_iter)
returnM_v_i :: a -> Iter -> IO (a, Iter)
returnM_v_i !a !iter = returnM (a, iter)
post_bind p_0 p_1 = \ !a !iter -> do
(!b, !iter') <- p_0 a iter
p_1 b iter'
resolve_iter :: BufferDelegate bd => Size -> BDIter bd -> IO (BDIter bd)
resolve_iter 0 !bd_iter = returnM bd_iter
resolve_iter !required_size !bd_iter = case max_bytes_final bd_iter of
0 -> case required_size > max_bytes_avail bd_iter of
True -> gen_region required_size (buffer_delegate bd_iter)
False -> returnM ( bd_iter { max_bytes_final = required_size } )
finalized_size -> case required_size + finalized_size > max_bytes_avail bd_iter of
True -> gen_region required_size =<< finalize_region bd_iter
False -> returnM ( bd_iter { max_bytes_final = finalized_size + required_size } )
instance ( bd_2 ~ bd_0
, bd_2 ~ bd_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
) => Bind (DynAction Sealed Sealed Sealed bd_0 tag_0)
(DynAction Sealed Sealed Sealed bd_1 tag_1)
(DynAction Sealed Sealed Sealed bd_2 tag_2)
where
(>>=) (SealedSealedAction ma) fmb = SealedSealedAction
( \ eval_cont -> ma (\v -> case fmb v of
SealedSealedAction mb -> mb eval_cont
)
)
instance ( post_s_0 ~ post_sa_0
, BufferDelegate bd_2
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
) => Bind (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction Sealed Sealed Sealed bd_1 tag_1)
(DynAction Sealed Sealed Sealed bd_2 tag_2)
where
(>>=) (SealedOpenAction ma post) fmb = SealedSealedAction
( \ eval_cont -> ma post (\v -> case fmb v of
SealedSealedAction mb -> mb eval_cont
)
)
instance ( pre_s_2 ~ pre_s_0
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
) => Bind (DynAction (Open pre_s_0) Sealed Sealed bd_0 tag_0)
(DynAction Sealed Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_2 tag_2)
where
(>>=) (OpenSealedAction pre_accum ma) fmb = OpenSealedAction
pre_accum
(\ pre eval_cont ->
ma pre
(\v -> case fmb v of
SealedSealedAction mb -> mb eval_cont
)
)
instance ( pre_s_2 ~ pre_s_0
, post_s_0 ~ post_sa_0
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
) => Bind (DynAction (Open pre_s_0) (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction Sealed Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_2 tag_2)
where
(>>=) (OpenOpenAction pre ma post) fmb = OpenSealedAction
pre
(\ pre_final eval_cont ->
ma pre_final
post
(\a -> case fmb a of
SealedSealedAction mb -> mb eval_cont
)
)
instance ( pre_s_2 ~ static_size
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (StaticMemAction tag_0 static_size)
(DynAction Sealed Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_2 tag_2)
where
(>>=) (StaticMemAction ma) fmb = OpenSealedAction
(io_eval_static (StaticMemAction ma))
(\ pre eval_cont !bd_iter -> do
(v, (Ptr p')) <- pre (Ptr (curr_addr bd_iter))
case fmb v of
SealedSealedAction mb -> mb eval_cont (bd_iter {curr_addr = p'})
)
instance ( post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed Sealed Sealed bd_0 tag_0)
(DynAction Sealed (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedSealedAction ma) fmb = SealedOpenAction
(\ post
(eval_cont :: c -> BDIter bd_2 -> IO d)
!bd_iter -> do
(a, !bd_iter') <- ma returnM_v_bd bd_iter
case fmb a of
SealedOpenAction mb mb_post -> do
mb (mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, post_s_0 ~ post_sa_0
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction Sealed (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedOpenAction ma ma_post) fmb = SealedOpenAction
(\ post
(eval_cont :: c -> BDIter bd_2 -> IO d)
!bd_iter -> do
(a, !bd_iter') <- ma ma_post (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
SealedOpenAction mb mb_post -> mb (mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) Sealed Sealed bd_0 tag_0)
(DynAction Sealed (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenSealedAction !pre !ma) !fmb = OpenOpenAction
pre
(\ pre
post
(eval_cont :: c -> BDIter bd_2 -> IO d)
!bd_iter -> do
(a, !bd_iter') <- ma pre (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
SealedOpenAction mb mb_post -> mb (mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, post_s_0 ~ post_sa_0
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction Sealed (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenOpenAction ma_pre ma ma_post) fmb = OpenOpenAction
ma_pre
(\ pre
post
(eval_cont :: c -> BDIter bd_2 -> IO d)
!bd_iter -> do
(a, !bd_iter') <- ma pre ma_post (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
SealedOpenAction mb mb_post -> mb (mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ static_size
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (StaticMemAction tag_0 static_size)
(DynAction Sealed (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (StaticMemAction ma) fmb = OpenOpenAction
(io_eval_static (StaticMemAction ma))
(\ pre
post
(eval_cont :: c -> BDIter bd_2 -> IO d)
!bd_iter -> do
(!a, (Ptr p')) <- pre (Ptr (curr_addr bd_iter))
let !bd_iter' = bd_iter { curr_addr = p' }
case fmb a of
SealedOpenAction mb mb_post -> mb (mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( Nat pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed Sealed Sealed bd_0 tag_0)
(DynAction (Open pre_s_1) Sealed Sealed bd_1 tag_1)
(DynAction Sealed Sealed Sealed bd_2 tag_2)
where
(>>=) (SealedSealedAction ma) fmb = case toInt (undefined :: pre_s_1) of
!required_size -> SealedSealedAction
(\ eval_cont !bd_iter -> do
(a, !bd_iter') <- ma (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
OpenSealedAction pre mb -> mb pre eval_cont =<< resolve_iter required_size bd_iter'
)
instance ( post_s_0 ~ Add post_sa_0 pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction (Open pre_s_1) Sealed Sealed bd_1 tag_1)
(DynAction Sealed Sealed Sealed bd_2 tag_2)
where
(>>=) (SealedOpenAction ma post) fmb = SealedSealedAction
(\ eval_cont !bd_iter -> do
(a, !bd_iter') <- ma post (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
OpenSealedAction pre mb -> mb pre eval_cont bd_iter'
)
instance ( pre_s_2 ~ pre_s_0
, Nat pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) Sealed Sealed bd_0 tag_0)
(DynAction (Open pre_s_1) Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_2 tag_2)
where
(>>=) (OpenSealedAction ma_pre ma) fmb = case toInt (undefined :: pre_s_1) of
!required_size -> OpenSealedAction
ma_pre
(\ pre
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma pre returnM_v_bd bd_iter
case fmb a of
OpenSealedAction mb_pre mb -> mb mb_pre eval_cont =<< resolve_iter required_size bd_iter'
)
instance ( pre_s_2 ~ pre_s_0
, post_s_0 ~ Add post_sa_0 pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction (Open pre_s_1) Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_2 tag_2)
where
(>>=) (OpenOpenAction ma_pre ma ma_post) fmb = OpenSealedAction
ma_pre
(\ pre
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma pre ma_post (\a !bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
OpenSealedAction mb_pre mb -> mb mb_pre eval_cont bd_iter'
)
instance ( pre_s_2 ~ Add static_size pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (StaticMemAction tag_0 static_size)
(DynAction (Open pre_s_1) Sealed Sealed bd_1 tag_1)
(DynAction (Open pre_s_2) Sealed Sealed bd_1 tag_1)
where
(>>=) (StaticMemAction !ma) !fmb = OpenSealedAction
(io_eval_static (StaticMemAction ma))
(\ pre eval_cont !bd_iter -> do
(a, (Ptr p')) <- pre (Ptr (curr_addr bd_iter))
case fmb a of
OpenSealedAction mb_pre mb -> mb mb_pre eval_cont (bd_iter {curr_addr=p'})
)
instance ( post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, Nat pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed Sealed Sealed bd_0 tag_0)
(DynAction (Open pre_s_1) (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedSealedAction ma) fmb = case toInt (undefined :: pre_s_1) of
!required_size -> SealedOpenAction
(\ post
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma (\a bd_iter' -> returnM (a, bd_iter')) bd_iter
case fmb a of
OpenOpenAction mb_pre mb mb_post ->
mb mb_pre
(mb_post `post_bind` post)
eval_cont
=<< resolve_iter required_size bd_iter'
)
returnM_v_i
instance ( post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, post_s_0 ~ Add post_sa_0 pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction (Open pre_s_1) (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedOpenAction ma ma_post) fmb = SealedOpenAction
(\ post
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma ma_post returnM_v_bd bd_iter
case fmb a of
OpenOpenAction mb_pre mb mb_post -> mb mb_pre
(mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, Nat pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) Sealed Sealed bd_0 tag_0)
(DynAction (Open pre_s_1) (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenSealedAction ma_pre ma) fmb = case toInt (undefined :: pre_s_1) of
!required_size -> OpenOpenAction
ma_pre
(\ pre
post
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma ma_pre returnM_v_bd bd_iter
case fmb a of
OpenOpenAction mb_pre mb mb_post ->
mb mb_pre
(mb_post `post_bind` post)
eval_cont
=<< resolve_iter required_size bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, post_s_0 ~ Add post_sa_0 pre_s_1
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(DynAction (Open pre_s_1) (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenOpenAction ma_pre ma ma_post) fmb = OpenOpenAction
ma_pre
(\ pre
post
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma pre ma_post returnM_v_bd bd_iter
case fmb a of
OpenOpenAction mb_pre mb mb_post -> mb mb_pre
(mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( pre_s_2 ~ Add static_size pre_s_1
, post_sa_2 ~ post_sa_1
, post_s_2 ~ post_s_1
, tag_0 ~ tag_1
, tag_1 ~ tag_2
, bd_2 ~ bd_1
, BufferDelegate bd_2
) => Bind (StaticMemAction tag_0 static_size)
(DynAction (Open pre_s_1) (Open post_sa_1) (Open post_s_1) bd_1 tag_1)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (StaticMemAction ma) fmb = OpenOpenAction
(io_eval_static (StaticMemAction ma))
(\ pre
post
eval_cont
!bd_iter -> do
(a, (Ptr p')) <- pre (Ptr (curr_addr bd_iter))
let !bd_iter' = bd_iter { curr_addr = p' }
case fmb a of
OpenOpenAction mb_pre mb mb_post -> mb mb_pre
(mb_post `post_bind` post)
eval_cont
bd_iter'
)
returnM_v_i
instance ( post_sa_2 ~ static_size
, Nat post_s_2
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, BufferDelegate bd_2
) => Bind (DynAction Sealed Sealed Sealed bd_0 tag_0)
(StaticMemAction tag_1 static_size)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedSealedAction ma) fmb = case toInt (undefined :: post_s_2) of
!required_size -> SealedOpenAction
(\ post eval_cont !bd_iter -> do
(a, !bd_iter') <- ma returnM_v_bd bd_iter
!bd_iter'' <- resolve_iter required_size bd_iter'
(!c, (Ptr p''')) <- post a (Ptr (curr_addr bd_iter''))
eval_cont c (bd_iter'' {curr_addr = p'''})
)
(io_eval_static . fmb)
instance ( post_sa_2 ~ Add post_sa_0 static_size
, post_s_0 ~ post_s_2
, tag_2 ~ tag_0
, tag_2 ~ tag_1
, bd_2 ~ bd_0
, BufferDelegate bd_2
) => Bind (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(StaticMemAction tag_1 static_size)
(DynAction Sealed (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (SealedOpenAction ma ma_post) fmb = SealedOpenAction
ma
(\ !a !iter -> do
(!b, !iter') <- ma_post a iter
io_eval_static (fmb b) iter'
)
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ static_size
, Nat post_s_2
, tag_0 ~ tag_1
, tag_1 ~ tag_2
, bd_2 ~ bd_0
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) Sealed Sealed bd_0 tag_0)
(StaticMemAction tag_1 static_size)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenSealedAction ma_pre ma) fmb = case toInt ( undefined :: post_s_2 ) of
!required_size -> OpenOpenAction
ma_pre
(\ pre
post
eval_cont
!bd_iter -> do
(a, !bd_iter') <- ma ma_pre returnM_v_bd bd_iter
!bd_iter'' <- resolve_iter required_size bd_iter'
(!c, (Ptr p''')) <- post a (Ptr (curr_addr bd_iter''))
eval_cont c (bd_iter'' { curr_addr = p''' })
)
(io_eval_static . fmb)
instance ( pre_s_2 ~ pre_s_0
, post_sa_2 ~ Add post_sa_0 static_size
, post_s_0 ~ post_s_2
, tag_0 ~ tag_1
, tag_1 ~ tag_2
, bd_2 ~ bd_0
, BufferDelegate bd_2
) => Bind (DynAction (Open pre_s_0) (Open post_sa_0) (Open post_s_0) bd_0 tag_0)
(StaticMemAction tag_1 static_size)
(DynAction (Open pre_s_2) (Open post_sa_2) (Open post_s_2) bd_2 tag_2)
where
(>>=) (OpenOpenAction ma_pre ma ma_post) fmb = OpenOpenAction
ma_pre
ma
(\ !a !iter -> do
(!b, !iter') <- ma_post a iter
io_eval_static (fmb b) iter'
)
instance BufferDelegate bd => Fail (DynAction Sealed Sealed Sealed bd tag) where
fail !err_txt = SealedSealedAction (\ eval_cont !bd_iter -> fail err_txt)
instance BufferDelegate bd => Fail (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd tag) where
fail !err_txt = SealedOpenAction (\ post eval_cont !bd_iter -> fail err_txt) (returnM_v_i)
dyn_fail :: forall bd tag a . BufferDelegate bd
=> String -> DynAction Sealed Sealed Sealed bd tag a
dyn_fail = fail
class SealedDynAction (action :: * -> *) bd where
type DynActionTag action
dyn_action :: action a -> DynAction Sealed Sealed Sealed
bd
(DynActionTag action)
a
instance ( bd_1 ~ bd_0
, BufferDelegate bd_1
) => SealedDynAction (DynAction Sealed Sealed Sealed bd_0 tag) bd_1 where
type DynActionTag (DynAction Sealed Sealed Sealed bd_0 tag) = tag
dyn_action (SealedSealedAction a) = SealedSealedAction a
instance ( BufferDelegate bd
, Nat size
) => SealedDynAction (StaticMemAction tag size) bd where
type DynActionTag (StaticMemAction tag size) = tag
dyn_action (StaticMemAction ma) = case toInt (undefined :: size) of
!required_size -> SealedSealedAction
( \ eval_cont !bd_iter -> do
!bd_iter' <- resolve_iter required_size bd_iter
ma (\ !v !p' -> eval_cont v ( bd_iter' { curr_addr = p' } )) fail (curr_addr bd_iter')
)
instance ( BufferDelegate bd_1
, bd_0 ~ bd_1
, Nat pre_s
) => SealedDynAction (DynAction (Open pre_s) Sealed Sealed bd_0 tag) bd_1 where
type DynActionTag (DynAction (Open pre_s) Sealed Sealed bd_0 tag) = tag
dyn_action (OpenSealedAction pre m) = case toInt (undefined :: pre_s) of
!required_size -> SealedSealedAction
(\ eval_cont !bd_iter -> do
m pre eval_cont =<< resolve_iter required_size bd_iter
)
instance ( BufferDelegate bd_1
, bd_0 ~ bd_1
, post_s_0 ~ post_sa_0
) => SealedDynAction (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag) bd_1 where
type DynActionTag (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag) = tag
dyn_action (SealedOpenAction m post) = SealedSealedAction (m post)
instance ( post_s ~ post_sa
, Nat pre_s
, BufferDelegate bd_0
, bd_0 ~ bd_1
) => SealedDynAction (DynAction (Open pre_s) (Open post_sa) (Open post_s) bd_0 tag) bd_1 where
type DynActionTag (DynAction (Open pre_s) (Open post_sa) (Open post_s) bd_0 tag) = tag
dyn_action (OpenOpenAction pre m post) = case toInt (undefined :: pre_s) of
!required_size -> SealedSealedAction
(\ eval_cont !bd_iter -> do
m pre post eval_cont =<< resolve_iter required_size bd_iter
)