//! Argumentation semantics: extensions, labellings, and their interplay.
//!
//! In abstract argumentation (Dung, 1995) the acceptability of arguments is
//! determined by a *semantics* — a principled criterion for selecting
//! coherent subsets of arguments (extensions) or three-valued argument
//! classifications (labellings).
//!
//! # Extensions
//!
//! An [`Extension`] is a set of [`ArgumentId`]s that are jointly acceptable
//! under a given [`Semantics`]. The framework supports the classical Dung
//! semantics:
//!
//! | Semantics        | Intuition |
//! |------------------|-----------|
//! | [`Grounded`](Semantics::Grounded)     | Unique smallest complete extension — maximally sceptical |
//! | [`Complete`](Semantics::Complete)      | Every defended argument is accepted |
//! | [`Preferred`](Semantics::Preferred)    | Maximal (w.r.t. ⊆) complete extensions |
//! | [`Stable`](Semantics::Stable)          | Complete extensions that defeat every non-member |
//! | [`SemiStable`](Semantics::SemiStable)  | Complete extensions minimising undecided arguments |
//! | [`Ideal`](Semantics::Ideal)            | Largest admissible set contained in every preferred extension |
//! | [`Eager`](Semantics::Eager)            | Largest admissible set contained in every semi-stable extension |
//! | [`Admissible`](Semantics::Admissible)  | Conflict-free and self-defending sets |
//!
//! # Labellings
//!
//! A [`Labelling`] assigns every argument one of three labels:
//!
//! - **[`In`](Label::In)** — the argument is accepted,
//! - **[`Out`](Label::Out)** — the argument is rejected (defeated by an
//!   accepted argument),
//! - **[`Undec`](Label::Undec)** — the argument is undecided.
//!
//! Every extension induces a labelling via [`Labelling::from_extension`],
//! and conversely the [`In`](Label::In)-labelled arguments of a complete
//! labelling form a complete extension. The two views are interchangeable
//! but each is more convenient in different contexts: extensions for
//! set-based reasoning, labellings for inspecting individual argument
//! status.

use std::collections::{BTreeSet, HashMap};

use crate::framework::abstract_af::AbstractFramework;
use crate::framework::argument::ArgumentId;

// ── Extensions ──────────────────────────────────────────────────────────

/// A set of argument IDs jointly accepted under some semantics.
///
/// Represented as a [`BTreeSet`] to give deterministic iteration order,
/// which simplifies testing and serialisation.
pub type Extension = BTreeSet<ArgumentId>;

/// The Dung semantics supported by the framework.
///
/// Each variant corresponds to a well-known acceptability criterion from
/// Dung (1995) and its later refinements. Solver implementations live in
/// [`crate::pipeline::evaluation`].
///
/// # Example
///
/// ```
/// use pickaxe_rs::prelude::*;
///
/// let (system, _) = AspicSystemBuilder::new()
///     .ordinary_premise(formula!(p))
///     .defeasible_rule("d1", vec![formula!(p)], formula!(q))
///     .with_classical_negation()
///     .build();
///
/// let ordering: Box<dyn ArgumentOrdering> = Box::new(FlatOrdering);
/// let pipeline = AspicPipeline::classical(system, ordering);
///
/// // The grounded semantics always yields exactly one extension.
/// let result = pipeline.evaluate(Semantics::Grounded).unwrap();
/// assert_eq!(result.extensions.len(), 1);
/// ```
#[derive(Clone, Copy, Debug, Eq, Hash, PartialEq)]
pub enum Semantics {
    /// The unique smallest complete extension (sceptical baseline).
    Grounded,
    /// Maximal complete extensions (credulous baseline).
    Preferred,
    /// Complete extensions that attack every non-member.
    Stable,
    /// Extensions where every defended argument is included.
    Complete,
    /// Complete extensions whose range is maximal.
    SemiStable,
    /// The largest admissible set inside every preferred extension.
    Ideal,
    /// The largest admissible set inside every semi-stable extension.
    Eager,
    /// Conflict-free and self-defending sets (not necessarily complete).
    Admissible,
}

// ── Labellings ──────────────────────────────────────────────────────────

/// A three-valued label assigned to an argument in a labelling.
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum Label {
    /// The argument is accepted.
    In,
    /// The argument is rejected — it is defeated by an accepted argument.
    Out,
    /// The argument is neither accepted nor rejected.
    Undec,
}

/// A complete labelling of an [`AbstractFramework`].
///
/// Maps every argument to a [`Label`]. A labelling can be derived from an
/// extension via [`from_extension`](Labelling::from_extension), or
/// constructed directly by a solver.
#[derive(Clone, Debug, Eq, PartialEq)]
pub struct Labelling {
    labels: HashMap<ArgumentId, Label>,
}

impl Labelling {
    /// Build a labelling from an explicit label map.
    pub fn new(labels: HashMap<ArgumentId, Label>) -> Self {
        Labelling { labels }
    }

    /// Look up the label for a single argument, defaulting to
    /// [`Undec`](Label::Undec) if the argument is absent from the map.
    pub fn label_of(&self, id: ArgumentId) -> Label {
        self.labels.get(&id).cloned().unwrap_or(Label::Undec)
    }

    /// All argument IDs labelled [`In`](Label::In).
    pub fn in_args(&self) -> BTreeSet<ArgumentId> {
        self.labels
            .iter()
            .filter(|(_, l)| **l == Label::In)
            .map(|(id, _)| *id)
            .collect()
    }

    /// All argument IDs labelled [`Out`](Label::Out).
    pub fn out_args(&self) -> BTreeSet<ArgumentId> {
        self.labels
            .iter()
            .filter(|(_, l)| **l == Label::Out)
            .map(|(id, _)| *id)
            .collect()
    }

    /// All argument IDs labelled [`Undec`](Label::Undec).
    pub fn undec_args(&self) -> BTreeSet<ArgumentId> {
        self.labels
            .iter()
            .filter(|(_, l)| **l == Label::Undec)
            .map(|(id, _)| *id)
            .collect()
    }

    /// Derive a labelling from an extension and an abstract framework.
    ///
    /// - Arguments in `ext` are labelled [`In`](Label::In).
    /// - Arguments defeated by at least one `In` argument are labelled
    ///   [`Out`](Label::Out).
    /// - All remaining arguments are labelled [`Undec`](Label::Undec).
    pub fn from_extension(ext: &BTreeSet<ArgumentId>, af: &AbstractFramework) -> Self {
        let mut labels = HashMap::new();
        for &arg in &af.arguments {
            if ext.contains(&arg) {
                labels.insert(arg, Label::In);
            } else if ext.iter().any(|&a| af.defeats(a, arg)) {
                labels.insert(arg, Label::Out);
            } else {
                labels.insert(arg, Label::Undec);
            }
        }
        Labelling { labels }
    }
}
