//
// # Example: The finite field _F4_.
//
// The values {`O`,`I`, `A`, `B`} form a _finite field_ known as _F4_ or
// _GF(4)_ [GF4] with operations as defined by [GF4].
//
// [GF4]: https://en.wikipedia.org/wiki/Field_(mathematics)
//
#![allow(non_snake_case)]

use proptest_derive::*;
use un_algebra::tests::*;
use un_algebra::prelude::*;


//
// The finite field with four elements _F4_ or _GF(4)_.
//
#[derive(Clone, Copy, PartialEq, Debug, Arbitrary)]
pub enum F4 {
  O, I, A, B
}


//
// F4 values form an additive magma.
//
impl AddMagma for F4 {

  // Magma addition as per the F4 definition.
  fn add(&self, other: &Self) -> Self {

    // Magma operations as per the definition of F4. Redundant branch
    // expressions used for clarity.
    match (self, other) {
      (F4::O, F4::O) => F4::O,
      (F4::O, F4::I) => F4::I,
      (F4::O, F4::A) => F4::A,
      (F4::O, F4::B) => F4::B,
      (F4::I, F4::O) => F4::I,
      (F4::I, F4::I) => F4::O,
      (F4::I, F4::A) => F4::B,
      (F4::I, F4::B) => F4::A,
      (F4::A, F4::O) => F4::A,
      (F4::A, F4::I) => F4::B,
      (F4::A, F4::A) => F4::O,
      (F4::A, F4::B) => F4::I,
      (F4::B, F4::O) => F4::B,
      (F4::B, F4::I) => F4::A,
      (F4::B, F4::A) => F4::I,
      (F4::B, F4::B) => F4::O,
    }
  }
}


//
// F4 values form an additive semigroup.
//
impl AddSemigroup for F4 {}


//
// F4 values form an additive monoid.
//
impl AddMonoid for F4 {

  // The F4 _O_ element acts as zero.
  fn zero() -> Self {
    F4::O
  }
}


//
// F4 values form an additive group.
//
impl AddGroup for F4 {

  // F4 elements are their own additive inverses.
  fn negate(&self) -> Self {
    *self
  }
}


//
// F4 values form an additive commutative group.
//
impl AddComGroup for F4 {}



//
// F4 values form a multiplicative magma.
//
impl MulMagma for F4 {

  // Magma addition as per the F4 definition.
  fn mul(&self, other: &Self) -> Self {

    // Magma operations as per the definition of F4. Redundant branch
    // expressions used for clarity.
    match (self, other) {
      (F4::O, F4::O) => F4::O,
      (F4::O, F4::I) => F4::O,
      (F4::O, F4::A) => F4::O,
      (F4::O, F4::B) => F4::O,
      (F4::I, F4::O) => F4::O,
      (F4::I, F4::I) => F4::I,
      (F4::I, F4::A) => F4::A,
      (F4::I, F4::B) => F4::B,
      (F4::A, F4::O) => F4::O,
      (F4::A, F4::I) => F4::A,
      (F4::A, F4::A) => F4::B,
      (F4::A, F4::B) => F4::I,
      (F4::B, F4::O) => F4::O,
      (F4::B, F4::I) => F4::B,
      (F4::B, F4::A) => F4::I,
      (F4::B, F4::B) => F4::A,
    }
  }
}


//
// F4 values form a multiplicative semigroup.
//
impl MulSemigroup for F4 {}


//
// F4 values form a multiplicative monoid.
//
impl MulMonoid for F4 {

  // The F4 _I_ value acts as one.
  fn one() -> Self {
    F4::I
  }
}


//
// F4 values form a multiplicative group.
//
impl MulGroup for F4 {

  // Multiplicative inverses as per the F4 definition.
  fn invert(&self) -> Self {
    match self {
      F4::O => F4::O,
      F4::I => F4::I,
      F4::A => F4::B,
      F4::B => F4::A,
    }
  }


  // Non-zero F4 elements are invertible.
  fn is_invertible(&self) -> bool {
    *self != F4::O
  }
}


//
// F4 values form a multiplicative commutative group.
//
impl MulComGroup for F4 {}


//
// F4 values form a ring.
//
impl Ring for F4 {}


//
// F4 values form a commutative ring.
//
impl ComRing for F4 {}


//
// F4 values form a field.
//
impl Field for F4 {

  // Field inverses as per the F4 definition.
  fn invert(&self) -> Self {
    match self {
      F4::O => F4::O,
      F4::I => F4::I,
      F4::A => F4::B,
      F4::B => F4::A,
    }
  }


  // Non-zero F4 elements are invertible.
  fn is_invertible(&self) -> bool {
    *self != F4::O
  }
}


//
// Generative tests of F4 algebraic axioms and properties.
//
proptest! {
  #![proptest_config(config::standard())]


  #[test]
  fn add_closure((x, y) in any::<(F4, F4)>()) {
    prop_assert!(AddMagmaLaws::closure(&x, &y))
  }


  #[test]
  fn mul_closure((x, y) in any::<(F4, F4)>()) {
    prop_assert!(MulMagmaLaws::closure(&x, &y))
  }


  #[test]
  fn mul_closure_a1((x, y) in any::<(F4, F4)>()) {
    prop_assert!(MulMagmaLaws::closure(&[x], &[y]))
  }


  #[test]
  fn mul_associative([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(MulSemigroupLaws::associativity(&x, &y, &z))
  }


  #[test]
  fn mul_associative_a1([xs, ys, zs] in any::<[[F4; 1]; 3]>()) {
    prop_assert!(MulSemigroupLaws::associativity(&xs, &ys, &zs))
  }


  #[test]
  fn add_associative([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(AddSemigroupLaws::associativity(&x, &y, &z))
  }


  #[test]
  fn add_associative_a1([xs, ys, zs] in any::<[[F4; 1]; 3]>()) {
    prop_assert!(AddSemigroupLaws::associativity(&xs, &ys, &zs))
  }


  #[test]
  fn left_add_identity(x in any::<F4>()) {
    prop_assert!(AddMonoidLaws::left_identity(&x))
  }


  #[test]
  fn right_add_identity(x in any::<F4>()) {
    prop_assert!(AddMonoidLaws::right_identity(&x))
  }


  #[test]
  fn right_add_identity_a2(xs in any::<[F4; 2]>()) {
    prop_assert!(AddMonoidLaws::right_identity(&xs))
  }


  #[test]
  fn left_mul_identity(x in any::<F4>()) {
    prop_assert!(MulMonoidLaws::left_identity(&x))
  }


  #[test]
  fn right_mul_identity(x in any::<F4>()) {
    prop_assert!(MulMonoidLaws::right_identity(&x))
  }


  #[test]
  fn right_mul_identity_a2(xs in any::<[F4; 2]>()) {
    prop_assert!(MulMonoidLaws::right_identity(&xs))
  }


  #[test]
  fn left_add_inverse(x in any::<F4>()) {
    prop_assert!(AddGroupLaws::left_inverse(&x))
  }


  #[test]
  fn left_add_inverse_a1(x in any::<F4>()) {
    prop_assert!(AddGroupLaws::left_inverse(&[x]))
  }


  #[test]
  fn right_add_inverse(x in any::<F4>()) {
    prop_assert!(AddGroupLaws::right_inverse(&x))
  }


  #[test]
  fn left_mul_inverse(x in any::<F4>()) {
    prop_assume!(MulGroup::is_invertible(&x));

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


  #[test]
  fn right_mul_inverse(x in any::<F4>()) {
    prop_assume!(MulGroup::is_invertible(&x));

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


  #[test]
  fn right_mul_inverse_a2(xs in any::<[F4; 2]>()) {
    prop_assume!(MulGroup::is_invertible(&xs));

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


  #[test]
  fn add_commutivity((x, y) in any::<(F4, F4)>()) {
    prop_assert!(AddComGroupLaws::commutivity(&x, &y))
  }


  #[test]
  fn mul_commutivity((x, y) in any::<(F4, F4)>()) {
    prop_assert!(MulComGroupLaws::commutivity(&x, &y))
  }


  #[test]
  fn mul_commutivity_a1((x, y) in any::<(F4, F4)>()) {
    prop_assert!(MulComGroupLaws::commutivity(&[x], &[y]))
  }


  #[test]
  fn left_distributivity([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(RingLaws::left_distributivity(&x, &y, &z))
  }


  #[test]
  fn right_distributivity([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(RingLaws::right_distributivity(&x, &y, &z))
  }


  #[test]
  fn left_absorption(x in any::<F4>()) {
    prop_assert!(RingLaws::left_absorption(&x))
  }


  #[test]
  fn right_absorption(x in any::<F4>()) {
    prop_assert!(RingLaws::right_absorption(&x))
  }


  #[test]
  fn left_negation((x, y) in any::<(F4, F4)>()) {
    prop_assert!(RingLaws::left_negation(&x, &y))
  }


  #[test]
  fn right_negation((x, y) in any::<(F4, F4)>()) {
    prop_assert!(RingLaws::right_negation(&x, &y))
  }


  #[test]
  fn commutivity((x, y) in any::<(F4, F4)>()) {
    prop_assert!(ComRingLaws::commutivity(&x, &y))
  }


  #[test]
  fn field_left_inverse(x in any::<F4>()) {
    prop_assume!(Field::is_invertible(&x));

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


  #[test]
  fn field_right_inverse(x in any::<F4>()) {
    prop_assume!(Field::is_invertible(&x));

    prop_assert!(FieldLaws::right_inverse(&x))
  }


  #[test]
  fn zero_cancellation((x, y) in any::<(F4, F4)>()) {
    prop_assert!(FieldLaws::zero_cancellation(&x, &y))
  }


  #[test]
  fn add_cancellation([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(FieldLaws::add_cancellation(&x, &y, &z))
  }


  #[test]
  fn mul_cancellation([x, y, z] in any::<[F4; 3]>()) {
    prop_assert!(FieldLaws::mul_cancellation(&x, &y, &z))
  }
}


fn main() {
}