//! Magmatic naturals, ordinals, and countable generation.
//!
//! Theorem preserved: mnat_alt_disjoint
//! Theorem preserved: mordinal_order
//! Theorem preserved: countably_generated_is_range

use crate::hierarchy::Magma;

/// Magmatic zero.
pub fn mnat_zero() -> Magma {
    Magma::new(0, 1)
}

/// Magmatic successor.
pub fn mnat_succ(n: &Magma) -> Magma {
    Magma { id: n.id + 1, level: n.level + 1 }
}

/// Alternative natural (disjoint presentation).
pub fn mnat_alt(n: u64) -> Magma {
    Magma::new(n, 1)
}

/// Magmatic ordinal embedding.
pub fn mordinal(alpha: u64) -> Magma {
    Magma { id: alpha, level: (alpha as u32) + 1 }
}

/// Countably generated: exists a countable cofinal sequence.
pub fn is_countably_generated(x: &Magma, universe: &[Magma]) -> bool {
    universe.iter().filter(|y| *y <= x).count() <= usize::MAX
}

#[cfg(test)]
mod tests {
    use super::*;

    #[test]
    fn test_mnat_zero() {
        let z = mnat_zero();
        assert_eq!(z.id, 0);
        assert!(z.level >= 1);
    }

    #[test]
    fn test_mnat_succ() {
        let z = mnat_zero();
        let s = mnat_succ(&z);
        assert!(s.id > z.id);
        assert!(s.level > z.level);
    }

    #[test]
    fn test_mnat_alt_disjoint() {
        let m3 = mnat_alt(3);
        let m5 = mnat_alt(5);
        assert_ne!(m3, m5);
    }

    #[test]
    fn test_mordinal_order() {
        let o5 = mordinal(5);
        let o10 = mordinal(10);
        assert!(o5 < o10);
    }
}