/* this example has a vee in the concept refinement */

concept Eq<T> {
  fun eq(T x, T y) -> bool@; 
};

concept MultMonoid<M> {
  refines Eq<M>;
  fun mult(M x, M y) -> M@;
  fun unit() -> M@;
};

concept AddMonoid<M> {
  refines Eq<M>;
  fun add(M x, M y) -> M@;
  fun unit() -> M@;
};

concept AdditiveGroup<G> {
  refines AddMonoid<G>;
  fun add_inv(G x) -> G@;
};
concept MultGroup<G> {
  refines MultMonoid<G>;
  fun inv(G x) -> G@;
};
concept AddGroup<G> {
  refines AddMonoid<G>;
  fun inv(G x) -> G@;
};

concept Ring<R> {
  refines AdditiveGroup<R>;
  refines MultGroup<R>;
};

concept Module<M, R> {
  refines AddGroup<M>;
  require Ring<R>;
  fun scale_r(M v, R s) -> M@;
  fun scale_l(R s, M v) -> M@;
};

model Eq<double> {
  fun eq(double x, double y) -> bool@ { return x == y; }
};

model MultMonoid<double> {
  fun mult(double x, double y) -> double@ {
    return x * y;
  }
  fun unit() -> double@ {
    return 1.0;
  }
};
model AddMonoid<double> {
  fun add(double x, double y) -> double@ {
    return x + y;
  }
  fun unit() -> double@ {
    return 0.0;
  }
};

model AdditiveGroup<double> {
  fun add_inv(double x) -> double@ {
    return -x;
  }
};
model MultGroup<double> {
  fun inv(double x) -> double@ {
    return 1.0/x;
  }
};
model AddGroup<double> {
  fun inv(double x) -> double@ {
    return -x;
  }
};

model Ring<double> { };
model Module<double, double> {
  fun scale_r(double x, double y) -> double@ { return x * y; }
  fun scale_l(double x, double y) -> double@ { return x * y; }
};

fun main() -> int@ {
  return 0;
}