package prolog.builtins

import org.junit.jupiter.api.Assertions.*
import org.junit.jupiter.api.Test
import org.junit.jupiter.api.assertThrows
import prolog.Substitutions
import prolog.ast.terms.Integer
import prolog.ast.terms.Term
import prolog.ast.terms.Variable
import prolog.logic.equivalent

class ArithmeticOperatorsTests {
    @Test
    fun `1 evaluates to 1`() {
        val op1 = EvaluatesTo(
            Integer(1),
            Integer(1)
        )

        var result = op1.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "1 should be equal to 1")
        assertTrue(result[0].isSuccess, "1 should be equal to 1")
        val subs = result[0].getOrNull()!!
        assertTrue(subs.isEmpty(), "1 should not be rebound")

        val op2 = EvaluatesToDifferent(
            Integer(1),
            Integer(1)
        )

        result = op2.satisfy(emptyMap()).toList()

        assertEquals(0, result.size, "1 should not be different from 1")
    }

    @Test
    fun `1 does not evaluate to 2`() {
        val op1 = EvaluatesTo(
            Integer(1),
            Integer(2)
        )

        var result = op1.satisfy(emptyMap()).toList()

        assertEquals(0, result.size, "1 should not be equal to 2")

        val op2 = EvaluatesToDifferent(
            Integer(1),
            Integer(2)
        )

        result = op2.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "1 should be different from 2")
        assertTrue(result[0].isSuccess, "1 should be different from 2")
        val subs = result[0].getOrNull()!!
        assertTrue(subs.isEmpty(), "1 should not be rebound")
    }

    @Test
    fun `2 + 3 evaluates to 5`() {
        val op = EvaluatesTo(
            Add(Integer(2), Integer(3)),
            Integer(5)
        )

        var result = op.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "2 + 3 should be equal to 5")
        assertTrue(result[0].isSuccess, "2 + 3 should be equal to 5")
        val subs = result[0].getOrNull()!!
        assertTrue(subs.isEmpty(), "2 + 3 should not be rebound")

        val op2 = EvaluatesToDifferent(
            Add(Integer(2), Integer(3)),
            Integer(5)
        )

        result = op2.satisfy(emptyMap()).toList()

        assertEquals(0, result.size, "2 + 3 should not be different from 5")
    }

    @Test
    fun `2 + 3 evaluates to 4 + 1`() {
        val op = EvaluatesTo(
            Add(Integer(2), Integer(3)),
            Add(Integer(4), Integer(1))
        )

        var result = op.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "2 + 3 should be equal to 4 + 1")
        assertTrue(result[0].isSuccess, "2 + 3 should be equal to 4 + 1")
        val subs = result[0].getOrNull()!!
        assertTrue(subs.isEmpty(), "2 + 3 should not be rebound")

        val op2 = EvaluatesToDifferent(
            Add(Integer(2), Integer(3)),
            Add(Integer(4), Integer(1))
        )

        result = op2.satisfy(emptyMap()).toList()

        assertEquals(0, result.size, "2 + 3 should not be different from 4 + 1")
    }

    @Test
    fun `1 evaluates to variable not sufficiently instantiated`() {
        val op = EvaluatesTo(
            Integer(1),
            Variable("X")
        )

        var result = op.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "One exception should be thrown")
        assertTrue(result[0].isFailure, "One exception should be thrown")
        var exceptions = result[0].exceptionOrNull()
        assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")

        val op2 = EvaluatesToDifferent(
            Integer(1),
            Variable("X")
        )

        result = op2.satisfy(emptyMap()).toList()

        assertEquals(1, result.size, "One exception should be thrown")
        assertTrue(result[0].isFailure, "One exception should be thrown")
        exceptions = result[0].exceptionOrNull()
        assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
    }

    @Test
    fun `(1 + var) evaluates to 1 not sufficiently instantiated`() {
        val op = EvaluatesTo(
            Add(Integer(1), Variable("X")),
            Integer(1)
        )

        assertThrows<IllegalArgumentException> { op.satisfy(emptyMap()) }

        val op2 = EvaluatesToDifferent(
            Add(Integer(1), Variable("X")),
            Integer(1)
        )

        assertThrows<IllegalArgumentException> { op2.satisfy(emptyMap()) }
    }

    @Test
    fun `1 is 1`() {
        val op = Is(
            Integer(1),
            Integer(1)
        )

        val result = op.satisfy(emptyMap())

        assertTrue(result.any(), "1 should be equal to 1")
    }

    @Test
    fun `1 is not 2`() {
        val op = Is(
            Integer(1),
            Integer(2)
        )

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

        assertTrue(result.isEmpty(), "1 should not be equal to 2")
    }

    @Test
    fun `bound-to-1-var is 1`() {
        val t1 = Variable("X")
        val op = Is(
            t1,
            Integer(1)
        )

        val result = op.satisfy(mapOf(t1 to Integer(1))).toList()

        assertEquals(1, result.size, "X should be equal to 1")
        assertTrue(result.first().isSuccess, "X should be equal to 1")
        assertTrue(result.first().getOrNull()!!.isEmpty(), "X should not be rebound")
    }

    @Test
    fun `bound-to-2-var is not 1`() {
        val t1 = Variable("X")
        val op = Is(
            t1,
            Integer(1)
        )

        val result = op.satisfy(mapOf(t1 to Integer(2)))

        assertFalse(result.any(), "X should not be equal to 1")
    }

    @Test
    fun `variable is 1`() {
        val op = Is(
            Variable("X"),
            Integer(1)
        )

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

        assertFalse(result.isEmpty(), "X should be equal to 1")
        assertTrue(result.first().isSuccess, "X should be equal to 1")
        assertEquals(1, result[0].getOrNull()!!.size, "X should be rebound")
        assertTrue(equivalent(Integer(1), result[0].getOrNull()!![Variable("X")]!!, emptyMap()), "X should be equal to 1")
    }

    @Test
    fun `variable is 1 + 2`() {
        val op = Is(
            Variable("X"),
            Add(Integer(1), Integer(2))
        )

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

        assertFalse(result.isEmpty(), "X should be equal to 3")
        assertTrue(result.first().isSuccess, "X should be equal to 3")

        val subs = result[0].getOrNull()!!

        assertEquals(1, subs.size, "X should be rebound")
        assertTrue(
            equivalent(Integer(3), subs[Variable("X")]!!, emptyMap()),
            "X should be equal to 3"
        )
    }

    @Test
    fun `var is var should throw`() {
        val op = Is(
            Variable("X"),
            Variable("Y")
        )

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

        assertEquals(1, result.size, "One exception should be thrown")
        assertTrue(result[0].isFailure, "One exception should be thrown")
        val exceptions = result[0].exceptionOrNull()
        assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
    }

    @Test
    fun `1 is var should throw`() {
        val op = Is(
            Integer(1),
            Variable("X")
        )

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

        assertEquals(1, result.size, "One exception should be thrown")
        assertTrue(result[0].isFailure, "One exception should be thrown")
        val exceptions = result[0].exceptionOrNull()
        assertTrue(exceptions is IllegalArgumentException, "One exception should be thrown")
    }

    /**
     * ?- X = 1, Y = 1 + 2, X is Y.
     * false.
     */
    @Test
    fun `var is bound-to-sum-var`() {
        val t1 = Variable("X")
        val t2 = Variable("Y")

        val op = Is(t1, t2)
        val map: Substitutions = mapOf(t1 to Integer(1), t2 to Add(Integer(1), Integer(2)))

        val result = op.satisfy(map).toList()

        assertEquals(0, result.size, "X should not be equal to Y")
    }

    /**
     * ?- between(1, 2, X), Y is 1 + X.
     * X = 1, Y = 2 ;
     * X = 2, Y = 3 .
     */
    @Test
    fun `between 1 and 2 plus 1 to get 2 and 3`() {
        val t1 = Integer(1)
        val t2 = Integer(2)
        val t3 = Variable("X")
        val t4 = Variable("Y")

        val op = Conjunction(
            Between(t1, t2, t3),
            Is(t4, Add(Integer(1), t3))
        )
    }

    @Test
    fun `negate 1 to get -1`() {
        val t1 = Integer(1)

        val result = Negate(t1).simplify(emptyMap())

        assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1")
    }

    @Test
    fun `negate 0 to get 0`() {
        val t1 = Integer(0)

        val result = Negate(t1).simplify(emptyMap())

        assertEquals(Integer(0), result.to, "negate(0) should be equal to 0")
    }

    @Test
    fun `negate -1 to get 1`() {
        val t1 = Integer(-1)

        val result = Negate(t1).simplify(emptyMap())

        assertEquals(Integer(1), result.to, "negate(-1) should be equal to 1")
    }

    @Test
    fun `negate bound-to-1-var to get -1`() {
        val t1 = Variable("X")

        val map: Substitutions = mapOf(t1 to Integer(1))

        val result = Negate(t1).simplify(map)

        assertEquals(Integer(-1), result.to, "negate(1) should be equal to -1")
    }

    @Test
    fun `negate 1 + 3 to get -4`() {
        val t1 = Integer(1)
        val t2 = Integer(3)

        val result = Negate(Add(t1, t2)).simplify(emptyMap())

        assertEquals(Integer(-4), result.to, "negate(1 + 3) should be equal to -4")
    }

    @Test
    fun `Add 1 and 2 to get 3`() {
        val t1 = Integer(1)
        val t2 = Integer(2)

        val result = Add(t1, t2).simplify(emptyMap())

        assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3")
    }

    @Test
    fun `Add 1 and bound-to-2-var to get 3`() {
        val t1 = Integer(1)
        val t2 = Variable("X")

        val subs: Substitutions = mapOf(t2 to Integer(2))
        val result = Add(t1, t2).simplify(subs)

        assertEquals(Integer(3), result.to, "1 + 2 should be equal to 3")
    }

    @Test
    fun `Subtract 1 and 2 to get -1`() {
        val t1 = Integer(1)
        val t2 = Integer(2)

        val result = Subtract(t1, t2).simplify(emptyMap())

        assertEquals(Integer(-1), result.to, "1 - 2 should be equal to -1")
    }

    @Test
    fun `Subtract 3 and 1 to get 2`() {
        val t1 = Integer(3)
        val t2 = Integer(1)

        val result = Subtract(t1, t2).simplify(emptyMap())

        assertEquals(Integer(2), result.to, "3 - 1 should be equal to 2")
    }

    @Test
    fun `Multiply 0 and 0 to get 0`() {
        val t1 = Integer(0)
        val t2 = Integer(0)

        val result = Multiply(t1, t2).simplify(emptyMap())

        assertEquals(Integer(0), result.to, "0 * 0 should be equal to 0")
    }

    @Test
    fun `Multiply 1 and 0 to get 0`() {
        val t1 = Integer(1)
        val t2 = Integer(0)

        val result = Multiply(t1, t2).simplify(emptyMap())

        assertEquals(Integer(0), result.to, "1 * 0 should be equal to 0")
    }

    @Test
    fun `Multiply 0 and 1 to get 0`() {
        val t1 = Integer(0)
        val t2 = Integer(1)

        val result = Multiply(t1, t2).simplify(emptyMap())

        assertEquals(Integer(0), result.to, "0 * 1 should be equal to 0")
    }

    @Test
    fun `Multiply 3 and 1 to get 3`() {
        val t1 = Integer(3)
        val t2 = Integer(1)

        val result = Multiply(t1, t2).simplify(emptyMap())

        assertEquals(Integer(3), result.to, "3 * 1 should be equal to 3")
    }

    @Test
    fun `Multiply 2 and 3 to get 6`() {
        val t1 = Integer(2)
        val t2 = Integer(3)

        val result = Multiply(t1, t2).simplify(emptyMap())

        assertEquals(Integer(6), result.to, "2 * 3 should be equal to 6")
    }
}