//! Trait abstractions for each stage of the ASPIC+ evaluation pipeline.
//!
//! The pipeline proceeds through four stages:
//!
//! 1. **Grounding** ([`Grounder`]) — eliminate variables by substituting all
//!    constants from the Herbrand base, producing a [`GroundedSystem`].
//! 2. **Argument construction** ([`ArgumentConstructor`]) — build the set of
//!    all arguments from grounded knowledge and rules, stored in an
//!    [`ArgumentStore`].
//! 3. **Attack computation** ([`AttackComputer`]) — identify rebut, undermine,
//!    and undercut attacks between arguments using the contrariness function.
//! 4. **Evaluation** ([`Evaluator`]) — compute extensions/labellings under a
//!    chosen [`Semantics`] and preference ordering.
//!
//! Each stage is represented by a trait so that implementations can be swapped
//! independently (e.g. naive vs. indexed attack computation, SAT-based vs.
//! labelling-based evaluation).  The concrete pipeline orchestrator lives in
//! [`super::AspicPipeline`].
//!
//! [`SemanticsSolver`] is a lower-level trait used internally by evaluators
//! that delegate to a Dung-style abstract argumentation framework solver.

use crate::error::AspicError;
use crate::framework::abstract_af::AbstractFramework;
use crate::framework::argument_store::ArgumentStore;
use crate::framework::attack::Attack;
use crate::framework::semantics::{Extension, Labelling, Semantics};
use crate::language::grounding::GroundedSystem;
use crate::system::contrariness::ContrarinessFunction;
use crate::system::ordering::{ArgumentOrdering, SetPreference};
use crate::system::AspicSystem;

/// The output of an [`Evaluator`]: paired extension sets and their labellings.
///
/// Each extension has a corresponding labelling at the same index.  Task modes
/// like [`Evaluator::find_one`] and [`Evaluator::count`] may truncate or omit
/// entries; callers should not assume the vectors are non-empty.
#[derive(Clone, Debug)]
pub struct EvaluationResult {
    /// One [`Labelling`] per computed extension, mapping every argument to
    /// `In`, `Out`, or `Undec`.
    pub labellings: Vec<Labelling>,
    /// The set of extensions under the chosen semantics, where each extension
    /// is a `BTreeSet<ArgumentId>`.
    pub extensions: Vec<Extension>,
}

/// Top-level preference configuration for the pipeline.
///
/// Different evaluators require different kinds of preference relation:
/// the classical evaluator compares individual arguments, while the
/// accrual evaluator compares *sets* of arguments.  This enum surfaces
/// that choice at the pipeline level so that it can be configured
/// declaratively and inspected at runtime.
pub enum PreferenceConfig {
    /// Classical argument-level ordering used for defeat computation
    /// (Modgil & Prakken 2014, Definition 3.14).
    ///
    /// Suitable for [`crate::pipeline::evaluation::classical::ClassicalEvaluator`].
    ArgumentOrdering(Box<dyn ArgumentOrdering>),
    /// Set-level preference used for l-defeat computation in the accrual
    /// framework (Prakken 2019, Definition 4.4).
    ///
    /// Suitable for [`crate::pipeline::evaluation::accrual::AccrualEvaluator`].
    SetPreference(Box<dyn SetPreference>),
}

impl PreferenceConfig {
    /// Try to extract the argument ordering, returning `None` if this is a
    /// set preference.
    pub fn as_argument_ordering(&self) -> Option<&dyn ArgumentOrdering> {
        match self {
            PreferenceConfig::ArgumentOrdering(o) => Some(&**o),
            PreferenceConfig::SetPreference(_) => None,
        }
    }

    /// Try to extract the set preference, returning `None` if this is an
    /// argument ordering.
    pub fn as_set_preference(&self) -> Option<&dyn SetPreference> {
        match self {
            PreferenceConfig::SetPreference(p) => Some(&**p),
            PreferenceConfig::ArgumentOrdering(_) => None,
        }
    }
}

/// **Stage 1 — Grounding.**  Eliminates variables from an [`AspicSystem`] by
/// substituting every combination of constants from the Herbrand base.
///
/// The default implementation is [`NaiveGrounder`](crate::pipeline::grounding::NaiveGrounder),
/// which performs full Herbrand enumeration.
pub trait Grounder: Send + Sync {
    /// Produce a fully ground system from `system`, or return an error if the
    /// system is malformed.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if `system` cannot be grounded (e.g. it is
    /// malformed or violates constraints checked during grounding).
    fn ground(&self, system: &AspicSystem) -> Result<GroundedSystem, AspicError>;
}

/// **Stage 2 — Argument construction.**  Builds the complete set of ASPIC+
/// arguments from grounded rules and knowledge.
///
/// The default implementation is
/// [`ForwardChainingConstructor`](crate::pipeline::construction::ForwardChainingConstructor),
/// which applies forward chaining until no new arguments can be derived.
pub trait ArgumentConstructor: Send + Sync {
    /// Construct all arguments derivable from `system` and return them in an
    /// [`ArgumentStore`].
    fn construct(&self, system: &GroundedSystem) -> ArgumentStore;
}

/// **Stage 3 — Attack computation.**  Identifies all attack relations
/// (rebut, undermine, undercut) between arguments using the system's
/// [`ContrarinessFunction`].
///
/// Two implementations ship with the crate:
/// - [`PairwiseAttackComputer`](crate::pipeline::attack::PairwiseAttackComputer)
///   — O(n²) brute-force enumeration.
/// - [`IndexedAttackComputer`](crate::pipeline::attack::IndexedAttackComputer)
///   — hash-indexed lookup.
pub trait AttackComputer: Send + Sync {
    /// Return every attack between arguments in `store`, given `contrariness`.
    fn compute(&self, store: &ArgumentStore, contrariness: &ContrarinessFunction) -> Vec<Attack>;
}

/// **Stage 4 — Evaluation.**  Computes extensions and labellings for a given
/// [`Semantics`] and [`PreferenceConfig`].
///
/// This trait abstracts over the full evaluation step: defeat computation
/// (applying preferences to attacks), abstract-framework construction, and
/// semantics solving.  Two built-in implementations exist:
///
/// - [`ClassicalEvaluator`](super::evaluation::classical::ClassicalEvaluator) — standard
///   ASPIC+ evaluation via an [`AbstractFramework`] and a [`SemanticsSolver`].
/// - [`AccrualEvaluator`](super::evaluation::accrual::AccrualEvaluator) — accrual-based
///   evaluation (Prakken 2019) using set-level preferences and l-defeats.
///
/// The trait also provides [`find_one`](Self::find_one) and
/// [`count`](Self::count) for task-mode optimisations; backends may override
/// the default implementations for better performance.
pub trait Evaluator: Send + Sync {
    /// Compute all extensions and their labellings under `semantics`.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if the evaluator encounters an unsupported
    /// semantics or an internal solver failure.
    fn evaluate(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<EvaluationResult, AspicError>;

    /// Return at most one extension for the given semantics.
    ///
    /// The default implementation delegates to [`evaluate`](Self::evaluate)
    /// and truncates the result. Backends may override for performance.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if the underlying evaluation fails.
    fn find_one(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<EvaluationResult, AspicError> {
        let mut result = self.evaluate(store, attacks, semantics, preference)?;
        result.extensions.truncate(1);
        result.labellings.truncate(1);
        Ok(result)
    }

    /// Return the number of extensions for the given semantics.
    ///
    /// The default implementation delegates to [`evaluate`](Self::evaluate)
    /// and returns the length. Backends may override to avoid per-extension
    /// allocation.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if the underlying evaluation fails.
    fn count(
        &self,
        store: &ArgumentStore,
        attacks: &[Attack],
        semantics: Semantics,
        preference: &PreferenceConfig,
    ) -> Result<usize, AspicError> {
        Ok(self
            .evaluate(store, attacks, semantics, preference)?
            .extensions
            .len())
    }
}

/// Low-level solver for Dung-style abstract argumentation frameworks.
///
/// Operates on an [`AbstractFramework`] (a directed attack graph) rather than
/// the full ASPIC+ structure.  [`Evaluator`] implementations typically
/// delegate to a `SemanticsSolver` after converting attacks into defeats.
///
/// Built-in backends:
/// - Labelling-based solver (no feature flags required).
/// - SAT-based solver (`sat` feature) via `rustsat-batsat` or `rustsat-cadical`.
/// - SCC-decomposing solver (`sat` feature) that partitions the framework by
///   strongly connected components before solving.
/// - External ICCMA / Aspartix solvers (behind `iccma` / `aspartix` features).
pub trait SemanticsSolver: Send + Sync {
    /// Enumerate all extensions of `af` under semantics `sem`.
    fn extensions(&self, af: &AbstractFramework, sem: Semantics) -> Vec<Extension>;

    /// Return a single extension for the given semantics, or `None` if no
    /// extension exists.
    ///
    /// The default implementation delegates to [`extensions`](Self::extensions).
    /// Backends may override for performance (e.g. a single SAT call instead
    /// of full enumeration).
    fn find_one(&self, af: &AbstractFramework, sem: Semantics) -> Option<Extension> {
        self.extensions(af, sem).into_iter().next()
    }

    /// Return the number of extensions for the given semantics.
    ///
    /// The default implementation delegates to [`extensions`](Self::extensions).
    /// Backends may override to avoid per-extension allocation.
    fn count(&self, af: &AbstractFramework, sem: Semantics) -> usize {
        self.extensions(af, sem).len()
    }

    /// Derive labellings from the computed extensions.
    ///
    /// The default implementation calls [`extensions`](Self::extensions) and
    /// converts each extension into a [`Labelling`] via
    /// [`Labelling::from_extension`].
    fn labellings(&self, af: &AbstractFramework, sem: Semantics) -> Vec<Labelling> {
        self.extensions(af, sem)
            .into_iter()
            .map(|ext| Labelling::from_extension(&ext, af))
            .collect()
    }
}
