/* From notes of meeting with Alex Stepanov */
include_c "stdlib.h";
use "basic_concepts.g";

concept BinaryOperation<Op, T>
{
  fun apply(Op, T, T) -> T@;
};

concept UnaryFunction<Op, T, R>
{
  fun apply(Op, T) -> R@;
};

concept Semigroup_<Op, T> 
{
  refines BinaryOperation<Op,T>;
  /*
  axiom Associativity(T x, T y, T z, Op op) { 
    assert(op(x, op(y, z)) == op(op(x, y), z)); 
    }
  */
};

concept Monoid_<Op, T> 
{
  refines Semigroup_<Op, T>;
  fun identity_element(Op) -> T;

  /*
  axiom Identity(Op op, T x) { 
    T id(identity_element(op));
    assert(op(id, x) == x);
    assert(op(x, id) == x);
  }
  */
};


concept Group<Op,T>
{
  refines Monoid_<Op,T>;
  type inverse_t;
  require UnaryFunction<inverse_t, T, T>;
  fun inverse(Op) -> inverse_t@;

  /*
  axiom Invertibility(Op op, T x, Ty) {
    T id(identity_element(op));
    assert(op(inverse(op)(x), x) == id);
    assert(op(x, inverse(op)(x)) == id);
  }
  */
};


fun left_power<T, I, Op>
where { Regular<T>, SignedIntegral<I>, BinaryOperation<Op, T> }
(T@ a, I@ n, Op op) -> T@ {
  let result = a;
  while (--n != zero())
    result = apply(op, result, a);
  return result;
}


fun power_semigroup<T,I,Op>
where { Regular<T>, SignedIntegral<I>, Semigroup_<Op,T> }
(T a, I n, Op op) -> T@
{
  /*assert(n > zero());*/
  return left_power(a, n, op);
}


fun power_monoid<T,I,Op>
where { Regular<T>, SignedIntegral<I>, Monoid_<Op,T> }
(T a, I n, Op op) -> T@
{
  /*assert(n >= 0);*/
  if (n == zero()) return identity_element(op);
  else {
    return power_semigroup(a, n, op);
  }
}


fun power_group<T,I,Op>
  where { Regular<T>, SignedIntegral<I>, Group<Op,T> }
(T a, I n, Op op) -> T@
{
  if (n < zero()) return power_group(apply(inverse(op), a), -n, op);
  else {
    return power_monoid(a, n, op);
  }
}

fun power<T,I,Op>
where { Regular<T>, SignedIntegral<I>, Semigroup_<Op,T> }
(T a, I n, Op op) -> T@
{ return power_semigroup(a, n, op); }

fun power<T,I,Op>
where { Regular<T>, SignedIntegral<I>, Monoid_<Op,T> }
(T a, I n, Op op) -> T@
{ return power_monoid(a, n, op); }

fun power<T,I,Op>
where { Regular<T>, SignedIntegral<I>, Group<Op,T> }
(T a, I n, Op op) -> T@
{ return power_group(a, n, op); }

fun main() -> int@
{
  /* add models and a call to power... */
  return 0;
}