//! Contrariness and contradictoriness relations between formulae.
//!
//! Implements Definition 5.1 of Modgil & Prakken (2014). The contrariness
//! function maps each formula to its contraries (asymmetric) and
//! contradictories (symmetric). An optional classical-negation mode
//! automatically treats φ and ¬φ as contradictory.

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

use crate::language::formula::{Formula, Term};
use crate::language::grounding::GroundingContext;

/// Whether a contrariness relation is asymmetric (contrary) or symmetric
/// (contradictory).
#[derive(Clone, Debug, Eq, PartialEq)]
pub enum ContrarinessRelation {
    /// Asymmetric: attacker attacks target, but not vice versa.
    Contrary,
    /// Symmetric: each attacks the other.
    Contradictory,
}

/// Maps formulae to their contraries and contradictories (Definition 5.1,
/// Modgil & Prakken 2014).
///
/// # Well-formedness condition
///
/// The ASPIC+ framework requires that if φ is a contrary of ψ, then ψ is
/// not an axiom premise and not the consequent of a strict rule (see §5
/// of the tutorial). This condition is **not enforced** by the library;
/// users must ensure it holds when constructing asymmetric contrary
/// relations. Violating it may produce semantically unsound results.
#[derive(Clone, Debug, Default)]
pub struct ContrarinessFunction {
    entries: HashMap<Formula, Vec<(Formula, ContrarinessRelation)>>,
    classical_negation: bool,
}

impl ContrarinessFunction {
    /// Create an empty contrariness function with no entries and classical
    /// negation disabled.
    pub fn new() -> Self {
        Self::default()
    }

    /// Declare that `attacker` is a contrary of `target`.
    /// Asymmetric: only `attacker` attacks `target`.
    pub fn add_contrary(&mut self, target: Formula, attacker: Formula) {
        self.entries
            .entry(target)
            .or_default()
            .push((attacker, ContrarinessRelation::Contrary));
    }

    /// Declare that `a` and `b` are contradictories.
    /// Symmetric: each attacks the other.
    pub fn add_contradictory(&mut self, a: Formula, b: Formula) {
        self.entries
            .entry(a.clone())
            .or_default()
            .push((b.clone(), ContrarinessRelation::Contradictory));
        self.entries
            .entry(b)
            .or_default()
            .push((a, ContrarinessRelation::Contradictory));
    }

    /// Retrieve all formulae that are contraries or contradictories of `phi`.
    pub fn contraries_of(&self, phi: &Formula) -> Vec<Formula> {
        let mut result = Vec::new();

        if let Some(entries) = self.entries.get(phi) {
            for (f, _) in entries {
                result.push(f.clone());
            }
        }

        if self.classical_negation {
            let negated = phi.classical_negation();
            if !result.contains(&negated) {
                result.push(negated);
            }
        }

        result
    }

    /// Check whether `attacker` is contrary to `target`.
    pub fn is_contrary(&self, target: &Formula, attacker: &Formula) -> bool {
        if let Some(entries) = self.entries.get(target) {
            if entries.iter().any(|(f, _)| f == attacker) {
                return true;
            }
        }

        if self.classical_negation {
            let negated = target.classical_negation();
            if *attacker == negated {
                return true;
            }
        }

        false
    }

    /// Enable classical-negation mode: φ and ¬φ are treated as contradictories.
    pub fn with_classical_negation(mut self) -> Self {
        self.classical_negation = true;
        self
    }

    /// Returns the specific [`ContrarinessRelation`] between two formulae, if one exists.
    ///
    /// Per Definition 5.1 (Modgil & Prakken 2014), distinguishing `Contrary`
    /// (asymmetric) from `Contradictory` (symmetric) is necessary for the defeat
    /// layer to determine whether an attack always succeeds regardless of
    /// preferences. Returns `None` if no contrariness relation is defined.
    pub fn relation_between(
        &self,
        target: &Formula,
        attacker: &Formula,
    ) -> Option<ContrarinessRelation> {
        if let Some(entries) = self.entries.get(target) {
            if let Some((_, relation)) = entries.iter().find(|(f, _)| f == attacker) {
                return Some(relation.clone());
            }
        }

        if self.classical_negation {
            let negated = target.classical_negation();
            if *attacker == negated {
                return Some(ContrarinessRelation::Contradictory);
            }
        }

        None
    }

    /// Check if classical negation mode is enabled.
    pub fn has_classical_negation(&self) -> bool {
        self.classical_negation
    }

    /// Ground any non-ground entries using the given context.
    ///
    /// Variables shared between target and attacker are coordinated: a single
    /// joint substitution is applied to both, mirroring how rule grounding
    /// works in `GroundingContext::ground_system`.
    pub(crate) fn ground(&mut self, ctx: &GroundingContext) {
        let old_entries: Vec<(Formula, Vec<(Formula, ContrarinessRelation)>)> =
            self.entries.drain().collect();

        let mut seen: HashSet<(Formula, Formula)> = HashSet::new();

        for (target, attackers) in old_entries {
            for (attacker, relation) in &attackers {
                let all_vars = collect_vars_from_pair(&target, attacker);
                if all_vars.is_empty() {
                    if seen.insert((target.clone(), attacker.clone())) {
                        self.entries
                            .entry(target.clone())
                            .or_default()
                            .push((attacker.clone(), relation.clone()));
                    }
                    continue;
                }
                let substitutions = ctx.all_substitutions(&all_vars);
                for subst in substitutions {
                    let mut gt = target.clone();
                    let mut ga = attacker.clone();
                    for (var, constant) in &subst {
                        let term = Term::Const(constant.clone());
                        gt = gt.substitute(var, &term);
                        ga = ga.substitute(var, &term);
                    }
                    if seen.insert((gt.clone(), ga.clone())) {
                        self.entries
                            .entry(gt)
                            .or_default()
                            .push((ga, relation.clone()));
                    }
                }
            }
        }
    }

    /// Provide read access to the raw entries (used for serialization).
    pub fn entries(&self) -> &HashMap<Formula, Vec<(Formula, ContrarinessRelation)>> {
        &self.entries
    }
}

/// Collect the deduplicated union of variables from two formulae,
/// preserving insertion order.
fn collect_vars_from_pair(a: &Formula, b: &Formula) -> Vec<String> {
    let mut seen = HashSet::new();
    let a_vars = a.variables();
    let b_vars = b.variables();
    a_vars
        .into_iter()
        .chain(b_vars)
        .filter(|v| seen.insert((*v).clone()))
        .cloned()
        .collect()
}
