/* Filename : Bin.cvl
   Authors  : XXX
   Created  : 2025-01-13
   Modified : 2025-01-17

   Implements Bin.h, a collection supporting put and get without
   equality.  This Bin is implemented like a FIFO queue: items
   are "put" at the end of a list and "get" removes an item at
   the front of the list.

   some Lab
   some division
   some institution
 */
#pragma CIVL ACSL
#include "ArrayList.h"
#include "Bin.h"
#include <stdlib.h>

struct Bin {
  ArrayList list;
};

Bin Bin_create(void) {
  Bin bin = malloc(sizeof(struct Bin));
  bin->list = ArrayList_create();
  return bin;
}

void  Bin_destroy(Bin bin) {
  ArrayList_destroy(bin->list);
  free(bin);
}

//@ depends_on \access(bin);
$atomic_f void Bin_put(Bin bin, T item) {
  ArrayList_add(bin->list, item);
}

//@ depends_on \access(bin);
$atomic_f T Bin_get(Bin bin) {
  if (ArrayList_size(bin->list) == 0)
    return -1;
  else
    return ArrayList_remove_index(bin->list, 0);
}

//@ depends_on \access(bin);
$atomic_f bool Bin_isEmpty(Bin bin) {
  return ArrayList_size(bin->list) == 0;
}

void Bin_print(Bin bin) {
  ArrayList_print(bin->list);
}