/// Lean 4 → Rust transpilation: SupportIsSearch.Contextual.Context
/// Source: SupportIsSearch/Contextual/Context.lean (23 lines)
///
/// Atomic bases and base extension. This is where the paper-to-code gap
/// lives: the paper defines bases as programs, but this formalization
/// uses atomic bases.

use crate::syntax::Atom;

/// An atomic base: a set of atoms.
#[derive(Debug, Clone)]
pub struct Base {
    pub atoms: Vec<Atom>,
}

/// Base extension: B extends to C iff every atom in B is also in C.
pub fn base_extends(b: &Base, c: &Base) -> bool {
    b.atoms.iter().all(|a| c.atoms.contains(a))
}

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

    #[test]
    fn test_base_extends_refl() {
        let b = Base { atoms: vec![Atom { id: 0 }, Atom { id: 1 }] };
        assert!(base_extends(&b, &b));
    }

    #[test]
    fn test_base_extends_subset() {
        let b = Base { atoms: vec![Atom { id: 0 }] };
        let c = Base { atoms: vec![Atom { id: 0 }, Atom { id: 1 }] };
        assert!(base_extends(&b, &c));
        assert!(!base_extends(&c, &b));
    }
}