/// Lean 4 → Rust transpilation: SupportIsSearch.IPL
/// Source: SupportIsSearch/IPL.lean (48 lines)

use crate::syntax::Atom;

/// Intuitionistic propositional logic formulas.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum IPL {
    Atom(Atom),
    Bot,
    Conj(Box<IPL>, Box<IPL>),
    Disj(Box<IPL>, Box<IPL>),
    Imp(Box<IPL>, Box<IPL>),
}

/// Peirce's formula: ((p → q) → p) → p
pub fn peirce_formula(p: Atom, q: Atom) -> IPL {
    IPL::Imp(
        Box::new(IPL::Imp(
            Box::new(IPL::Imp(Box::new(IPL::Atom(p)), Box::new(IPL::Atom(q)))),
            Box::new(IPL::Atom(p)),
        )),
        Box::new(IPL::Atom(p)),
    )
}

/// Identity formula: p → p
pub fn identity_formula(p: Atom) -> IPL {
    IPL::Imp(Box::new(IPL::Atom(p)), Box::new(IPL::Atom(p)))
}

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

    #[test]
    fn test_peirce_is_implication() {
        let f = peirce_formula(Atom { id: 0 }, Atom { id: 1 });
        assert!(matches!(f, IPL::Imp(_, _)));
    }

    #[test]
    fn test_identity_is_implication() {
        let f = identity_formula(Atom { id: 0 });
        assert!(matches!(f, IPL::Imp(_, _)));
    }
}