//! Symbolic Regression Translation AST
//!
//! Provenance: Lean 4 → Safe Rust
//! Source: HeytingLean.Discovery.SRTranslation
//!
//! Expression tree for representing conjectured formulas over the 8
//! boundary-matrix features. The conjecturing agent builds these trees;
//! the provability oracle pattern-matches against certified templates.

use std::fmt;

/// The 8 boundary-matrix features extracted from chain complexes.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum SRVariable {
    HeightD1,  // V (vertices)
    WidthD1,   // E (edges)
    HeightD2,  // E (edges)
    WidthD2,   // F (faces)
    RankD1,    // rank of d1
    RankD2,    // rank of d2
    NullD1,    // nullity of d1
    NullD2,    // nullity of d2
}

impl fmt::Display for SRVariable {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::HeightD1 => write!(f, "height_d1"),
            Self::WidthD1  => write!(f, "width_d1"),
            Self::HeightD2 => write!(f, "height_d2"),
            Self::WidthD2  => write!(f, "width_d2"),
            Self::RankD1   => write!(f, "rank_d1"),
            Self::RankD2   => write!(f, "rank_d2"),
            Self::NullD1   => write!(f, "null_d1"),
            Self::NullD2   => write!(f, "null_d2"),
        }
    }
}

/// Binary operators in the expression tree.
#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash)]
pub enum SROp {
    Add,
    Sub,
    Mul,
    Eq,
    And,
}

impl fmt::Display for SROp {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Add => write!(f, "+"),
            Self::Sub => write!(f, "-"),
            Self::Mul => write!(f, "*"),
            Self::Eq  => write!(f, "="),
            Self::And => write!(f, "and"),
        }
    }
}

/// Symbolic regression expression tree.
#[derive(Debug, Clone, PartialEq, Eq)]
pub enum SRExpr {
    Var(SRVariable),
    Lit(i64),
    BinOp {
        op: SROp,
        lhs: Box<SRExpr>,
        rhs: Box<SRExpr>,
    },
}

impl SRExpr {
    /// Count feature-variable leaves in the expression tree.
    /// Matches the Lean definition: featureArity.
    pub fn feature_arity(&self) -> u32 {
        match self {
            Self::Var(_) => 1,
            Self::Lit(_) => 0,
            Self::BinOp { lhs, rhs, .. } => lhs.feature_arity() + rhs.feature_arity(),
        }
    }
}

impl fmt::Display for SRExpr {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Var(v) => write!(f, "{v}"),
            Self::Lit(n) => write!(f, "{n}"),
            Self::BinOp { op, lhs, rhs } => write!(f, "({lhs} {op} {rhs})"),
        }
    }
}

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

    #[test]
    fn test_render_euler_formula() {
        // V - E + F = 2  →  ((height_d1 - width_d1) + width_d2) = 2
        let expr = SRExpr::BinOp {
            op: SROp::Eq,
            lhs: Box::new(SRExpr::BinOp {
                op: SROp::Add,
                lhs: Box::new(SRExpr::BinOp {
                    op: SROp::Sub,
                    lhs: Box::new(SRExpr::Var(SRVariable::HeightD1)),
                    rhs: Box::new(SRExpr::Var(SRVariable::WidthD1)),
                }),
                rhs: Box::new(SRExpr::Var(SRVariable::WidthD2)),
            }),
            rhs: Box::new(SRExpr::Lit(2)),
        };
        assert_eq!(
            expr.to_string(),
            "(((height_d1 - width_d1) + width_d2) = 2)"
        );
        assert_eq!(expr.feature_arity(), 3);
    }

    #[test]
    fn test_render_betti_one() {
        // null_d1 - rank_d2 = 2
        let expr = SRExpr::BinOp {
            op: SROp::Eq,
            lhs: Box::new(SRExpr::BinOp {
                op: SROp::Sub,
                lhs: Box::new(SRExpr::Var(SRVariable::NullD1)),
                rhs: Box::new(SRExpr::Var(SRVariable::RankD2)),
            }),
            rhs: Box::new(SRExpr::Lit(2)),
        };
        assert_eq!(expr.to_string(), "((null_d1 - rank_d2) = 2)");
        assert_eq!(expr.feature_arity(), 2);
    }

    #[test]
    fn test_literal_arity_zero() {
        assert_eq!(SRExpr::Lit(42).feature_arity(), 0);
    }

    #[test]
    fn test_variable_arity_one() {
        assert_eq!(SRExpr::Var(SRVariable::RankD1).feature_arity(), 1);
    }
}