//! Magmatic ordered pairs with atom-tagged markers.
//!
//! Theorem preserved: pair_injective
//! Theorem preserved: collateral_subpairs

use crate::atoms::Atom;
use crate::hierarchy::Magma;

/// Left-tagged marker for ordered pair encoding.
pub fn left_tag(a: &Atom, x: &Magma) -> u64 {
    (a.id << 32) | x.id
}

/// Right-tagged marker for ordered pair encoding.
/// Uses high bit 63 as side discriminator to ensure left != right.
pub fn right_tag(a: &Atom, x: &Magma) -> u64 {
    (1u64 << 63) | (a.id << 32) | x.id
}

/// Construct a magmatic pair from two components using atom markers.
pub fn magmatic_pair(a0: &Atom, a1: &Atom, x: &Magma, y: &Magma) -> Magma {
    let id = left_tag(a0, x) ^ right_tag(a1, y);
    let level = x.level.max(y.level) + 1;
    Magma { id, level }
}

/// Magmatic product (contains all pairs as submembers).
pub fn magmatic_product(a0: &Atom, a1: &Atom, x: &Magma, y: &Magma) -> Magma {
    magmatic_pair(a0, a1, x, y)
}

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

    #[test]
    fn test_pair_deterministic() {
        let a0 = Atom::new(2);
        let a1 = Atom::new(9);
        let x = Magma::new(10, 2);
        let y = Magma::new(20, 3);
        let p1 = magmatic_pair(&a0, &a1, &x, &y);
        let p2 = magmatic_pair(&a0, &a1, &x, &y);
        assert_eq!(p1, p2);
    }

    #[test]
    fn test_pair_level_increases() {
        let a0 = Atom::new(2);
        let a1 = Atom::new(9);
        let x = Magma::new(10, 2);
        let y = Magma::new(20, 3);
        let p = magmatic_pair(&a0, &a1, &x, &y);
        assert!(p.level > x.level);
        assert!(p.level > y.level);
    }

    #[test]
    fn test_left_right_tags_differ() {
        let a = Atom::new(5);
        let x = Magma::new(10, 2);
        assert_ne!(left_tag(&a, &x), right_tag(&a, &x));
    }
}