//! Magmatic atoms: a partial order with no minimal elements.
//!
//! Theorem preserved: predecessors_infinite
//! Theorem preserved: predecessors_eq_iff
//! Theorem preserved: descendingChain_injective

/// An atom in the magmatic universe.
#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash)]
pub struct Atom {
    pub id: u64,
}

impl Atom {
    pub fn new(id: u64) -> Self {
        Self { id }
    }

    /// Two atoms are incomparable when neither lies below the other.
    pub fn incomparable(&self, other: &Atom) -> bool {
        self.id != other.id && !(self.id < other.id) && !(other.id < self.id)
    }
}

/// The predecessor set of an atom (all atoms <= a).
pub fn predecessors(a: &Atom) -> Vec<Atom> {
    (0..=a.id).map(Atom::new).collect()
}

/// Canonical infinite descending chain below an atom.
pub fn descending_chain(a: &Atom, n: u64) -> Atom {
    Atom::new(a.id.saturating_sub(n))
}

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

    #[test]
    fn test_atom_ordering() {
        let a = Atom::new(5);
        let b = Atom::new(3);
        assert!(b < a);
        assert!(!(a < b));
    }

    #[test]
    fn test_predecessors_nonempty() {
        let a = Atom::new(5);
        let preds = predecessors(&a);
        assert!(preds.len() >= 5);
        assert!(preds.contains(&a));
    }

    #[test]
    fn test_descending_chain_injective() {
        let a = Atom::new(10);
        let c0 = descending_chain(&a, 0);
        let c1 = descending_chain(&a, 1);
        let c2 = descending_chain(&a, 2);
        assert_ne!(c0, c1);
        assert_ne!(c1, c2);
        assert_ne!(c0, c2);
    }
}