package prolog.logic

import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.Disabled
import org.junit.jupiter.api.Test
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable
import prolog.builtins.equivalent

/*
 * Based on: https://en.wikipedia.org/wiki/Unification_%28computer_science%29#Examples_of_syntactic_unification_of_first-order_terms
 */
class UnifyTest {
    @Test
    fun identical_atoms_unify() {
        val atom1 = Atom("a")
        val atom2 = Atom("a")

        val result = unify(atom1, atom2)

        assertTrue(result.isPresent, "Identical atoms should unify")
        assertEquals(0, result.get().size, "No substitutions should be made")
    }

    @Test
    fun different_atoms_do_not_unify() {
        val atom1 = Atom("a")
        val atom2 = Atom("b")

        val result = unify(atom1, atom2)

        assertFalse(result.isPresent, "Different atoms should not unify")
    }

    /**
     * ?- X = X.
     * true.
     */
    @Test
    fun identical_variables_unify() {
        val variable1 = Variable("X")
        val variable2 = Variable("X")

        val result = unify(variable1, variable2)

        assertTrue(result.isPresent, "Identical variables should unify")
        assertEquals(0, result.get().size, "No substitutions should be made")
    }

    @Test
    fun variable_unifies_with_atom() {
        val variable = Variable("X")
        val atom = Atom("a")

        val result = unify(atom, variable)

        assertTrue(result.isPresent, "Variable should unify with atom")
        assertEquals(1, result.get().size, "There should be one substitution")
        assertEquals(atom, variable.alias().get(), "Variable should be substituted with atom")
    }

    @Test
    fun variables_alias_when_unified() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")

        val result = unify(variable1, variable2)

        assertTrue(result.isPresent)
        assertEquals(1, result.get().size)
        assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2")
    }

    @Test
    fun identical_compound_terms_unify() {
        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))

        val result = unify(structure1, structure2)

        assertTrue(result.isPresent, "Identical compound terms should unify")
        assertEquals(0, result.get().size, "No substitutions should be made")
    }

    @Test
    fun compound_terms_with_different_arguments_do_not_unify() {
        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("c")))

        val result = unify(structure1, structure2)

        assertFalse(result.isPresent, "Different compound terms should not unify")
    }

    @Test
    fun compound_terms_with_different_functors_do_not_unify() {
        val structure1 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))
        val structure2 = Structure(Atom("g"), listOf(Atom("a"), Atom("b")))

        val result = unify(structure1, structure2)

        assertFalse(result.isPresent, "Compound terms with different functors should not unify")
    }

    /**
     * ?- X = f(a, b).
     * X = f(a, b).
     */
    @Test
    fun variable_unifies_with_compound_term() {
        val variable = Variable("X")
        val structure = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))

        val result = unify(variable, structure)

        assertTrue(result.isPresent, "Variable should unify with compound term")
        assertEquals(1, result.get().size, "There should be one substitution")
        assertTrue(
            equivalent(Structure(Atom("f"), listOf(Atom("a"), Atom("b"))), variable.alias().get()),
            "Variable should be substituted with compound term"
        )
    }

    @Test
    fun compound_term_with_variable_unifies_with_part() {
        val variable = Variable("X")
        val structure1 = Structure(Atom("f"), listOf(Atom("a"), variable))
        val structure2 = Structure(Atom("f"), listOf(Atom("a"), Atom("b")))

        val result = unify(structure1, structure2)

        assertTrue(result.isPresent, "Compound term with variable should unify with part")
        assertEquals(1, result.get().size, "There should be one substitution")
        val equivalence = equivalent(Atom("b"), variable.alias().get())
        assertTrue(equivalence, "Variable should be substituted with atom")
    }

    @Test
    fun compound_terms_with_variable_arguments_lists_alias_variables() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")

        val structure1 = Structure(Atom("f"), listOf(variable1))
        val structure2 = Structure(Atom("f"), listOf(variable2))

        val result = unify(structure1, structure2)

        assertTrue(result.isPresent, "Compound terms with variable arguments should unify")
        assertEquals(1, result.get().size, "There should be one substitution")
        assertEquals(variable2, variable1.alias().get(), "Variable 1 should alias to variable 2")
    }

    /**
     * f(X) = f(Y, Z)
     */
    @Test
    fun compound_terms_with_different_arity_do_not_unify() {
        val structure1 = Structure(Atom("f"), listOf(Variable("X")))
        val structure2 = Structure(Atom("f"), listOf(Variable("Y"), Variable("Z")))

        val result = unify(structure1, structure2)

        assertFalse(result.isPresent, "Compound terms with different arity should not unify")
    }

    /**
     * ?- f(g(X)) = f(Y).
     * Y = g(X).
     */
    @Test
    fun nested_compound_terms_with_variables_unify() {
        val variable2 = Variable("Y")

        val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(Variable("X")))))
        val structure2 = Structure(Atom("f"), listOf(variable2))

        val result = unify(structure1, structure2)

        assertTrue(result.isPresent, "Nested compound terms with variables should unify")
        assertEquals(1, result.get().size, "There should be one substitution")
        assertTrue(
            equivalent(Structure(Atom("g"), listOf(Variable("X"))), variable2.alias().get()),
            "Variable should be substituted with compound term"
        )
    }

    /**
     * ?- f(g(X), X) = f(Y, a).
     * X = a,
     * Y = g(a).
     */
    @Test
    fun compound_terms_with_more_variables() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")

        val structure1 = Structure(Atom("f"), listOf(Structure(Atom("g"), listOf(variable1)), variable1))
        val structure2 = Structure(Atom("f"), listOf(variable2, Atom("a")))

        val result = unify(structure1, structure2)

        assertTrue(result.isPresent, "Compound terms with more variables should unify")
        assertEquals(2, result.get().size, "There should be two substitutions")

        assertTrue(
            equivalent(Atom("a"), variable1.alias().get()),
            "Variable 1 should be substituted with atom"
        )
        val equivalence = equivalent(Structure(Atom("g"), listOf(Atom("a"))), variable2.alias().get())
        assertTrue(equivalence, "Variable 2 should be substituted with compound term")
    }

    /**
     * ?- X = f(X).
     * X = f(f(X)).
     */
    @Test
    fun recursive_unification() {
        val variable1 = Variable("X")
        val structure2 = Structure(Atom("f"), listOf(Variable("X")))

        val result = unify(variable1, structure2)

        assertTrue(result.isPresent, "Recursive unification should succeed")
        assertEquals(1, result.get().size, "There should be one substitution")
        assertEquals(structure2, variable1.alias().get(), "Variable should be substituted with compound term")
    }

    /**
     * ?- X = bar, Y = bar, X = Y.
     * X = Y, Y = bar.
     */
    @Disabled
    @Test
    fun multiple_unification() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")
        val atom = Atom("bar")

        variable1.bind(atom)
        variable2.bind(atom)

        val result = unify(variable1, variable2)

        assertTrue(result.isPresent, "Multiple unification should succeed")
        assertEquals(0, result.get().size, "No substitutions should be made")
    }

    /**
     * ?- a = a().
     * false.
     */
    @Test
    fun atom_with_different_arity() {
        val atom1 = Atom("a")
        val structure2 = Structure(Atom("a"), emptyList())

        val result = unify(atom1, structure2)

        assertFalse(result.isPresent, "Atom with different arity should not unify")
    }
}