package prolog.builtins

import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.BeforeEach
import org.junit.jupiter.api.Nested
import org.junit.jupiter.api.Test
import org.junit.jupiter.api.assertThrows
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.logic.Fact
import prolog.ast.logic.Rule
import prolog.ast.terms.CompoundTerm
import prolog.ast.terms.AnonymousVariable
import prolog.ast.terms.Atom
import prolog.ast.terms.Structure
import prolog.ast.terms.Variable

class AnalysisOperatorsTests {
    @Test
    fun `functor(foo, foo, 0)`() {
        val functor = FunctorOp(Atom("foo"), Atom("foo"), Integer(0))

        val result = functor.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        assertTrue(result[0].getOrNull()!!.isEmpty(), "Expected empty substitutions")
    }

    @Test
    fun `functor(foo(X), foo, Y)`() {
        val functor = FunctorOp(
            Structure(Atom("foo"), listOf(Variable("X"))),
            Atom("foo"),
            Variable("Y")
        )

        val result = functor.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        val subs = result[0].getOrNull()!!
        assertEquals(1, subs.size, "Expected 1 substitution")
        assertEquals(Integer(1), subs[Variable("Y")])
    }

    @Test
    fun `functor(foo, X, Y)`() {
        val atom = Atom("foo")
        val functor = FunctorOp(atom, Variable("X"), Variable("Y"))

        val result = functor.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        val subs = result[0].getOrNull()!!
        assertEquals(2, subs.size, "Expected 2 substitutions")
        assertEquals(atom.functor.name, subs[Variable("X")])
        assertEquals(atom.functor.arity, subs[Variable("Y")])
    }

    @Test
    fun `functor(X, foo, 1)`() {
        val functor = FunctorOp(Variable("X"), Atom("foo"), Integer(1))

        val result = functor.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        val subs = result[0].getOrNull()!!
        assertEquals(1, subs.size, "Expected 1 substitution")
        assertInstanceOf(Structure::class.java, subs[Variable("X")])
        val structure = subs[Variable("X")] as Structure
        assertEquals(Atom("foo"), structure.name)
        assertEquals(1, structure.arguments.size)
        assertInstanceOf(AnonymousVariable::class.java, structure.arguments[0])
    }

    @Test
    fun `functor(foo(a), foo, 0)`() {
        val functor = FunctorOp(Structure(Atom("foo"), listOf(Atom("a"))), Atom("foo"), Integer(0))

        val result = functor.satisfy(emptyMap()).toList()

        assertTrue(result.isEmpty(), "Expected no results")
    }

    @Test
    fun `functor(foo(X), foo, 0)`() {
        val functor = FunctorOp(Structure(Atom("foo"), listOf(Variable("X"))), Atom("foo"), Integer(0))

        val result = functor.satisfy(emptyMap()).toList()

        assertTrue(result.isEmpty(), "Expected no results")
    }

    @Test
    fun `functor(X, Y, 1)`() {
        val functor = FunctorOp(Variable("X"), Variable("Y"), Integer(1))

        val exception = assertThrows<Exception> {
            functor.satisfy(emptyMap()).toList()
        }
        assertEquals("Arguments are not sufficiently instantiated", exception.message)
    }

    @Test
    fun `arg without variables`() {
        val arg = Arg(
            Integer(1),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Atom("a")
        )

        val result = arg.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        val subs = result[0].getOrNull()!!
        assertTrue(subs.isEmpty(), "Expected no substitutions")
    }

    @Test
    fun `arg with variable value`() {
        val arg = Arg(
            Integer(1),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Variable("Term")
        )

        val result = arg.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "Expected 1 result")
        assertTrue(result[0].isSuccess, "Expected success")
        val subs = result[0].getOrNull()!!
        assertEquals(1, subs.size, "Expected 1 substitution")
        assertEquals(Atom("a"), subs[Variable("Term")])
    }

    @Test
    fun `arg with variable arg`() {
        val arguments = listOf(Atom("a"), Atom("b"), Atom("c"))
        for (i in arguments.indices) {
            val arg = Arg(
                Variable("Arg"),
                Structure(Atom("f"), arguments),
                arguments[i]
            )

            val result = arg.satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result for arg $i")
            assertTrue(result[0].isSuccess, "Expected success for arg $i")
            val subs = result[0].getOrNull()!!
            assertEquals(1, subs.size, "Expected 1 substitution for arg $i")
            assertEquals(Integer(i + 1), subs[Variable("Arg")], "Expected arg to be $i + 1")
        }
    }

    @Test
    fun `arg with backtracking`() {
        val arg = Arg(
            Variable("Position"),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Variable("Term")
        )

        val result = arg.satisfy(emptyMap()).toList()

        assertEquals(3, result.size, "Expected 3 results")

        assertTrue(result[0].isSuccess, "Expected success")
        val subs1 = result[0].getOrNull()!!
        assertEquals(2, subs1.size, "Expected 2 substitutions")
        assertEquals(Integer(1), subs1[Variable("Position")])
        assertEquals(Atom("a"), subs1[Variable("Term")])

        assertTrue(result[1].isSuccess, "Expected success")
        val subs2 = result[1].getOrNull()!!
        assertEquals(2, subs2.size, "Expected 2 substitutions")
        assertEquals(Integer(2), subs2[Variable("Position")])
        assertEquals(Atom("b"), subs2[Variable("Term")])

        assertTrue(result[2].isSuccess, "Expected success")
        val subs3 = result[2].getOrNull()!!
        assertEquals(2, subs3.size, "Expected 2 substitutions")
        assertEquals(Integer(3), subs3[Variable("Position")])
        assertEquals(Atom("c"), subs3[Variable("Term")])
    }

    @Test
    fun `arg raises error if Arg is not compound`() {
        val arg = Arg(Integer(1), Atom("foo"), Variable("X"))

        val exception = assertThrows<IllegalArgumentException> {
            arg.satisfy(emptyMap()).toList()
        }
        assertEquals("Type error: `structure' expected, found `foo' (atom)", exception.message)
    }

    @Test
    fun `arg fails silently if arg = 0`() {
        val arg = Arg(
            Integer(0),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Variable("Term")
        )

        val result = arg.satisfy(emptyMap()).toList()

        assertTrue(result.isEmpty(), "Expected no results")
    }

    @Test
    fun `arg fails silently if arg gt arity`() {
        val arg = Arg(
            Integer(4),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Variable("Term")
        )

        val result = arg.satisfy(emptyMap()).toList()

        assertTrue(result.isEmpty(), "Expected no results")
    }

    @Test
    fun `arg raises error if arg lt 0`() {
        val arg = Arg(
            Integer(-1),
            Structure(Atom("f"), listOf(Atom("a"), Atom("b"), Atom("c"))),
            Variable("Term")
        )

        val exception = assertThrows<IllegalArgumentException> {
            arg.satisfy(emptyMap()).toList()
        }
        assertEquals("Domain error: not_less_than_zero", exception.message)
    }

    @Nested
    class `Clause operator` {
        @BeforeEach
        fun setup() {
            Program.reset()
        }

        @Test
        fun `clause fact atom without variables`() {
            Program.load(listOf(Fact(Atom("foo"))))

            val result = ClauseOp(
                Atom("foo"),
                True
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertTrue(subs.isEmpty(), "Expected empty substitutions")
        }

        @Test
        fun `clause fact compound without variables`() {
            Program.load(
                listOf(
                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))))
                )
            )

            val result = ClauseOp(
                CompoundTerm(Atom("foo"), listOf(Atom("a"), Atom("b"))),
                True
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertTrue(subs.isEmpty(), "Expected empty substitutions")
        }

        @Test
        fun `clause rule without variables`() {
            Program.load(listOf(Rule(Atom("foo"), Atom("bar"))))

            val result = ClauseOp(
                Atom("foo"),
                Atom("bar")
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertTrue(subs.isEmpty(), "Expected empty substitutions")
        }

        @Test
        fun `clause fact variable body`() {
            Program.load(listOf(Fact(Atom("foo"))))

            val variable = Variable("Term")
            val result = ClauseOp(
                Atom("foo"),
                variable
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertEquals(1, subs.size, "Expected 1 substitution")
            assertEquals(True, subs[variable])
        }

        @Test
        fun `clause fact with variable head`() {
            Program.load(
                listOf(
                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a"))))
                )
            )

            val result = ClauseOp(
                CompoundTerm(Atom("foo"), listOf(Variable("X"))),
                True
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertEquals(1, subs.size, "Expected 1 substitution")
            assertEquals(Atom("a"), subs[Variable("X")])
        }

        @Test
        fun `clause rule with variable body`() {
            Program.load(listOf(Rule(Atom("foo"), Atom("bar"))))

            val result = ClauseOp(
                Atom("foo"),
                Variable("Term")
            ).satisfy(emptyMap()).toList()

            assertEquals(1, result.size, "Expected 1 result")
            assertTrue(result[0].isSuccess, "Expected success")
            val subs = result[0].getOrNull()!!
            assertEquals(1, subs.size, "Expected 1 substitution")
            assertEquals(Atom("bar"), subs[Variable("Term")])
        }

        @Test
        fun `clause fact variable value with backtracking`() {
            Program.load(
                listOf(
                    Fact(CompoundTerm(Atom("bar"), listOf(Atom("d")))),
                    Fact(CompoundTerm(Atom("bar"), listOf(Atom("e")))),
                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("a")))),
                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("b")))),
                    Fact(CompoundTerm(Atom("foo"), listOf(Atom("c")))),
                    Rule(
                        CompoundTerm(Atom("foo"), listOf(Variable("X"))),
                        CompoundTerm(Atom("bar"), listOf(Variable("X")))
                    )
                )
            )

            val x = Variable("X")
            val term = Variable("Term")

            val result = ClauseOp(
                CompoundTerm(Atom("foo"), listOf(x)),
                term
            ).satisfy(emptyMap()).toList()

            assertEquals(4, result.size, "Expected 4 results")

            assertTrue(result[0].isSuccess, "Expected success")
            val subs1 = result[0].getOrNull()!!
            assertEquals(2, subs1.size, "Expected 2 substitutions")
            assertEquals(Atom("a"), subs1[x], "Expected a")
            assertEquals(True, subs1[term], "Expected True")

            assertTrue(result[1].isSuccess, "Expected success")
            val subs2 = result[1].getOrNull()!!
            assertEquals(2, subs2.size, "Expected 2 substitutions")
            assertEquals(Atom("b"), subs2[x], "Expected b")
            assertEquals(True, subs2[term], "Expected True")

            assertTrue(result[2].isSuccess, "Expected success")
            val subs3 = result[2].getOrNull()!!
            assertEquals(2, subs3.size, "Expected 2 substitutions")
            assertEquals(Atom("c"), subs3[x], "Expected c")
            assertEquals(True, subs3[term], "Expected True")

            assertTrue(result[3].isSuccess, "Expected success")
            val subs4 = result[3].getOrNull()!!
            assertEquals(1, subs4.size, "Expected 2 substitutions")
            assertEquals(
                CompoundTerm(Atom("bar"), listOf(Variable("X"))),
                subs4[term],
                "Expected bar(X)"
            )
        }
    }
}