//! Well-definedness warnings for argumentation theories.
//!
//! An argumentation theory AT = (AS, K) must satisfy certain well-definedness
//! conditions for the rationality postulates to hold (§4.2 of Modgil & Prakken,
//! 2014). The [`Warning`] enum represents violations detected at build time by
//! [`AspicSystemBuilder::build()`](super::builder::AspicSystemBuilder::build).
//!
//! # Checked conditions
//!
//! - **Axiom consistency**: Kn must be indirectly consistent (§4.2).
//! - **Closure under transposition** (Definition 4.2): for every strict rule
//!   φ₁, …, φₙ → ψ in Rs and every i = 1..n, the transposed rule
//!   φ₁, …, φᵢ₋₁, ¬ψ, φᵢ₊₁, …, φₙ → ¬φᵢ must also be in Rs.
//!
//! # Deferred conditions
//!
//! - **Closure under contraposition** (Definition 4.3) is a semantic property
//!   best checked post-grounding, potentially via SAT solving. It is not
//!   checked at build time.

use crate::language::formula::Formula;
use crate::system::rules::RuleId;

/// A well-definedness warning detected during
/// [`AspicSystemBuilder::build()`](super::builder::AspicSystemBuilder::build).
///
/// Warnings are informational — construction always succeeds. Inspect the
/// returned `Vec<Warning>` to determine whether the argumentation theory
/// satisfies the prerequisites for the rationality postulates.
#[derive(Debug, Clone)]
pub enum Warning {
    /// The axiom premises Kn are not indirectly consistent (§4.2).
    ///
    /// The strict closure Cl(Kn) contains a formula and one of its
    /// contraries, violating the prerequisite for the rationality
    /// postulates.
    AxiomInconsistency,

    /// A required transposition of a strict rule is absent from Rs
    /// (Definition 4.2).
    ///
    /// For strict rule with id `rule_id`, the transposition obtained by
    /// swapping antecedent at `antecedent_index` with the negated consequent
    /// is missing. The expected transposed rule would have the given
    /// antecedents and consequent.
    MissingTransposition {
        rule_id: RuleId,
        antecedent_index: usize,
        expected_antecedents: Vec<Formula>,
        expected_consequent: Formula,
    },

    /// The §5 well-formedness condition for contraries is violated
    /// (Modgil & Prakken 2013, §5).
    ///
    /// If φ is a contrary (asymmetric) of ψ, then ψ must not be an axiom
    /// premise or the consequent of a strict rule.
    ContraryWellFormedness {
        target: Formula,
        reason: ContraryWellFormednessReason,
    },
}

/// The specific reason a §5 well-formedness violation was detected.
#[derive(Debug, Clone)]
pub enum ContraryWellFormednessReason {
    /// The target formula is an axiom premise.
    TargetIsAxiom,
    /// The target formula is the consequent of a strict rule.
    TargetIsStrictConsequent,
}

impl std::fmt::Display for Warning {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        match self {
            Warning::AxiomInconsistency => {
                write!(
                    f,
                    "axiom premises (Kn) are not indirectly consistent — \
                     Cl(Kn) contains a formula and one of its contraries (§4.2)"
                )
            }
            Warning::MissingTransposition {
                rule_id,
                antecedent_index,
                expected_antecedents,
                expected_consequent,
            } => {
                let antes: Vec<String> = expected_antecedents
                    .iter()
                    .map(std::string::ToString::to_string)
                    .collect();
                write!(
                    f,
                    "strict rule `{rule_id}` is missing transposition at antecedent index \
                     {antecedent_index}: expected {antes} → {expected_consequent} in Rs \
                     (Definition 4.2)",
                    antes = antes.join(", "),
                )
            }
            Warning::ContraryWellFormedness { target, reason } => {
                let reason_str = match reason {
                    ContraryWellFormednessReason::TargetIsAxiom => "an axiom premise",
                    ContraryWellFormednessReason::TargetIsStrictConsequent => {
                        "the consequent of a strict rule"
                    }
                };
                write!(
                    f,
                    "§5 well-formedness violation: formula `{target}` is the target of a \
                     contrary relation but is {reason_str} (Modgil & Prakken 2013, §5)"
                )
            }
        }
    }
}
