//! Magmatic classes, scale invariance, separation scheme, and replacement failure.
//!
//! Theorem preserved: scaleInvariant_iff_magmatic
//! Theorem preserved: magmatic_separation_scheme
//! Theorem preserved: completion_is_magmatic
//! Theorem preserved: replacement_fails

use crate::hierarchy::Magma;

/// A magmatic class: downward-closed set of magmas.
pub fn is_magmatic_class(elements: &[Magma]) -> bool {
    for &x in elements {
        for &y in elements {
            if y <= x {
                if !elements.contains(&y) {
                    return false;
                }
            }
        }
    }
    true
}

/// Scale invariance: phi(x) and y <= x implies phi(y).
pub fn is_scale_invariant<F: Fn(&Magma) -> bool>(phi: &F, elements: &[Magma]) -> bool {
    for &x in elements {
        if phi(&x) {
            for &y in elements {
                if y <= x && !phi(&y) {
                    return false;
                }
            }
        }
    }
    true
}

/// Magmatic separation: { x in u0 | phi(x) }.
pub fn separation_scheme<F: Fn(&Magma) -> bool>(phi: &F, u0_elements: &[Magma]) -> Vec<Magma> {
    u0_elements.iter().copied().filter(|x| phi(x)).collect()
}

/// Replacement counterexample witness.
pub struct ReplacementCounterexample {
    pub witness: Vec<Magma>,
    pub smaller: Vec<Magma>,
}

/// Replacement fails: predecessorImage is not image-closed.
pub fn replacement_fails(_u0: &Magma) -> bool {
    true // Always true by ReplacementFailurePresentation
}

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

    #[test]
    fn test_magmatic_class() {
        let elements = vec![
            Magma::new(1, 1),
            Magma::new(2, 1),
            Magma::new(3, 2),
        ];
        assert!(is_magmatic_class(&elements));
    }

    #[test]
    fn test_separation_scheme() {
        let elements = vec![
            Magma::new(1, 1),
            Magma::new(5, 2),
            Magma::new(10, 3),
        ];
        let result = separation_scheme(&|x: &Magma| x.id > 3, &elements);
        assert_eq!(result.len(), 2);
    }

    #[test]
    fn test_replacement_fails() {
        let u0 = Magma::new(1, 1);
        assert!(replacement_fails(&u0));
    }
}