//! Integration tests for Prime-Radiant Advanced Math Modules
//!
//! Tests cross-module interactions and end-to-end workflows including:
//! - Category theory operations
//! - HoTT path algebra
//! - Cross-module coherence

use prime_radiant_category::category::{
    Category, SetCategory, VectorCategory,
};
use prime_radiant_category::hott::{
    Term, Path, PathOps,
};

// ============================================================================
// CATEGORY THEORY INTEGRATION TESTS
// ============================================================================

mod category_integration {
    use super::*;

    /// Test SetCategory creation and basic operations
    #[test]
    fn test_set_category_basics() {
        let cat = SetCategory::new();
        assert_eq!(cat.objects().len(), 0);
        assert!(cat.verify_laws());
    }

    /// Test VectorCategory creation and dimension
    #[test]
    fn test_vector_category_basics() {
        let cat = VectorCategory::new(768);
        assert_eq!(cat.dimension(), 768);
        assert!(cat.verify_laws());
    }

    /// Test VectorCategory with different dimensions
    #[test]
    fn test_vector_category_dimensions() {
        // Common embedding dimensions
        let dims = [64, 128, 256, 384, 512, 768, 1024, 1536];

        for dim in dims {
            let cat = VectorCategory::new(dim);
            assert_eq!(cat.dimension(), dim);
        }
    }
}

// ============================================================================
// HOTT PATH ALGEBRA TESTS
// ============================================================================

mod hott_integration {
    use super::*;

    /// Test that path composition corresponds to morphism composition
    #[test]
    fn test_path_composition() {
        let a = Term::var("a");
        let b = Term::var("b");
        let c = Term::var("c");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let q = Path::new(b.clone(), c.clone(), Term::var("q"));

        // Path composition should work like morphism composition
        let composed = p.compose(&q);
        assert!(composed.is_some(), "Composable paths should compose");

        let pq = composed.unwrap();
        assert_eq!(pq.source(), &a);
        assert_eq!(pq.target(), &c);
    }

    /// Test that reflexivity paths act as identity morphisms
    #[test]
    fn test_reflexivity_as_identity() {
        let x = Term::var("x");
        let refl_x = Path::refl(x.clone());

        // Reflexivity is the identity path
        assert!(refl_x.is_refl());
        assert_eq!(refl_x.source(), refl_x.target());
    }

    /// Test categorical unit laws through HoTT path algebra
    #[test]
    fn test_unit_laws() {
        let a = Term::var("a");
        let b = Term::var("b");

        // Path p : a = b
        let p = Path::new(a.clone(), b.clone(), Term::var("p"));

        // Reflexivity paths
        let refl_a = Path::refl(a.clone());
        let refl_b = Path::refl(b.clone());

        // refl_a . p should give path from a to b (like p)
        let left_unit = refl_a.compose(&p);
        assert!(left_unit.is_some());
        let lu = left_unit.unwrap();
        assert_eq!(lu.source(), &a);
        assert_eq!(lu.target(), &b);

        // p . refl_b should give path from a to b (like p)
        let right_unit = p.compose(&refl_b);
        assert!(right_unit.is_some());
        let ru = right_unit.unwrap();
        assert_eq!(ru.source(), &a);
        assert_eq!(ru.target(), &b);
    }

    /// Test path inverse (symmetry)
    #[test]
    fn test_path_inverse() {
        let a = Term::var("a");
        let b = Term::var("b");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let p_inv = p.inverse();

        // Inverse reverses endpoints
        assert_eq!(p_inv.source(), &b);
        assert_eq!(p_inv.target(), &a);

        // Composing with inverse should give loop
        let round_trip = p.compose(&p_inv);
        assert!(round_trip.is_some());

        let rt = round_trip.unwrap();
        assert_eq!(rt.source(), &a);
        assert_eq!(rt.target(), &a);
    }

    /// Test associativity of path composition
    #[test]
    fn test_path_associativity() {
        let a = Term::var("a");
        let b = Term::var("b");
        let c = Term::var("c");
        let d = Term::var("d");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let q = Path::new(b.clone(), c.clone(), Term::var("q"));
        let r = Path::new(c.clone(), d.clone(), Term::var("r"));

        // (p . q) . r
        let pq = p.compose(&q).unwrap();
        let left = pq.compose(&r);
        assert!(left.is_some());

        // p . (q . r)
        let qr = q.compose(&r).unwrap();
        let right = p.compose(&qr);
        assert!(right.is_some());

        // Both should have same endpoints
        let left = left.unwrap();
        let right = right.unwrap();
        assert_eq!(left.source(), right.source());
        assert_eq!(left.target(), right.target());
    }

    /// Test functoriality via ap
    #[test]
    fn test_ap_functoriality() {
        let a = Term::var("a");
        let b = Term::var("b");
        let f = Term::var("f");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let ap_p = p.ap(&f);

        // ap f p : f(a) = f(b)
        // The endpoints should be function applications
        assert!(!ap_p.is_refl() || a.structural_eq(&b));
    }

    /// Test path composition fails on mismatch
    #[test]
    fn test_composition_mismatch() {
        let a = Term::var("a");
        let b = Term::var("b");
        let c = Term::var("c");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let q = Path::new(c.clone(), a.clone(), Term::var("q")); // c != b

        // Should fail - endpoints don't match
        assert!(p.compose(&q).is_none());
    }
}

// ============================================================================
// CROSS-MODULE INTEGRATION TESTS
// ============================================================================

mod cross_module_integration {
    use super::*;

    /// Test that HoTT paths correspond to category morphisms
    #[test]
    fn test_hott_category_correspondence() {
        // In HoTT, a category is a type with:
        // - Objects as terms
        // - Morphisms as paths
        // - Composition as path composition

        let a = Term::var("a");
        let b = Term::var("b");
        let c = Term::var("c");

        // Morphisms are paths
        let f = Path::new(a.clone(), b.clone(), Term::var("f"));
        let g = Path::new(b.clone(), c.clone(), Term::var("g"));

        // Composition is path composition
        let gf = f.compose(&g);
        assert!(gf.is_some());

        // Identity is reflexivity
        let id_a = Path::refl(a.clone());
        assert!(id_a.is_refl());

        // Identity laws hold via path algebra
        let f_id = f.compose(&Path::refl(b.clone()));
        assert!(f_id.is_some());
    }

    /// Test belief modeling with paths
    #[test]
    fn test_belief_path_integration() {
        // Model belief transitions as paths
        let belief_a = Term::var("belief_a");
        let belief_b = Term::var("belief_b");

        // Evidence for transition
        let evidence = Path::new(
            belief_a.clone(),
            belief_b.clone(),
            Term::var("evidence"),
        );

        // Can compose evidence chains
        let belief_c = Term::var("belief_c");
        let more_evidence = Path::new(
            belief_b.clone(),
            belief_c.clone(),
            Term::var("more_evidence"),
        );

        let full_path = evidence.compose(&more_evidence);
        assert!(full_path.is_some());
    }

    /// Test category-path interaction
    #[test]
    fn test_category_path_interaction() {
        // Create a category
        let cat = VectorCategory::new(768);
        assert!(cat.verify_laws());

        // Model categorical morphism composition with paths
        let obj_a = Term::var("vec_a");
        let obj_b = Term::var("vec_b");
        let obj_c = Term::var("vec_c");

        // Linear maps as paths
        let linear_f = Path::new(obj_a.clone(), obj_b.clone(), Term::var("f"));
        let linear_g = Path::new(obj_b.clone(), obj_c.clone(), Term::var("g"));

        // Composition
        let gf = linear_f.compose(&linear_g);
        assert!(gf.is_some());

        let composed = gf.unwrap();
        assert_eq!(composed.source(), &obj_a);
        assert_eq!(composed.target(), &obj_c);
    }
}

// ============================================================================
// EDGE CASES AND ROBUSTNESS
// ============================================================================

mod edge_cases {
    use super::*;

    /// Test path composition with identity
    #[test]
    fn test_path_identity_composition() {
        let a = Term::var("a");

        // Identity path
        let refl_a = Path::refl(a.clone());

        // Composing identity with itself should give identity
        let composed = refl_a.compose(&refl_a);
        assert!(composed.is_some());

        let c = composed.unwrap();
        assert_eq!(c.source(), &a);
        assert_eq!(c.target(), &a);
    }

    /// Test multiple path inversions
    #[test]
    fn test_double_inverse() {
        let a = Term::var("a");
        let b = Term::var("b");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let p_inv = p.inverse();
        let p_inv_inv = p_inv.inverse();

        // Double inverse should return to original endpoints
        assert_eq!(p_inv_inv.source(), &a);
        assert_eq!(p_inv_inv.target(), &b);
    }

    /// Test long path chains
    #[test]
    fn test_long_path_chain() {
        // Create a chain of 10 paths
        let points: Vec<Term> = (0..11)
            .map(|i| Term::var(&format!("p{}", i)))
            .collect();

        let paths: Vec<Path> = (0..10)
            .map(|i| Path::new(
                points[i].clone(),
                points[i + 1].clone(),
                Term::var(&format!("path{}", i)),
            ))
            .collect();

        // Compose all paths
        let mut composed = paths[0].clone();
        for path in paths.iter().skip(1) {
            composed = composed.compose(path).expect("Composition should succeed");
        }

        // Result should go from first to last point
        assert_eq!(composed.source(), &points[0]);
        assert_eq!(composed.target(), &points[10]);
    }

    /// Test category with many objects
    #[test]
    fn test_large_category() {
        let cat = VectorCategory::new(768);

        // Creating many vector spaces should work
        for _ in 0..100 {
            // VectorCategory should handle multiple dimensions
            assert!(cat.verify_laws());
        }
    }

    /// Test paths with numeric variable names
    #[test]
    fn test_numeric_variable_paths() {
        let vars: Vec<Term> = (0..5)
            .map(|i| Term::var(&i.to_string()))
            .collect();

        // Create paths between sequential points
        for i in 0..4 {
            let p = Path::new(
                vars[i].clone(),
                vars[i + 1].clone(),
                Term::var(&format!("p{}", i)),
            );
            assert_eq!(p.source(), &vars[i]);
            assert_eq!(p.target(), &vars[i + 1]);
        }
    }

    /// Test reflexivity on complex terms
    #[test]
    fn test_complex_term_reflexivity() {
        // Create a lambda term
        let body = Term::var("x");
        let lambda = Term::lambda("x", body);

        // Reflexivity should work on any term
        let refl = Path::refl(lambda.clone());
        assert!(refl.is_refl());
        assert_eq!(refl.source(), &lambda);
        assert_eq!(refl.target(), &lambda);
    }
}

// ============================================================================
// PERFORMANCE TESTS
// ============================================================================

mod performance_tests {
    use super::*;

    /// Test path composition performance
    #[test]
    fn test_path_composition_performance() {
        let start = std::time::Instant::now();

        // Create and compose many paths
        for i in 0..1000 {
            let a = Term::var(&format!("a{}", i));
            let b = Term::var(&format!("b{}", i));
            let c = Term::var(&format!("c{}", i));

            let p = Path::new(a.clone(), b.clone(), Term::var("p"));
            let q = Path::new(b.clone(), c.clone(), Term::var("q"));

            let _ = p.compose(&q);
        }

        let duration = start.elapsed();

        // Should complete quickly
        assert!(duration.as_secs() < 5,
            "Path composition should be fast: {:?}", duration);
    }

    /// Test category operations performance
    #[test]
    fn test_category_operations_performance() {
        let start = std::time::Instant::now();

        for _ in 0..100 {
            let cat = VectorCategory::new(768);
            let _ = cat.verify_laws();
        }

        let duration = start.elapsed();

        assert!(duration.as_secs() < 10,
            "Category operations should be fast: {:?}", duration);
    }

    /// Test path inverse performance
    #[test]
    fn test_path_inverse_performance() {
        let start = std::time::Instant::now();

        for i in 0..1000 {
            let a = Term::var(&format!("a{}", i));
            let b = Term::var(&format!("b{}", i));

            let p = Path::new(a, b, Term::var("p"));
            let _ = p.inverse();
        }

        let duration = start.elapsed();

        assert!(duration.as_secs() < 5,
            "Path inverse should be fast: {:?}", duration);
    }

    /// Test long composition chain performance
    #[test]
    fn test_long_chain_performance() {
        let start = std::time::Instant::now();

        // Create chain of 100 paths
        let points: Vec<Term> = (0..101)
            .map(|i| Term::var(&format!("p{}", i)))
            .collect();

        let paths: Vec<Path> = (0..100)
            .map(|i| Path::new(
                points[i].clone(),
                points[i + 1].clone(),
                Term::var(&format!("path{}", i)),
            ))
            .collect();

        // Compose all
        let mut composed = paths[0].clone();
        for path in paths.iter().skip(1) {
            composed = composed.compose(path).expect("Should compose");
        }

        let duration = start.elapsed();

        assert!(duration.as_secs() < 5,
            "Long chain composition should be fast: {:?}", duration);
        assert_eq!(composed.source(), &points[0]);
        assert_eq!(composed.target(), &points[100]);
    }
}

// ============================================================================
// GROUPOID STRUCTURE TESTS
// ============================================================================

mod groupoid_structure {
    use super::*;

    /// Test that paths form a groupoid (category where every morphism is invertible)
    #[test]
    fn test_groupoid_structure() {
        let a = Term::var("a");
        let b = Term::var("b");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));

        // Every path has an inverse
        let p_inv = p.inverse();
        assert_eq!(p_inv.source(), &b);
        assert_eq!(p_inv.target(), &a);

        // p . p^(-1) gives identity (loop at source)
        let loop_a = p.compose(&p_inv);
        assert!(loop_a.is_some());
        let loop_a = loop_a.unwrap();
        assert_eq!(loop_a.source(), &a);
        assert_eq!(loop_a.target(), &a);

        // p^(-1) . p gives identity (loop at target)
        let loop_b = p_inv.compose(&p);
        assert!(loop_b.is_some());
        let loop_b = loop_b.unwrap();
        assert_eq!(loop_b.source(), &b);
        assert_eq!(loop_b.target(), &b);
    }

    /// Test inverse properties
    #[test]
    fn test_inverse_properties() {
        let a = Term::var("a");
        let b = Term::var("b");
        let c = Term::var("c");

        let p = Path::new(a.clone(), b.clone(), Term::var("p"));
        let q = Path::new(b.clone(), c.clone(), Term::var("q"));

        // (p . q)^(-1) should have endpoints reversed
        let pq = p.compose(&q).unwrap();
        let pq_inv = pq.inverse();

        assert_eq!(pq_inv.source(), &c);
        assert_eq!(pq_inv.target(), &a);

        // Compare with q^(-1) . p^(-1)
        let q_inv = q.inverse();
        let p_inv = p.inverse();
        let reversed = q_inv.compose(&p_inv).unwrap();

        assert_eq!(reversed.source(), &c);
        assert_eq!(reversed.target(), &a);
    }

    /// Test reflexivity inverse is itself
    #[test]
    fn test_refl_inverse() {
        let a = Term::var("a");
        let refl_a = Path::refl(a.clone());
        let refl_a_inv = refl_a.inverse();

        // Inverse of refl should still be a loop at a
        assert_eq!(refl_a_inv.source(), &a);
        assert_eq!(refl_a_inv.target(), &a);
    }
}