//! Inference rules for ASPIC+ systems.
//!
//! ASPIC+ distinguishes strict rules (→, certain inference) from defeasible
//! rules (⇒, tentative inference). Each rule has a unique [`RuleId`]. Defeasible
//! rules may optionally carry a *name* formula; asserting the contrary of a
//! rule's name constitutes an undercut attack (Definition 3.13, Modgil &
//! Prakken 2014).

use serde::{Deserialize, Serialize};
use std::fmt;

use crate::language::formula::Formula;

/// A unique identifier for a rule in the argumentation system.
///
/// Used to reference rules in orderings, attacks, and serialisation.
#[derive(Clone, Debug, Eq, Hash, PartialEq, Ord, PartialOrd, Serialize, Deserialize)]
pub struct RuleId(pub String);

impl fmt::Display for RuleId {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        write!(f, "{}", self.0)
    }
}

/// A strict rule: φ₁, …, φₙ → ψ.
///
/// Strict rules represent certain inference. An argument built entirely from
/// axioms and strict rules is *firm and strict* — it cannot be attacked via
/// rebuttal or undercut (only its ordinary-premise leaves may be undermined).
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
pub struct StrictRule {
    pub id: RuleId,
    pub antecedents: Vec<Formula>,
    pub consequent: Formula,
}

/// A defeasible rule: φ₁, …, φₙ ⇒ ψ.
///
/// Defeasible rules represent tentative inference. Arguments using defeasible
/// rules are subject to rebuttal (attacking the conclusion) and, if a [`name`]
/// is assigned, undercut (attacking the rule application itself).
///
/// [`name`]: DefeasibleRule::name
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
pub struct DefeasibleRule {
    pub id: RuleId,
    pub antecedents: Vec<Formula>,
    pub consequent: Formula,
    /// The name of this rule as a formula in the object language.
    ///
    /// When present, asserting the contrary of this name constitutes an
    /// undercut attack on any argument that applies this rule.
    pub name: Option<Formula>,
}

/// A rule that is either strict or defeasible.
///
/// This unified enum is used in contexts where both rule kinds are handled
/// uniformly (e.g. argument construction, attack computation).
#[derive(Clone, Debug, Eq, PartialEq, Hash)]
pub enum Rule {
    Strict(StrictRule),
    Defeasible(DefeasibleRule),
}

impl Rule {
    /// The unique identifier of this rule.
    pub fn id(&self) -> &RuleId {
        match self {
            Rule::Strict(r) => &r.id,
            Rule::Defeasible(r) => &r.id,
        }
    }

    /// The antecedent formulae (premises) of this rule.
    pub fn antecedents(&self) -> &[Formula] {
        match self {
            Rule::Strict(r) => &r.antecedents,
            Rule::Defeasible(r) => &r.antecedents,
        }
    }

    /// The consequent formula (conclusion) derived by this rule.
    pub fn consequent(&self) -> &Formula {
        match self {
            Rule::Strict(r) => &r.consequent,
            Rule::Defeasible(r) => &r.consequent,
        }
    }

    /// Returns `true` if this is a strict rule (→).
    pub fn is_strict(&self) -> bool {
        matches!(self, Rule::Strict(_))
    }

    /// Returns `true` if this is a defeasible rule (⇒).
    pub fn is_defeasible(&self) -> bool {
        matches!(self, Rule::Defeasible(_))
    }
}
