//! Lower-open subsets of the atom preorder.
//!
//! Theorem preserved: lowerOpen_infinite
//! Theorem preserved: no_minimal_magma
//! Theorem preserved: principal_le_iff

use crate::atoms::Atom;

/// A lower-open, nonempty subset of atoms.
#[derive(Debug, Clone)]
pub struct LowerOpen {
    pub elements: Vec<Atom>,
}

impl LowerOpen {
    /// The principal lower-open set generated by an atom.
    pub fn principal(a: &Atom) -> Self {
        let elements: Vec<Atom> = (0..=a.id).map(Atom::new).collect();
        Self { elements }
    }

    pub fn is_nonempty(&self) -> bool {
        !self.elements.is_empty()
    }

    pub fn contains(&self, a: &Atom) -> bool {
        self.elements.contains(a)
    }

    pub fn le(&self, other: &LowerOpen) -> bool {
        self.elements.iter().all(|a| other.contains(a))
    }
}

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

    #[test]
    fn test_principal_nonempty() {
        let a = Atom::new(5);
        let lo = LowerOpen::principal(&a);
        assert!(lo.is_nonempty());
        assert!(lo.contains(&a));
    }

    #[test]
    fn test_principal_le() {
        let a = Atom::new(3);
        let b = Atom::new(5);
        let la = LowerOpen::principal(&a);
        let lb = LowerOpen::principal(&b);
        assert!(la.le(&lb));
        assert!(!lb.le(&la));
    }
}