//! Property-based and deterministic tests for the ASPIC+ rationality postulates.
//!
//! Verifies that well-defined argumentation theories satisfy all four
//! rationality postulates, reproduces literature examples of postulate
//! violation and restoration, and tests the contraposition closure check.
//!
//! References: Caminada & Amgoud (2007); Modgil & Prakken (2014) §4.2,
//! Examples 4.1 and 4.4; Definition 4.3.

mod common;

use std::collections::HashSet;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;
use pickaxe_rs::system::consistency::check_contraposition_closure;

use common::{last_link, EqualOrdering};
use proptest::prelude::*;

// --- Property test: postulates hold on well-defined ATs ---

/// Generate a set of strict rules closed under transposition by construction.
/// For each base rule, adds all its transpositions.
fn close_under_transposition(
    base_rules: Vec<(Vec<Formula>, Formula)>,
) -> Vec<(String, Vec<Formula>, Formula)> {
    let mut result: Vec<(String, Vec<Formula>, Formula)> = Vec::new();
    let mut id_counter = 0u32;

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

    for (antecedents, consequent) in &base_rules {
        let mut sorted = antecedents.clone();
        sorted.sort();
        signatures.insert((sorted, consequent.clone()));
    }

    for (antecedents, consequent) in &base_rules {
        let mut sorted = antecedents.clone();
        sorted.sort();
        if signatures.contains(&(sorted.clone(), consequent.clone())) {
            let id = format!("s{id_counter}");
            id_counter += 1;
            result.push((id, antecedents.clone(), consequent.clone()));
        }

        for i in 0..antecedents.len() {
            let mut transposed: Vec<Formula> = antecedents
                .iter()
                .enumerate()
                .filter(|(j, _)| *j != i)
                .map(|(_, a)| a.clone())
                .collect();
            transposed.push(consequent.classical_negation());
            transposed.sort();
            let transposed_consequent = antecedents[i].classical_negation();

            if signatures.insert((transposed.clone(), transposed_consequent.clone())) {
                let id = format!("s{id_counter}");
                id_counter += 1;
                result.push((id, transposed, transposed_consequent));
            }
        }
    }

    result
}

/// proptest strategy: generate a well-defined AT with a reasonable ordering.
fn arb_well_defined_at(
) -> impl Strategy<Value = (AspicSystem, Vec<Warning>, Box<dyn ArgumentOrdering>)> {
    let atom_count = 3..=5usize;
    let num_base_strict = 0..=2usize;
    let num_axioms = 1..=2usize;
    let num_ordinary = 1..=3usize;
    let num_defeasible = 1..=3usize;
    let use_last_link = proptest::bool::ANY;

    (
        atom_count,
        num_base_strict,
        num_axioms,
        num_ordinary,
        num_defeasible,
        use_last_link,
    )
        .prop_flat_map(|(n_atoms, n_strict, n_ax, n_ord, n_def, last)| {
            let atoms: Vec<Formula> = (0..n_atoms)
                .map(|i| {
                    let name = format!("p{i}");
                    Formula::Lit(pickaxe_rs::language::formula::Literal::Pos(
                        pickaxe_rs::language::formula::Atom {
                            predicate: name,
                            terms: vec![],
                        },
                    ))
                })
                .collect();

            let all_formulae: Vec<Formula> = atoms
                .iter()
                .flat_map(|a| vec![a.clone(), a.classical_negation()])
                .collect();
            let n_all = all_formulae.len();

            let strict_rules_strat = proptest::collection::vec(
                (
                    proptest::sample::subsequence((0..n_all).collect::<Vec<_>>(), 1..=2),
                    (0..n_all),
                ),
                0..=n_strict,
            );

            let axiom_indices = proptest::sample::subsequence(
                (0..n_atoms).collect::<Vec<_>>(),
                1..=n_ax.min(n_atoms),
            );

            let ordinary_indices = proptest::sample::subsequence(
                (0..n_atoms).collect::<Vec<_>>(),
                1..=n_ord.min(n_atoms),
            );

            let def_rules_strat = proptest::collection::vec(
                (
                    proptest::sample::subsequence((0..n_all).collect::<Vec<_>>(), 1..=2),
                    (0..n_all),
                ),
                1..=n_def,
            );

            let rule_perm = proptest::collection::vec(0..10u32, 0..=5);
            let prem_perm = proptest::collection::vec(0..10u32, 0..=5);

            (
                Just(all_formulae),
                Just(atoms),
                strict_rules_strat,
                axiom_indices,
                ordinary_indices,
                def_rules_strat,
                Just(last),
                rule_perm,
                prem_perm,
            )
        })
        .prop_filter_map(
            "well-defined AT",
            |(
                all_formulae,
                atoms,
                strict_raw,
                ax_idx,
                ord_idx,
                def_raw,
                use_last,
                _rule_perm,
                _prem_perm,
            )| {
                let base_strict: Vec<(Vec<Formula>, Formula)> = strict_raw
                    .into_iter()
                    .filter_map(|(ante_idx, cons_idx)| {
                        let antes: Vec<Formula> =
                            ante_idx.iter().map(|&i| all_formulae[i].clone()).collect();
                        let cons = all_formulae.get(cons_idx)?.clone();
                        if antes.contains(&cons) {
                            return None;
                        }
                        Some((antes, cons))
                    })
                    .collect();

                let closed_strict = close_under_transposition(base_strict);

                let mut builder = AspicSystemBuilder::new().with_classical_negation();

                for &i in &ax_idx {
                    builder = builder.axiom(atoms[i].clone());
                }
                for &i in &ord_idx {
                    builder = builder.ordinary_premise(atoms[i].clone());
                }
                for (id, antes, cons) in &closed_strict {
                    builder = builder.strict_rule(id.as_str(), antes.clone(), cons.clone());
                }

                let mut def_id = 0u32;
                let mut def_rule_ids = Vec::new();
                for (ante_idx, cons_idx) in &def_raw {
                    let antes: Vec<Formula> =
                        ante_idx.iter().map(|&i| all_formulae[i].clone()).collect();
                    if let Some(cons) = all_formulae.get(*cons_idx) {
                        if antes.contains(cons) {
                            continue;
                        }
                        let id = format!("d{def_id}");
                        let name_formula =
                            Formula::Lit(pickaxe_rs::language::formula::Literal::Pos(
                                pickaxe_rs::language::formula::Atom {
                                    predicate: id.clone(),
                                    terms: vec![],
                                },
                            ));
                        builder =
                            builder.named_defeasible_rule(&id, name_formula, antes, cons.clone());
                        def_rule_ids.push(RuleId(id));
                        def_id += 1;
                    }
                }

                if def_rule_ids.is_empty() {
                    return None;
                }

                let (system, warnings) = builder.build();

                let has_axiom_inconsistency = warnings
                    .iter()
                    .any(|w| matches!(w, Warning::AxiomInconsistency));
                let has_missing_transposition = warnings
                    .iter()
                    .any(|w| matches!(w, Warning::MissingTransposition { .. }));
                if has_axiom_inconsistency || has_missing_transposition {
                    return None;
                }

                let ordering: Box<dyn ArgumentOrdering> = if use_last {
                    Box::new(LastLinkOrdering {
                        rule_ordering: Box::new(TieredOrdering::new(
                            def_rule_ids.iter().map(|r| vec![r.clone()]).collect(),
                        )),
                        premise_ordering: Box::new(NoPreference),
                        lifting: LiftingStrategy::Elitist,
                    })
                } else {
                    Box::new(WeakestLinkOrdering {
                        rule_ordering: Box::new(TieredOrdering::new(
                            def_rule_ids.iter().map(|r| vec![r.clone()]).collect(),
                        )),
                        premise_ordering: Box::new(NoPreference),
                        lifting: LiftingStrategy::Elitist,
                    })
                };

                Some((system, warnings, ordering))
            },
        )
}

proptest! {
    #![proptest_config(ProptestConfig::with_cases(64))]

    /// For any well-defined AT with a reasonable ordering, all four
    /// rationality postulates hold on every complete extension.
    ///
    /// References: Caminada & Amgoud (2007); Modgil & Prakken (2014) §4.2,
    /// Theorem 4.1.
    #[test]
    fn postulate_satisfaction(
        (system, _warnings, ordering) in arb_well_defined_at()
    ) {
        let pipeline = AspicPipeline::classical(
            system.clone(),
            ordering,
        );
        let result = pipeline.evaluate(Semantics::Complete).unwrap();
        let store = &result.store;

        for ext in &result.extensions {
            prop_assert!(
                check_sub_argument_closure(ext, store),
                "sub-argument closure violated"
            );
            prop_assert!(
                check_strict_closure(ext, store, &result.grounded_system.strict_rules),
                "closure under strict rules violated"
            );
            prop_assert!(
                check_direct_consistency(ext, store, &result.grounded_system.contrariness),
                "direct consistency violated"
            );
            prop_assert!(
                check_indirect_consistency(
                    ext,
                    store,
                    &result.grounded_system.strict_rules,
                    &result.grounded_system.contrariness
                ),
                "indirect consistency violated"
            );
        }
    }
}

// --- Literature examples: postulate violation and restoration ---

// Example 4.1 — Bachelor/Married without transposition
//
// Kp = {WearsRing, PartyAnimal}
// Rd = {d1: WearsRing ⇒ Married, d2: PartyAnimal ⇒ Bachelor}
// Rs = {s1: Married → ¬Bachelor}  (s2 MISSING)
// Ordering: last-link with d1 < d2
//
// Expected: the unique complete extension contains arguments for both
// Bachelor and ¬Bachelor, violating direct consistency.
//
// Reference: Modgil & Prakken (2014), Example 4.1 and §4.2.
#[test]
fn bachelor_married_no_transposition() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(WearsRing))
        .ordinary_premise(formula!(PartyAnimal))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(WearsRing)],
            formula!(Married),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(PartyAnimal)],
            formula!(Bachelor),
        )
        .strict_rule("s1", vec![formula!(Married)], formula!(!Bachelor))
        .build();

    let ordering = last_link(
        vec![vec![RuleId("d2".into())], vec![RuleId("d1".into())]],
        vec![],
    );

    let pipeline = AspicPipeline::classical(system.clone(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Complete).unwrap();
    let store = &result.store;

    assert!(
        !result.extensions.is_empty(),
        "should have at least one complete extension"
    );

    let has_violation = result
        .extensions
        .iter()
        .any(|ext| !check_direct_consistency(ext, store, &result.grounded_system.contrariness));
    assert!(
        has_violation,
        "without transposition, at least one complete extension should violate direct consistency"
    );
}

// Example 4.1 — Bachelor/Married with transposition
//
// Kp = {WearsRing, PartyAnimal}
// Rd = {d1: WearsRing ⇒ Married, d2: PartyAnimal ⇒ Bachelor}
// Rs = {s1: Married → ¬Bachelor, s2: Bachelor → ¬Married}
// Ordering: last-link with d1 < d2
//
// Expected: all four postulates hold on every complete extension.
//
// Reference: Modgil & Prakken (2014), Example 4.1 and §4.2.
#[test]
fn bachelor_married_with_transposition() {
    let (system, warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .ordinary_premise(formula!(WearsRing))
        .ordinary_premise(formula!(PartyAnimal))
        .named_defeasible_rule(
            "d1",
            formula!(d1),
            vec![formula!(WearsRing)],
            formula!(Married),
        )
        .named_defeasible_rule(
            "d2",
            formula!(d2),
            vec![formula!(PartyAnimal)],
            formula!(Bachelor),
        )
        .strict_rule("s1", vec![formula!(Married)], formula!(!Bachelor))
        .strict_rule("s2", vec![formula!(Bachelor)], formula!(!Married))
        .build();

    assert!(
        !warnings
            .iter()
            .any(|w| matches!(w, Warning::MissingTransposition { .. })),
        "with both s1 and s2, no transposition warnings"
    );

    let ordering = last_link(
        vec![vec![RuleId("d2".into())], vec![RuleId("d1".into())]],
        vec![],
    );

    let pipeline = AspicPipeline::classical(system.clone(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Complete).unwrap();
    let store = &result.store;

    for ext in &result.extensions {
        assert!(
            check_sub_argument_closure(ext, store),
            "sub-argument closure should hold"
        );
        assert!(
            check_strict_closure(ext, store, &result.grounded_system.strict_rules),
            "closure under strict rules should hold"
        );
        assert!(
            check_direct_consistency(ext, store, &result.grounded_system.contrariness),
            "direct consistency should hold"
        );
        assert!(
            check_indirect_consistency(
                ext,
                store,
                &result.grounded_system.strict_rules,
                &result.grounded_system.contrariness
            ),
            "indirect consistency should hold"
        );
    }
}

// Example 3.7/4.4 — without transposition
//
// The running example from the tutorial (Scenario A ordering: d5 > d2 > d4,
// s > u,x). Without transposition of s2, C3 attacks B1 but doesn't defeat it
// (B1 is a premise, preferred), and B1 cannot rebut C3 (no rule s → ¬v).
// Both s and ¬s appear in the grounded extension.
//
// Reference: Modgil & Prakken (2014), Example 4.4 and §4.2.
#[test]
fn example_4_4_no_transposition() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(p))
        .ordinary_premise(formula!(s))
        .ordinary_premise(formula!(u))
        .ordinary_premise(formula!(x))
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .strict_rule("s2", vec![formula!(v)], formula!(!s))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(q))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(s)], formula!(t))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(t)], formula!(!d1))
        .named_defeasible_rule("d4", formula!(d4), vec![formula!(u)], formula!(v))
        .named_defeasible_rule(
            "d5",
            formula!(d5),
            vec![formula!(v), formula!(x)],
            formula!(!t),
        )
        .named_defeasible_rule("d6", formula!(d6), vec![formula!(s)], formula!(!p))
        .build();

    // Scenario A: d5 > d2 > d4, s > u > x
    // C3 undermines B1 but doesn't defeat it (B1 is preferred as premise).
    // B1 can't rebut C3 because there's no rule s → ¬v.
    let ordering = last_link(
        vec![
            vec![RuleId("d5".into())],
            vec![RuleId("d2".into())],
            vec![RuleId("d4".into())],
        ],
        vec![vec![formula!(s)], vec![formula!(u), formula!(x)]],
    );

    let pipeline = AspicPipeline::classical(system.clone(), Box::new(ordering));
    let result = pipeline.evaluate(Semantics::Complete).unwrap();
    let store = &result.store;

    let has_consistency_violation = result
        .extensions
        .iter()
        .any(|ext| !check_direct_consistency(ext, store, &result.grounded_system.contrariness));
    assert!(
        has_consistency_violation,
        "without transposition of s2, some complete extension should violate direct consistency"
    );
}

// Example 3.7/4.4 — with transposition
//
// Same AT but with transposition of s2 added: s2' = s → ¬v.
// Now B1 can be extended to rebut C2, restoring consistency.
//
// Reference: Modgil & Prakken (2014), Example 4.4 and §4.2.
#[test]
fn example_4_4_with_transposition() {
    let (system, warnings) = AspicSystemBuilder::new()
        .with_classical_negation()
        .axiom(formula!(p))
        .ordinary_premise(formula!(s))
        .ordinary_premise(formula!(u))
        .ordinary_premise(formula!(x))
        // s1: p, q → r  (1 antecedent to swap yields: ¬r, q → ¬p  and  ¬r, p → ¬q)
        .strict_rule("s1", vec![formula!(p), formula!(q)], formula!(r))
        .strict_rule("s1_t0", vec![formula!(!r), formula!(q)], formula!(!p))
        .strict_rule("s1_t1", vec![formula!(!r), formula!(p)], formula!(!q))
        // s2: v → ¬s  (transposition: s → ¬v)
        .strict_rule("s2", vec![formula!(v)], formula!(!s))
        .strict_rule("s2_t", vec![formula!(s)], formula!(!v))
        .named_defeasible_rule("d1", formula!(d1), vec![formula!(p)], formula!(q))
        .named_defeasible_rule("d2", formula!(d2), vec![formula!(s)], formula!(t))
        .named_defeasible_rule("d3", formula!(d3), vec![formula!(t)], formula!(!d1))
        .named_defeasible_rule("d4", formula!(d4), vec![formula!(u)], formula!(v))
        .named_defeasible_rule(
            "d5",
            formula!(d5),
            vec![formula!(v), formula!(x)],
            formula!(!t),
        )
        .named_defeasible_rule("d6", formula!(d6), vec![formula!(s)], formula!(!p))
        .build();

    let no_transposition_warning = !warnings
        .iter()
        .any(|w| matches!(w, Warning::MissingTransposition { .. }));
    assert!(
        no_transposition_warning,
        "with full transposition, no MissingTransposition warnings"
    );

    let pipeline = AspicPipeline::classical(system.clone(), Box::new(EqualOrdering));
    let result = pipeline.evaluate(Semantics::Complete).unwrap();
    let store = &result.store;

    for ext in &result.extensions {
        assert!(
            check_direct_consistency(ext, store, &result.grounded_system.contrariness),
            "with transposition, direct consistency should hold"
        );
        assert!(
            check_indirect_consistency(
                ext,
                store,
                &result.grounded_system.strict_rules,
                &result.grounded_system.contrariness
            ),
            "with transposition, indirect consistency should hold"
        );
    }
}

// --- Contraposition closure check ---

// No strict rules → vacuously closed under contraposition.
#[test]
fn contraposition_closure_empty_rules() {
    let language: HashSet<Formula> = [formula!(p), formula!(!p), formula!(q), formula!(!q)]
        .into_iter()
        .collect();
    let cf = ContrarinessFunction::new().with_classical_negation();

    assert!(
        check_contraposition_closure(&language, &[], &cf).unwrap(),
        "no strict rules → vacuously closed under contraposition"
    );
}

// Strict rules forming a complete classical logic fragment
// (closed under transposition) satisfy contraposition closure.
#[test]
fn contraposition_closure_classical_logic() {
    // p, q → r  with all transpositions:
    // ¬r, q → ¬p
    // ¬r, p → ¬q
    let rules = vec![
        StrictRule {
            id: RuleId("s1".into()),
            antecedents: vec![formula!(p), formula!(q)],
            consequent: formula!(r),
        },
        StrictRule {
            id: RuleId("s1_t0".into()),
            antecedents: vec![formula!(!r), formula!(q)],
            consequent: formula!(!p),
        },
        StrictRule {
            id: RuleId("s1_t1".into()),
            antecedents: vec![formula!(!r), formula!(p)],
            consequent: formula!(!q),
        },
    ];

    let language: HashSet<Formula> = [
        formula!(p),
        formula!(!p),
        formula!(q),
        formula!(!q),
        formula!(r),
        formula!(!r),
    ]
    .into_iter()
    .collect();

    let cf = ContrarinessFunction::new().with_classical_negation();

    assert!(
        check_contraposition_closure(&language, &rules, &cf).unwrap(),
        "rules closed under transposition should satisfy contraposition closure"
    );
}

// Modus ponens without modus tollens — not closed under contraposition.
#[test]
fn contraposition_closure_missing_modus_tollens() {
    // p, q → r  WITHOUT transpositions
    let rules = vec![StrictRule {
        id: RuleId("s1".into()),
        antecedents: vec![formula!(p), formula!(q)],
        consequent: formula!(r),
    }];

    let language: HashSet<Formula> = [
        formula!(p),
        formula!(!p),
        formula!(q),
        formula!(!q),
        formula!(r),
        formula!(!r),
    ]
    .into_iter()
    .collect();

    let cf = ContrarinessFunction::new().with_classical_negation();

    assert!(
        !check_contraposition_closure(&language, &rules, &cf).unwrap(),
        "without transpositions, contraposition closure should fail"
    );
}
