//! Property-based tests for the chase algorithm using proptest.
//!
//! All tests use explicit seeds for reproducibility.

use proptest::prelude::*;
use proptest::test_runner::{Config, TestRng, TestRunner};

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

// =============================================================================
// Test Configuration
// =============================================================================

/// Create a test runner with an explicit seed for reproducibility.
fn seeded_runner(seed: u64, cases: u32) -> TestRunner {
    let config = Config::with_cases(cases);
    // Create a deterministic seed from u64
    let mut seed_bytes = [0u8; 32];
    seed_bytes[..8].copy_from_slice(&seed.to_le_bytes());
    let rng = TestRng::from_seed(proptest::test_runner::RngAlgorithm::ChaCha, &seed_bytes);
    TestRunner::new_with_rng(config, rng)
}

// =============================================================================
// Strategies
// =============================================================================

/// 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
// =============================================================================

#[test]
fn chase_always_terminates() {
    const SEED: u64 = 12345;
    let mut runner = seeded_runner(SEED, 50);

    runner
        .run(&instance_strategy(), |instance| {
            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 || result.steps > 0);
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn chase_is_monotonic() {
    const SEED: u64 = 23456;
    let mut runner = seeded_runner(SEED, 50);

    runner
        .run(&instance_strategy(), |instance| {
            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]);

            for fact in &initial_facts {
                prop_assert!(
                    result.instance.contains(fact),
                    "Original fact {:?} was removed",
                    fact
                );
            }

            prop_assert!(result.instance.len() >= initial_facts.len());
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn fixpoint_is_stable() {
    const SEED: u64 = 34567;
    let mut runner = seeded_runner(SEED, 30);

    runner
        .run(&instance_strategy(), |instance| {
            let rule = RuleBuilder::new()
                .when("P", vec![Term::var("X")])
                .then("Q", vec![Term::var("X")])
                .build();

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

            let result2 = chase(result1.instance.clone(), &[rule]);

            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());
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn all_facts_are_ground() {
    const SEED: u64 = 45678;
    let mut runner = seeded_runner(SEED, 50);

    runner
        .run(&instance_strategy(), |instance| {
            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);
            }
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn no_existentials_means_no_nulls() {
    const SEED: u64 = 56789;
    let mut runner = seeded_runner(SEED, 50);

    runner
        .run(&instance_strategy(), |instance| {
            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
                    );
                }
            }
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn existentials_create_unique_nulls() {
    const SEED: u64 = 67890;
    let mut runner = seeded_runner(SEED, 30);

    runner
        .run(&(1usize..5), |num_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();

            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");

            prop_assert_eq!(q_facts.len(), num_constants);

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

            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");
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn transitive_closure_chain() {
    const SEED: u64 = 78901;
    let mut runner = seeded_runner(SEED, 20);

    runner
        .run(&(2usize..6), |chain_length| {
            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();

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

            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");

            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
            );
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn empty_instance_stays_bounded() {
    const SEED: u64 = 89012;
    let mut runner = seeded_runner(SEED, 100);

    runner
        .run(&(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());
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn substitution_ground_term_unchanged() {
    const SEED: u64 = 90123;
    let mut runner = seeded_runner(SEED, 100);

    runner
        .run(&constant_strategy(), |c| {
            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"
            );
            Ok(())
        })
        .unwrap();
}

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

#[test]
fn substitution_replaces_variable() {
    const SEED: u64 = 11111;
    let mut runner = seeded_runner(SEED, 100);

    runner
        .run(
            &(variable_strategy(), constant_strategy()),
            |(var, replacement)| {
                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"
                );
                Ok(())
            },
        )
        .unwrap();
}

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

#[test]
fn substitution_preserves_arity() {
    const SEED: u64 = 22222;
    let mut runner = seeded_runner(SEED, 50);

    let strategy = (
        predicate_strategy(),
        prop::collection::vec(variable_strategy(), 1..4),
        constant_strategy(),
    );

    runner
        .run(&strategy, |(pred, vars, replacement)| {
            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);
            Ok(())
        })
        .unwrap();
}