//! Weakest-link argument ordering.
//!
//! Compares arguments by their weakest elements — both defeasible rules
//! and ordinary premises — using the corrected set comparison from
//! arXiv:1804.06763 Definition 21. Three cases are distinguished based on
//! whether arguments are strict (no defeasible rules) or firm (all axiom
//! premises).

use std::collections::HashSet;

use super::{
    lifted_strict, ArgumentOrdering, LiftingStrategy, Preference, PremiseOrdering, RuleOrdering,
};
use crate::framework::argument::ArgumentId;
use crate::framework::argument_store::ArgumentStore;
use crate::system::knowledge::PremiseKind;
use crate::system::rules::DefeasibleRule;

/// Weakest-link argument ordering (corrected Definition 21, arXiv:1804.06763).
///
/// Compares arguments by their weakest elements using the set comparison ◁
/// selected by [`LiftingStrategy`]. Three cascading cases:
///
/// 1. Both strict (`DefRules` = ∅): compare `OrdPrems` only.
/// 2. Both firm (Prem ⊆ `K_n)`: compare `DefRules` only.
/// 3. Otherwise: B ≺ A iff OrdPrems(B) ◁ OrdPrems(A) AND DefRules(B) ◁ DefRules(A).
///
/// # Example
///
/// ```
/// use pickaxe_rs::prelude::*;
///
/// let ordering = WeakestLinkOrdering {
///     rule_ordering: Box::new(NoPreference),
///     premise_ordering: Box::new(NoPreference),
///     lifting: LiftingStrategy::Democratic,
/// };
///
/// let (system, _) = AspicSystemBuilder::new()
///     .ordinary_premise(formula!(p))
///     .defeasible_rule("d1", vec![formula!(p)], formula!(q))
///     .with_classical_negation()
///     .build();
///
/// let pipeline = AspicPipeline::classical(system, Box::new(ordering));
/// let result = pipeline.evaluate(Semantics::Grounded).unwrap();
/// assert_eq!(result.extensions.len(), 1);
/// ```
#[derive(Debug)]
pub struct WeakestLinkOrdering {
    pub rule_ordering: Box<dyn RuleOrdering>,
    pub premise_ordering: Box<dyn PremiseOrdering>,
    pub lifting: LiftingStrategy,
}

impl ArgumentOrdering for WeakestLinkOrdering {
    fn compare(&self, a: ArgumentId, b: ArgumentId, store: &ArgumentStore) -> Preference {
        let Some(arg_a) = store.get(a) else {
            return Preference::Incomparable;
        };
        let Some(arg_b) = store.get(b) else {
            return Preference::Incomparable;
        };

        let def_rules_a = arg_a.defeasible_rules(store);
        let def_rules_b = arg_b.defeasible_rules(store);
        let a_strict = def_rules_a.is_empty();
        let b_strict = def_rules_b.is_empty();
        let a_firm = arg_a.is_firm(store);
        let b_firm = arg_b.is_firm(store);

        let ord_prems_a: Vec<_> = arg_a
            .premises(store)
            .into_iter()
            .filter(|p| p.kind != PremiseKind::Axiom)
            .collect();
        let ord_prems_b: Vec<_> = arg_b
            .premises(store)
            .into_iter()
            .filter(|p| p.kind != PremiseKind::Axiom)
            .collect();

        let lifting = &self.lifting;

        let prems_strict = |a_prems: &[_], b_prems: &[_]| {
            lifted_strict(a_prems, b_prems, lifting, |pa, pb| {
                self.premise_ordering.compare(pa, pb).is_strictly_less()
            })
        };
        let rules_strict = |a_rules: &[DefeasibleRule], b_rules: &[DefeasibleRule]| {
            lifted_strict(a_rules, b_rules, lifting, |ra, rb| {
                self.rule_ordering
                    .compare(&ra.id, &rb.id)
                    .is_strictly_less()
            })
        };

        let prems_ids_equal = || -> bool {
            let ids_a: HashSet<_> = ord_prems_a.iter().map(|p| &p.formula).collect();
            let ids_b: HashSet<_> = ord_prems_b.iter().map(|p| &p.formula).collect();
            ids_a == ids_b
        };
        let rules_ids_equal = || -> bool {
            let ids_a: HashSet<_> = def_rules_a.iter().map(|r| &r.id).collect();
            let ids_b: HashSet<_> = def_rules_b.iter().map(|r| &r.id).collect();
            ids_a == ids_b
        };

        if a_strict && b_strict {
            if prems_ids_equal() {
                return Preference::Equal;
            }
            let a_s_b = prems_strict(&ord_prems_a, &ord_prems_b);
            let b_s_a = prems_strict(&ord_prems_b, &ord_prems_a);
            return match (a_s_b, b_s_a) {
                (true, false) => Preference::StrictlyDispreferred,
                (false, true) => Preference::StrictlyPreferred,
                _ => Preference::Incomparable,
            };
        }

        if a_firm && b_firm {
            if rules_ids_equal() {
                return Preference::Equal;
            }
            let a_s_b = rules_strict(&def_rules_a, &def_rules_b);
            let b_s_a = rules_strict(&def_rules_b, &def_rules_a);
            return match (a_s_b, b_s_a) {
                (true, false) => Preference::StrictlyDispreferred,
                (false, true) => Preference::StrictlyPreferred,
                _ => Preference::Incomparable,
            };
        }

        if prems_ids_equal() && rules_ids_equal() {
            return Preference::Equal;
        }

        let a_s_b =
            prems_strict(&ord_prems_a, &ord_prems_b) && rules_strict(&def_rules_a, &def_rules_b);
        let b_s_a =
            prems_strict(&ord_prems_b, &ord_prems_a) && rules_strict(&def_rules_b, &def_rules_a);
        match (a_s_b, b_s_a) {
            (true, false) => Preference::StrictlyDispreferred,
            (false, true) => Preference::StrictlyPreferred,
            _ => Preference::Incomparable,
        }
    }
}
