bind-marshal-0.1: Data marshaling library that uses type level equations to optimize buffering.




returnM_v_bd :: a -> BDIter bd -> IO (a, BDIter bd)Source

returnM_v_i :: a -> Iter -> IO (a, Iter)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.

Associated Types

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