/// Lean 4 → Rust transpilation: SupportIsSearch.Contextual.Encoding
/// Source: SupportIsSearch/Contextual/Encoding.lean (28 lines)
///
/// CPS encoding of IPL formulas as goals.

use crate::syntax::*;
use crate::ipl::IPL;

/// CPS encoding: IPL → Goal
///
/// - atom p     ↦ atom p
/// - bot        ↦ ∀x. x
/// - conj φ ψ  ↦ ∀k. (⟦φ⟧ → ⟦ψ⟧ → k) → k
/// - disj φ ψ  ↦ ∀k. (⟦φ⟧ → k) → (⟦ψ⟧ → k) → k
/// - imp φ ψ   ↦ ⟦φ⟧ → ⟦ψ⟧
pub fn encode(phi: &IPL) -> Goal {
    match phi {
        IPL::Atom(a) => Goal::Atom(AtomVar::Atom(*a)),
        IPL::Bot => Goal::All(Box::new(Goal::Atom(AtomVar::Bvar(0)))),
        IPL::Conj(l, r) => {
            let k = Goal::Atom(AtomVar::Bvar(0));
            let el = encode(l);
            let er = encode(r);
            let inner = Goal::Imp(Box::new(el), Box::new(Goal::Imp(Box::new(er), Box::new(k))));
            let k2 = Goal::Atom(AtomVar::Bvar(0));
            Goal::All(Box::new(Goal::Imp(Box::new(inner), Box::new(k2))))
        }
        IPL::Disj(l, r) => {
            let k = Goal::Atom(AtomVar::Bvar(0));
            let el = encode(l);
            let er = encode(r);
            let branch_l = Goal::Imp(Box::new(el), Box::new(k));
            let k2 = Goal::Atom(AtomVar::Bvar(0));
            let branch_r = Goal::Imp(Box::new(er), Box::new(k2));
            let k3 = Goal::Atom(AtomVar::Bvar(0));
            Goal::All(Box::new(Goal::Imp(
                Box::new(branch_l),
                Box::new(Goal::Imp(Box::new(branch_r), Box::new(k3))),
            )))
        }
        IPL::Imp(l, r) => Goal::Imp(Box::new(encode(l)), Box::new(encode(r))),
    }
}

/// Encode an atomic base as a program of atom goals.
pub fn encode_base(atoms: &[Atom]) -> Program {
    atoms.iter().map(|a| Goal::Atom(AtomVar::Atom(*a))).collect()
}

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

    #[test]
    fn test_encode_atom() {
        let a = Atom { id: 0 };
        assert_eq!(encode(&IPL::Atom(a)), Goal::Atom(AtomVar::Atom(a)));
    }

    #[test]
    fn test_encode_bot_is_forall() {
        let g = encode(&IPL::Bot);
        assert!(matches!(g, Goal::All(_)));
    }

    #[test]
    fn test_encode_imp_preserves_structure() {
        let p = Atom { id: 0 };
        let q = Atom { id: 1 };
        let f = IPL::Imp(Box::new(IPL::Atom(p)), Box::new(IPL::Atom(q)));
        let g = encode(&f);
        assert!(matches!(g, Goal::Imp(_, _)));
    }
}