//! Preference orderings for ASPIC+ argumentation systems.
//!
//! ASPIC+ parameterises defeat by preference orderings over rules, premises,
//! and arguments (Definition 3.19, Modgil & Prakken 2014). This module
//! provides both the **traits** and the **concrete implementations**:
//!
//! ## Infrastructure (traits and base types)
//!
//! - [`Preference`] — the four-valued outcome of a pairwise comparison.
//! - [`RuleOrdering`], [`PremiseOrdering`], [`ArgumentOrdering`] — element-level
//!   ordering traits.
//! - [`SetPreference`] — set-level ordering trait for accrual semantics.
//! - [`LiftingStrategy`] — dispatch between elitist and democratic set comparisons.
//! - Set-comparison functions: [`elitist_strict`], [`democratic_strict`],
//!   [`lifted_strict`].
//!
//! ## Implementations
//!
//! | Type | Principle | Reference |
//! |------|-----------|-----------|
//! | [`TieredOrdering`] | Explicit tier-based comparison | — |
//! | [`NoPreference`] | All items equally preferred | — |
//! | [`FlatOrdering`] | All arguments equally preferred | — |
//! | [`LastLinkOrdering`] | Compare by topmost defeasible rules | Definition 20 (corrected) |
//! | [`WeakestLinkOrdering`] | Compare by weakest rules and premises | Definition 21 (corrected) |
//! | [`LiftedSetPreference`] | Derive set-level from argument-level ordering | Definition 19 |

pub mod flat;
pub mod last_link;
pub mod lifted_set;
pub mod weakest_link;

pub use flat::FlatOrdering;
pub use last_link::LastLinkOrdering;
pub use lifted_set::LiftedSetPreference;
pub use weakest_link::WeakestLinkOrdering;

use std::collections::BTreeSet;
use std::collections::HashMap;
use std::hash::Hash;

use crate::framework::argument::ArgumentId;
use crate::framework::argument_store::ArgumentStore;
use crate::system::knowledge::Premise;
use crate::system::rules::RuleId;

/// The result of comparing two items under a preference ordering.
///
/// ASPIC+ orderings are partial pre-orders: two items may be incomparable.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum Preference {
    /// The first item is strictly preferred over the second.
    StrictlyPreferred,
    /// Both items are equally preferred.
    Equal,
    /// The first item is strictly less preferred than the second.
    StrictlyDispreferred,
    /// No preference relationship exists between the items.
    Incomparable,
}

impl Preference {
    /// True when `self` indicates "less than or equal" (weaker or same).
    pub fn is_leq(&self) -> bool {
        matches!(self, Preference::StrictlyDispreferred | Preference::Equal)
    }

    /// True only for `StrictlyDispreferred` (strict <).
    ///
    /// Used by the corrected set comparisons (arXiv:1804.06763 Definition 19)
    /// which define ◁ directly in terms of the strict element ordering.
    pub fn is_strictly_less(&self) -> bool {
        matches!(self, Preference::StrictlyDispreferred)
    }
}

/// Corrected Elitist strict set comparison (arXiv:1804.06763 Definition 19).
///
/// `Sigma ◁_Eli Sigma'` iff there EXISTS X in Sigma such that
/// FOR ALL Y in Sigma': X < Y (using strict <, not ≤).
///
/// This directly computes the strict ordering without deriving it from ≤,
/// which avoids the consistency-postulate violation identified by Dyrkolbotn.
pub fn elitist_strict<T>(
    sigma: &[T],
    sigma_prime: &[T],
    is_strictly_less: impl Fn(&T, &T) -> bool,
) -> bool {
    if sigma.is_empty() {
        return false;
    }
    if sigma_prime.is_empty() {
        return true;
    }
    sigma
        .iter()
        .any(|x| sigma_prime.iter().all(|y| is_strictly_less(x, y)))
}

/// Corrected Democratic strict set comparison (arXiv:1804.06763 Definition 19).
///
/// `Sigma ◁_Dem Sigma'` iff FOR ALL X in Sigma, there EXISTS Y in Sigma'
/// such that X < Y (using strict <, not ≤).
///
/// This directly computes the strict ordering without deriving it from ≤,
/// which avoids the consistency-postulate violation identified by Dyrkolbotn.
pub fn democratic_strict<T>(
    sigma: &[T],
    sigma_prime: &[T],
    is_strictly_less: impl Fn(&T, &T) -> bool,
) -> bool {
    if sigma.is_empty() {
        return false;
    }
    if sigma_prime.is_empty() {
        return true;
    }
    sigma
        .iter()
        .all(|x| sigma_prime.iter().any(|y| is_strictly_less(x, y)))
}

/// Dispatch a strict set comparison through a [`LiftingStrategy`].
///
/// Returns `true` when `sigma ◁ sigma'` under the chosen lifting
/// (elitist or democratic) using the provided strict element ordering.
pub fn lifted_strict<T>(
    sigma: &[T],
    sigma_prime: &[T],
    lifting: &LiftingStrategy,
    is_strictly_less: impl Fn(&T, &T) -> bool + Copy,
) -> bool {
    match lifting {
        LiftingStrategy::Elitist => elitist_strict(sigma, sigma_prime, is_strictly_less),
        LiftingStrategy::Democratic => democratic_strict(sigma, sigma_prime, is_strictly_less),
    }
}

/// A partial pre-order over rule identifiers.
///
/// Implementations define how rules are compared for the purpose of
/// computing defeat via last-link or weakest-link principles.
pub trait RuleOrdering: std::fmt::Debug + Send + Sync {
    fn compare(&self, a: &RuleId, b: &RuleId) -> Preference;
}

/// A partial pre-order over premises (by their formulae).
///
/// Used by weakest-link to compare the premise bases of arguments.
pub trait PremiseOrdering: std::fmt::Debug + Send + Sync {
    fn compare(&self, a: &Premise, b: &Premise) -> Preference;
}

/// A partial pre-order over arguments, derived from rule/premise orderings
/// via a link principle (last-link or weakest-link).
pub trait ArgumentOrdering: std::fmt::Debug + Send + Sync {
    fn compare(&self, a: ArgumentId, b: ArgumentId, store: &ArgumentStore) -> Preference;

    fn is_strictly_preferred(&self, a: ArgumentId, b: ArgumentId, store: &ArgumentStore) -> bool {
        self.compare(a, b, store) == Preference::StrictlyPreferred
    }
}

/// An ordering defined by explicit lists of tiers (most preferred first).
///
/// Items assigned to a tier are compared by tier index (lower = more preferred).
/// Items *not* assigned to any tier are treated as **incomparable** with all
/// other items — both tiered and untiered. This follows the standard
/// partial-order reading: absence of a stated preference means no relationship
/// exists (see Modgil & Prakken 2014, Definition 3.19).
///
/// # Example
///
/// ```
/// use pickaxe_rs::prelude::*;
///
/// // Tier 0 (most preferred): s1.  Tier 1: d1, d2.
/// let rule_ord = TieredOrdering::new(vec![
///     vec![RuleId("s1".into())],
///     vec![RuleId("d1".into()), RuleId("d2".into())],
/// ]);
///
/// assert_eq!(
///     rule_ord.compare(&RuleId("s1".into()), &RuleId("d1".into())),
///     Preference::StrictlyPreferred,
/// );
/// assert_eq!(
///     rule_ord.compare(&RuleId("d1".into()), &RuleId("d2".into())),
///     Preference::Equal,
/// );
/// ```
#[derive(Clone, Debug)]
pub struct TieredOrdering<K: Eq + Hash + Clone> {
    tiers: HashMap<K, usize>,
}

impl<K: Eq + Hash + Clone> TieredOrdering<K> {
    /// Create from a list of tiers: `tiers[0]` is the most preferred tier.
    pub fn new(tiers: Vec<Vec<K>>) -> Self {
        let mut map = HashMap::new();
        for (tier_idx, tier) in tiers.into_iter().enumerate() {
            for item in tier {
                map.insert(item, tier_idx);
            }
        }
        TieredOrdering { tiers: map }
    }

    fn compare_items(&self, a: &K, b: &K) -> Preference {
        match (self.tiers.get(a), self.tiers.get(b)) {
            (Some(ta), Some(tb)) => match ta.cmp(tb) {
                std::cmp::Ordering::Less => Preference::StrictlyPreferred,
                std::cmp::Ordering::Equal => Preference::Equal,
                std::cmp::Ordering::Greater => Preference::StrictlyDispreferred,
            },
            _ => Preference::Incomparable,
        }
    }
}

impl RuleOrdering for TieredOrdering<RuleId> {
    fn compare(&self, a: &RuleId, b: &RuleId) -> Preference {
        self.compare_items(a, b)
    }
}

impl PremiseOrdering for TieredOrdering<crate::language::formula::Formula> {
    fn compare(&self, a: &Premise, b: &Premise) -> Preference {
        self.compare_items(&a.formula, &b.formula)
    }
}

/// An ordering that treats all items as equally preferred.
#[derive(Clone, Debug)]
pub struct NoPreference;

impl RuleOrdering for NoPreference {
    fn compare(&self, _a: &RuleId, _b: &RuleId) -> Preference {
        Preference::Equal
    }
}

impl PremiseOrdering for NoPreference {
    fn compare(&self, _a: &Premise, _b: &Premise) -> Preference {
        Preference::Equal
    }
}

// ---------------------------------------------------------------------------
// Set-level preference
// ---------------------------------------------------------------------------

/// Preference ordering over sets of arguments, used by the accrual evaluator
/// to compare accrual sets.
pub trait SetPreference: Send + Sync {
    fn compare(
        &self,
        set_a: &BTreeSet<ArgumentId>,
        set_b: &BTreeSet<ArgumentId>,
        store: &ArgumentStore,
    ) -> Preference;
}

/// Strategy for lifting an element-level ordering to a set-level ordering.
///
/// Both strategies are defined in Modgil & Prakken (2014) Definition 3.19
/// (corrected in arXiv:1804.06763 Definition 19).
#[derive(Clone, Debug)]
pub enum LiftingStrategy {
    /// Elitist: S2 ⊴ S1 iff ∃b∈S2: ∀a∈S1: b ≤ a.
    Elitist,
    /// Democratic: S2 ⊴ S1 iff ∀b∈S2: ∃a∈S1: b ≤ a.
    Democratic,
}
