package prolog.logic

import org.junit.jupiter.api.Assertions.assertFalse
import org.junit.jupiter.api.Assertions.assertTrue
import org.junit.jupiter.api.Test
import prolog.Substitutions
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable

class VerificationTests {
    @Test
    fun unbound_variable_is_var() {
        val variable = Variable("X")
        assertTrue(variable(variable))
    }

    @Test
    fun variable_bound_to_atom_is_not_var() {
        val variable = Variable("X")

        assertTrue(variable(variable))

        val atom = Atom("a")

        assertFalse(variable(variable, mapOf(variable to atom)))
    }

    @Test
    fun variable_bound_to_compound_term_is_not_var() {
        val variable = Variable("X")

        assertTrue(variable(variable))

        val structure = Structure(Atom("a"), listOf(Atom("b")))

        assertFalse(variable(variable, mapOf(variable to structure)))
    }

    /**
     * ?- X = X, var(X).
     * true.
     */
    @Test
    fun variable_bound_to_itself_is_var() {
        val variable = Variable("X")
        assertTrue(variable(variable, mapOf(variable to variable)))
    }

    /**
     * ?- X = Y, var(X).
     * X = Y.
     */
    @Test
    fun variable_bound_to_another_variable_is_var() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")
        assertTrue(variable(variable1, mapOf(variable1 to variable2)))
    }

    /**
     * ?- Y = a, X = Y, var(X).
     * false.
     */
    @Test
    fun variable_bound_to_bound_variable_is_not_var() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")
        val map: Substitutions = mapOf(
            variable1 to variable2,
            variable2 to Atom("a")
        )
        assertFalse(variable(variable1, map))
    }

    @Test
    fun atom_is_not_var() {
        val atom = Atom("a")
        assertFalse(variable(atom))
    }

    @Test
    fun compound_term_is_not_var() {
        val structure = Structure(Atom("a"), listOf(Atom("b")))
        assertFalse(variable(structure))
    }

    @Test
    fun compound_term_with_var_is_not_var() {
        val structure = Structure(Atom("a"), listOf(Variable("X")))
        assertFalse(variable(structure))
    }

    @Test
    fun unbound_variable_is_not_nonvar() {
        val variable = Variable("X")
        assertFalse(nonvariable(variable))
    }

    /**
     * ?- A = a, nonvar(A).
     * A = a.
     */
    @Test
    fun variable_bound_to_atom_is_nonvar() {
        val variable = Variable("X")

        assertFalse(nonvariable(variable))

        val atom = Atom("a")

        assertTrue(nonvariable(variable, mapOf(variable to atom)))
    }

    /**
     * ?- A = f(b), nonvar(A).
     * A = f(b).
     */
    @Test
    fun variable_bound_to_compound_term_is_nonvar() {
        val variable = Variable("X")

        assertFalse(nonvariable(variable))

        val structure = Structure(Atom("a"), listOf(Atom("b")))

        assertTrue(nonvariable(variable, mapOf(variable to structure)))
    }

    /**
     * ?- X = X, nonvar(X).
     * false.
     */
    @Test
    fun variable_bound_to_itself_is_not_nonvar() {
        val variable = Variable("X")
        assertFalse(nonvariable(variable, mapOf(variable to variable)))
    }

    /**
     * ?- X = Y, nonvar(X).
     * false.
     */
    @Test
    fun variable_bound_to_another_variable_is_not_nonvar() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")
        assertFalse(nonvariable(variable1, mapOf(variable1 to variable2)))
    }

    @Test
    fun atom_is_nonvar() {
        val atom = Atom("a")
        assertTrue(nonvariable(atom))
    }

    @Test
    fun compound_term_is_nonvar() {
        val structure = Structure(Atom("a"), listOf(Atom("b")))
        assertTrue(nonvariable(structure))
    }

    @Test
    fun compound_term_with_var_is_nonvar() {
        val structure = Structure(Atom("a"), listOf(Variable("X")))
        assertTrue(nonvariable(structure))
    }

    @Test
    fun unbound_variable_is_not_compound() {
        val variable = Variable("X")
        assertFalse(compound(variable))
    }

    /**
     * ?- A = a, compound(A).
     * false.
     */
    @Test
    fun bound_variable_to_atom_is_not_compound() {
        val variable = Variable("X")
        val atom = Atom("a")
        assertFalse(compound(variable, mapOf(variable to atom)))
    }

    /**
     * ?- A = f(b), compound(A).
     * A = f(b).
     */
    @Test
    fun bound_variable_to_compound_term_is_compound() {
        val variable = Variable("X")
        val structure = Structure(Atom("a"), listOf(Atom("b")))
        assertTrue(compound(variable, mapOf(variable to structure)))
    }

    /**
     * ?- Y = f(b), X = Y, compound(X).
     * Y = X, X = f(b).
     */
    @Test
    fun variable_bound_to_bound_variable_is_compound() {
        val variable1 = Variable("X")
        val variable2 = Variable("Y")
        val structure = Structure(Atom("a"), listOf(Atom("b")))

        val subs: Substitutions = mapOf(
            variable1 to variable2,
            variable2 to structure
        )

        assertTrue(compound(variable1, subs))
    }

    @Test
    fun atom_is_not_compound() {
        val atom = Atom("a")
        assertFalse(compound(atom))
    }

    @Test
    fun compound_term_is_compound() {
        val structure = Structure(Atom("a"), listOf(Atom("b")))
        assertTrue(compound(structure))
    }

    /**
     * ?- compound(a()).
     * true.
     */
    @Test
    fun compound_term_with_no_arguments_is_compound() {
        val structure = Structure(Atom("a"), emptyList())
        assertTrue(compound(structure))
    }
}