//! Rationality postulate checks for ASPIC+ extensions.
//!
//! Implements the four rationality postulates from Caminada & Amgoud (2007),
//! adapted for the generalised ASPIC+ framework per Modgil & Prakken (2014)
//! §4.2. These postulates hold on every complete extension of any well-defined
//! argumentation theory with a reasonable ordering:
//!
//! 1. **Sub-argument closure**: if A ∈ E then Sub(A) ⊆ E.
//! 2. **Closure under strict rules**: Concs(E) = Cl(Concs(E)).
//! 3. **Direct consistency**: Concs(E) is directly consistent.
//! 4. **Indirect consistency**: Cl(Concs(E)) is directly consistent.
//!
//! Well-definedness conditions (§4.2): axiom consistency, closure under
//! transposition (Definition 4.2) or contraposition (Definition 4.3), and
//! a reasonable ordering. See [`super::builder`] for build-time checks of
//! axiom consistency and transposition closure, and
//! [`super::consistency::check_contraposition_closure`] for the contraposition
//! alternative.
//!
//! # References
//!
//! - Caminada, M. & Amgoud, L. (2007). On the evaluation of argumentation
//!   formalisms. *Artificial Intelligence*, 171(5–6), 286–310.
//! - Modgil, S. & Prakken, H. (2014). The ASPIC+ framework for structured
//!   argumentation: a tutorial. *Argument & Computation*, 5(1), 31–62.

use std::collections::HashSet;

use crate::framework::argument_store::ArgumentStore;
use crate::framework::semantics::Extension;
use crate::language::formula::Formula;
use crate::system::consistency::{
    is_directly_consistent, is_indirectly_consistent, strict_closure,
};
use crate::system::contrariness::ContrarinessFunction;
use crate::system::rules::StrictRule;

/// Check sub-argument closure on extension E: for every argument A ∈ E,
/// all sub-arguments of A are also in E.
///
/// # References
///
/// Caminada & Amgoud (2007), adapted per §4.2 of Modgil & Prakken (2014):
/// "For any argument A in E, all sub-arguments of A are in E, i.e.
/// for all A ∈ E: if A' ∈ Sub(A) then A' ∈ E."
pub fn check_sub_argument_closure(extension: &Extension, store: &ArgumentStore) -> bool {
    for &arg_id in extension {
        if let Some(arg) = store.get(arg_id) {
            for sub_id in arg.sub_argument_ids(store) {
                if !extension.contains(&sub_id) {
                    return false;
                }
            }
        }
    }
    true
}

/// Check closure under strict rules on extension E:
/// Concs(E) = Cl(Concs(E)), where Concs(E) = {Conc(A) | A ∈ E}.
///
/// # References
///
/// Caminada & Amgoud (2007), adapted per §4.2 of Modgil & Prakken (2014):
/// "If E contains arguments with conclusions α₁, ..., αₙ, then any
/// arguments obtained by applying only strict inference rules to these
/// conclusions, are in E, i.e. {Conc(A)|A ∈ E} = Cl({Conc(A)|A ∈ E})."
pub fn check_strict_closure(
    extension: &Extension,
    store: &ArgumentStore,
    strict_rules: &[StrictRule],
) -> bool {
    let concs = conclusions_of(extension, store);
    let closure = strict_closure(&concs, strict_rules);
    concs == closure
}

/// Check direct consistency on extension E: no two conclusions in
/// Concs(E) are in conflict.
///
/// # References
///
/// Caminada & Amgoud (2007), adapted per §4.2 and §5 of Modgil &
/// Prakken (2014): "The conclusions of arguments in E are directly
/// consistent, i.e. {Conc(A)|A ∈ E} is consistent."
pub fn check_direct_consistency(
    extension: &Extension,
    store: &ArgumentStore,
    contrariness: &ContrarinessFunction,
) -> bool {
    let concs = conclusions_of(extension, store);
    is_directly_consistent(&concs, contrariness)
}

/// Check indirect consistency on extension E: Cl(Concs(E)) is directly
/// consistent.
///
/// # References
///
/// Caminada & Amgoud (2007), adapted per §4.2 of Modgil & Prakken
/// (2014): "The conclusions of arguments in E are indirectly consistent,
/// i.e. Cl({Conc(A)|A ∈ E}) is consistent."
pub fn check_indirect_consistency(
    extension: &Extension,
    store: &ArgumentStore,
    strict_rules: &[StrictRule],
    contrariness: &ContrarinessFunction,
) -> bool {
    let concs = conclusions_of(extension, store);
    is_indirectly_consistent(&concs, strict_rules, contrariness)
}

fn conclusions_of(extension: &Extension, store: &ArgumentStore) -> HashSet<Formula> {
    extension
        .iter()
        .filter_map(|id| store.get(*id))
        .map(|a| a.conclusion().clone())
        .collect()
}
