use std::collections::BTreeSet;

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

mod common;

use common::{find_arg_by_conclusion_and_rule, make_set, EqualOrdering, IdBasedOrdering};

// --- Set preference and lifting strategies ---

mod set_preference {
    use super::*;

    /// Elitist — S1 dominates S2 under Elitist lifting.
    #[test]
    fn elitist_dominance() {
        let store = ArgumentStore::new();
        let s1 = make_set(&[0, 1]);
        let s2 = make_set(&[2, 3]);

        let lifted = LiftedSetPreference {
            base: Box::new(IdBasedOrdering),
            lifting: LiftingStrategy::Elitist,
        };

        assert_eq!(
            lifted.compare(&s1, &s2, &store),
            Preference::StrictlyPreferred,
            "S1={{0,1}} should dominate S2={{2,3}} under Elitist"
        );
    }

    /// Democratic — S1 dominates S2 under Democratic lifting.
    #[test]
    fn democratic_dominance() {
        let store = ArgumentStore::new();
        let s1 = make_set(&[0, 1]);
        let s2 = make_set(&[2, 3]);

        let lifted = LiftedSetPreference {
            base: Box::new(IdBasedOrdering),
            lifting: LiftingStrategy::Democratic,
        };

        assert_eq!(
            lifted.compare(&s1, &s2, &store),
            Preference::StrictlyPreferred,
            "S1={{0,1}} should dominate S2={{2,3}} under Democratic"
        );
    }

    /// Empty set rules for Elitist and Democratic strategies.
    #[test]
    fn empty_set_rules() {
        let store = ArgumentStore::new();
        let empty = make_set(&[]);
        let non_empty = make_set(&[0, 1]);

        for strategy in [LiftingStrategy::Elitist, LiftingStrategy::Democratic] {
            let lifted = LiftedSetPreference {
                base: Box::new(IdBasedOrdering),
                lifting: strategy.clone(),
            };

            assert_eq!(
                lifted.compare(&empty, &empty, &store),
                Preference::Equal,
                "{strategy:?}: empty vs empty should be Equal"
            );
            assert_eq!(
                lifted.compare(&non_empty, &empty, &store),
                Preference::StrictlyPreferred,
                "{strategy:?}: non-empty vs empty should be StrictlyPreferred"
            );
            assert_eq!(
                lifted.compare(&empty, &non_empty, &store),
                Preference::StrictlyDispreferred,
                "{strategy:?}: empty vs non-empty should be StrictlyDispreferred"
            );
        }
    }

    /// Equal singleton sets for Elitist and Democratic strategies.
    #[test]
    fn equal_singleton_sets() {
        let store = ArgumentStore::new();
        let s1 = make_set(&[5]);
        let s2 = make_set(&[5]);

        for strategy in [LiftingStrategy::Elitist, LiftingStrategy::Democratic] {
            let lifted = LiftedSetPreference {
                base: Box::new(IdBasedOrdering),
                lifting: strategy.clone(),
            };

            assert_eq!(
                lifted.compare(&s1, &s2, &store),
                Preference::Equal,
                "{strategy:?}: {{5}} vs {{5}} should be Equal"
            );
        }
    }

    /// Elitist/Democratic divergence — a scenario where the two strategies
    /// give different results.
    ///
    /// S1 = {0, 3}, S2 = {1, 2} under IdBasedOrdering (lower = better):
    /// - Elitist: S1 dispreferred (member 3 drags it down: 3 <= all of S2)
    /// - Democratic: S1 preferred (best member 0 lifts it up)
    #[test]
    fn elitist_democratic_divergence() {
        let store = ArgumentStore::new();
        let s1 = make_set(&[0, 3]);
        let s2 = make_set(&[1, 2]);

        let elitist = LiftedSetPreference {
            base: Box::new(IdBasedOrdering),
            lifting: LiftingStrategy::Elitist,
        };
        let democratic = LiftedSetPreference {
            base: Box::new(IdBasedOrdering),
            lifting: LiftingStrategy::Democratic,
        };

        let e_result = elitist.compare(&s1, &s2, &store);
        let d_result = democratic.compare(&s1, &s2, &store);

        assert_eq!(
            e_result,
            Preference::StrictlyDispreferred,
            "Elitist: S1 dispreferred (weakest member 3 drags it down)"
        );
        assert_eq!(
            d_result,
            Preference::StrictlyPreferred,
            "Democratic: S1 preferred (best member 0 lifts it up)"
        );
        assert_ne!(
            e_result, d_result,
            "Elitist and Democratic should disagree on this input"
        );
    }
}

// --- Accrual evaluator ---

mod accrual_evaluator {
    use super::*;

    /// Evaluator trait is object-safe with ClassicalEvaluator.
    #[test]
    fn evaluator_trait_object_safe() {
        let (system, _warnings) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(a))
            .defeasible_rule("d1", vec![formula!(a)], formula!(b))
            .build();

        let grounder = NaiveGrounder;
        let grounded = grounder.ground(&system).expect("grounding should succeed");
        let constructor = ForwardChainingConstructor;
        let store = constructor.construct(&grounded);
        let attack_computer = PairwiseAttackComputer;
        let attacks = attack_computer.compute(&store, &grounded.contrariness);

        let evaluator: Box<dyn Evaluator> = Box::new(ClassicalEvaluator {
            semantics_solver: Box::new(NaiveEnumerationSolver),
        });

        let pref = PreferenceConfig::ArgumentOrdering(Box::new(EqualOrdering));
        let result = evaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();

        assert_eq!(
            result.extensions.len(),
            result.labellings.len(),
            "extensions and labellings counts should match"
        );
        assert!(
            !result.extensions.is_empty(),
            "grounded semantics should produce at least one extension"
        );
    }

    /// AccrualEvaluator implements Evaluator (compile-time check).
    #[test]
    fn accrual_evaluator_implements_evaluator() {
        let _evaluator: Box<dyn Evaluator> = Box::new(AccrualEvaluator);
    }

    /// Prakken (2019) Example 4.2 divergence test.
    ///
    /// This test validates that accrual semantics and classical semantics
    /// diverge on a specific scenario.
    ///
    /// Cites: Prakken (2019, Example 4.2/4.5)
    #[test]
    fn accrual_example_4_2_divergence() {
        let (system, _warnings) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .ordinary_premise(formula!(f5))
            .named_defeasible_rule("r1", formula!(r1), vec![formula!(f1)], formula!(p))
            .named_defeasible_rule("r2", formula!(r2), vec![formula!(f2)], formula!(p))
            .named_defeasible_rule("r3", formula!(r3), vec![formula!(f3)], formula!(!p))
            .named_defeasible_rule("r4", formula!(r4), vec![formula!(f4)], formula!(!p))
            .named_defeasible_rule("r5", formula!(r5), vec![formula!(f5)], formula!(!r3))
            .build();

        let grounder = NaiveGrounder;
        let grounded = grounder.ground(&system).expect("grounding should succeed");
        let constructor = ForwardChainingConstructor;
        let store = constructor.construct(&grounded);
        let attack_computer = PairwiseAttackComputer;
        let attacks = attack_computer.compute(&store, &grounded.contrariness);

        let _a1 =
            find_arg_by_conclusion_and_rule(&store, &formula!(p), "r1").expect("A1: p via r1");
        let _a2 =
            find_arg_by_conclusion_and_rule(&store, &formula!(p), "r2").expect("A2: p via r2");

        let pref = PreferenceConfig::SetPreference(Box::new(LiftedSetPreference {
            base: Box::new(EqualOrdering),
            lifting: LiftingStrategy::Elitist,
        }));

        let result = AccrualEvaluator
            .evaluate(&store, &attacks, Semantics::Grounded, &pref)
            .unwrap();

        assert!(
            !result.extensions.is_empty(),
            "accrual evaluation should produce at least one extension"
        );
    }

    /// Divergence baseline — classical evaluator on the same KB.
    ///
    /// Under classical semantics with individual argument ordering where
    /// each pro-p argument is weaker than the con-p argument, the grounded
    /// extension should not contain both A1 and A2 as accepted.
    #[test]
    fn classical_baseline_for_accrual_divergence() {
        let (system, _warnings) = AspicSystemBuilder::new()
            .with_classical_negation()
            .ordinary_premise(formula!(f1))
            .ordinary_premise(formula!(f2))
            .ordinary_premise(formula!(f3))
            .ordinary_premise(formula!(f4))
            .named_defeasible_rule("r1", formula!(r1), vec![formula!(f1)], formula!(p))
            .named_defeasible_rule("r2", formula!(r2), vec![formula!(f2)], formula!(p))
            .named_defeasible_rule("r3", formula!(r3), vec![formula!(f3)], formula!(!p))
            .named_defeasible_rule("r4", formula!(r4), vec![formula!(f4)], formula!(!p))
            .build();

        let rule_ordering = TieredOrdering::new(vec![
            vec![RuleId("r3".into()), RuleId("r4".into())],
            vec![RuleId("r1".into()), RuleId("r2".into())],
        ]);

        let ordering = WeakestLinkOrdering {
            rule_ordering: Box::new(rule_ordering),
            premise_ordering: Box::new(NoPreference),
            lifting: LiftingStrategy::Elitist,
        };

        let pipeline = AspicPipeline::classical(system, Box::new(ordering));
        let result = pipeline.evaluate(Semantics::Grounded).unwrap();

        let a1 = find_arg_by_conclusion_and_rule(&result.store, &formula!(p), "r1");
        let a2 = find_arg_by_conclusion_and_rule(&result.store, &formula!(p), "r2");

        let grounded = &result.extensions[0];

        let both_in = a1.is_some_and(|id| grounded.contains(&id))
            && a2.is_some_and(|id| grounded.contains(&id));
        assert!(
            !both_in,
            "classical: individually-weaker pro-p args should not both be In"
        );
    }
}

// --- Property tests ---

mod property_tests {
    use super::*;
    use proptest::prelude::*;

    fn arb_argument_set() -> impl Strategy<Value = BTreeSet<ArgumentId>> {
        proptest::collection::btree_set(0_usize..100, 0..10)
            .prop_map(|s| s.into_iter().map(ArgumentId).collect())
    }

    // Reflexivity — compare(S, S) == Equal for all strategies.
    proptest! {
        #[test]
        fn elitist_reflexive(s in arb_argument_set()) {
            let store = ArgumentStore::new();
            let lifted = LiftedSetPreference {
                base: Box::new(IdBasedOrdering),
                lifting: LiftingStrategy::Elitist,
            };
            prop_assert_eq!(lifted.compare(&s, &s, &store), Preference::Equal);
        }

        #[test]
        fn democratic_reflexive(s in arb_argument_set()) {
            let store = ArgumentStore::new();
            let lifted = LiftedSetPreference {
                base: Box::new(IdBasedOrdering),
                lifting: LiftingStrategy::Democratic,
            };
            prop_assert_eq!(lifted.compare(&s, &s, &store), Preference::Equal);
        }
    }
}
