//! Superposition inference rule.
//!
//! Rewrites subterms in clauses using positive equality literals from another clause.
//! This is the key rule for handling equality in first-order theorem proving.
//!
//! - **Superposition Left**: rewrite into negative literals
//! - **Superposition Right**: rewrite into positive equality literals
//!
//! For each positive equality `l = r` in the equation clause, and each non-variable
//! subterm `u` in the target clause, if `mgu(l, u) = σ` and `lσ ≻ rσ`,
//! produce a new clause with `u` replaced by `r`, under `σ`.

use std::collections::HashSet;

use mrs_core::Atom;
use mrs_core::SymbolId;
use mrs_core::clause::{Clause, ClauseIdGen, ClauseSource, Literal};
use mrs_core::term::Term;

use crate::ordering::{TermComparison, TermOrdering};
use crate::rename::{max_var, rename_clause};

/// Performs all superposition inferences from `eq_clause` into `target`.
///
/// For each positive equality literal in `eq_clause`, rewrites matching
/// subterms in all literals of `target`.
///
/// Both orientations of each equality (l=r and r=l) are tried.
pub fn superpose(
    eq_clause: &Clause,
    target: &Clause,
    ordering: &TermOrdering,
    id_gen: &mut ClauseIdGen,
) -> Vec<Clause> {
    superpose_selected(eq_clause, target, ordering, id_gen, None, &HashSet::new())
}

/// Like [`superpose`], but only rewrites into selected literals of the target.
///
/// `target_sel` restricts which literals in the target clause are eligible
/// for rewriting. `None` means all target literals are eligible.
/// The eq_clause's positive equalities are always eligible (no restriction).
///
/// `comm` is the set of binary function symbols treated as commutative for
/// unification of the `from` term against target subterms.
pub fn superpose_selected(
    eq_clause: &Clause,
    target: &Clause,
    ordering: &TermOrdering,
    id_gen: &mut ClauseIdGen,
    target_sel: Option<&[usize]>,
    comm: &HashSet<SymbolId>,
) -> Vec<Clause> {
    let offset = max_var(eq_clause);
    let target_r = rename_clause(target, offset);
    let mut results = Vec::new();

    for (i, eq_lit) in eq_clause.literals.iter().enumerate() {
        // Only superpose from positive equality literals
        if !eq_lit.is_positive() {
            continue;
        }
        let (left, right) = match &eq_lit.atom {
            Atom::Eq(l, r) => (l, r),
            _ => continue,
        };

        // Try both orientations: l→r and r→l
        for (from, to) in [(left, right), (right, left)] {
            // Standard superposition condition: don't superpose from a variable.
            // A variable from-term unifies with every non-variable subterm,
            // producing many useless inferences that explode the search space.
            if matches!(from, Term::Var(_)) {
                continue;
            }
            superpose_with(
                eq_clause,
                &target_r,
                i,
                from,
                to,
                ordering,
                id_gen,
                target_sel,
                comm,
                &mut results,
            );
        }
    }

    results
}

/// Tries superposition with a specific oriented equality `from → to`.
#[allow(clippy::too_many_arguments)]
fn superpose_with(
    eq_clause: &Clause,
    target: &Clause,
    eq_lit_idx: usize,
    from: &Term,
    to: &Term,
    ordering: &TermOrdering,
    id_gen: &mut ClauseIdGen,
    target_sel: Option<&[usize]>,
    comm: &HashSet<SymbolId>,
    results: &mut Vec<Clause>,
) {
    for (j, target_lit) in target.literals.iter().enumerate() {
        // Skip non-selected target literals
        if let Some(sel) = target_sel
            && !sel.contains(&j)
        {
            continue;
        }
        // Collect non-variable positions from the terms in this literal
        let term_positions = literal_term_positions(target_lit);

        for (base_term, positions) in &term_positions {
            for pos in positions {
                let subterm = match base_term.subterm_at(pos) {
                    Some(t) => t,
                    None => continue,
                };

                // Try to unify `from` with this subterm
                let sigma = match mrs_unify::unify_comm(from, subterm, comm) {
                    Ok(s) => s,
                    Err(_) => continue,
                };

                // Check ordering: from·σ ≻ to·σ (or incomparable)
                let from_s = sigma.apply_term(from);
                let to_s = sigma.apply_term(to);
                let comp = ordering.compare(&from_s, &to_s);
                if comp == TermComparison::Less || comp == TermComparison::Equal {
                    continue;
                }

                // Build the result clause
                let replaced_term = base_term.replace_at(pos, to);
                let replaced_lit = rebuild_literal(target_lit, base_term, &replaced_term);
                let replaced_lit = sigma.apply_literal(&replaced_lit);

                let mut new_lits = Vec::new();
                // Add remaining literals from eq_clause (except the equality used)
                for (k, lit) in eq_clause.literals.iter().enumerate() {
                    if k != eq_lit_idx {
                        new_lits.push(sigma.apply_literal(lit));
                    }
                }
                // Add remaining literals from target (except the one being rewritten)
                for (k, lit) in target.literals.iter().enumerate() {
                    if k != j {
                        new_lits.push(sigma.apply_literal(lit));
                    }
                }
                // Add the rewritten literal
                new_lits.push(replaced_lit);

                let mut new_avatar = eq_clause.avatar.clone();
                new_avatar.extend_from_slice(&target.avatar);

                results.push(Clause::new_avatar(
                    id_gen.next(),
                    new_lits,
                    ClauseSource::Inference {
                        rule: "superposition".into(),
                        parents: vec![eq_clause.id, target.id],
                    },
                    new_avatar,
                ));
            }
        }
    }
}

/// Returns the terms from a literal along with their non-variable positions.
///
/// For `Pred(p, args)`: each argument and its positions.
/// For `Eq(l, r)`: both sides and their positions.
fn literal_term_positions(lit: &Literal) -> Vec<(&Term, Vec<Vec<usize>>)> {
    match &lit.atom {
        Atom::Pred(_, args) => args
            .iter()
            .map(|arg| (arg, arg.non_variable_positions()))
            .collect(),
        Atom::Eq(l, r) => {
            vec![
                (l, l.non_variable_positions()),
                (r, r.non_variable_positions()),
            ]
        }
    }
}

/// Rebuilds a literal after replacing a term.
///
/// Finds which part of the literal matches `original` and replaces it with `replacement`.
fn rebuild_literal(lit: &Literal, original: &Term, replacement: &Term) -> Literal {
    let new_atom = match &lit.atom {
        Atom::Pred(p, args) => {
            let new_args: Vec<Term> = args
                .iter()
                .map(|a| {
                    if std::ptr::eq(a, original) {
                        replacement.clone()
                    } else {
                        a.clone()
                    }
                })
                .collect();
            Atom::Pred(*p, new_args)
        }
        Atom::Eq(l, r) => {
            let new_l = if std::ptr::eq(l, original) {
                replacement.clone()
            } else {
                l.clone()
            };
            let new_r = if std::ptr::eq(r, original) {
                replacement.clone()
            } else {
                r.clone()
            };
            Atom::Eq(new_l, new_r)
        }
    };
    Literal {
        positive: lit.positive,
        atom: new_atom,
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    use mrs_core::clause::{Clause, ClauseIdGen, ClauseSource};
    use mrs_core::{Atom, Literal, SymbolTable, Term};

    fn input_clause(id_gen: &mut ClauseIdGen, lits: Vec<Literal>, name: &str) -> Clause {
        Clause::new(
            id_gen.next(),
            lits,
            ClauseSource::Input {
                name: name.into(),
                role: "axiom".into(),
            },
        )
    }

    #[test]
    fn superpose_simple_rewrite() {
        // Clause 1: f(a) = b
        // Clause 2: g(f(a)) != c  (negated goal)
        // Expected: g(b) != c (by replacing f(a) with b)
        let mut syms = SymbolTable::new();
        let f = syms.intern("f");
        let g = syms.intern("g");
        let a = syms.intern("a");
        let b = syms.intern("b");
        let c = syms.intern("c");
        let mut id_gen = ClauseIdGen::new();
        let ordering = TermOrdering::KBO;

        let c1 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::eq(
                Term::app(f, vec![Term::constant(a)]),
                Term::constant(b),
            ))],
            "ax1",
        );

        let c2 = input_clause(
            &mut id_gen,
            vec![Literal::neg(Atom::eq(
                Term::app(g, vec![Term::app(f, vec![Term::constant(a)])]),
                Term::constant(c),
            ))],
            "goal",
        );

        let results = superpose(&c1, &c2, &ordering, &mut id_gen);
        assert!(
            !results.is_empty(),
            "should produce at least one superposition result"
        );

        // Check that at least one result contains g(b)
        let has_rewritten = results.iter().any(|clause| {
            clause.literals.iter().any(|lit| match &lit.atom {
                Atom::Eq(l, _r) => *l == Term::app(g, vec![Term::constant(b)]),
                _ => false,
            })
        });
        assert!(
            has_rewritten,
            "should contain g(b) after rewriting f(a) to b"
        );
    }

    #[test]
    fn superpose_no_equality_no_result() {
        // Clause 1: p(a) (no equality literal)
        // Clause 2: q(a)
        // No superposition possible
        let mut syms = SymbolTable::new();
        let p = syms.intern("p");
        let q = syms.intern("q");
        let a = syms.intern("a");
        let mut id_gen = ClauseIdGen::new();
        let ordering = TermOrdering::KBO;

        let c1 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::pred(p, vec![Term::constant(a)]))],
            "ax1",
        );
        let c2 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::pred(q, vec![Term::constant(a)]))],
            "ax2",
        );

        let results = superpose(&c1, &c2, &ordering, &mut id_gen);
        assert!(results.is_empty());
    }

    #[test]
    fn superpose_into_predicate() {
        // Clause 1: a = b
        // Clause 2: p(a)
        // Expected: p(b) (by replacing a with b in p(a))
        let mut syms = SymbolTable::new();
        let p = syms.intern("p");
        let a = syms.intern("a");
        let b = syms.intern("b");
        let mut id_gen = ClauseIdGen::new();
        let ordering = TermOrdering::KBO;

        let c1 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::eq(Term::constant(a), Term::constant(b)))],
            "ax1",
        );
        let c2 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::pred(p, vec![Term::constant(a)]))],
            "ax2",
        );

        let _results = superpose(&c1, &c2, &ordering, &mut id_gen);
        // a and b are constants with same weight. Precedence: b > a (later SymbolId).
        // So b > a, meaning a = b oriented as b → a. Try a → b: a !> b. Try b → a: b > a.
        // For superposition into p(a): need to unify "from" with "a".
        // When from=b, to=a: unify(b, a) fails (different constants).
        // When from=a, to=b: unify(a, a) succeeds, but need a > b? No, a < b. Skip.
        // Hmm, this means neither orientation works for rewriting a to b.
        //
        // Actually for a=b where b > a: the orientation should be b→a.
        // To rewrite p(a), we'd need from=something that unifies with a and from>to.
        // With from=a, to=b: a < b, so this fails.
        // With from=b, to=a: unify(b, a) fails since they're different constants.
        //
        // This is correct: superposition with ordering can't rewrite a→b
        // when b > a. We'd need the equality b=a or to use it the other way.
        // This is actually a feature of KBO: not all rewrites are allowed.
        //
        // For the search engine to solve a=b ⊢ p(b)→p(a) etc, it needs to
        // also try superposing c2 into c1 (the other direction).
        // That test belongs to the search integration.
    }

    #[test]
    fn superpose_with_variable() {
        // Clause 1: f(X) = X  (collapse rule)
        // Clause 2: ¬p(f(a))  (negative literal)
        // Expected: ¬p(a)     (by unifying X=a, replacing f(a) with a)
        let mut syms = SymbolTable::new();
        let f = syms.intern("f");
        let p = syms.intern("p");
        let a = syms.intern("a");
        let mut id_gen = ClauseIdGen::new();
        let ordering = TermOrdering::KBO;

        let c1 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::eq(
                Term::app(f, vec![Term::var(0)]),
                Term::var(0),
            ))],
            "ax1",
        );
        let c2 = input_clause(
            &mut id_gen,
            vec![Literal::neg(Atom::pred(
                p,
                vec![Term::app(f, vec![Term::constant(a)])],
            ))],
            "ax2",
        );

        let results = superpose(&c1, &c2, &ordering, &mut id_gen);
        // f(X) > X under KBO (weight 2 > weight 1), so orientation f(X) → X is valid.
        // Unify f(X) with f(a): X=a. Replace f(a) with a. Result: ¬p(a).
        assert!(!results.is_empty(), "should produce superposition result");
        let has_pa = results.iter().any(|clause| {
            clause.literals.iter().any(|lit| {
                lit.is_negative()
                    && match &lit.atom {
                        Atom::Pred(_, args) => args.len() == 1 && args[0] == Term::constant(a),
                        _ => false,
                    }
            })
        });
        assert!(has_pa, "should contain ¬p(a)");
    }

    #[test]
    fn superpose_tracks_parents() {
        let mut syms = SymbolTable::new();
        let f = syms.intern("f");
        let a = syms.intern("a");
        let _b = syms.intern("b");
        let p = syms.intern("p");
        let mut id_gen = ClauseIdGen::new();
        let ordering = TermOrdering::KBO;

        let c1 = input_clause(
            &mut id_gen,
            vec![Literal::pos(Atom::eq(
                Term::app(f, vec![Term::var(0)]),
                Term::var(0),
            ))],
            "ax1",
        );
        let c2 = input_clause(
            &mut id_gen,
            vec![Literal::neg(Atom::pred(
                p,
                vec![Term::app(f, vec![Term::constant(a)])],
            ))],
            "ax2",
        );

        let results = superpose(&c1, &c2, &ordering, &mut id_gen);
        for clause in &results {
            if let ClauseSource::Inference { rule, parents } = &clause.source {
                assert_eq!(rule, "superposition");
                assert_eq!(parents.len(), 2);
                assert_eq!(parents[0], c1.id);
                // Note: parent[1] is the original target id, not the renamed one
            }
        }
    }
}
