//! The ASPIC+ evaluation pipeline: from system to extensions.
//!
//! This module orchestrates the four-stage pipeline that transforms an
//! [`AspicSystem`] into argumentation-theoretic extensions and labellings:
//!
//! 1. **Grounding** ([`Grounder`]) — eliminate first-order variables via
//!    Herbrand substitution.
//! 2. **Argument construction** ([`ArgumentConstructor`]) — build the set of
//!    all derivable ASPIC+ arguments.
//! 3. **Attack computation** ([`AttackComputer`]) — identify rebut, undermine,
//!    and undercut attacks between arguments.
//! 4. **Evaluation** ([`Evaluator`]) — compute defeats (applying preference
//!    orderings to attacks), build the abstract framework, and solve for
//!    extensions under a chosen [`Semantics`].
//!
//! # Infrastructure vs. implementations
//!
//! The pipeline separates **infrastructure** (traits and orchestration) from
//! **implementations** (concrete algorithms):
//!
//! | Layer          | Module                  | Contents |
//! |----------------|-------------------------|----------|
//! | Infrastructure | [`traits`]              | Stage traits, [`PreferenceConfig`], [`EvaluationResult`] |
//! | Infrastructure | [`config`]              | Declarative [`PipelineConfig`] and its builder |
//! | Infrastructure | (this module)           | [`AspicPipeline`] orchestrator and [`PipelineResult`] |
//! | Implementation | [`grounding`]           | [`NaiveGrounder`](grounding::NaiveGrounder), [`SemiNaiveGrounder`](grounding::SemiNaiveGrounder) |
//! | Implementation | [`construction`]        | [`ForwardChainingConstructor`](construction::ForwardChainingConstructor) |
//! | Implementation | [`attack`]              | [`PairwiseAttackComputer`](attack::PairwiseAttackComputer), [`IndexedAttackComputer`](attack::IndexedAttackComputer) |
//! | Implementation | [`evaluation`]          | [`ClassicalEvaluator`](evaluation::classical::ClassicalEvaluator), [`AccrualEvaluator`](evaluation::accrual::AccrualEvaluator), solver backends |
//!
//! Argument orderings and set preferences live in [`crate::system::ordering`]
//! alongside their trait definitions, since they are part of the ASPIC+
//! system specification rather than pipeline-specific logic.
//!
//! Each stage trait is defined once in [`traits`]; concrete implementations
//! live in their respective submodule. New implementations can be added
//! without modifying the infrastructure — just implement the trait and
//! register the variant in [`config`].
//!
//! # Quick start
//!
//! ```
//! 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);
//! let result = pipeline.evaluate(Semantics::Preferred).unwrap();
//! ```

pub mod attack;
pub mod config;
pub mod construction;
pub mod evaluation;
pub mod grounding;
pub mod traits;

pub use traits::*;

use crate::error::{AspicError, PipelineStage};
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::ordering::ArgumentOrdering;
use crate::system::AspicSystem;

use crate::pipeline::config::PipelineConfig;
use crate::system::ordering::SetPreference;

/// The full ASPIC+ pipeline: Grounder → `ArgumentConstructor` → `AttackComputer` → Evaluator.
pub struct AspicPipeline {
    /// The ASPIC+ system being evaluated.
    pub system: AspicSystem,
    /// Stage 1: grounds first-order variables via Herbrand substitution.
    pub grounder: Box<dyn Grounder>,
    /// Stage 2: builds the set of all derivable ASPIC+ arguments.
    pub arg_constructor: Box<dyn ArgumentConstructor>,
    /// Stage 3: identifies rebut, undermine, and undercut attacks.
    pub attack_computer: Box<dyn AttackComputer>,
    /// Stage 4: computes defeats, builds the abstract framework, and solves for extensions.
    pub evaluator: Box<dyn Evaluator>,
    /// The preference ordering used for defeat computation, surfaced here for
    /// introspection and declarative configuration.
    pub preference: PreferenceConfig,
}

/// The result of a full pipeline evaluation.
///
/// Contains the grounded system, constructed arguments, raw attacks,
/// and the computed extensions and labellings. Use the [`store`](Self::store)
/// field to look up argument details by [`ArgumentId`](crate::framework::argument::ArgumentId).
///
/// # 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);
/// let result = pipeline.evaluate(Semantics::Grounded).unwrap();
///
/// // Inspect the grounded extension's conclusions.
/// for &arg_id in &result.extensions[0] {
///     let arg = result.store.get(arg_id).unwrap();
///     println!("{}", arg.conclusion());
/// }
/// ```
#[derive(Clone, Debug)]
pub struct PipelineResult {
    /// The system after grounding (all variables eliminated).
    pub grounded_system: GroundedSystem,
    /// The constructed ASPIC+ arguments.
    pub store: ArgumentStore,
    /// Raw attacks identified between arguments (before preference filtering).
    pub attacks: Vec<Attack>,
    /// Argument labellings produced by the semantics solver.
    pub labellings: Vec<Labelling>,
    /// Extensions computed under the chosen semantics.
    pub extensions: Vec<Extension>,
}

impl AspicPipeline {
    /// Convenience constructor for the standard classical pipeline with
    /// naive implementations at every stage. Delegates to
    /// [`PipelineConfig::classical`].
    ///
    /// # 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);
    /// let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    /// assert!(!result.extensions.is_empty());
    /// ```
    pub fn classical(system: AspicSystem, ordering: Box<dyn ArgumentOrdering>) -> Self {
        PipelineConfig::classical().build(system, PreferenceConfig::ArgumentOrdering(ordering))
    }

    /// Convenience constructor for an optimised pipeline that uses:
    /// - Indexed attack computation (hash-lookup instead of O(n^2) pairwise)
    /// - SCC-decomposing solver wrapping a SAT solver (`BatSat` backend)
    ///
    /// For a different SAT backend, construct the pipeline manually with
    /// `SatSolver::<YourSolver>::default()`.
    ///
    /// Requires the `sat` feature. Delegates to [`PipelineConfig::optimised`].
    ///
    /// # 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::optimised(system, ordering);
    /// let result = pipeline.evaluate(Semantics::Preferred).unwrap();
    /// assert!(!result.extensions.is_empty());
    /// ```
    #[cfg(feature = "sat")]
    pub fn optimised(system: AspicSystem, ordering: Box<dyn ArgumentOrdering>) -> Self {
        PipelineConfig::optimised().build(system, PreferenceConfig::ArgumentOrdering(ordering))
    }

    /// Convenience constructor for the accrual pipeline (Prakken 2019).
    ///
    /// Uses `AccrualEvaluator` with the provided `SetPreference`.
    /// Delegates to [`PipelineConfig::accrual`].
    ///
    /// # 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 arg_ordering: Box<dyn ArgumentOrdering> = Box::new(FlatOrdering);
    /// let set_pref: Box<dyn SetPreference> = Box::new(LiftedSetPreference {
    ///     base: arg_ordering,
    ///     lifting: LiftingStrategy::Elitist,
    /// });
    /// let pipeline = AspicPipeline::accrual(system, set_pref);
    /// let result = pipeline.evaluate(Semantics::Grounded).unwrap();
    /// assert!(!result.extensions.is_empty());
    /// ```
    pub fn accrual(system: AspicSystem, set_preference: Box<dyn SetPreference>) -> Self {
        PipelineConfig::accrual().build(system, PreferenceConfig::SetPreference(set_preference))
    }

    /// Run only the grounding stage.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if grounding fails (e.g. the system is malformed).
    pub fn ground(&self) -> Result<GroundedSystem, AspicError> {
        self.grounder.ground(&self.system)
    }

    /// Run only the argument construction stage on a pre-grounded system.
    pub fn construct(&self, grounded_system: &GroundedSystem) -> ArgumentStore {
        self.arg_constructor.construct(grounded_system)
    }

    /// Run only the attack computation stage.
    pub fn compute_attacks(
        &self,
        store: &ArgumentStore,
        contrariness: &crate::system::contrariness::ContrarinessFunction,
    ) -> Vec<Attack> {
        self.attack_computer.compute(store, contrariness)
    }

    /// Run the full pipeline end-to-end.
    ///
    /// Errors are wrapped with [`PipelineStage`] context so callers can
    /// identify which stage failed.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if grounding or evaluation fails; the error
    /// records which [`PipelineStage`] failed.
    pub fn evaluate(&self, semantics: Semantics) -> Result<PipelineResult, AspicError> {
        let (grounded_system, store, attacks) = self.run_stages()?;

        let eval = self
            .evaluator
            .evaluate(&store, &attacks, semantics, &self.preference)
            .map_err(|e| e.in_stage(PipelineStage::Evaluation))?;

        Ok(PipelineResult {
            grounded_system,
            store,
            attacks,
            labellings: eval.labellings,
            extensions: eval.extensions,
        })
    }

    /// Run the full pipeline but return at most one extension.
    ///
    /// Identical to [`evaluate`](Self::evaluate) except the evaluation stage
    /// calls [`Evaluator::find_one`] instead of [`Evaluator::evaluate`].
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if grounding or evaluation fails; the error
    /// records which [`PipelineStage`] failed.
    pub fn find_one(&self, semantics: Semantics) -> Result<PipelineResult, AspicError> {
        let (grounded_system, store, attacks) = self.run_stages()?;

        let eval = self
            .evaluator
            .find_one(&store, &attacks, semantics, &self.preference)
            .map_err(|e| e.in_stage(PipelineStage::Evaluation))?;

        Ok(PipelineResult {
            grounded_system,
            store,
            attacks,
            labellings: eval.labellings,
            extensions: eval.extensions,
        })
    }

    /// Run the full pipeline and return only the extension count.
    ///
    /// Runs the same grounding, construction, and attack stages as
    /// [`evaluate`](Self::evaluate), but calls [`Evaluator::count`] to
    /// avoid materialising extension sets.
    ///
    /// # Errors
    ///
    /// Returns [`AspicError`] if grounding or evaluation fails; the error
    /// records which [`PipelineStage`] failed.
    pub fn count(&self, semantics: Semantics) -> Result<usize, AspicError> {
        let (_grounded_system, store, attacks) = self.run_stages()?;

        self.evaluator
            .count(&store, &attacks, semantics, &self.preference)
            .map_err(|e| e.in_stage(PipelineStage::Evaluation))
    }

    fn run_stages(&self) -> Result<(GroundedSystem, ArgumentStore, Vec<Attack>), AspicError> {
        let grounded_system = self
            .ground()
            .map_err(|e| e.in_stage(PipelineStage::Grounding))?;
        let store = self.construct(&grounded_system);
        let attacks = self.compute_attacks(&store, &grounded_system.contrariness);
        Ok((grounded_system, store, attacks))
    }
}
