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

/// The classic "Tweety Triangle" example.
/// - Tweety is a bird and a penguin.
/// - Birds (defeasibly) fly.
/// - Penguins (defeasibly) don't fly.
/// - Penguins are (strictly) birds.
/// - "penguin => not fly" is preferred over "bird => fly".
///
/// Expected: under grounded semantics with d2 preferred, Tweety does not fly.
#[test]
fn tweety_triangle() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(penguin(tweety)))
        .strict_rule("s1", vec![formula!(penguin(X))], formula!(bird(X)))
        .named_defeasible_rule(
            "d1",
            formula!(r_flies),
            vec![formula!(bird(X))],
            formula!(flies(X)),
        )
        .named_defeasible_rule(
            "d2",
            formula!(r_not_flies),
            vec![formula!(penguin(X))],
            formula!(!flies(X)),
        )
        .build();

    let rule_ord = TieredOrdering::new(vec![
        vec![RuleId("d2_0".into())],
        vec![RuleId("d1_0".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();

    assert!(
        !result.store.is_empty(),
        "should have constructed arguments"
    );
    assert!(
        !result.extensions.is_empty(),
        "should have at least one extension"
    );

    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))),
        "Tweety should not fly. Conclusions: {:?}",
        conclusions
    );
}

/// The "Nixon Diamond" example.
/// - Nixon is a republican and a quaker.
/// - Republicans (defeasibly) are not pacifists.
/// - Quakers (defeasibly) are pacifists.
/// - No preference between the two rules.
///
/// Expected: under grounded semantics with no preference, neither conclusion
/// is in the grounded extension (both are undecided).
#[test]
fn nixon_diamond() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(republican(nixon)))
        .ordinary_premise(formula!(quaker(nixon)))
        .defeasible_rule("d1", vec![formula!(republican(X))], formula!(!pacifist(X)))
        .defeasible_rule("d2", vec![formula!(quaker(X))], formula!(pacifist(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();

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

    // Neither pacifist(nixon) nor -pacifist(nixon) should be in grounded
    assert!(
        !conclusions.contains(&formula!(pacifist(nixon))),
        "pacifist(nixon) should not be in grounded extension"
    );
    assert!(
        !conclusions.contains(&formula!(!pacifist(nixon))),
        "-pacifist(nixon) should not be in grounded extension"
    );
}

/// Simple strict-only reasoning.
///
/// - tweety is a bird (axiom).
/// - birds have wings (strict rule).
///
/// Expected: has_wings(tweety) is derivable.
#[test]
fn strict_reasoning() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(bird(tweety)))
        .strict_rule("s1", vec![formula!(bird(X))], formula!(has_wings(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();

    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!(has_wings(tweety))),
        "has_wings(tweety) should be derived. Conclusions: {:?}",
        conclusions
    );
}

/// Chained reasoning: A -> B -> C.
#[test]
fn chained_strict_reasoning() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(a))
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .strict_rule("s2", vec![formula!(b)], formula!(c))
        .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();

    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!(a)));
    assert!(conclusions.contains(&formula!(b)));
    assert!(conclusions.contains(&formula!(c)));
}
