//! Core chase algorithm implementation.

use std::collections::{HashMap, HashSet};

use super::atom::Atom;
use super::instance::Instance;
use super::rule::Rule;
use super::substitution::{Substitution, unify_atom};
use super::term::Term;

/// Result of running the chase algorithm.
#[derive(Debug)]
pub struct ChaseResult {
    /// The final instance after the chase terminates.
    pub instance: Instance,
    /// Number of chase steps performed.
    pub steps: usize,
    /// Whether the chase terminated (vs hitting a limit).
    pub terminated: bool,
}

/// Configuration for the chase algorithm.
#[derive(Debug, Clone)]
pub struct ChaseConfig {
    /// Maximum number of chase steps before giving up.
    pub max_steps: usize,
}

impl Default for ChaseConfig {
    fn default() -> Self {
        ChaseConfig { max_steps: 10_000 }
    }
}

/// Counter for generating fresh null values.
#[derive(Debug, Default)]
struct NullGenerator {
    counter: usize,
}

impl NullGenerator {
    fn fresh(&mut self) -> Term {
        let id = self.counter;
        self.counter += 1;
        Term::Null(id)
    }
}

/// A trigger represents a rule application: (rule_index, frontier_variable_bindings).
/// We use this to track which rule applications have already been performed,
/// preventing infinite loops with existential variables.
#[derive(Debug, Clone, PartialEq, Eq, Hash)]
struct Trigger {
    rule_index: usize,
    /// Bindings for frontier variables (those appearing in both body and head).
    /// Sorted by variable name for consistent hashing.
    frontier_bindings: Vec<(String, Term)>,
}

impl Trigger {
    fn new(rule_index: usize, rule: &Rule, subst: &Substitution) -> Self {
        let frontier = rule.frontier_variables();
        let mut bindings: Vec<_> = frontier
            .into_iter()
            .filter_map(|v| subst.get(&v).map(|t| (v, t.clone())))
            .collect();
        bindings.sort_by(|a, b| a.0.cmp(&b.0));

        Trigger {
            rule_index,
            frontier_bindings: bindings,
        }
    }
}

/// Run the standard chase algorithm.
///
/// The chase repeatedly applies rules to derive new facts until no more
/// facts can be derived (fixpoint) or a limit is reached.
///
/// This implementation uses the "restricted chase" approach which tracks
/// applied triggers to ensure termination with existential rules.
pub fn chase(instance: Instance, rules: &[Rule]) -> ChaseResult {
    chase_with_config(instance, rules, ChaseConfig::default())
}

/// Run the chase with custom configuration.
pub fn chase_with_config(
    mut instance: Instance,
    rules: &[Rule],
    config: ChaseConfig,
) -> ChaseResult {
    let mut null_gen = NullGenerator::default();
    let mut applied_triggers: HashSet<Trigger> = HashSet::new();
    let mut steps = 0;

    loop {
        if steps >= config.max_steps {
            return ChaseResult {
                instance,
                steps,
                terminated: false,
            };
        }

        let new_facts = chase_step(&instance, rules, &mut null_gen, &mut applied_triggers);

        if new_facts.is_empty() {
            // Fixpoint reached
            return ChaseResult {
                instance,
                steps,
                terminated: true,
            };
        }

        for fact in new_facts {
            instance.add(fact);
        }
        steps += 1;
    }
}

/// Perform a single chase step: find all applicable rule instances and derive new facts.
fn chase_step(
    instance: &Instance,
    rules: &[Rule],
    null_gen: &mut NullGenerator,
    applied_triggers: &mut HashSet<Trigger>,
) -> Vec<Atom> {
    let mut new_facts = Vec::new();

    for (rule_idx, rule) in rules.iter().enumerate() {
        // Find all ways to match the rule body against the instance
        let matches = find_body_matches(instance, &rule.body);

        for subst in matches {
            // Create a trigger to check if we've already applied this
            let trigger = Trigger::new(rule_idx, rule, &subst);

            // Skip if already applied (prevents infinite loops with existentials)
            if applied_triggers.contains(&trigger) {
                continue;
            }

            // For rules without existentials, check if head is already satisfied
            if rule.existential_variables().is_empty() {
                let head_facts: Vec<_> = rule
                    .head
                    .iter()
                    .map(|atom| subst.apply_atom(atom))
                    .collect();

                // Skip if all head facts already exist
                if head_facts.iter().all(|f| instance.contains(f)) {
                    continue;
                }
            }

            // Mark this trigger as applied
            applied_triggers.insert(trigger);

            // Generate head atoms with this substitution
            let derived = apply_rule_head(rule, &subst, null_gen);

            for fact in derived {
                if !instance.contains(&fact) {
                    new_facts.push(fact);
                }
            }
        }
    }

    new_facts
}

/// Find all substitutions that satisfy the rule body against the instance.
fn find_body_matches(instance: &Instance, body: &[Atom]) -> Vec<Substitution> {
    if body.is_empty() {
        return vec![Substitution::new()];
    }

    let mut results = vec![Substitution::new()];

    for body_atom in body {
        let mut new_results = Vec::new();

        for subst in &results {
            // Apply current substitution to the body atom
            let pattern = subst.apply_atom(body_atom);

            // Find all facts that match this pattern
            for fact in instance.facts_for_predicate(&pattern.predicate) {
                if let Some(new_subst) = unify_atom(&pattern, fact) {
                    // Combine substitutions
                    let mut combined = subst.clone();
                    for (var, term) in new_subst.iter() {
                        combined.bind(var.clone(), term.clone());
                    }
                    new_results.push(combined);
                }
            }
        }

        results = new_results;
    }

    results
}

/// Apply a rule head with the given substitution, generating fresh nulls for existentials.
fn apply_rule_head(rule: &Rule, subst: &Substitution, null_gen: &mut NullGenerator) -> Vec<Atom> {
    let existentials = rule.existential_variables();

    // Create a mapping for existential variables to fresh nulls
    let mut extended_subst = subst.clone();
    let mut null_map: HashMap<String, Term> = HashMap::new();

    for var in &existentials {
        let null = null_gen.fresh();
        null_map.insert(var.clone(), null);
    }

    // Add null mappings to substitution
    for (var, null) in null_map {
        extended_subst.bind(var, null);
    }

    // Generate head atoms
    rule.head
        .iter()
        .map(|atom| extended_subst.apply_atom(atom))
        .collect()
}

#[cfg(test)]
mod tests {
    use super::*;
    use crate::chase::rule::RuleBuilder;

    #[test]
    fn test_simple_chase() {
        // Initial facts
        let instance: Instance = vec![
            Atom::new(
                "Parent",
                vec![Term::constant("alice"), Term::constant("bob")],
            ),
            Atom::new(
                "Parent",
                vec![Term::constant("bob"), Term::constant("carol")],
            ),
        ]
        .into_iter()
        .collect();

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

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

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

        assert!(result.terminated);

        // Check derived facts
        let ancestors = result.instance.facts_for_predicate("Ancestor");
        assert_eq!(ancestors.len(), 3); // alice->bob, bob->carol, alice->carol
    }

    #[test]
    fn test_chase_with_existentials() {
        // Initial facts
        let instance: Instance = vec![Atom::new("Person", vec![Term::constant("alice")])]
            .into_iter()
            .collect();

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

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

        assert!(result.terminated);

        let has_ssn = result.instance.facts_for_predicate("HasSSN");
        assert_eq!(has_ssn.len(), 1);

        // Check that a null was generated
        let fact = has_ssn[0];
        assert!(matches!(fact.terms[1], Term::Null(_)));
    }

    #[test]
    fn test_chase_multiple_existentials() {
        // Test that each person gets their own SSN
        let instance: Instance = vec![
            Atom::new("Person", vec![Term::constant("alice")]),
            Atom::new("Person", vec![Term::constant("bob")]),
        ]
        .into_iter()
        .collect();

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

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

        assert!(result.terminated);

        let has_ssn = result.instance.facts_for_predicate("HasSSN");
        assert_eq!(has_ssn.len(), 2);

        // Verify different nulls were generated
        let nulls: Vec<_> = has_ssn.iter().map(|f| &f.terms[1]).collect();
        assert_ne!(nulls[0], nulls[1]);
    }

    #[test]
    fn test_empty_chase() {
        let instance = Instance::new();
        let result = chase(instance, &[]);

        assert!(result.terminated);
        assert_eq!(result.steps, 0);
    }

    #[test]
    fn test_chase_fixpoint() {
        // With no applicable rules, chase should terminate immediately
        let instance: Instance = vec![Atom::new("Fact", vec![Term::constant("a")])]
            .into_iter()
            .collect();

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

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

        assert!(result.terminated);
        assert_eq!(result.instance.len(), 1);
    }

    #[test]
    fn test_chase_no_duplicate_applications() {
        // Ensure the same rule isn't applied twice for the same body match
        let instance: Instance = vec![Atom::new("A", vec![Term::constant("x")])]
            .into_iter()
            .collect();

        // A(X) -> B(X, Y) - should only fire once per X value
        let rule = RuleBuilder::new()
            .when("A", vec![Term::var("X")])
            .then("B", vec![Term::var("X"), Term::var("Y")])
            .build();

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

        assert!(result.terminated);
        assert_eq!(result.instance.facts_for_predicate("B").len(), 1);
    }
}