use std::collections::HashSet;

use pickaxe_rs::formula;
use pickaxe_rs::prelude::*;

/// Strict rules forming a cycle (a → b, b → a) do not produce infinite
/// arguments because forward chaining terminates once no new conclusions
/// are derived. This test documents that such cycles are handled safely
/// (albeit without explicit cycle detection).
#[test]
fn strict_cycle_terminates_safely() {
    let (system, _) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(a))
        .strict_rule("s1", vec![formula!(a)], formula!(b))
        .strict_rule("s2", vec![formula!(b)], formula!(a))
        .build();
    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).expect("grounding should not hang");
    let store = ForwardChainingConstructor.construct(&grounded);

    let conclusions: HashSet<_> = store
        .all_arguments()
        .map(|(_, a)| a.conclusion().clone())
        .collect();
    assert!(conclusions.contains(&formula!(a)));
    assert!(conclusions.contains(&formula!(b)));
}

/// Test that grounding instantiates variables with all constants.
#[test]
fn grounding_single_variable() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(bird(polly)))
        .defeasible_rule("d1", vec![formula!(bird(X))], formula!(flies(X)))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    // Should have 2 premise instances (already ground)
    assert_eq!(grounded.knowledge_base.premises.len(), 2);

    // Should have 2 grounded defeasible rules: one for tweety, one for polly
    assert_eq!(grounded.defeasible_rules.len(), 2);

    let consequents: Vec<&Formula> = grounded
        .defeasible_rules
        .iter()
        .map(|r| &r.consequent)
        .collect();
    assert!(consequents.contains(&&formula!(flies(tweety))));
    assert!(consequents.contains(&&formula!(flies(polly))));
}

/// Test that grounding with multiple variables produces the Cartesian product.
#[test]
fn grounding_multiple_variables() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(likes(a, b)))
        .strict_rule("s1", vec![formula!(likes(X, Y))], formula!(friend(X, Y)))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    // 2 constants, 2 variables => 2^2 = 4 ground rules
    assert_eq!(grounded.strict_rules.len(), 4);
}

/// Ground formulae (no variables) pass through unchanged — rules, premises,
/// contrariness, and RuleIds are all preserved without suffix.
#[test]
fn grounding_already_ground() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(sunny))
        .strict_rule("s1", vec![formula!(sunny)], formula!(hot))
        .defeasible_rule("d1", vec![formula!(sunny)], formula!(warm))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    assert_eq!(grounded.knowledge_base.premises.len(), 1);

    assert_eq!(grounded.strict_rules.len(), 1);
    assert_eq!(grounded.strict_rules[0].consequent, formula!(hot));
    assert_eq!(grounded.strict_rules[0].id, RuleId("s1".into()));

    assert_eq!(grounded.defeasible_rules.len(), 1);
    assert_eq!(grounded.defeasible_rules[0].consequent, formula!(warm));
    assert_eq!(grounded.defeasible_rules[0].id, RuleId("d1".into()));
}

/// Test formula substitution.
#[test]
fn formula_substitution() {
    let f = formula!(bird(X));
    let result = f.substitute("X", &Term::Const("tweety".into()));
    assert_eq!(result, formula!(bird(tweety)));
}

/// Test is_ground.
#[test]
fn formula_is_ground() {
    assert!(formula!(bird(tweety)).is_ground());
    assert!(!formula!(bird(X)).is_ground());
    assert!(formula!(sunny).is_ground());
}

/// Test that contrariness grounding with shared variables produces joint
/// substitutions, not the Cartesian product of independent groundings.
#[test]
fn contrariness_grounding_shared_variables() {
    let (mut system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(bird(polly)))
        .build();

    // Manually add a contrary with shared variable X
    system
        .contrariness
        .add_contrary(formula!(flies(X)), formula!(!flies(X)));

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    // Should have exactly 2 entries (one per constant), not 4.
    // flies(tweety) -> !flies(tweety), flies(polly) -> !flies(polly)
    let entries = grounded.contrariness.entries();
    let total: usize = entries.values().map(|v| v.len()).sum();
    assert_eq!(
        total, 2,
        "joint grounding should produce 2 entries, not the Cartesian product of 4"
    );

    assert!(grounded
        .contrariness
        .is_contrary(&formula!(flies(tweety)), &formula!(!flies(tweety))));
    assert!(grounded
        .contrariness
        .is_contrary(&formula!(flies(polly)), &formula!(!flies(polly))));
    // Cross-substitutions should NOT exist
    assert!(!grounded
        .contrariness
        .is_contrary(&formula!(flies(tweety)), &formula!(!flies(polly))));
    assert!(!grounded
        .contrariness
        .is_contrary(&formula!(flies(polly)), &formula!(!flies(tweety))));
}

/// Test variable and constant collection.
#[test]
fn formula_variable_collection() {
    let f = formula!(bird(X));
    let vars = f.variables();
    assert_eq!(vars.len(), 1);
    assert_eq!(*vars[0], "X");

    let f_tweety = formula!(bird(tweety));
    let consts = f_tweety.constants();
    assert_eq!(consts.len(), 1);
    assert_eq!(*consts[0], "tweety");
}

/// Named defeasible rules have their name formula jointly substituted
/// with the rule body during grounding.
#[test]
fn grounding_preserves_defeasible_rule_names() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(bird(polly)))
        .named_defeasible_rule(
            "d1",
            formula!(d1(X)),
            vec![formula!(bird(X))],
            formula!(flies(X)),
        )
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    assert_eq!(grounded.defeasible_rules.len(), 2);

    for rule in &grounded.defeasible_rules {
        let name = rule.name.as_ref().expect("ground rule should retain name");
        let consequent_consts = rule.consequent.constants();
        let name_consts = name.constants();
        assert_eq!(
            consequent_consts, name_consts,
            "name and consequent must receive the same substitution"
        );
    }

    let names: HashSet<&Formula> = grounded
        .defeasible_rules
        .iter()
        .map(|r| r.name.as_ref().unwrap())
        .collect();
    assert!(names.contains(&formula!(d1(tweety))));
    assert!(names.contains(&formula!(d1(polly))));
}

/// PremiseKind is preserved through grounding — Axiom and Ordinary
/// premises retain their kind in the output.
#[test]
fn grounding_preserves_premise_kinds() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .axiom(formula!(p))
        .ordinary_premise(formula!(q))
        .defeasible_rule("d1", vec![formula!(q)], formula!(s))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    assert_eq!(grounded.knowledge_base.premises.len(), 2);

    let find_kind = |f: &Formula| -> PremiseKind {
        grounded
            .knowledge_base
            .premises
            .iter()
            .find(|p| &p.formula == f)
            .unwrap_or_else(|| panic!("premise {f:?} not found"))
            .kind
            .clone()
    };

    assert_eq!(find_kind(&formula!(p)), PremiseKind::Axiom);
    assert_eq!(find_kind(&formula!(q)), PremiseKind::Ordinary);
}

/// When no constants exist anywhere in the system, the synthetic `_default`
/// constant is injected into the Herbrand universe.
#[test]
fn grounding_injects_default_when_no_constants() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(p(X)))
        .defeasible_rule("d1", vec![formula!(p(X))], formula!(q(X)))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    assert_eq!(grounded.defeasible_rules.len(), 1);
    assert_eq!(
        grounded.defeasible_rules[0].consequent,
        formula!(q(_default))
    );
    assert_eq!(
        grounded.defeasible_rules[0].antecedents[0],
        formula!(p(_default))
    );

    assert_eq!(grounded.knowledge_base.premises.len(), 1);
    assert_eq!(
        grounded.knowledge_base.premises[0].formula,
        formula!(p(_default))
    );
}

/// When at least one constant exists, `_default` is NOT injected — only
/// user-provided constants populate the universe.
#[test]
fn grounding_does_not_inject_default_when_constants_exist() {
    let (system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(p(a)))
        .defeasible_rule("d1", vec![formula!(p(X))], formula!(q(X)))
        .build();

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    assert_eq!(grounded.defeasible_rules.len(), 1);
    assert_eq!(grounded.defeasible_rules[0].consequent, formula!(q(a)));

    for premise in &grounded.knowledge_base.premises {
        for c in premise.formula.constants() {
            assert_ne!(c.as_str(), "_default");
        }
    }
    for rule in &grounded.defeasible_rules {
        for c in rule.consequent.constants() {
            assert_ne!(c.as_str(), "_default");
        }
    }
}

/// ContrarinessRelation types (Contrary and Contradictory) are preserved
/// through grounding.
#[test]
fn grounding_preserves_contrariness_relation_types() {
    let (mut system, _warnings) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(t(a)))
        .build();

    system
        .contrariness
        .add_contrary(formula!(p(X)), formula!(q(X)));
    system
        .contrariness
        .add_contradictory(formula!(r(X)), formula!(s(X)));

    let grounder = NaiveGrounder;
    let grounded = grounder.ground(&system).unwrap();

    let entries = grounded.contrariness.entries();

    let p_a_attackers = entries
        .get(&formula!(p(a)))
        .expect("ground contrary entry for p(a) should exist");
    assert_eq!(p_a_attackers.len(), 1);
    assert_eq!(p_a_attackers[0].0, formula!(q(a)));
    assert_eq!(p_a_attackers[0].1, ContrarinessRelation::Contrary);

    let r_a_attackers = entries
        .get(&formula!(r(a)))
        .expect("ground contradictory entry for r(a) should exist");
    assert_eq!(r_a_attackers.len(), 1);
    assert_eq!(r_a_attackers[0].0, formula!(s(a)));
    assert_eq!(r_a_attackers[0].1, ContrarinessRelation::Contradictory);

    let s_a_attackers = entries
        .get(&formula!(s(a)))
        .expect("symmetric contradictory entry for s(a) should exist");
    assert_eq!(s_a_attackers.len(), 1);
    assert_eq!(s_a_attackers[0].0, formula!(r(a)));
    assert_eq!(s_a_attackers[0].1, ContrarinessRelation::Contradictory);
}

/// A grounded system produces the same arguments as a manually constructed
/// ground system (conservative instantiation criterion).
#[test]
fn grounding_conservative_instantiation() {
    let (schematic_system, _) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(bird(polly)))
        .defeasible_rule("d1", vec![formula!(bird(X))], formula!(flies(X)))
        .with_classical_negation()
        .build();

    let grounder = NaiveGrounder;
    let grounded_auto = grounder.ground(&schematic_system).unwrap();

    let (manual_system, _) = AspicSystemBuilder::new()
        .ordinary_premise(formula!(bird(tweety)))
        .ordinary_premise(formula!(bird(polly)))
        .defeasible_rule(
            "d1_tweety",
            vec![formula!(bird(tweety))],
            formula!(flies(tweety)),
        )
        .defeasible_rule(
            "d1_polly",
            vec![formula!(bird(polly))],
            formula!(flies(polly)),
        )
        .with_classical_negation()
        .build();

    let grounded_manual = grounder.ground(&manual_system).unwrap();

    let constructor = ForwardChainingConstructor;
    let store_auto = constructor.construct(&grounded_auto);
    let store_manual = constructor.construct(&grounded_manual);

    let conclusions_auto: HashSet<&Formula> = store_auto
        .all_arguments()
        .map(|(_, arg)| arg.conclusion())
        .collect();
    let conclusions_manual: HashSet<&Formula> = store_manual
        .all_arguments()
        .map(|(_, arg)| arg.conclusion())
        .collect();

    assert_eq!(
        conclusions_auto, conclusions_manual,
        "grounded system must produce the same argument conclusions as manual instantiation"
    );
    assert_eq!(
        store_auto.len(),
        store_manual.len(),
        "argument count must match"
    );
}
