//! Magmatic universe hierarchy with level function.
//!
//! Theorem preserved: hierarchy_cumulative
//! Theorem preserved: strict_predecessor_drops_level
//! Theorem preserved: hierarchy_level_positive

/// A magma (element of the magmatic universe).
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct Magma {
    pub id: u64,
    pub level: u32,
}

impl Magma {
    pub fn new(id: u64, level: u32) -> Self {
        assert!(level >= 1, "hierarchy_level_positive: level must be >= 1");
        Self { id, level }
    }
}

impl PartialOrd for Magma {
    fn partial_cmp(&self, other: &Self) -> Option<std::cmp::Ordering> {
        Some(self.id.cmp(&other.id))
    }
}

impl Ord for Magma {
    fn cmp(&self, other: &Self) -> std::cmp::Ordering {
        self.id.cmp(&other.id)
    }
}

/// Hierarchy level of a magma.
pub fn hierarchy_level(x: &Magma) -> u32 {
    x.level
}

/// Predecessor map: pr(x) characterizes { y | y <= x }.
pub fn pr_contains(x: &Magma, y: &Magma) -> bool {
    y <= x
}

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

    #[test]
    fn test_level_positive() {
        let x = Magma::new(10, 3);
        assert!(hierarchy_level(&x) >= 1);
    }

    #[test]
    fn test_hierarchy_cumulative() {
        let x = Magma::new(5, 2);
        let y = Magma::new(10, 4);
        assert!(x <= y);
        assert!(hierarchy_level(&x) <= hierarchy_level(&y));
    }

    #[test]
    fn test_pr_reflexive() {
        let x = Magma::new(42, 3);
        assert!(pr_contains(&x, &x));
    }

    #[test]
    #[should_panic]
    fn test_level_zero_panics() {
        Magma::new(1, 0);
    }
}