//! The ASPIC+ argumentation system definition.
//!
//! This module contains the pre-grounding representation of an ASPIC+
//! argumentation system (AS, K) as defined in Modgil & Prakken (2014).
//! An argumentation system comprises:
//!
//! - A **knowledge base** ([`knowledge::KnowledgeBase`]) of axiom and ordinary premises.
//! - **Strict rules** ([`rules::StrictRule`]) that produce certain inferences.
//! - **Defeasible rules** ([`rules::DefeasibleRule`]) that produce tentative inferences.
//! - A **contrariness function** ([`contrariness::ContrarinessFunction`]) defining
//!   contrary and contradictory relations between formulae.
//!
//! Use [`builder::AspicSystemBuilder`] to construct an [`AspicSystem`] with
//! automatic well-definedness checks (axiom consistency, transposition closure,
//! and contrary well-formedness).
//!
//! # Sub-modules
//!
//! | Module | Purpose |
//! |---|---|
//! | [`builder`] | Fluent builder with build-time validation |
//! | [`consistency`] | Strict closure, direct/indirect consistency (Definition 3.4) |
//! | [`contrariness`] | Contrary and contradictory relations (Definition 5.1) |
//! | [`knowledge`] | Knowledge base, premises, and premise kinds |
//! | [`ordering`] | Preference orderings over rules, premises, arguments, and sets |
//! | [`postulates`] | Rationality postulate checks (Caminada & Amgoud 2007) |
//! | [`rules`] | Strict and defeasible inference rules |
//! | [`warning`] | Well-definedness warnings emitted at build time |

pub mod builder;
pub mod consistency;
pub mod contrariness;
pub mod knowledge;
pub mod ordering;
pub mod postulates;
pub mod rules;
pub mod warning;

use std::collections::BTreeSet;

use crate::language::formula::Formula;
use crate::system::contrariness::ContrarinessFunction;
use crate::system::knowledge::KnowledgeBase;
use crate::system::rules::{DefeasibleRule, StrictRule};

/// An ASPIC+ argumentation system (pre-grounding).
///
/// This is the top-level container for a complete ASPIC+ specification before
/// grounding. It holds the knowledge base K = (Kn, Kp), strict rules Rs,
/// defeasible rules Rd, and the contrariness function.
///
/// Construct via [`builder::AspicSystemBuilder`] to obtain well-definedness
/// [`warning::Warning`]s automatically.
#[derive(Clone, Debug)]
pub struct AspicSystem {
    /// The knowledge base K = (Kn, Kp) containing axiom and ordinary premises.
    pub knowledge_base: KnowledgeBase,
    /// Strict inference rules (→): certain, non-defeasible inferences.
    pub strict_rules: Vec<StrictRule>,
    /// Defeasible inference rules (⇒): tentative, attackable inferences.
    pub defeasible_rules: Vec<DefeasibleRule>,
    /// Maps formulae to their contraries and contradictories.
    pub contrariness: ContrarinessFunction,
}

impl AspicSystem {
    /// Collect all constants appearing anywhere in the system.
    ///
    /// Scans premises, rule antecedents, rule consequents, and defeasible rule
    /// names for ground constants. If no constants are found, returns
    /// `{"_default"}` so that grounding always has at least one constant to
    /// substitute.
    pub fn collect_constants(&self) -> BTreeSet<String> {
        let premise_formulae = self.knowledge_base.premises.iter().map(|p| &p.formula);

        let strict_formulae = self
            .strict_rules
            .iter()
            .flat_map(|r| r.antecedents.iter().chain(std::iter::once(&r.consequent)));

        let defeasible_formulae = self.defeasible_rules.iter().flat_map(|r| {
            r.antecedents
                .iter()
                .chain(std::iter::once(&r.consequent))
                .chain(r.name.iter())
        });

        let all_formulae: Box<dyn Iterator<Item = &Formula>> = Box::new(
            premise_formulae
                .chain(strict_formulae)
                .chain(defeasible_formulae),
        );

        let mut constants: BTreeSet<String> = all_formulae
            .flat_map(|f| f.constants().into_iter().cloned())
            .collect();

        if constants.is_empty() {
            constants.insert("_default".to_string());
        }

        constants
    }
}
