- returnM_v_bd :: a -> BDIter bd -> IO (a, BDIter bd)
- returnM_v_i :: a -> Iter -> IO (a, Iter)
- resolve_iter :: BufferDelegate bd => Size -> BDIter bd -> IO (BDIter bd)
- dyn_fail :: forall bd tag a. BufferDelegate bd => String -> DynAction Sealed Sealed Sealed bd tag a
- class SealedDynAction action bd where
- type DynActionTag action
- dyn_action :: action a -> DynAction Sealed Sealed Sealed bd (DynActionTag action) a
- module Bind.Marshal.Action.Monad.Static
Documentation
returnM_v_bd :: a -> BDIter bd -> IO (a, BDIter bd)Source
returnM_v_i :: a -> Iter -> IO (a, Iter)Source
resolve_iter :: BufferDelegate bd => Size -> BDIter bd -> IO (BDIter bd)Source
dyn_fail :: forall bd tag a. BufferDelegate bd => String -> DynAction Sealed Sealed Sealed bd tag aSource
class SealedDynAction action bd whereSource
Converts an action to a sealed dynamic memory action value. Possibly inserts gen_region or finalize_region passes.
type DynActionTag action Source
dyn_action :: action a -> DynAction Sealed Sealed Sealed bd (DynActionTag action) aSource
(BufferDelegate bd, Nat size) => SealedDynAction (StaticMemAction tag size) bd | a dynamic block that already has an empty tail and a DMNil pre model can be trivially lifted to a fixed dynamic block. XXX: Any easier way to unify the input type parameter a with the action's type parameter a? |
(post_s ~ post_sa, bd_0 ~ bd_1, Nat pre_s, BufferDelegate bd_0) => SealedDynAction (DynAction (Open pre_s) (Open post_sa) (Open post_s) bd_0 tag) bd_1 | A dynamic block can be lifted to a fixed Dyn by capping the post_m_tail with DMNil and then reifying the pre_m model |
(bd_0 ~ bd_1, BufferDelegate bd_1, Nat pre_s) => SealedDynAction (DynAction (Open pre_s) Sealed Sealed bd_0 tag) bd_1 | |
(bd_0 ~ bd_1, post_s_0 ~ post_sa_0, BufferDelegate bd_1) => SealedDynAction (DynAction Sealed (Open post_sa_0) (Open post_s_0) bd_0 tag) bd_1 | |
(bd_1 ~ bd_0, BufferDelegate bd_1) => SealedDynAction (DynAction Sealed Sealed Sealed bd_0 tag) bd_1 |