dnl template for a statically sized list/queue/stack
dnl
dnl This file defines, as an M4¹ template, a type-generic Murphi list data
dnl structure. To use this, include the template and then call the macro "_list"
dnl with 4 parameters:
dnl   • "name" – a prefix for the generated list data structure and its
dnl     supporting functions
dnl   • "index_t" – a Murphi type for indexing the list
dnl   • "elem_t" – a Murphi type for the elements of the list
dnl   • "size" – one more than the number of elements in type "index_t",
dnl     defaulting to 2³¹-1 (see discussion of this below)
dnl E.g.:
dnl
dnl   include(`_list')dnl
dnl
dnl   type
dnl     int: 0..32;
dnl
dnl   _list(`ints', `0..10', `int')dnl
dnl
dnl Pre-process your model with M4:
dnl
dnl   $ m4 --include=/path/to/rumur/install/share/rumur/lib model.m >out.m
dnl
dnl This generates a type and some supporting functions:
dnl
dnl   type
dnl     ints_t: …
dnl
dnl   function ints_is_empty(list_: ints_t): boolean;
dnl   function ints_is_full(list_: ints_t): boolean;
dnl   function ints_size(list_: ints_t): 0..2147483647;
dnl   procedure ints_push_back(var list_: ints_t; elem_: int);
dnl   function ints_try_push_back(var list_: ints_t; elem_: int): boolean;
dnl   function ints_pop_front(var list_: ints_t): int;
dnl   function ints_pop_back(var list_: ints_t): int;
dnl
dnl You can then go on to use the "ints_t" type in your handwritten model code.
dnl
dnl "index_t" can be an arbitrary type; the only requirement is that it is
dnl iterable. It can be a previously defined type or a type literal. The
dnl underlying type could be boolean, a range, a scalarset, or an enum. Though
dnl it is unlikely anything except a range makes sense.
dnl
dnl "elem_t" can be an arbitrary type. It can be a previously defined type or a
dnl type literal, though you probably want to name it in order to more easily
dnl use the push and pop functions.
dnl
dnl "size" does not need to be supplied unless (a) your indexing type "index_t"
dnl has more than 2³¹-2 elements or (b) you are trying to optimise your model by
dnl using a value type narrower than "int32_t". In either case, you still do not
dnl need to supply "size" if you never call the "*_size()" function; it is not
dnl used internally within this template. If you call "*_size()" and your usage
dnl falls into the (a) or (b) cases above, supply a "size" that is the number of
dnl elements in "index_t" plus 1. Note that, e.g. if your indexing type is
dnl "0..255", your size will need to be ≥ 256, preventing you using the value
dnl type "uint8_t" which is not large enough to hold the value 256.
dnl
dnl This template is in the public domain. You may use it for any purpose and
dnl its inclusion in a model does not affect the legal status of that model.
dnl
dnl ¹ https://en.wikipedia.org/wiki/M4_(computer_language)
dnl
define(`_list', `dnl
-------------------------------------------------------------------------------
-- interface for $1_t, a list of $3 values indexed by $2
-------------------------------------------------------------------------------

type
  $1_t: array[$2] of record
    -- Does this slot hold an item? The type 1..1 is used to model a boolean
    -- without incurring an extra bit for the undefined value. I.e.
    --   false = isundefined(is_populated_)
    --   true = !isundefined(is_populated_)
    is_populated_: 1..1;
    -- the contents of the slot, if !isundefined(is_populated_)
    value_: $3;
  end;

function $1_is_empty(list_: $1_t): boolean;
begin
  -- use a single-iteration loop to check the first element to avoid assuming
  -- the lower bound of type $2
  for i_: $2 do
    if !isundefined(list_[i_].is_populated_) then
      return false;
    else
      return true;
    end;
  end;
  -- in the edge case where $2 is an empty type, consider the list always empty
  return true;
end;

-- get the number of elements present in a list
function $1_size(list_: $1_t): 0..ifelse(`$4', `', `2147483647', `$4');
  var count_: 0..ifelse(`$4', `', `2147483647', `$4');
begin
  -- We have no easy way of checking the number of members in the type $2 at
  -- generation time. So we use a runtime sanity check here that our return type
  -- is large enough to represent the maximum size. A decent compiler will
  -- constant fold and eliminate this in the common case where the type is
  -- indeed large enough.
  count_ := 0;
  for i_: $2 do
    assert
      "0..ifelse(`$4', `', `2147483647', `$4') too small to represent $1_t size"
      count_ < ifelse(`$4', `', `2147483647', `$4');
    count_ := count_ + 1;
  end;

  count_ := 0;
  for i_: $2 do
    if !isundefined(list_[i_].is_populated_) then
      count_ := count_ + 1;
    end;
  end;
  return count_;
end;

function $1_is_full(list_: $1_t): boolean;
begin
  -- use a loop to check the last element to avoid assuming the upper bound of
  -- type $2
  for i_: $2 do
    if isundefined(list_[i_].is_populated_) then
      return false;
    end;
  end;
  return true;
end;

-- Treating a $1_t as a first-in-first-out queue, enqueue an item. Or
-- equivalently, treating a $1_t as a last-in-first-out stack, stack an item.
procedure $1_push_back(var list_: $1_t; elem_: $3);
begin
  assert "attempting to push into a full $1_t" !$1_is_full(list_);
  -- use a loop to find the first empty slot to avoid assuming the upper bound
  -- of type $2
  for i_: $2 do
    if isundefined(list_[i_].is_populated_) then
      list_[i_].value_ := elem_;
      list_[i_].is_populated_ := 1;
      return;
    end;
  end;
  assert "unreachable code executed" false;
end;

-- Treating a $1_t as a first-in-first-out queue, enqueue an item and return
-- true if possible. Or equivalently, treating a $1_t as a last-in-first-out
-- stack, stack an item and return true if possible. If it is not possible to
-- insert the new item, do nothing and return false.
function $1_try_push_back(var list_: $1_t; elem_: $3): boolean;
begin
  if $1_is_full(list_) then
    return false;
  end;
  $1_push_back(list_, elem_);
  return true;
end;

-- treating a $1_t as a first-in-first-out queue, dequeue an item
function $1_pop_front(var list_: $1_t): $3;
var
  first_: $3;
  successor_: boolean;
begin
  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
  for i_: $2 do

    -- extract the first element
    assert "corrupted list" !isundefined(list_[i_].is_populated_);
    first_ := list_[i_].value_;

    -- Shuffle the remaining elements forwards. We do this with an unorthodox
    -- double loop to avoid assuming anything about the bounds of $2 or
    -- even whether its members are orderable.
    for j_: $2 do
      undefine list_[j_];
      successor_ := false;
      for k_: $2 do
        if j_ = k_ then
          assert "incorrect shuffle logic" !successor_;
          successor_ := true;
        elsif successor_ then
          list_[j_] := list_[k_];
          successor_ := false;
        end;
      end;
    end;

    return first_;
  end;
end;

-- treating a $1_t as a last-in-first-out stack, unstack an item
function $1_pop_back(var list_: $1_t): $3;
var
  last_: $3;
  has_successor_: boolean;
  successor_: boolean;
begin
  assert "attempting to pop from an empty $1_t" !$1_is_empty(list_);
  for i_: $2 do

    -- Is this element the last? We do this with an unorthodox loop to avoid
    -- assuming anything about the bounds of $2 or even whether its members
    -- are orderable.
    has_successor_ := false;
    for j_: $2 do
      if i_ = j_ then
        successor_ := true;
      elsif successor_ then
        has_successor_ := !isundefined(list_[j_].is_populated_);
        successor_ := false;
      end;
    end;

    -- if this is the last element, extract and return it
    if !has_successor_ then
      last_ := list_[i_].value_;
      undefine list_[i_];
      return last_;
    end;
  end;
end;

-------------------------------------------------------------------------------
-- end interface for $1_t
-------------------------------------------------------------------------------
')dnl