//! Property-based tests for the chase algorithm using proptest.

use proptest::prelude::*;

use chase_rs::chase::rule::RuleBuilder;
use chase_rs::{Atom, Instance, Term, chase};

/// Strategy for generating constant names
fn constant_strategy() -> impl Strategy<Value = String> {
    prop::sample::select(vec![
        "a".to_string(),
        "b".to_string(),
        "c".to_string(),
        "d".to_string(),
        "e".to_string(),
    ])
}

/// Strategy for generating variable names
fn variable_strategy() -> impl Strategy<Value = String> {
    prop::sample::select(vec![
        "X".to_string(),
        "Y".to_string(),
        "Z".to_string(),
        "W".to_string(),
    ])
}

/// Strategy for generating predicate names
fn predicate_strategy() -> impl Strategy<Value = String> {
    prop::sample::select(vec![
        "P".to_string(),
        "Q".to_string(),
        "R".to_string(),
        "S".to_string(),
    ])
}

/// Strategy for generating ground atoms (facts)
fn ground_atom_strategy() -> impl Strategy<Value = Atom> {
    (
        predicate_strategy(),
        prop::collection::vec(constant_strategy(), 1..=3),
    )
        .prop_map(|(pred, consts)| {
            Atom::new(pred, consts.into_iter().map(Term::constant).collect())
        })
}

/// Strategy for generating a small instance (set of facts)
fn instance_strategy() -> impl Strategy<Value = Instance> {
    prop::collection::vec(ground_atom_strategy(), 0..10)
        .prop_map(|atoms| atoms.into_iter().collect())
}

// =============================================================================
// Property: Chase always terminates
// =============================================================================

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

    #[test]
    fn chase_always_terminates(instance in instance_strategy()) {
        // Simple rule: P(X) -> Q(X)
        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X")])
            .build();

        let result = chase(instance, &[rule]);

        // Chase should always terminate (either fixpoint or max iterations)
        prop_assert!(result.terminated || result.steps > 0);
    }
}

// =============================================================================
// Property: Chase is monotonic (facts are only added, never removed)
// =============================================================================

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

    #[test]
    fn chase_is_monotonic(instance in instance_strategy()) {
        let initial_facts: Vec<_> = instance.iter().cloned().collect();

        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X")])
            .build();

        let result = chase(instance, &[rule]);

        // All original facts should still be present
        for fact in &initial_facts {
            prop_assert!(
                result.instance.contains(fact),
                "Original fact {:?} was removed", fact
            );
        }

        // Result should have at least as many facts as the input
        prop_assert!(result.instance.len() >= initial_facts.len());
    }
}

// =============================================================================
// Property: Fixpoint is stable (running chase again produces no changes)
// =============================================================================

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

    #[test]
    fn fixpoint_is_stable(instance in instance_strategy()) {
        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X")])
            .build();

        // Run chase to fixpoint
        let result1 = chase(instance, &[rule.clone()]);
        prop_assert!(result1.terminated);

        // Run chase again on the result
        let result2 = chase(result1.instance.clone(), &[rule]);

        // Should terminate immediately with no new facts
        prop_assert!(result2.terminated);
        prop_assert_eq!(result2.steps, 0, "Second chase should produce no changes");
        prop_assert_eq!(result1.instance.len(), result2.instance.len());
    }
}

// =============================================================================
// Property: All derived facts are ground (no variables)
// =============================================================================

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

    #[test]
    fn all_facts_are_ground(instance in instance_strategy()) {
        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X"), Term::var("Y")])
            .then("R", vec![Term::var("X"), Term::var("Y")])
            .build();

        let result = chase(instance, &[rule]);

        for fact in result.instance.iter() {
            prop_assert!(
                fact.is_ground(),
                "Fact {:?} contains variables", fact
            );
        }
    }
}

// =============================================================================
// Property: Rules without existentials don't create nulls
// =============================================================================

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

    #[test]
    fn no_existentials_means_no_nulls(instance in instance_strategy()) {
        // Rule with all head variables appearing in body
        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X")])
            .build();

        let result = chase(instance, &[rule]);

        for fact in result.instance.iter() {
            for term in &fact.terms {
                prop_assert!(
                    !matches!(term, Term::Null(_)),
                    "Found null in fact {:?} but rule has no existentials", fact
                );
            }
        }
    }
}

// =============================================================================
// Property: Existential rules create exactly one null per trigger
// =============================================================================

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

    #[test]
    fn existentials_create_unique_nulls(
        num_constants in 1usize..5
    ) {
        // Create facts P(c0), P(c1), P(c2), ... with unique constants
        let constants: Vec<String> = (0..num_constants).map(|i| format!("c{}", i)).collect();
        let instance: Instance = constants
            .iter()
            .map(|c| Atom::new("P", vec![Term::constant(c)]))
            .collect();

        // Rule: P(X) -> Q(X, Y) where Y is existential
        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X"), Term::var("Y")])
            .build();

        let result = chase(instance, &[rule]);

        let q_facts: Vec<_> = result.instance.facts_for_predicate("Q");

        // Should have exactly as many Q facts as P facts
        prop_assert_eq!(q_facts.len(), num_constants);

        // Each Q fact should have a null in the second position
        for fact in &q_facts {
            prop_assert!(
                matches!(fact.terms[1], Term::Null(_)),
                "Expected null in second position of {:?}", fact
            );
        }

        // All nulls should be unique
        let nulls: Vec<_> = q_facts
            .iter()
            .filter_map(|f| match &f.terms[1] {
                Term::Null(id) => Some(*id),
                _ => None,
            })
            .collect();

        let mut unique_nulls = nulls.clone();
        unique_nulls.sort();
        unique_nulls.dedup();
        prop_assert_eq!(nulls.len(), unique_nulls.len(), "Nulls should be unique");
    }
}

// =============================================================================
// Property: Transitive closure computes correct number of facts
// =============================================================================

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

    #[test]
    fn transitive_closure_chain(chain_length in 2usize..6) {
        // Create a chain: E(0,1), E(1,2), ..., E(n-1,n)
        let mut facts = Vec::new();
        for i in 0..chain_length {
            facts.push(Atom::new(
                "E",
                vec![Term::constant(format!("{}", i)), Term::constant(format!("{}", i + 1))],
            ));
        }
        let instance: Instance = facts.into_iter().collect();

        // E(X,Y) -> T(X,Y)
        let rule1 = RuleBuilder::new()
            .when("E", vec![Term::var("X"), Term::var("Y")])
            .then("T", vec![Term::var("X"), Term::var("Y")])
            .build();

        // T(X,Y), E(Y,Z) -> T(X,Z)
        let rule2 = RuleBuilder::new()
            .when("T", vec![Term::var("X"), Term::var("Y")])
            .when("E", vec![Term::var("Y"), Term::var("Z")])
            .then("T", vec![Term::var("X"), Term::var("Z")])
            .build();

        let result = chase(instance, &[rule1, rule2]);
        prop_assert!(result.terminated);

        let t_facts = result.instance.facts_for_predicate("T");

        // For a chain of n edges, transitive closure has n*(n+1)/2 pairs
        let expected = chain_length * (chain_length + 1) / 2;
        prop_assert_eq!(
            t_facts.len(),
            expected,
            "Chain of {} edges should have {} transitive pairs",
            chain_length,
            expected
        );
    }
}

// =============================================================================
// Property: Empty instance with any rules produces empty or stays empty
// =============================================================================

proptest! {
    #[test]
    fn empty_instance_stays_bounded(_seed in 0u64..1000) {
        let instance = Instance::new();

        let rule = RuleBuilder::new()
            .when("P", vec![Term::var("X")])
            .then("Q", vec![Term::var("X")])
            .build();

        let result = chase(instance, &[rule]);

        prop_assert!(result.terminated);
        prop_assert_eq!(result.steps, 0);
        prop_assert!(result.instance.is_empty());
    }
}

// =============================================================================
// Property: Substitution application is idempotent for ground terms
// =============================================================================

use chase_rs::Substitution;

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

    #[test]
    fn substitution_ground_term_unchanged(c in constant_strategy()) {
        let term = Term::constant(&c);
        let mut subst = Substitution::new();
        subst.bind("X".to_string(), Term::constant("other"));

        let result = subst.apply_term(&term);

        prop_assert_eq!(result, term, "Ground term should be unchanged by substitution");
    }
}

// =============================================================================
// Property: Substitution correctly replaces variables
// =============================================================================

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

    #[test]
    fn substitution_replaces_variable(
        var in variable_strategy(),
        replacement in constant_strategy()
    ) {
        let term = Term::var(&var);
        let mut subst = Substitution::new();
        subst.bind(var.clone(), Term::constant(&replacement));

        let result = subst.apply_term(&term);

        prop_assert_eq!(
            result,
            Term::constant(&replacement),
            "Variable should be replaced"
        );
    }
}

// =============================================================================
// Property: Atom arity is preserved through substitution
// =============================================================================

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

    #[test]
    fn substitution_preserves_arity(
        pred in predicate_strategy(),
        vars in prop::collection::vec(variable_strategy(), 1..4),
        replacement in constant_strategy()
    ) {
        let atom = Atom::new(
            &pred,
            vars.iter().map(|v| Term::var(v)).collect(),
        );

        let mut subst = Substitution::new();
        for var in &vars {
            subst.bind(var.clone(), Term::constant(&replacement));
        }

        let result = subst.apply_atom(&atom);

        prop_assert_eq!(result.arity(), atom.arity());
        prop_assert_eq!(result.predicate, atom.predicate);
    }
}