//! Validation tests for the argumentation system, knowledge base, and
//! argumentation theory layers against Modgil & Prakken (2014).

use std::collections::HashSet;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;
use pickaxe_rs::system::consistency::is_indirectly_consistent;

// --- Strict and defeasible inference rules (Definition 3.2) ---

#[test]
fn strict_rule_has_id_antecedents_consequent() {
    let rule = StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    };
    assert_eq!(rule.id, RuleId("s1".into()));
    assert_eq!(rule.antecedents, vec![formula!(p), formula!(q)]);
    assert_eq!(rule.consequent, formula!(r));
}

#[test]
fn defeasible_rule_has_id_antecedents_consequent_name() {
    let rule = DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(bird)],
        consequent: formula!(flies),
        name: Some(formula!(d1_name)),
    };
    assert_eq!(rule.id, RuleId("d1".into()));
    assert_eq!(rule.antecedents, vec![formula!(bird)]);
    assert_eq!(rule.consequent, formula!(flies));
    assert_eq!(rule.name, Some(formula!(d1_name)));
}

// Rs ∩ Rd = ∅ enforced structurally
#[test]
fn strict_and_defeasible_rules_in_separate_collections() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .defeasible_rule("d1", vec![formula!(c)], formula!(d))
        .build();

    assert_eq!(system.strict_rules.len(), 1);
    assert_eq!(system.defeasible_rules.len(), 1);
    assert_eq!(system.strict_rules[0].id, RuleId("s1".into()));
    assert_eq!(system.defeasible_rules[0].id, RuleId("d1".into()));
}

// Rule enum accessors
#[test]
fn rule_enum_id_accessor() {
    let strict = Rule::Strict(StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(a)],
        consequent: formula!(b),
    });
    let defeasible = Rule::Defeasible(DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(c)],
        consequent: formula!(d),
        name: None,
    });

    assert_eq!(strict.id(), &RuleId("s1".into()));
    assert_eq!(defeasible.id(), &RuleId("d1".into()));
}

#[test]
fn rule_enum_antecedents_accessor() {
    let rule = Rule::Strict(StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    });
    assert_eq!(rule.antecedents(), &[formula!(p), formula!(q)]);
}

#[test]
fn rule_enum_consequent_accessor() {
    let rule = Rule::Defeasible(DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(a)],
        consequent: formula!(b),
        name: None,
    });
    assert_eq!(rule.consequent(), &formula!(b));
}

#[test]
fn rule_enum_is_strict_is_defeasible() {
    let strict = Rule::Strict(StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![],
        consequent: formula!(a),
    });
    let defeasible = Rule::Defeasible(DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![],
        consequent: formula!(b),
        name: None,
    });

    assert!(strict.is_strict());
    assert!(!strict.is_defeasible());
    assert!(defeasible.is_defeasible());
    assert!(!defeasible.is_strict());
}

// Rules are meta-level; both domain-specific and scheme-based
#[test]
fn rules_are_meta_level_not_formulae_in_l() {
    let rule = StrictRule {
        id: RuleId("modus_ponens".into()),
        antecedents: vec![formula!(alpha), formula!(alpha_implies_beta)],
        consequent: formula!(beta),
    };
    assert_eq!(rule.antecedents.len(), 2);
    assert_eq!(rule.consequent, formula!(beta));
}

#[test]
fn domain_specific_rules() {
    let rule = DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(bird)],
        consequent: formula!(flies),
        name: Some(formula!(d1_name)),
    };
    assert_eq!(rule.antecedents, vec![formula!(bird)]);
    assert_eq!(rule.consequent, formula!(flies));
}

// The n function — partial function from Rd to L
#[test]
fn named_rule_has_n_defined() {
    let rule = DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(a)],
        consequent: formula!(b),
        name: Some(formula!(d1_name)),
    };
    assert_eq!(rule.name, Some(formula!(d1_name)));
}

#[test]
fn unnamed_rule_has_n_undefined() {
    let rule = DefeasibleRule {
        id: RuleId("d2".into()),
        antecedents: vec![formula!(c)],
        consequent: formula!(d),
        name: None,
    };
    assert_eq!(rule.name, None);
}

// RuleId vs name distinction
#[test]
fn rule_id_and_name_are_distinct() {
    let rule = DefeasibleRule {
        id: RuleId("d1".into()),
        antecedents: vec![formula!(a)],
        consequent: formula!(b),
        name: Some(formula!(n_d1)),
    };
    assert_eq!(rule.id.0, "d1");
    assert_eq!(rule.name, Some(formula!(n_d1)));
}

// --- Knowledge base with premises (Definition 3.3) ---

// KnowledgeBase contains Premise values; K ⊆ L via Formula type
#[test]
fn knowledge_base_contains_premises() {
    let kb = KnowledgeBase {
        premises: vec![
            Premise {
                formula: formula!(p),
                kind: PremiseKind::Axiom,
            },
            Premise {
                formula: formula!(q),
                kind: PremiseKind::Ordinary,
            },
        ],
    };
    assert_eq!(kb.premises.len(), 2);
    assert_eq!(kb.premises[0].formula, formula!(p));
    assert_eq!(kb.premises[1].formula, formula!(q));
}

// PremiseKind::Axiom maps to Kn
#[test]
fn axiom_premise_kind() {
    let premise = Premise {
        formula: formula!(p),
        kind: PremiseKind::Axiom,
    };
    assert_eq!(premise.kind, PremiseKind::Axiom);
}

// PremiseKind::Ordinary maps to Kp
#[test]
fn ordinary_premise_kind() {
    let premise = Premise {
        formula: formula!(q),
        kind: PremiseKind::Ordinary,
    };
    assert_eq!(premise.kind, PremiseKind::Ordinary);
}

// Premise kind partition is exhaustive and disjoint
#[test]
fn premise_kind_partition_exhaustive() {
    let kinds = [PremiseKind::Axiom, PremiseKind::Ordinary];
    assert_eq!(kinds.len(), 2);

    assert_ne!(PremiseKind::Axiom, PremiseKind::Ordinary);
}

// Two-way premise classification
#[test]
fn two_way_premise_classification_via_builder() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(a))
        .ordinary_premise(formula!(b))
        .build();

    let axioms: Vec<_> = system
        .knowledge_base
        .premises
        .iter()
        .filter(|p| p.kind == PremiseKind::Axiom)
        .collect();
    let ordinary: Vec<_> = system
        .knowledge_base
        .premises
        .iter()
        .filter(|p| p.kind == PremiseKind::Ordinary)
        .collect();

    assert_eq!(axioms.len(), 1);
    assert_eq!(ordinary.len(), 1);
    assert_eq!(axioms[0].formula, formula!(a));
    assert_eq!(ordinary[0].formula, formula!(b));
}

// --- Argumentation theory via builder (Definition 3.5) ---

// AspicSystem bundles AS and K
#[test]
fn aspic_system_bundles_as_and_k() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .strict_rule("s1", vec![formula!(p)], formula!(q))
        .defeasible_rule("d1", vec![formula!(q)], formula!(r))
        .with_classical_negation()
        .build();

    assert_eq!(system.knowledge_base.premises.len(), 1);
    assert_eq!(system.strict_rules.len(), 1);
    assert_eq!(system.defeasible_rules.len(), 1);
}

// Builder fluent API
#[test]
fn builder_fluent_api_all_methods() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(a))
        .ordinary_premise(formula!(b))
        .strict_rule("s1", vec![formula!(a)], formula!(d))
        .defeasible_rule("d1", vec![formula!(b)], formula!(e))
        .named_defeasible_rule("d2", formula!(d2_name), vec![formula!(b)], formula!(f))
        .contrary(formula!(g), formula!(h))
        .contradictory(formula!(i), formula!(j))
        .with_classical_negation()
        .build();

    assert_eq!(system.knowledge_base.premises.len(), 2);
    assert_eq!(system.strict_rules.len(), 1);
    assert_eq!(system.defeasible_rules.len(), 2);

    let d2 = &system.defeasible_rules[1];
    assert_eq!(d2.name, Some(formula!(d2_name)));
}

// build() returns (AspicSystem, Vec<Warning>); empty warnings for well-defined AT
#[test]
fn build_returns_tuple_with_empty_warnings_for_well_defined_at() {
    let (system, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .ordinary_premise(formula!(q))
        .strict_rule("s1", vec![formula!(p)], formula!(r))
        .strict_rule("s2", vec![formula!(!r)], formula!(!p))
        .with_classical_negation()
        .build();

    assert_eq!(system.knowledge_base.premises.len(), 2);
    assert!(warnings.is_empty());
}

// Edge cases: empty K, Rs, Rd
#[test]
fn edge_case_empty_knowledge_base() {
    let (system, warnings) = AspicSystemBuilder::new().build();

    assert!(system.knowledge_base.premises.is_empty());
    assert!(system.strict_rules.is_empty());
    assert!(system.defeasible_rules.is_empty());
    assert!(warnings.is_empty());
}

#[test]
fn edge_case_empty_strict_rules() {
    let (system, warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(a))
        .defeasible_rule("d1", vec![formula!(a)], formula!(b))
        .build();

    assert!(system.strict_rules.is_empty());
    assert_eq!(system.defeasible_rules.len(), 1);
    assert!(warnings.is_empty());
}

#[test]
fn edge_case_empty_defeasible_rules() {
    let (system, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(a))
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .strict_rule("s2", vec![formula!(!b)], formula!(!a))
        .with_classical_negation()
        .build();

    assert!(system.defeasible_rules.is_empty());
    assert_eq!(system.strict_rules.len(), 2);
    assert!(warnings.is_empty());
}

#[test]
fn edge_case_duplicate_formulae_across_premise_kinds() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .ordinary_premise(formula!(p))
        .build();

    assert_eq!(system.knowledge_base.premises.len(), 2);
    assert_eq!(system.knowledge_base.premises[0].kind, PremiseKind::Axiom);
    assert_eq!(
        system.knowledge_base.premises[1].kind,
        PremiseKind::Ordinary
    );
}

// --- Well-definedness checks (§4.2, Definitions 4.2 and 4.3) ---

// Axiom inconsistency warning
#[test]
fn inconsistent_axioms_produce_warning() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .axiom(formula!(!p))
        .with_classical_negation()
        .build();

    assert!(
        warnings
            .iter()
            .any(|w| matches!(w, Warning::AxiomInconsistency)),
        "expected AxiomInconsistency warning for Kn = {{p, ¬p}}"
    );
}

#[test]
fn consistent_axioms_no_warning() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .axiom(formula!(q))
        .with_classical_negation()
        .build();

    assert!(
        !warnings
            .iter()
            .any(|w| matches!(w, Warning::AxiomInconsistency)),
        "consistent Kn should produce no AxiomInconsistency warning"
    );
}

#[test]
fn indirect_axiom_inconsistency_via_strict_closure() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .axiom(formula!(q))
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(!p))
        .with_classical_negation()
        .build();

    assert!(
        warnings
            .iter()
            .any(|w| matches!(w, Warning::AxiomInconsistency)),
        "Kn = {{p, q}} with strict rule p, q → ¬p should be indirectly inconsistent"
    );
}

// Transposition closure warnings
#[test]
fn missing_transposition_produces_warning() {
    let (_, warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(married)], formula!(!bachelor))
        .with_classical_negation()
        .build();

    assert!(
        warnings
            .iter()
            .any(|w| matches!(w, Warning::MissingTransposition { .. })),
        "strict rule married → ¬bachelor without transposition bachelor → ¬married \
         should produce MissingTransposition warning"
    );
}

#[test]
fn closed_transposition_no_warning() {
    let (_, warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(married)], formula!(!bachelor))
        .strict_rule("s2", vec![formula!(bachelor)], formula!(!married))
        .with_classical_negation()
        .build();

    let transposition_warnings: Vec<_> = warnings
        .iter()
        .filter(|w| matches!(w, Warning::MissingTransposition { .. }))
        .collect();
    assert!(
        transposition_warnings.is_empty(),
        "with both s1 and s2 present, no MissingTransposition warning expected"
    );
}

#[test]
fn multi_antecedent_transposition() {
    // p, q → r requires transpositions:
    // ¬r, q → ¬p  AND  p, ¬r → ¬q
    let (_, warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .with_classical_negation()
        .build();

    let missing: Vec<_> = warnings
        .iter()
        .filter(|w| matches!(w, Warning::MissingTransposition { .. }))
        .collect();
    assert_eq!(
        missing.len(),
        2,
        "p, q → r should produce 2 MissingTransposition warnings (one per antecedent)"
    );
}

#[test]
fn multi_antecedent_fully_closed() {
    // Provide the rule and both transpositions
    let (_, warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .strict_rule("s2", vec![formula!(!r), formula!(q)], formula!(!p))
        .strict_rule("s3", vec![formula!(p), formula!(!r)], formula!(!q))
        // s2 requires transpositions: p, q → r (= s1) and ¬r, p → ¬q
        // But ¬r, p → ¬q has different order than s3 (p, ¬r → ¬q) — order should not matter
        // s3 requires transpositions: p, q → r (= s1) and ¬q, ¬r → ¬p
        // We'd need further transpositions, but let's just check s1's are covered
        .with_classical_negation()
        .build();

    let s1_missing: Vec<_> = warnings
        .iter()
        .filter(|w| match w {
            Warning::MissingTransposition { rule_id, .. } => rule_id == &RuleId("s1".into()),
            _ => false,
        })
        .collect();
    assert!(
        s1_missing.is_empty(),
        "s1's transpositions (s2 and s3) are present, so no warnings for s1"
    );
}

// Contraposition is NOT checked at build time
#[test]
fn contraposition_not_checked_at_build_time() {
    // A system that may violate contraposition but satisfies transposition
    let (_, warnings) = AspicSystemBuilder::new()
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .strict_rule("s2", vec![formula!(!b)], formula!(!a))
        .with_classical_negation()
        .build();

    let non_transposition_warnings: Vec<_> = warnings
        .iter()
        .filter(|w| {
            !matches!(w, Warning::MissingTransposition { .. })
                && !matches!(w, Warning::AxiomInconsistency)
        })
        .collect();
    assert!(
        non_transposition_warnings.is_empty(),
        "no contraposition-related warnings should be present"
    );
}

// Edge case: both axiom inconsistency AND missing transpositions
#[test]
fn edge_case_combined_warnings() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .axiom(formula!(!p))
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .with_classical_negation()
        .build();

    let has_axiom_warning = warnings
        .iter()
        .any(|w| matches!(w, Warning::AxiomInconsistency));
    let has_transposition_warning = warnings
        .iter()
        .any(|w| matches!(w, Warning::MissingTransposition { .. }));

    assert!(has_axiom_warning, "should have AxiomInconsistency");
    assert!(
        has_transposition_warning,
        "should have MissingTransposition"
    );
}

// Verify standalone is_indirectly_consistent still works for user-initiated checks
#[test]
fn standalone_consistency_check_still_available() {
    let (system, _) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .axiom(formula!(!p))
        .with_classical_negation()
        .build();

    let axioms: HashSet<Formula> = system
        .knowledge_base
        .premises
        .iter()
        .filter(|p| p.kind == PremiseKind::Axiom)
        .map(|p| p.formula.clone())
        .collect();

    assert!(
        !is_indirectly_consistent(&axioms, &system.strict_rules, &system.contrariness),
        "standalone check should also detect inconsistency"
    );
}

// --- Well-formedness for contraries (Modgil & Prakken 2013, §5) ---

// Contrary targeting an axiom premise emits ContraryWellFormedness
#[test]
fn contrary_well_formedness_target_is_axiom() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .ordinary_premise(formula!(q))
        // q is a contrary of p — but p is an axiom, so this violates §5
        .contrary(formula!(p), formula!(q))
        .build();

    let has_warning = warnings.iter().any(|w| {
        matches!(
            w,
            Warning::ContraryWellFormedness {
                target,
                reason: pickaxe_rs::system::warning::ContraryWellFormednessReason::TargetIsAxiom,
            } if *target == formula!(p)
        )
    });
    assert!(
        has_warning,
        "should emit ContraryWellFormedness for axiom target"
    );
}

// Contrary targeting a strict rule consequent emits ContraryWellFormedness
#[test]
fn contrary_well_formedness_target_is_strict_consequent() {
    let (_, warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(b))
        .strict_rule("s1", vec![formula!(a)], formula!(c))
        // b is a contrary of c — but c is a strict-rule consequent, so this violates §5
        .contrary(formula!(c), formula!(b))
        .build();

    let has_warning = warnings.iter().any(|w| {
        matches!(
            w,
            Warning::ContraryWellFormedness {
                target,
                reason: pickaxe_rs::system::warning::ContraryWellFormednessReason::TargetIsStrictConsequent,
            } if *target == formula!(c)
        )
    });
    assert!(
        has_warning,
        "should emit ContraryWellFormedness for strict consequent target"
    );
}

// Contradictory (symmetric) relations do NOT trigger ContraryWellFormedness
#[test]
fn contrary_well_formedness_no_warning_for_contradictory() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .ordinary_premise(formula!(q))
        // p and q are contradictory (symmetric) — §5 only applies to contrary (asymmetric)
        .contradictory(formula!(p), formula!(q))
        .build();

    let has_well_formedness = warnings
        .iter()
        .any(|w| matches!(w, Warning::ContraryWellFormedness { .. }));
    assert!(
        !has_well_formedness,
        "contradictory relations should not trigger ContraryWellFormedness"
    );
}

// Contrary targeting an ordinary premise (not axiom, not strict consequent) is fine
#[test]
fn contrary_well_formedness_no_warning_when_valid() {
    let (_, warnings) = AspicSystemBuilder::new()
        .axiom(formula!(a))
        .ordinary_premise(formula!(b))
        .ordinary_premise(formula!(c))
        // c is a contrary of b — b is ordinary, not axiom, not strict consequent → OK
        .contrary(formula!(b), formula!(c))
        .build();

    let has_well_formedness = warnings
        .iter()
        .any(|w| matches!(w, Warning::ContraryWellFormedness { .. }));
    assert!(
        !has_well_formedness,
        "contrary targeting ordinary premise should not trigger warning"
    );
}
