/// Lean 4 → Rust transpilation: SupportIsSearch.Syntax
/// Source: SupportIsSearch/Syntax.lean (162 lines)

/// Atom: identified by a natural number.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub struct Atom {
    pub id: u32,
}

/// AtomVar: either a concrete atom or a de Bruijn bound variable.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum AtomVar {
    Atom(Atom),
    Bvar(u32),
}

/// Goal: the goal language for the contextual kernel.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum Goal {
    Atom(AtomVar),
    Imp(Box<Goal>, Box<Goal>),
    Conj(Box<Goal>, Box<Goal>),
    Disj(Box<Goal>, Box<Goal>),
    All(Box<Goal>),
}

/// Program: a list of goals (clauses).
pub type Program = Vec<Goal>;

/// Substitute bvar `n` with concrete atom `a` in an AtomVar.
pub fn subst_atomvar(n: u32, a: Atom, v: &AtomVar) -> AtomVar {
    match v {
        AtomVar::Bvar(k) if *k == n => AtomVar::Atom(a),
        other => *other,
    }
}

/// Substitute bvar `n` with concrete atom `a` in a Goal.
pub fn subst_goal(g: &Goal, n: u32, a: Atom) -> Goal {
    match g {
        Goal::Atom(v) => Goal::Atom(subst_atomvar(n, a, v)),
        Goal::Imp(l, r) => Goal::Imp(
            Box::new(subst_goal(l, n, a)),
            Box::new(subst_goal(r, n, a)),
        ),
        Goal::Conj(l, r) => Goal::Conj(
            Box::new(subst_goal(l, n, a)),
            Box::new(subst_goal(r, n, a)),
        ),
        Goal::Disj(l, r) => Goal::Disj(
            Box::new(subst_goal(l, n, a)),
            Box::new(subst_goal(r, n, a)),
        ),
        Goal::All(body) => Goal::All(Box::new(subst_goal(body, n + 1, a))),
    }
}

/// Collect all concrete atoms appearing in a goal.
pub fn goal_atoms(g: &Goal) -> Vec<Atom> {
    match g {
        Goal::Atom(AtomVar::Atom(a)) => vec![*a],
        Goal::Atom(AtomVar::Bvar(_)) => vec![],
        Goal::Imp(l, r) | Goal::Conj(l, r) | Goal::Disj(l, r) => {
            let mut v = goal_atoms(l);
            v.extend(goal_atoms(r));
            v
        }
        Goal::All(body) => goal_atoms(body),
    }
}

/// Collect all concrete atoms in a program.
pub fn program_atoms(p: &Program) -> Vec<Atom> {
    p.iter().flat_map(goal_atoms).collect()
}

/// Compute a fresh atom not appearing in the program or goal.
pub fn fresh_atom_for_goal(p: &Program, g: &Goal) -> Atom {
    let mut max_id = 0u32;
    for a in program_atoms(p).iter().chain(goal_atoms(g).iter()) {
        if a.id > max_id {
            max_id = a.id;
        }
    }
    Atom { id: max_id + 1 }
}

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

    #[test]
    fn test_subst_atomvar_bvar_match() {
        let result = subst_atomvar(0, Atom { id: 42 }, &AtomVar::Bvar(0));
        assert_eq!(result, AtomVar::Atom(Atom { id: 42 }));
    }

    #[test]
    fn test_subst_atomvar_bvar_no_match() {
        let result = subst_atomvar(0, Atom { id: 42 }, &AtomVar::Bvar(1));
        assert_eq!(result, AtomVar::Bvar(1));
    }

    #[test]
    fn test_fresh_atom() {
        let p: Program = vec![Goal::Atom(AtomVar::Atom(Atom { id: 3 }))];
        let g = Goal::Atom(AtomVar::Atom(Atom { id: 5 }));
        assert_eq!(fresh_atom_for_goal(&p, &g), Atom { id: 6 });
    }
}