Mavryk_webassembly_interpreter.Input_buffer
This module implements a FIFO queue to model the input. The messages are queued in an input_buffer in their order of appearance in the inbox.
val pp_message :
Ppx_deriving_runtime.Format.formatter ->
message ->
Ppx_deriving_runtime.unit
val show_message : message -> Ppx_deriving_runtime.string
An element of type t will have a content which is a lazy_vector of messages and a pointer to the number of elements to be able to dequeue. At this point there is no cleanup operation so an input_buffer content will likely have more than num_elements
messages (see #3340).
val alloc : unit -> t
alloc ()
returns an empty input_buffer.
val num_elements : t -> Z.t
num_elements buffer
is the number of elements of buffer
. It is used by dequeue
to pick the current message. Note that it is not necessarily equal to the length of the content of the inbox (see #3340).
val reset : t -> unit
reset buffer
removes the current contents of the buffer.
dequeue buffer
pops the current message from buffer and returns it. Note that the input buffer models a FIFO queue so the current message is the oldest in the queue. If the queue is empty it raises Dequeue_from_empty_queue
.
enqueue buffer message
pushes the given message
into the buffer
. Note that the message will have to have a higher raw_level/message_counter than than the newest message in the queue. If that fails it will raise the error Cannot_store_an_earlier_message
.