//! Fluent builder for constructing [`AspicSystem`] instances with validation.
//!
//! The builder provides a chainable API for assembling the knowledge base,
//! rules, and contrariness function. On [`build()`](AspicSystemBuilder::build),
//! it runs well-definedness checks and returns any [`Warning`]s alongside the
//! constructed system.

use std::collections::HashSet;

use crate::language::formula::Formula;
use crate::system::consistency::is_indirectly_consistent;
use crate::system::contrariness::ContrarinessFunction;
use crate::system::contrariness::ContrarinessRelation;
use crate::system::knowledge::{KnowledgeBase, Premise, PremiseKind};
use crate::system::rules::{DefeasibleRule, RuleId, StrictRule};
use crate::system::warning::{ContraryWellFormednessReason, Warning};
use crate::system::AspicSystem;

/// A fluent builder for constructing an [`AspicSystem`].
///
/// # Example
///
/// ```
/// use pickaxe_rs::formula;
/// use pickaxe_rs::prelude::*;
///
/// let (system, warnings) = AspicSystemBuilder::new()
///     .axiom(formula!(p))
///     .ordinary_premise(formula!(q))
///     .defeasible_rule("d1", vec![formula!(p), formula!(q)], formula!(r))
///     .with_classical_negation()
///     .build();
///
/// assert!(warnings.is_empty());
/// ```
pub struct AspicSystemBuilder {
    kb: KnowledgeBase,
    strict_rules: Vec<StrictRule>,
    defeasible_rules: Vec<DefeasibleRule>,
    contrariness: ContrarinessFunction,
}

impl AspicSystemBuilder {
    /// Create a new, empty builder with no premises, rules, or contrariness
    /// relations.
    pub fn new() -> Self {
        AspicSystemBuilder {
            kb: KnowledgeBase::default(),
            strict_rules: Vec::new(),
            defeasible_rules: Vec::new(),
            contrariness: ContrarinessFunction::new(),
        }
    }

    /// Add an axiom premise (Kn) — cannot be attacked.
    pub fn axiom(mut self, formula: Formula) -> Self {
        self.kb.premises.push(Premise {
            formula,
            kind: PremiseKind::Axiom,
        });
        self
    }

    /// Add an ordinary premise (Kp) — can be attacked via undermining.
    pub fn ordinary_premise(mut self, formula: Formula) -> Self {
        self.kb.premises.push(Premise {
            formula,
            kind: PremiseKind::Ordinary,
        });
        self
    }

    /// Add a strict rule: antecedents → consequent.
    pub fn strict_rule(
        mut self,
        id: impl Into<String>,
        antecedents: Vec<Formula>,
        consequent: Formula,
    ) -> Self {
        self.strict_rules.push(StrictRule {
            id: RuleId(id.into()),
            antecedents,
            consequent,
        });
        self
    }

    /// Add an unnamed defeasible rule: antecedents ⇒ consequent.
    pub fn defeasible_rule(
        mut self,
        id: impl Into<String>,
        antecedents: Vec<Formula>,
        consequent: Formula,
    ) -> Self {
        self.defeasible_rules.push(DefeasibleRule {
            id: RuleId(id.into()),
            antecedents,
            consequent,
            name: None,
        });
        self
    }

    /// Add a named defeasible rule: antecedents ⇒ consequent with a name
    /// formula that can be the target of an undercut attack.
    pub fn named_defeasible_rule(
        mut self,
        id: impl Into<String>,
        name: Formula,
        antecedents: Vec<Formula>,
        consequent: Formula,
    ) -> Self {
        self.defeasible_rules.push(DefeasibleRule {
            id: RuleId(id.into()),
            antecedents,
            consequent,
            name: Some(name),
        });
        self
    }

    /// Declare an asymmetric contrary: `attacker` is a contrary of `target`.
    pub fn contrary(mut self, target: Formula, attacker: Formula) -> Self {
        self.contrariness.add_contrary(target, attacker);
        self
    }

    /// Declare a symmetric contradictory relation between `a` and `b`.
    pub fn contradictory(mut self, a: Formula, b: Formula) -> Self {
        self.contrariness.add_contradictory(a, b);
        self
    }

    /// Enable classical-negation mode: φ and ¬φ are automatically contradictory.
    pub fn with_classical_negation(mut self) -> Self {
        self.contrariness = self.contrariness.with_classical_negation();
        self
    }

    /// Consume the builder and produce an [`AspicSystem`] along with any
    /// well-definedness [`Warning`]s.
    ///
    /// Checks performed:
    /// - Axiom consistency (§4.2): Kn must be indirectly consistent.
    /// - Closure under transposition (Definition 4.2).
    /// - Contrary well-formedness (§5): contrary targets must not be axioms
    ///   or strict-rule consequents.
    pub fn build(self) -> (AspicSystem, Vec<Warning>) {
        let mut warnings = Vec::new();

        let system = AspicSystem {
            knowledge_base: self.kb,
            strict_rules: self.strict_rules,
            defeasible_rules: self.defeasible_rules,
            contrariness: self.contrariness,
        };

        // FR-020: Check axiom consistency (§4.2)
        let axiom_formulae: HashSet<Formula> = system
            .knowledge_base
            .premises
            .iter()
            .filter(|p| p.kind == PremiseKind::Axiom)
            .map(|p| p.formula.clone())
            .collect();

        if !axiom_formulae.is_empty()
            && !is_indirectly_consistent(
                &axiom_formulae,
                &system.strict_rules,
                &system.contrariness,
            )
        {
            warnings.push(Warning::AxiomInconsistency);
        }

        // FR-021: Check closure under transposition (Definition 4.2)
        check_transposition_closure(&system.strict_rules, &mut warnings);

        // §5 well-formedness: if φ is a contrary of ψ, then ψ must not be
        // an axiom premise or the consequent of a strict rule.
        check_contrary_well_formedness(&system, &mut warnings);

        (system, warnings)
    }
}

impl Default for AspicSystemBuilder {
    fn default() -> Self {
        Self::new()
    }
}

/// Check closure under transposition (Definition 4.2) for strict rules.
///
/// For each strict rule φ₁, …, φₙ → ψ and each antecedent index i,
/// verifies that the transposed rule
///   φ₁, …, φᵢ₋₁, ¬ψ, φᵢ₊₁, …, φₙ → ¬φᵢ
/// exists in `strict_rules`. Antecedent comparison is order-independent
/// (set equality via sorted canonical form).
pub fn check_transposition_closure(strict_rules: &[StrictRule], warnings: &mut Vec<Warning>) {
    let rule_signatures: HashSet<(Vec<Formula>, Formula)> = strict_rules
        .iter()
        .map(|r| {
            let mut sorted = r.antecedents.clone();
            sorted.sort();
            (sorted, r.consequent.clone())
        })
        .collect();

    for rule in strict_rules {
        for (i, antecedent_i) in rule.antecedents.iter().enumerate() {
            let mut transposed_antes: Vec<Formula> = rule
                .antecedents
                .iter()
                .enumerate()
                .filter(|(j, _)| *j != i)
                .map(|(_, a)| a.clone())
                .collect();
            transposed_antes.push(rule.consequent.classical_negation());
            transposed_antes.sort();

            let transposed_consequent = antecedent_i.classical_negation();

            if !rule_signatures.contains(&(transposed_antes.clone(), transposed_consequent.clone()))
            {
                warnings.push(Warning::MissingTransposition {
                    rule_id: rule.id.clone(),
                    antecedent_index: i,
                    expected_antecedents: transposed_antes,
                    expected_consequent: transposed_consequent,
                });
            }
        }
    }
}

/// Check §5 well-formedness for contraries (Modgil & Prakken 2013, §5).
///
/// For each contrary (asymmetric) relation where some attacker targets ψ,
/// ψ must not be an axiom premise or the consequent of a strict rule.
fn check_contrary_well_formedness(system: &AspicSystem, warnings: &mut Vec<Warning>) {
    let axiom_formulae: HashSet<&Formula> = system
        .knowledge_base
        .premises
        .iter()
        .filter(|p| p.kind == PremiseKind::Axiom)
        .map(|p| &p.formula)
        .collect();

    let strict_consequents: HashSet<&Formula> =
        system.strict_rules.iter().map(|r| &r.consequent).collect();

    for (target, attackers) in system.contrariness.entries() {
        let has_contrary = attackers
            .iter()
            .any(|(_, rel)| *rel == ContrarinessRelation::Contrary);
        if !has_contrary {
            continue;
        }

        if axiom_formulae.contains(target) {
            warnings.push(Warning::ContraryWellFormedness {
                target: target.clone(),
                reason: ContraryWellFormednessReason::TargetIsAxiom,
            });
        }
        if strict_consequents.contains(target) {
            warnings.push(Warning::ContraryWellFormedness {
                target: target.clone(),
                reason: ContraryWellFormednessReason::TargetIsStrictConsequent,
            });
        }
    }
}
