geoit 0.0.2

use crate::algebra::blade_new::grade;
use crate::governance::expr::{EvalContext, Expr};
use crate::governance::governance::Governance;
use crate::governance::reading::VariableMap;
use crate::governance::rule::TransformRule;
use crate::scalar::{Rat, Scalar};

/// Result of structurally validating a construction against its class.
#[derive(Clone, Debug)]
pub struct ValidationResult {
    /// True if all grade constraints and equations are satisfied.
    pub valid: bool,
    /// Per-equation results.
    pub equation_results: Vec<bool>,
    /// True if all output blades are in permitted grades.
    pub grade_valid: bool,
    /// If invalid, a counterexample: parameter values that violate an equation.
    pub counterexample: Option<Vec<Scalar>>,
}

/// Compute the maximum polynomial degree of an Expr in its parameters.
/// Param → 1, Literal/Generator/DerivedGen → 0, Add → max, Mul → sum, Pow → base*n.
fn expr_param_degree(expr: &Expr) -> usize {
    match expr {
        Expr::Param(_) => 1,
        Expr::Generator(_) | Expr::DerivedGen(_) | Expr::Literal(_) => 0,
        Expr::Add(a, b) => expr_param_degree(a).max(expr_param_degree(b)),
        Expr::Mul(a, b) => expr_param_degree(a) + expr_param_degree(b),
        Expr::Neg(a) => expr_param_degree(a),
        Expr::Pow(base, n) => expr_param_degree(base) * (*n as usize),
        Expr::Construct(_, args) => args.iter().map(|a| expr_param_degree(a)).max().unwrap_or(0),
        Expr::Outer(a, b) => expr_param_degree(a) + expr_param_degree(b),
        Expr::Inner(a, b) => expr_param_degree(a) + expr_param_degree(b),
        Expr::Reverse(a) => expr_param_degree(a),
        Expr::Dual(a) => expr_param_degree(a),
        Expr::Sandwich(a, b) => expr_param_degree(a) * 2 + expr_param_degree(b),
        Expr::ValueRef(_) => 0,
        Expr::GradeProject(a, _) => expr_param_degree(a),
        Expr::LeftContract(a, b) => expr_param_degree(a) + expr_param_degree(b),
        Expr::ScalarProduct(a, b) => expr_param_degree(a) + expr_param_degree(b),
        Expr::Read(inner, _) => expr_param_degree(inner),
        Expr::WithGov(_, inner) => expr_param_degree(inner),
        Expr::Embed(inner, _) => expr_param_degree(inner),
        Expr::Morph(inner, _) => expr_param_degree(inner),
        Expr::Probe => 0,
        Expr::Object => 0,
    }
}

/// Maximum degree of a polynomial (in its own variables).
fn poly_max_degree(poly: &crate::governance::poly::Poly) -> usize {
    poly.terms
        .keys()
        .map(|exp| exp.iter().map(|&e| e as usize).sum::<usize>())
        .max()
        .unwrap_or(0)
}

/// Generate a grid of rational test points.
/// Returns (grid_size+1)^arity points using values 0, 1, ..., grid_size.
pub fn grid_points(arity: usize, grid_size: usize) -> Vec<Vec<Rat>> {
    if arity == 0 {
        return vec![vec![]];
    }
    let mut points = Vec::new();
    let sub = grid_points(arity - 1, grid_size);
    for val in 0..=grid_size {
        let r = Rat::from(val as i64);
        for s in &sub {
            let mut p = vec![r];
            p.extend_from_slice(s);
            points.push(p);
        }
    }
    points
}

/// Validate that a construction structurally satisfies its class equations.
///
/// The method: the composition (equation ∘ construction) is a polynomial
/// in the construction parameters. If this polynomial vanishes at a
/// sufficiently large grid of rational points, it is identically zero.
///
/// Grid size: for a polynomial of degree d in k variables, evaluating at
/// (d+1)^k points and getting all zeros proves the polynomial is zero.
/// The composed degree is equation_degree * construction_degree.
pub fn validate_construction(gov: &Governance, construction_idx: usize) -> ValidationResult {
    let constr = &gov.constructions[construction_idx];
    let class = &gov.geom_classes[constr.class_index];

    if class.equations.is_empty() {
        return ValidationResult {
            valid: true,
            equation_results: vec![],
            grade_valid: true,
            counterexample: None,
        };
    }

    let var_map = VariableMap::for_grade_mask(&gov.sig, class.grade_mask);

    // Compute required grid size
    let expr_deg = expr_param_degree(&constr.body);
    let max_eq_deg = class
        .equations
        .iter()
        .map(poly_max_degree)
        .max()
        .unwrap_or(0);
    let composed_deg = max_eq_deg * expr_deg;
    let grid_size = composed_deg + 1; // need degree+1 points per dimension

    // Cap grid to prevent combinatorial explosion
    let grid_size = grid_size.min(8);
    let points = grid_points(constr.arity, grid_size);

    let mut equation_results = vec![true; class.equations.len()];
    let mut counterexample = None;

    for pt in &points {
        // Evaluate construction at this point
        let params: Vec<Scalar> = pt.iter().map(|&r| Scalar::Rat(r)).collect();
        let mv = constr.body.eval(&EvalContext {
            params: &params,
            sig: &gov.sig,
            derived_gens: &gov.derived_gens,
            constructions: &gov.constructions,
            mv_table: &[],
            governances: &[],
            mv_governance_indices: &[],
            embeddings: &[],
            morphisms: &[],
            probe_mv: None,
            object_mv: None,
        });

        // Extract blade coefficients at permitted grades
        let values: Vec<Rat> = var_map
            .var_to_mask
            .iter()
            .map(|&mask| mv.coefficient(mask).try_as_rat().unwrap_or(Rat::ZERO))
            .collect();

        // Evaluate each equation
        for (i, eq) in class.equations.iter().enumerate() {
            let residual = eq.eval(&values);
            if !residual.is_zero() {
                equation_results[i] = false;
                if counterexample.is_none() {
                    counterexample = Some(params.clone());
                }
            }
        }
    }

    let valid = equation_results.iter().all(|&r| r);
    ValidationResult {
        valid,
        equation_results,
        grade_valid: true,
        counterexample,
    }
}

/// Validate that a transform rule produces output satisfying its declared output class.
///
/// Method: for each input class, find a construction. Generate grid-point inputs,
/// apply the rule's operation, and check the output against the output class's
/// grade constraints and polynomial equations.
///
/// Returns `None` if validation cannot proceed (missing constructions).
pub fn validate_transform_rule(gov: &Governance, rule: &TransformRule) -> Option<ValidationResult> {
    // Find a construction for each input class
    let input_constructions: Vec<&crate::governance::construction::Construction> = rule
        .input_classes
        .iter()
        .filter_map(|&ci| gov.constructions.iter().find(|c| c.class_index == ci))
        .collect();
    if input_constructions.len() != rule.input_classes.len() {
        return None; // can't validate without constructions for all inputs
    }

    let output_class = &gov.geom_classes[rule.output_class];
    let var_map = VariableMap::for_grade_mask(&gov.sig, output_class.grade_mask);

    // Generate grids for each input (cap at size 3 to prevent combinatorial explosion)
    let grids: Vec<Vec<Vec<Rat>>> = input_constructions
        .iter()
        .map(|c| grid_points(c.arity, 3))
        .collect();

    let mut equation_results = vec![true; output_class.equations.len()];
    let mut grade_valid = true;
    let mut counterexample: Option<Vec<Scalar>> = None;

    // For 1-input rules, iterate the single grid
    // For 2-input rules, iterate the cartesian product
    if grids.len() == 1 {
        for pt in &grids[0] {
            let params: Vec<Scalar> = pt.iter().map(|&r| Scalar::Rat(r)).collect();
            let mv = input_constructions[0].construct(
                &params,
                &gov.sig,
                &gov.derived_gens,
                &gov.constructions,
            );
            if let Ok(input_mv) = mv {
                let result = rule.operation.apply(&[&input_mv], &gov.sig);
                check_result_against_class(
                    &result,
                    output_class,
                    &var_map,
                    &mut equation_results,
                    &mut grade_valid,
                    &mut counterexample,
                    &params,
                );
            }
        }
    } else if grids.len() == 2 {
        // Cap total pairs
        let max_pairs = 200;
        let mut pair_count = 0;
        for pa in &grids[0] {
            for pb in &grids[1] {
                pair_count += 1;
                if pair_count > max_pairs {
                    break;
                }
                let params_a: Vec<Scalar> = pa.iter().map(|&r| Scalar::Rat(r)).collect();
                let params_b: Vec<Scalar> = pb.iter().map(|&r| Scalar::Rat(r)).collect();
                let mv_a = input_constructions[0].construct(
                    &params_a,
                    &gov.sig,
                    &gov.derived_gens,
                    &gov.constructions,
                );
                let mv_b = input_constructions[1].construct(
                    &params_b,
                    &gov.sig,
                    &gov.derived_gens,
                    &gov.constructions,
                );
                if let (Ok(a), Ok(b)) = (mv_a, mv_b) {
                    let result = rule.operation.apply(&[&a, &b], &gov.sig);
                    check_result_against_class(
                        &result,
                        output_class,
                        &var_map,
                        &mut equation_results,
                        &mut grade_valid,
                        &mut counterexample,
                        &params_a,
                    );
                }
            }
        }
    }

    let valid = grade_valid && equation_results.iter().all(|&r| r);
    Some(ValidationResult {
        valid,
        equation_results,
        grade_valid,
        counterexample,
    })
}

/// Check a result Mv against a class's grade constraint and equations.
fn check_result_against_class(
    result: &crate::algebra::mv::Mv,
    class: &crate::governance::geom_class::GeomClass,
    var_map: &VariableMap,
    equation_results: &mut [bool],
    grade_valid: &mut bool,
    counterexample: &mut Option<Vec<Scalar>>,
    params: &[Scalar],
) {
    // Grade check: verify all blades are in permitted grades
    for (mask, coeff) in result.blades() {
        if !coeff.is_zero() && !class.grade_permitted(grade(mask)) {
            *grade_valid = false;
            for r in equation_results.iter_mut() {
                *r = false;
            }
            if counterexample.is_none() {
                *counterexample = Some(params.to_vec());
            }
            return;
        }
    }

    // Equation check
    let values: Vec<Rat> = var_map
        .var_to_mask
        .iter()
        .map(|&mask| result.coefficient(mask).try_as_rat().unwrap_or(Rat::ZERO))
        .collect();

    for (i, eq) in class.equations.iter().enumerate() {
        let residual = eq.eval(&values);
        if !residual.is_zero() {
            equation_results[i] = false;
            if counterexample.is_none() {
                *counterexample = Some(params.to_vec());
            }
        }
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::algebra::mv::Mv;
    use crate::algebra::signature::Signature;
    use crate::governance::field::FieldOp;
    use crate::governance::geom_class::{inner_product_poly, norm_poly};
    use crate::governance::{Construction, Expr, GeomClass};
    use crate::scalar::Rat;

    fn vga3_vector_gov() -> Governance {
        Governance {
            sig: Signature::new(0, 0, 3).unwrap(),
            derived_gens: vec![],
            geom_classes: vec![GeomClass::grades_only(&[1])],
            constructions: vec![Construction {
                class_index: 0,
                arity: 3,
                body: Expr::Add(
                    Expr::add(
                        Expr::mul(Expr::param(0), Expr::gen(0)),
                        Expr::mul(Expr::param(1), Expr::gen(1)),
                    ),
                    Expr::mul(Expr::param(2), Expr::gen(2)),
                ),
            }],
            probe: None,
            transform_rules: vec![],
        }
    }

    fn cga3_point_gov() -> Governance {
        let sig = Signature::new(1, 0, 4).unwrap();
        let gm = 0b10u64;
        let eo = Mv::from_rat_terms(&[(0b00001, Rat::new(1, 2)), (0b00010, Rat::new(1, 2))]);
        let einf = Mv::from_rat_terms(&[(0b00001, Rat::from(-1)), (0b00010, Rat::from(1))]);
        let vm = VariableMap::for_grade_mask(&sig, gm);
        let null_eq = norm_poly(&sig, gm, vm.num_vars, &vm.mask_to_var);
        let ip_eq = inner_product_poly(&einf, &sig, gm, Rat::ONE, vm.num_vars, &vm.mask_to_var);

        let euclidean = Expr::Add(
            Expr::add(
                Expr::mul(Expr::param(0), Expr::gen(2)),
                Expr::mul(Expr::param(1), Expr::gen(3)),
            ),
            Expr::mul(Expr::param(2), Expr::gen(4)),
        );
        let r_sq = Expr::Add(
            Expr::add(
                Expr::mul(Expr::param(0), Expr::param(0)),
                Expr::mul(Expr::param(1), Expr::param(1)),
            ),
            Expr::mul(Expr::param(2), Expr::param(2)),
        );
        let neg_half_r2 = Expr::mul(
            Box::new(Expr::Literal(Scalar::Rat(Rat::new(-1, 2)))),
            Box::new(r_sq),
        );
        let conformal = Expr::Mul(neg_half_r2, Expr::dgen(1));
        let body = Expr::Add(
            Box::new(Expr::Add(Box::new(euclidean), Box::new(conformal))),
            Expr::dgen(0),
        );

        Governance {
            sig,
            derived_gens: vec![eo, einf],
            geom_classes: vec![GeomClass {
                grade_mask: gm,
                equations: vec![null_eq, ip_eq],
                inequalities: vec![],
                field_op: FieldOp::default(),
                expected_profile: None,
            }],
            constructions: vec![Construction {
                class_index: 0,
                arity: 3,
                body,
            }],
            probe: None,
            transform_rules: vec![],
        }
    }

    #[test]
    fn vga_vector_valid() {
        let gov = vga3_vector_gov();
        let r = validate_construction(&gov, 0);
        assert!(r.valid);
        assert!(r.equation_results.is_empty()); // no equations for VGA Vector
    }

    #[test]
    fn cga_point_valid() {
        let gov = cga3_point_gov();
        let r = validate_construction(&gov, 0);
        assert!(
            r.valid,
            "CGA Point construction should be structurally valid, got {:?}",
            r.counterexample
        );
        assert_eq!(r.equation_results.len(), 2);
        assert!(r.equation_results[0], "null equation should hold");
        assert!(r.equation_results[1], "normalization equation should hold");
    }

    #[test]
    fn cga_sphere_valid() {
        let sig = Signature::new(1, 0, 4).unwrap();
        let gm = 0b10u64;
        let vm = VariableMap::for_grade_mask(&sig, gm);
        // Sphere: normalization only (v1 + v2 - 1 = 0), no null
        let mut ip_eq = crate::governance::poly::Poly::zero(vm.num_vars);
        ip_eq.terms.insert(vec![1, 0, 0, 0, 0], Rat::ONE); // v1
        ip_eq.terms.insert(vec![0, 1, 0, 0, 0], Rat::ONE); // v2
        ip_eq.terms.insert(vec![0, 0, 0, 0, 0], -Rat::ONE); // -1

        // Construction: (1-cplus)*eminus + cplus*eplus + x*e1 + y*e2 + z*e3
        let body = Expr::Add(
            Expr::add(
                Expr::add(
                    Expr::mul(
                        Box::new(Expr::Add(Expr::lit(1), Expr::neg(Expr::param(0)))),
                        Expr::gen(0),
                    ),
                    Expr::mul(Expr::param(0), Expr::gen(1)),
                ),
                Expr::mul(Expr::param(1), Expr::gen(2)),
            ),
            Expr::add(
                Expr::mul(Expr::param(2), Expr::gen(3)),
                Expr::mul(Expr::param(3), Expr::gen(4)),
            ),
        );

        let gov = Governance {
            sig,
            derived_gens: vec![],
            geom_classes: vec![GeomClass {
                grade_mask: gm,
                equations: vec![ip_eq],
                inequalities: vec![],
                field_op: FieldOp::default(),
                expected_profile: None,
            }],
            constructions: vec![Construction {
                class_index: 0,
                arity: 4,
                body,
            }],
            probe: None,
            transform_rules: vec![],
        };
        let r = validate_construction(&gov, 0);
        assert!(
            r.valid,
            "Sphere construction should be valid, got {:?}",
            r.counterexample
        );
    }

    #[test]
    fn invalid_construction_detected() {
        // Deliberately wrong: claim grade-1 VGA Vector but actually construct a bivector
        let sig = Signature::new(0, 0, 3).unwrap();
        let vm = VariableMap::for_grade_mask(&sig, 0b10); // grade 1
                                                          // Equation: norm² = 0 (which a bivector won't satisfy via grade check...
                                                          // Actually let's do: equation v1 = 0 (blade g0 must be zero)
        let eq = crate::governance::poly::Poly::variable(0, vm.num_vars); // v1 = 0
        let class = GeomClass {
            grade_mask: 0b10,
            equations: vec![eq],
            inequalities: vec![],
            field_op: FieldOp::default(),
            expected_profile: None,
        };

        // Construction puts param 0 into g0 — violates v1=0 for nonzero param
        let body = *Expr::mul(Expr::param(0), Expr::gen(0));
        let gov = Governance {
            sig,
            derived_gens: vec![],
            geom_classes: vec![class],
            constructions: vec![Construction {
                class_index: 0,
                arity: 1,
                body,
            }],
            probe: None,
            transform_rules: vec![],
        };
        let r = validate_construction(&gov, 0);
        assert!(!r.valid, "Should detect invalid construction");
        assert!(r.counterexample.is_some());
    }

    #[test]
    fn pga_point_valid() {
        // PGA Point: grade 3, no equations (only inequality)
        let gov = Governance {
            sig: Signature::new(0, 1, 3).unwrap(),
            derived_gens: vec![],
            geom_classes: vec![GeomClass {
                grade_mask: 0b1000,
                equations: vec![],
                inequalities: vec![],
                field_op: FieldOp::default(),
                expected_profile: None,
            }],
            constructions: vec![Construction {
                class_index: 0,
                arity: 3,
                body: Expr::Add(
                    Expr::add(
                        Expr::add(
                            Expr::mul(
                                Expr::mul(Expr::mul(Expr::param(0), Expr::gen(0)), Expr::gen(2)),
                                Expr::gen(3),
                            ),
                            Expr::neg(Expr::mul(
                                Expr::mul(Expr::mul(Expr::param(1), Expr::gen(0)), Expr::gen(1)),
                                Expr::gen(3),
                            )),
                        ),
                        Expr::mul(
                            Expr::mul(Expr::mul(Expr::param(2), Expr::gen(0)), Expr::gen(1)),
                            Expr::gen(2),
                        ),
                    ),
                    Expr::mul(Expr::mul(Expr::gen(1), Expr::gen(2)), Expr::gen(3)),
                ),
            }],
            probe: None,
            transform_rules: vec![],
        };
        let r = validate_construction(&gov, 0);
        assert!(r.valid);
    }

    #[test]
    fn expr_degree_calculations() {
        assert_eq!(expr_param_degree(&Expr::Param(0)), 1);
        assert_eq!(expr_param_degree(&Expr::Literal(Scalar::from(5i64))), 0);
        assert_eq!(expr_param_degree(&Expr::Generator(0)), 0);
        // x * y → degree 2
        let xy = Expr::Mul(Expr::param(0), Expr::param(1));
        assert_eq!(expr_param_degree(&xy), 2);
        // x^2 + y → degree 2
        let x2_plus_y = Expr::Add(Box::new(Expr::Pow(Expr::param(0), 2)), Expr::param(1));
        assert_eq!(expr_param_degree(&x2_plus_y), 2);
        // (x^2 + y^2 + z^2) * einf → degree 2 (times degree 0)
        let r_sq = Expr::Add(
            Expr::add(
                Expr::mul(Expr::param(0), Expr::param(0)),
                Expr::mul(Expr::param(1), Expr::param(1)),
            ),
            Expr::mul(Expr::param(2), Expr::param(2)),
        );
        assert_eq!(expr_param_degree(&r_sq), 2);
        let scaled = Expr::Mul(Box::new(r_sq), Expr::dgen(0));
        assert_eq!(expr_param_degree(&scaled), 2);
    }

    #[test]
    fn validate_rule_sandwich_vectors_valid() {
        // In VGA(3): sandwich(vector, vector) produces a vector (reflection)
        use crate::governance::rule::{ReadingDerivation, TransformOp, TransformRule};
        let gov = vga3_vector_gov();
        let rule = TransformRule {
            name: "Reflect".into(),
            input_classes: vec![0, 0], // both vectors
            output_class: 0,           // result is a vector
            operation: TransformOp::Sandwich,
            reading_derivation: ReadingDerivation::Rederive,
        };
        let result = validate_transform_rule(&gov, &rule);
        assert!(result.is_some());
        assert!(
            result.unwrap().valid,
            "sandwich(vector, vector) should produce a vector in VGA(3)"
        );
    }

    #[test]
    fn validate_rule_reverse_vector_valid() {
        // reverse(vector) is still a vector (grade 1 is unchanged by reversal)
        use crate::governance::rule::{ReadingDerivation, TransformOp, TransformRule};
        let gov = vga3_vector_gov();
        let rule = TransformRule {
            name: "Rev".into(),
            input_classes: vec![0],
            output_class: 0,
            operation: TransformOp::Reverse,
            reading_derivation: ReadingDerivation::Rederive,
        };
        let result = validate_transform_rule(&gov, &rule);
        assert!(result.is_some());
        assert!(result.unwrap().valid);
    }

    #[test]
    fn validate_rule_geometric_produces_wrong_grade_invalid() {
        // geometric(vector, vector) in VGA produces scalar + bivector, NOT a vector
        use crate::governance::rule::{ReadingDerivation, TransformOp, TransformRule};
        let gov = vga3_vector_gov();
        let rule = TransformRule {
            name: "Bad".into(),
            input_classes: vec![0, 0],
            output_class: 0,                   // claims result is grade-1 vector
            operation: TransformOp::Geometric, // but geo product gives scalar + bivector
            reading_derivation: ReadingDerivation::Rederive,
        };
        let result = validate_transform_rule(&gov, &rule);
        assert!(result.is_some());
        assert!(
            !result.unwrap().valid,
            "geometric(vector, vector) should NOT validate as vector class"
        );
    }
}