//! Last-link argument ordering.
//!
//! Compares arguments by the last (topmost) defeasible rules applied,
//! using the corrected set comparison from arXiv:1804.06763 Definition 20.
//! Falls back to premise comparison when both arguments are premise-only
//! (strict, no defeasible rules).

use std::collections::HashSet;

use super::{
    lifted_strict, ArgumentOrdering, LiftingStrategy, Preference, PremiseOrdering, RuleOrdering,
};
use crate::framework::argument::ArgumentId;
use crate::framework::argument_store::ArgumentStore;

/// Last-link argument ordering (corrected Definition 20, arXiv:1804.06763).
///
/// Compares arguments by the last (topmost) defeasible rules applied,
/// using the set comparison ◁ selected by [`LiftingStrategy`].
///
/// Falls back to premise comparison when both arguments are premise-only.
///
/// # Example
///
/// ```
/// use pickaxe_rs::prelude::*;
///
/// let rule_ord = TieredOrdering::new(vec![
///     vec![RuleId("d1".into())],
///     vec![RuleId("d2".into())],
/// ]);
///
/// let ordering = LastLinkOrdering {
///     rule_ordering: Box::new(rule_ord),
///     premise_ordering: Box::new(NoPreference),
///     lifting: LiftingStrategy::Elitist,
/// };
///
/// // Use with the classical pipeline.
/// 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 LastLinkOrdering {
    pub rule_ordering: Box<dyn RuleOrdering>,
    pub premise_ordering: Box<dyn PremiseOrdering>,
    pub lifting: LiftingStrategy,
}

impl ArgumentOrdering for LastLinkOrdering {
    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 last_d_a = arg_a.last_defeasible_rules(store);
        let last_d_b = arg_b.last_defeasible_rules(store);

        if last_d_a.is_empty() && last_d_b.is_empty() {
            let prems_a = arg_a.premises(store);
            let prems_b = arg_b.premises(store);

            if prems_a.is_empty() && prems_b.is_empty() {
                return Preference::Equal;
            }

            return set_compare_premises(
                &prems_a,
                &prems_b,
                &*self.premise_ordering,
                &self.lifting,
            );
        }

        let ids_a: HashSet<_> = last_d_a.iter().map(|r| &r.id).collect();
        let ids_b: HashSet<_> = last_d_b.iter().map(|r| &r.id).collect();
        if ids_a == ids_b {
            return Preference::Equal;
        }

        let cmp = |ra: &crate::system::rules::DefeasibleRule,
                   rb: &crate::system::rules::DefeasibleRule| {
            self.rule_ordering
                .compare(&ra.id, &rb.id)
                .is_strictly_less()
        };

        let a_strict_b = lifted_strict(&last_d_a, &last_d_b, &self.lifting, cmp);
        let b_strict_a = lifted_strict(&last_d_b, &last_d_a, &self.lifting, cmp);

        match (a_strict_b, b_strict_a) {
            (true, false) => Preference::StrictlyDispreferred,
            (false, true) => Preference::StrictlyPreferred,
            _ => Preference::Incomparable,
        }
    }
}

fn set_compare_premises(
    a: &[crate::system::knowledge::Premise],
    b: &[crate::system::knowledge::Premise],
    ordering: &dyn PremiseOrdering,
    lifting: &LiftingStrategy,
) -> Preference {
    let ids_a: HashSet<_> = a.iter().map(|p| &p.formula).collect();
    let ids_b: HashSet<_> = b.iter().map(|p| &p.formula).collect();
    if ids_a == ids_b {
        return Preference::Equal;
    }

    let a_strict_b = lifted_strict(a, b, lifting, |pa, pb| {
        ordering.compare(pa, pb).is_strictly_less()
    });
    let b_strict_a = lifted_strict(b, a, lifting, |pb, pa| {
        ordering.compare(pb, pa).is_strictly_less()
    });

    match (a_strict_b, b_strict_a) {
        (true, false) => Preference::StrictlyDispreferred,
        (false, true) => Preference::StrictlyPreferred,
        _ => Preference::Incomparable,
    }
}
