Bind.Marshal.Action.Static

A memory action that operates on a statically sized buffer. -

Documentation

type StaticIter r = Addr# -> IO r

newtype StaticMemAction buffer_iter_tag size a

A buffer static memory action. When executed:

Constructors

StaticMemAction

Fields

static_eval :: forall c. (a -> StaticIter c) -> (String -> IO c) -> StaticIter c

Instances

Functor (StaticMemAction buffer_iter_tag size)

m ~ D0 => Return (StaticMemAction tag m)

The static memory action monad is constructed via the parameterized monad Return and Bind instances.

Fail (StaticMemAction tag m)

possibly-failing pattern matches require a Fail instance.

(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?

(size_2 ~ Add size_0 size_1, buffer_0 ~ buffer_1, buffer_0 ~ buffer_2) => Bind (StaticMemAction buffer_0 size_0) (StaticMemAction buffer_1 size_1) (StaticMemAction buffer_2 size_2)

The static memory action monad is constructed via the parameterized monad Return and Bind instances.

(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)

(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)

(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)

(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)

(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)

(pre_s_2 ~ pre_s_0, post_sa_2 ~ static_size, tag_0 ~ tag_1, tag_1 ~ tag_2, bd_2 ~ bd_0, Nat post_s_2, 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)

(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)

(post_sa_2 ~ static_size, tag_2 ~ tag_0, tag_2 ~ tag_1, bd_2 ~ bd_0, Nat post_s_2, 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)

io_eval_static :: StaticMemAction tag size a -> Iter -> IO (a, Iter)

static_replicateM :: (Pos n, size_2 ~ Add size_0 (Mul n size_1), Bind (StaticMemAction tag size_0) (StaticMemAction tag size_1) (StaticMemAction tag size_2)) => n -> StaticMemAction tag size_1 a -> StaticMemAction tag size_2 [a]