Draining the mailbox

[duncanatt]

Current Erlang examples need to drain the mailbox to balance it out manually. This ensures that all messages are consumed before a mailbox can be freed. For instance:

-spec pong() -> no_return().
pong() ->
  ?mb_assert_regex("*(Ping + Stop)"),
  receive
    {ping, Ping} ->
      Ping ! {pong},
      pong();
    {stop} ->
      pong_exit() % Drain mailbox
  end.

-spec pong_exit() -> no_return().
pong_exit() ->
  ?mb_assert_regex("*(Ping + Stop)"),
  receive
    {ping, Ping} ->
      pong_exit();
    {stop} ->
      pong_exit()
  end.

This is not something that is done in idiomatic Erlang since the GC takes care of disposing of the mailbox once a process terminates. We need a mechanism in Pat to cater for this paradigm. Alternatively, we could implement something from the Erlang side to generate these draining functions.