use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;

/// Test undercut: an argument attacking the applicability of a defeasible rule.
///
/// Setup:
/// - bird(tweety) is an ordinary premise.
/// - d1: bird(X) => flies(X), named r_d1.
/// - We have an ordinary premise for -r_d1 (the rule is inapplicable).
///
/// Under classical negation, -r_d1 is contrary to r_d1, so any argument
/// concluding -r_d1 undercuts arguments using d1.
#[test]
fn basic_undercut() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(!r_d1))
        .named_defeasible_rule(
            "d1",
            formula!(r_d1),
            vec![formula!(bird(X))],
            formula!(flies(X)),
        )
        .build();

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(NoPreference),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();

    // There should be attacks (specifically undercuts)
    let undercuts: Vec<_> = result
        .attacks
        .iter()
        .filter(|a| matches!(a.kind, AttackKind::Undercut { .. }))
        .collect();
    assert!(!undercuts.is_empty(), "There should be undercut attacks");

    // flies(tweety) should NOT be in the grounded extension because d1 is undercut
    let grounded = &result.extensions[0];
    let conclusions: Vec<Formula> = grounded
        .iter()
        .filter_map(|id| result.store.get(*id))
        .map(|a| a.conclusion().clone())
        .collect();

    assert!(
        !conclusions.contains(&formula!(flies(tweety))),
        "flies(tweety) should not be in grounded extension due to undercut"
    );
}

/// Test that undercuts always succeed regardless of preferences.
#[test]
fn undercut_always_succeeds() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(a))
        .ordinary_premise(formula!(!r_d1))
        .named_defeasible_rule("d1", formula!(r_d1), vec![formula!(a)], formula!(b))
        .build();

    // Even if d1 is maximally preferred, the undercut should still succeed
    let rule_ord = TieredOrdering::new(vec![vec![RuleId("d1".into())]]);

    let pipeline = AspicPipeline::classical(
        system,
        Box::new(LastLinkOrdering {
            rule_ordering: Box::new(rule_ord),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        }),
    );

    let result = pipeline.evaluate(Semantics::Grounded).unwrap();

    let grounded = &result.extensions[0];
    let conclusions: Vec<Formula> = grounded
        .iter()
        .filter_map(|id| result.store.get(*id))
        .map(|a| a.conclusion().clone())
        .collect();

    assert!(
        !conclusions.contains(&formula!(b)),
        "b should not be in grounded extension even with preferred rule, due to undercut"
    );
}
