/// Lean 4 → Rust transpilation: SupportIsSearch.Contextual.Kernel
/// Source: SupportIsSearch/Contextual/Kernel.lean (75 lines)
///
/// The core search kernel: fuel-bounded mutual recursion between
/// search, searchAnyAssumption, and fires.

use crate::syntax::*;

/// Fuel-bounded proof search for a goal in a program.
pub fn search(fuel: u32, p: &Program, g: &Goal) -> bool {
    if fuel == 0 {
        return false;
    }
    let f = fuel - 1;
    match g {
        Goal::Atom(a) => search_any_assumption(f, p, p, a),
        Goal::Imp(g1, g2) => {
            let mut extended = vec![g1.as_ref().clone()];
            extended.extend(p.iter().cloned());
            search(f, &extended, g2)
        }
        Goal::Conj(g1, g2) => search(f, p, g1) && search(f, p, g2),
        Goal::Disj(g1, g2) => search(f, p, g1) || search(f, p, g2),
        Goal::All(body) => {
            let fresh = fresh_atom_for_goal(p, body);
            let instantiated = subst_goal(body, 0, fresh);
            search(f, p, &instantiated)
        }
    }
}

/// Try firing each assumption against target atom.
pub fn search_any_assumption(fuel: u32, p: &Program, gs: &[Goal], a: &AtomVar) -> bool {
    match gs.split_first() {
        None => false,
        Some((head, tail)) => {
            fires(fuel, p, head, a) || search_any_assumption(fuel, p, tail, a)
        }
    }
}

/// Does assumption g fire for atom a in program P?
pub fn fires(fuel: u32, p: &Program, g: &Goal, a: &AtomVar) -> bool {
    if fuel == 0 {
        return false;
    }
    let f = fuel - 1;
    match g {
        Goal::Atom(b) => b == a,
        Goal::Imp(g1, g2) => search(f, p, g1) && fires(f, p, g2, a),
        Goal::Conj(_, _) | Goal::Disj(_, _) => false,
        Goal::All(body) => match a {
            AtomVar::Atom(atm) => {
                let instantiated = subst_goal(body, 0, *atm);
                fires(f, p, &instantiated, a)
            }
            AtomVar::Bvar(_) => {
                let fresh = fresh_atom_for_goal(p, body);
                let instantiated = subst_goal(body, 0, fresh);
                fires(f, p, &instantiated, a)
            }
        },
    }
}

/// SearchSupports: existential fuel — does there exist a fuel level
/// at which search succeeds?
pub fn search_supports(p: &Program, g: &Goal, max_fuel: u32) -> bool {
    (0..=max_fuel).any(|f| search(f, p, g))
}

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

    #[test]
    fn test_atom_self_search() {
        // An atom should be searchable from a program containing it
        let a = Atom { id: 0 };
        let g = Goal::Atom(AtomVar::Atom(a));
        let p = vec![Goal::Atom(AtomVar::Atom(a))];
        assert!(search_supports(&p, &g, 10));
    }

    #[test]
    fn test_atom_not_in_program() {
        let a = Atom { id: 0 };
        let b = Atom { id: 1 };
        let g = Goal::Atom(AtomVar::Atom(b));
        let p = vec![Goal::Atom(AtomVar::Atom(a))];
        assert!(!search_supports(&p, &g, 10));
    }

    #[test]
    fn test_identity_searchable() {
        // p → p should be searchable from any program
        let p_atom = Atom { id: 0 };
        let g = Goal::Imp(
            Box::new(Goal::Atom(AtomVar::Atom(p_atom))),
            Box::new(Goal::Atom(AtomVar::Atom(p_atom))),
        );
        assert!(search_supports(&vec![], &g, 10));
    }
}