//
// # Example: Integer subtraction modulo 3.
//
// The integers under subtraction modulo 3 (here called `SZ3`) form a
// quasigroup. The `SZ3` "multiplication" operator is `a - b` `(mod 3)`.
//
#![allow(non_snake_case)]

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


//
// Modulo 3 helper function, based on the proposed Rust _euclidean_
// _modulus_ function.
//
pub fn mod_3(x: i32) -> i32 {
  let r = x % 3;

  if r < 0 {r + 3} else {r}
}


//
// The signed integers under subtraction modulo 3 (`SZ3`). To keep this
// example simple we restrict integers to `i32`'s.
//
#[derive(Clone, Copy, PartialEq, Debug, Arbitrary)]
pub struct SZ3(i32);


//
// Create an SZ3 instance from an integer.
//
impl SZ3 {
  pub fn new(x: i32) -> Self {
    Self(mod_3(x))
  }
}


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

  // Magma "multiplication" is subtraction mod 3. We use wrapping
  // subtraction to avoid integer underflows.
  fn mul(&self, other: &Self) -> Self {
    Self(self.0.wrapping_sub(other.0))
  }
}


//
// SZ3 values form a quasigroup.
//
impl Quasigroup for SZ3 {

  // All SZ3 values are known divisors.
  fn is_divisor(&self) -> bool {
    true
  }


  // Quasigroup left-division inverts subtraction mod 3. We use wrapping
  // subtraction to avoid integer underflows.
  fn ldiv(&self, other: &Self) -> Self {
    Self(self.0.wrapping_sub(other.0))
  }


  // Quasigroup right-division cancels subtraction mod 3. We use
  // wrapping addition to avoid integer overflows.
  fn rdiv(&self, other: &Self) -> Self {
    Self(self.0.wrapping_add(other.0))
  }
}


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


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


  #[test]
  fn mul_closure_t2([w, x, y, z] in any::<[SZ3; 4]>()) {
    prop_assert!(MulMagmaLaws::closure(&(w, x), &(y, z)))
  }


  #[test]
  fn mul_closure_a2([w, x, y, z] in any::<[SZ3; 4]>()) {
    prop_assert!(MulMagmaLaws::closure(&[w, x], &[y, z]))
  }


  #[test]
  fn left_lcancellation((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!(x.left_lcancellation(&y))
  }


  #[test]
  fn left_lcancellation_t1((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!((x,).left_lcancellation(&(y,)))
  }


  #[test]
  fn left_lcancellation_a1((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!([x].left_lcancellation(&[y]))
  }


  #[test]
  fn right_lcancellation((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!(x.right_lcancellation(&y))
  }


  #[test]
  fn right_lcancellation_t2([xs, ys] in any::<[(SZ3, SZ3); 2]>()) {
    prop_assert!(xs.right_lcancellation(&ys))
  }


  #[test]
  fn right_lcancellation_a2([xs, ys] in any::<[[SZ3; 2]; 2]>()) {
    prop_assert!(xs.right_lcancellation(&ys))
  }


  #[test]
  fn left_rcancellation((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!(x.left_rcancellation(&y))
  }


  #[test]
  fn left_rcancellation_t1((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!((x,).left_rcancellation(&(y,)))
  }


  #[test]
  fn left_rcancellation_a1((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!([x].left_rcancellation(&[y]))
  }


  #[test]
  fn right_rcancellation((x, y) in any::<(SZ3, SZ3)>()) {
    prop_assert!(x.right_rcancellation(&y))
  }


  #[test]
  fn right_rcancellation_t2([xs, ys] in any::<[(SZ3, SZ3); 2]>()) {
    prop_assert!(xs.right_rcancellation(&ys))
  }


  #[test]
  fn right_rcancellation_a2([xs, ys] in any::<[[SZ3; 2]; 2]>()) {
    prop_assert!(xs.right_rcancellation(&ys))
  }
}


fn main() {
}