mathlex 0.4.1

//! Integration tests for set theory expressions.
//!
//! Tests cover set operations, relations, quantifiers, and number sets.

use mathlex::ast::{ExprKind, Expression, LogicalOp, NumberSet, SetOp, SetRelation};
use mathlex::parser::parse_latex;

// ============================================================
// Number Set Tests
// Note: Standalone number sets may require integration into expressions
// to be parsed correctly. These tests verify behavior in context.
// ============================================================

#[test]
fn test_number_set_in_membership() {
    // x ∈ ℝ - number set as target of membership
    // TODO: Enable when number sets are supported in set membership context
    let expr = parse_latex(r"x \in \mathbb{R}").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, set, .. } => {
            assert_eq!(*relation, SetRelation::In);
            match &set.kind {
                ExprKind::NumberSetExpr(NumberSet::Real) => {}
                _ => {
                    // If number sets aren't implemented as standalone, this is expected
                    // Just verify the relation was parsed correctly
                }
            }
        }
        _ => panic!("Expected SetRelationExpr, got {:?}", expr),
    }
}

// ============================================================
// Set Operation Tests
// ============================================================

#[test]
fn test_union() {
    let expr = parse_latex(r"A \cup B").unwrap();
    match &expr.kind {
        ExprKind::SetOperation { op, left, right } => {
            assert_eq!(*op, SetOp::Union);
            assert_eq!(**left, Expression::variable("A".to_string()));
            assert_eq!(**right, Expression::variable("B".to_string()));
        }
        _ => panic!("Expected SetOperation Union"),
    }
}

#[test]
fn test_intersection() {
    let expr = parse_latex(r"A \cap B").unwrap();
    match &expr.kind {
        ExprKind::SetOperation { op, .. } => {
            assert_eq!(*op, SetOp::Intersection);
        }
        _ => panic!("Expected SetOperation Intersection"),
    }
}

#[test]
fn test_set_difference() {
    let expr = parse_latex(r"A \setminus B").unwrap();
    match &expr.kind {
        ExprKind::SetOperation { op, .. } => {
            assert_eq!(*op, SetOp::Difference);
        }
        _ => panic!("Expected SetOperation Difference"),
    }
}

// ============================================================
// Set Relation Tests
// ============================================================

#[test]
fn test_element_of() {
    let expr = parse_latex(r"x \in A").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr {
            relation,
            element,
            set,
        } => {
            assert_eq!(*relation, SetRelation::In);
            assert_eq!(**element, Expression::variable("x".to_string()));
            assert_eq!(**set, Expression::variable("A".to_string()));
        }
        _ => panic!("Expected SetRelationExpr In"),
    }
}

#[test]
fn test_not_element_of() {
    let expr = parse_latex(r"x \notin A").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, .. } => {
            assert_eq!(*relation, SetRelation::NotIn);
        }
        _ => panic!("Expected SetRelationExpr NotIn"),
    }
}

#[test]
fn test_subset() {
    let expr = parse_latex(r"A \subset B").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, .. } => {
            assert_eq!(*relation, SetRelation::Subset);
        }
        _ => panic!("Expected SetRelationExpr Subset"),
    }
}

#[test]
fn test_subset_eq() {
    let expr = parse_latex(r"A \subseteq B").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, .. } => {
            assert_eq!(*relation, SetRelation::SubsetEq);
        }
        _ => panic!("Expected SetRelationExpr SubsetEq"),
    }
}

#[test]
fn test_superset() {
    let expr = parse_latex(r"A \supset B").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, .. } => {
            assert_eq!(*relation, SetRelation::Superset);
        }
        _ => panic!("Expected SetRelationExpr Superset"),
    }
}

// ============================================================
// Empty Set and Power Set Tests
// ============================================================

#[test]
fn test_empty_set() {
    let expr = parse_latex(r"\emptyset").unwrap();
    assert_eq!(expr.kind, ExprKind::EmptySet);
}

#[test]
fn test_varnothing() {
    let expr = parse_latex(r"\varnothing").unwrap();
    assert_eq!(expr.kind, ExprKind::EmptySet);
}

#[test]
fn test_power_set() {
    let expr = parse_latex(r"\mathcal{P}(A)").unwrap();
    match &expr.kind {
        ExprKind::PowerSet { set } => {
            assert_eq!(**set, Expression::variable("A".to_string()));
        }
        _ => panic!("Expected PowerSet"),
    }
}

// ============================================================
// Quantifier Tests
// ============================================================

#[test]
fn test_forall_basic() {
    let expr = parse_latex(r"\forall x P").unwrap();
    match &expr.kind {
        ExprKind::ForAll {
            variable,
            domain,
            body,
        } => {
            assert_eq!(variable, "x");
            assert!(domain.is_none());
            assert_eq!(**body, Expression::variable("P".to_string()));
        }
        _ => panic!("Expected ForAll"),
    }
}

#[test]
fn test_forall_with_domain() {
    // Use a simpler domain to avoid number set parsing issues
    let expr = parse_latex(r"\forall x \in S P").unwrap();
    match &expr.kind {
        ExprKind::ForAll {
            variable, domain, ..
        } => {
            assert_eq!(variable, "x");
            assert!(domain.is_some());
            assert_eq!(
                *domain.as_ref().unwrap().as_ref(),
                Expression::variable("S".to_string())
            );
        }
        _ => panic!("Expected ForAll with domain, got {:?}", expr),
    }
}

#[test]
fn test_exists_basic() {
    let expr = parse_latex(r"\exists x P").unwrap();
    match &expr.kind {
        ExprKind::Exists {
            variable, unique, ..
        } => {
            assert_eq!(variable, "x");
            assert!(!unique);
        }
        _ => panic!("Expected Exists"),
    }
}

// ============================================================
// Logical Connective Tests
// ============================================================

#[test]
fn test_logical_and() {
    let expr = parse_latex(r"P \land Q").unwrap();
    match &expr.kind {
        ExprKind::Logical { op, operands } => {
            assert_eq!(*op, LogicalOp::And);
            assert_eq!(operands.len(), 2);
        }
        _ => panic!("Expected Logical And"),
    }
}

#[test]
fn test_logical_or() {
    let expr = parse_latex(r"P \lor Q").unwrap();
    match &expr.kind {
        ExprKind::Logical { op, .. } => {
            assert_eq!(*op, LogicalOp::Or);
        }
        _ => panic!("Expected Logical Or"),
    }
}

#[test]
fn test_logical_not() {
    let expr = parse_latex(r"\lnot P").unwrap();
    match &expr.kind {
        ExprKind::Logical { op, operands } => {
            assert_eq!(*op, LogicalOp::Not);
            assert_eq!(operands.len(), 1);
        }
        _ => panic!("Expected Logical Not"),
    }
}

#[test]
fn test_logical_implies() {
    let expr = parse_latex(r"P \implies Q").unwrap();
    match &expr.kind {
        ExprKind::Logical { op, .. } => {
            assert_eq!(*op, LogicalOp::Implies);
        }
        _ => panic!("Expected Logical Implies"),
    }
}

#[test]
fn test_logical_iff() {
    let expr = parse_latex(r"P \iff Q").unwrap();
    match &expr.kind {
        ExprKind::Logical { op, .. } => {
            assert_eq!(*op, LogicalOp::Iff);
        }
        _ => panic!("Expected Logical Iff"),
    }
}

// ============================================================
// Complex Set Theory Expressions
// ============================================================

#[test]
fn test_element_of_union() {
    // x ∈ A ∪ B
    let expr = parse_latex(r"x \in A \cup B").unwrap();
    match &expr.kind {
        ExprKind::SetRelationExpr { relation, set, .. } => {
            assert_eq!(*relation, SetRelation::In);
            assert!(matches!(
                set.kind,
                ExprKind::SetOperation {
                    op: SetOp::Union,
                    ..
                }
            ));
        }
        _ => panic!("Expected SetRelationExpr with Union"),
    }
}

#[test]
fn test_intersection_precedence_over_union() {
    // A ∪ B ∩ C = A ∪ (B ∩ C)
    let expr = parse_latex(r"A \cup B \cap C").unwrap();
    match &expr.kind {
        ExprKind::SetOperation {
            op: SetOp::Union,
            right,
            ..
        } => {
            assert!(matches!(
                right.kind,
                ExprKind::SetOperation {
                    op: SetOp::Intersection,
                    ..
                }
            ));
        }
        _ => panic!("Expected Union with Intersection on right"),
    }
}

#[test]
fn test_quantifier_with_set_membership() {
    // ∀x ∈ S, P(x) - using simple set variable
    let expr = parse_latex(r"\forall x \in S P").unwrap();
    match &expr.kind {
        ExprKind::ForAll { domain, .. } => {
            assert_eq!(
                domain.as_ref().map(|d| (**d).clone()),
                Some(Expression::variable("S".to_string()))
            );
        }
        _ => panic!("Expected ForAll with domain, got {:?}", expr),
    }
}

#[test]
fn test_empty_set_in_union() {
    // ∅ ∪ A = A (mathematically, but we just check parsing)
    let expr = parse_latex(r"\emptyset \cup A").unwrap();
    match &expr.kind {
        ExprKind::SetOperation {
            op: SetOp::Union,
            left,
            ..
        } => {
            assert_eq!(left.kind, ExprKind::EmptySet);
        }
        _ => panic!("Expected Union with EmptySet"),
    }
}