//
// # Example: The _rational_ _numbers_ ℚ.
//
// The rational numbers (ℚ) form a _field_. Rust does not have a
// rational number type in the standard library so the rational number
// type used here is the `Ratio<T>` type from the very handy `num`
// crate.
//
use ::num::rational::*;
use un_algebra::tests::*;
use un_algebra::prelude::*;


//
// Integer "base" type for rational numerators and denominators. To keep
// this example simple-ish we limit rationals to `i128` components.
// Ideally, they should be unbounded integers, e.g. `num`'s `BigInt`
// type.
//
type Base = i128;


//
// We use a newtype wrapper around the `num` crate rational type to work
// within Rust's _trait_ _coherence_ rules.
//
#[derive(Copy, Clone, Debug, PartialEq)]
struct Rational(Ratio<Base>);


//
// Create a Rational instance from base integer components.
//
impl Rational {
  pub fn new(n: Base, d: Base) -> Self {
    Self(Ratio::new(n, d))
  }
}


//
// Rational numbers form an additive magma with (rational) addition as
// the operation.
//
impl AddMagma for Rational {

  fn add(&self, other: &Self) -> Self {
    Self(self.0 + other.0)
  }
}


//
// Rational numbers form an additive semigroup as (rational) addition is
// associative.
//
impl AddSemigroup for Rational {}


//
// Rational numbers form an additive monoid with (rational) zero as the
// additive identity.
//
impl AddMonoid for Rational {

  fn zero() -> Self {
    Self::new(0, 1)
  }
}


//
// Rational numbers form an additive group with (rational) negation as
// the group inverse.
//
impl AddGroup for Rational {

  fn negate(&self) -> Self {
    Self(-self.0)
  }
}


//
// Rational numbers form an additive commutative group as (rational)
// addition is commutative.
//
impl AddComGroup for Rational {}


//
// Rational numbers form a multiplicative magma with (rational)
// multiplication as the operation.
//
impl MulMagma for Rational {

  fn mul(&self, other: &Self) -> Self {
    Self(self.0 * other.0)
  }
}


//
// Rational numbers form a multiplicative semigroup as (rational)
// multiplication is associative.
//
impl MulSemigroup for Rational {}


// Non-zero rational numbers form a quasigroup with left and right
// division of non-zero (rational) values.
//
impl Quasigroup for Rational {

  fn is_divisor(&self) -> bool {
    *self != Self::new(0, 1)
  }


  fn ldiv(&self, other: &Self) -> Self {
    Self(other.0 / self.0)
  }


  fn rdiv(&self, other: &Self) -> Self {
    Self(self.0 / other.0)
  }
}


//
// Rational numbers form a multiplicative monoid with (rational) one as
// the multiplicative identity.
//
impl MulMonoid for Rational {

  fn one() -> Self {
    Self::new(1, 1)
  }
}


//
// Rational numbers form a multiplicative group with reciprocal of
// non-zero (rational) values as the group inverse.
//
impl MulGroup for Rational {

  fn is_invertible(&self) -> bool {
    *self != Self::new(0, 1)
  }


  fn invert(&self) -> Self {
    Self(self.0.recip())
  }
}


//
// Rational numbers form a multiplicative commutative group as
// (rational) multiplication is commutative.
//
impl MulComGroup for Rational {}


//
// Rational numbers form a ring.
//
impl Ring for Rational {}


//
// Rational numbers form a commutative ring.
//
impl ComRing for Rational {}


//
// Rational numbers (without zero) form a field with reciprocal of
// non-zero (rational) values as the field inverse.
//
impl Field for Rational {

  fn invert(&self) -> Self {
    Self(self.0.recip())
  }
}


//
// Generate `proptest` arbitrary (i.e. boxed strategy) Rational values
// from i32 components. Short function name to keep generator
// expressions manageable.
//
fn r32() -> impl Strategy<Value = Rational> {
  let ints = any::<(i32, i32)>(); // i32's to avoid overflow.

  ints.prop_map(|(n, d)| Rational::new(i128::from(n), i128::from(d)))
}


#[cfg(test)]
proptest! {
  #![proptest_config(config::standard())]


  #[test]
  fn add_closure([p, q] in [r32(), r32()]) {
    prop_assert!(AddMagmaLaws::closure(&p, &q))
  }


  #[test]
  fn mul_closure([p, q] in [r32(), r32()]) {
    prop_assert!(MulMagmaLaws::closure(&p, &q))
  }


  #[test]
  fn mul_associative([p, q, r] in [r32(), r32(), r32()]) {
    prop_assert!(MulSemigroupLaws::associativity(&p, &q, &r))
  }


  #[test]
  fn left_ldiv([p, q] in [r32(), r32()]) {
    prop_assume!(p.is_divisor());

    prop_assert!(p.left_lcancellation(&q))
  }


  #[test]
  fn right_ldiv([p, q] in [r32(), r32()]) {
    prop_assume!(q.is_divisor());

    prop_assert!(p.right_lcancellation(&q))
  }


  #[test]
  fn left_rdiv([p, q] in [r32(), r32()]) {
    prop_assume!(q.is_divisor());

    prop_assert!(p.left_rcancellation(&q))
  }


  #[test]
  fn right_rdiv([p, q] in [r32(), r32()]) {
    prop_assume!(q.is_divisor());

    prop_assert!(p.right_rcancellation(&q))
  }


  #[test]
  fn add_associative([p, q, r] in [r32(), r32(), r32()]) {
    prop_assert!(AddSemigroupLaws::associativity(&p, &q, &r))
  }


  #[test]
  fn left_add_identity(q in r32()) {
    prop_assert!(AddMonoidLaws::left_identity(&q))
  }


  #[test]
  fn right_add_identity(q in r32()) {
    prop_assert!(AddMonoidLaws::right_identity(&q))
  }


  #[test]
  fn left_mul_identity(q in r32()) {
    prop_assert!(MulMonoidLaws::left_identity(&q))
  }


  #[test]
  fn right_mul_identity(q in r32()) {
    prop_assert!(MulMonoidLaws::right_identity(&q))
  }


  #[test]
  fn left_add_inverse(q in r32()) {
    prop_assert!(AddGroupLaws::left_inverse(&q))
  }


  #[test]
  fn right_add_inverse(q in r32()) {
    prop_assert!(AddGroupLaws::right_inverse(&q))
  }


  #[test]
  fn left_mul_inverse(q in r32()) {
    prop_assume!(MulGroup::is_invertible(&q));

    prop_assert!(MulGroupLaws::left_inverse(&q))
  }


  #[test]
  fn right_mul_inverse(q in r32()) {
    prop_assume!(MulGroup::is_invertible(&q));

    prop_assert!(MulGroupLaws::right_inverse(&q))
  }


  #[test]
  fn add_commute([p, q] in [r32(), r32()]) {
    prop_assert!(AddComGroupLaws::commutivity(&p, &q))
  }


  #[test]
  fn mul_commute([p, q] in [r32(), r32()]) {
    prop_assert!(MulComGroupLaws::commutivity(&p, &q))
  }


  #[test]
  fn left_distributivity([q, r, s] in [r32(), r32(), r32()]) {
    prop_assert!(RingLaws::left_distributivity(&q, &r, &s))
  }


  #[test]
  fn right_distributivity([q, r, s] in [r32(), r32(), r32()]) {
    prop_assert!(RingLaws::right_distributivity(&q, &r, &s))
  }


  #[test]
  fn left_absorption(q in r32()) {
    prop_assert!(RingLaws::left_absorption(&q))
  }


  #[test]
  fn right_absorption(q in r32()) {
    prop_assert!(RingLaws::right_absorption(&q))
  }


  #[test]
  fn left_negation((q, r) in (r32(), r32())) {
    prop_assert!(RingLaws::left_negation(&q, &r))
  }


  #[test]
  fn right_negation((q, r) in (r32(), r32())) {
    prop_assert!(RingLaws::right_negation(&q, &r))
  }


  #[test]
  fn commutivity((q, r) in (r32(), r32())) {
    prop_assert!(ComRingLaws::commutivity(&q, &r))
  }


  #[test]
  fn field_left_inverse(q in r32()) {
    prop_assume!(Field::is_invertible(&q));

    prop_assert!(FieldLaws::left_inverse(&q))
  }


  #[test]
  fn field_right_inverse(q in r32()) {
    prop_assume!(Field::is_invertible(&q));

    prop_assert!(FieldLaws::left_inverse(&q))
  }


  #[test]
  fn zero_cancellation([p, q] in [r32(), r32()]) {
    prop_assert!(FieldLaws::zero_cancellation(&p, &q))
  }


  #[test]
  fn add_cancellation([q, r, s] in [r32(), r32(), r32()]) {
    prop_assert!(FieldLaws::add_cancellation(&q, &r, &s))
  }


  #[test]
  fn mul_cancellation([q, r, s] in [r32(), r32(), r32()]) {
    prop_assert!(FieldLaws::mul_cancellation(&q, &r, &s))
  }
}


fn main() {
}