//! Bridge to Heyting nucleus: omega_R, irreducible complement, Heyting gap.
//!
//! Theorem preserved: gap_zero_iff_fixed
//! Theorem preserved: irreducible_has_nonzero_gap
//! Theorem preserved: fixed_core_magmatic
//! Theorem preserved: scale_invariance_triple_equivalence

use crate::hierarchy::Magma;

/// familyOf(x) = { y | y <= x }
pub fn family_of(x: &Magma, universe: &[Magma]) -> Vec<Magma> {
    universe.iter().copied().filter(|y| y <= x).collect()
}

/// A nucleus operator on sets of magmas.
pub struct Nucleus<F: Fn(&[Magma]) -> Vec<Magma>> {
    pub apply: F,
}

/// MagmaticNucleus: a nucleus that preserves magmatic classes.
pub struct MagmaticNucleus<F: Fn(&[Magma]) -> Vec<Magma>> {
    pub nucleus: Nucleus<F>,
}

impl<F: Fn(&[Magma]) -> Vec<Magma>> MagmaticNucleus<F> {
    /// Heyting gap: N.R(familyOf x) \ familyOf x
    pub fn heyting_gap(&self, x: &Magma, universe: &[Magma]) -> Vec<Magma> {
        let fam = family_of(x, universe);
        let image = (self.nucleus.apply)(&fam);
        image.into_iter().filter(|y| !fam.contains(y)).collect()
    }

    /// x is in omega_R iff N.R(familyOf x) = familyOf x
    pub fn is_fixed(&self, x: &Magma, universe: &[Magma]) -> bool {
        let fam = family_of(x, universe);
        let image = (self.nucleus.apply)(&fam);
        fam.len() == image.len() && fam.iter().all(|y| image.contains(y))
    }

    /// x is computationally irreducible iff x not in omega_R
    pub fn is_irreducible(&self, x: &Magma, universe: &[Magma]) -> bool {
        !self.is_fixed(x, universe)
    }
}

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

    fn identity_nucleus() -> MagmaticNucleus<impl Fn(&[Magma]) -> Vec<Magma>> {
        MagmaticNucleus {
            nucleus: Nucleus {
                apply: |xs: &[Magma]| xs.to_vec(),
            },
        }
    }

    #[test]
    fn test_family_of() {
        let universe = vec![
            Magma::new(1, 1),
            Magma::new(3, 2),
            Magma::new(5, 3),
        ];
        let fam = family_of(&Magma::new(3, 2), &universe);
        assert_eq!(fam.len(), 2); // 1 and 3
    }

    #[test]
    fn test_identity_nucleus_fixed() {
        let n = identity_nucleus();
        let universe = vec![Magma::new(1, 1), Magma::new(3, 2)];
        let x = Magma::new(3, 2);
        assert!(n.is_fixed(&x, &universe));
    }

    #[test]
    fn test_identity_gap_empty() {
        let n = identity_nucleus();
        let universe = vec![Magma::new(1, 1), Magma::new(3, 2)];
        let x = Magma::new(3, 2);
        let gap = n.heyting_gap(&x, &universe);
        assert!(gap.is_empty());
    }
}