use "basic_models.g";

concept Iterator<X> {
  type value;
  refines Regular<X>;
  fun at_end(X a) -> bool@;
  fun operator++(X! c) -> X!;
  fun operator*(X b) -> value@;
};
/* Use refinement from Semigroup later */

fun accumulate<I>
where { Iterator<I>, 
	Monoid<Iterator<I>.value>,
        Regular<Iterator<I>.value> }
(I@ iter) -> Iterator<I>.value@
{
  if (at_end(iter))
    return identity_elt();
  else
    return binary_op(*iter, accumulate(++iter));
}

class ArrayIter {
  ArrayIter(ArrayIter i) : a(i.a), curr(i.curr), n(i.n) { }
  ArrayIter(int* a, int c, int n)
    : a(a), curr(c), n(n) { }
  int* a;
  int curr;
  int n;
};
fun operator=(ArrayIter! x, ArrayIter y) -> ArrayIter!
{
  x.a = y.a;
  x.curr = y.curr;
  x.n = y.n;
  return x;
}
model Regular<ArrayIter> { };

model Iterator<ArrayIter> {
  type value = int;
  fun operator++(ArrayIter! i) -> ArrayIter! { i.curr = i.curr + 1; return i; }
  fun operator*(ArrayIter i) -> int@ { return i.a[i.curr]; }
  fun at_end(ArrayIter i) -> bool@ { return i.curr == i.n; }
};

fun main() -> int@ {
  let a = new GC int[3];
  a[0] = 2;
  a[1] = -3;
  a[2] = 1;
  let i = @ArrayIter(a, 0, 3);
  let sum = accumulate(i);
  return sum;
}