package prolog.builtins

import prolog.Answers
import prolog.Substitutions
import prolog.ast.Database.Program
import prolog.ast.arithmetic.Integer
import prolog.ast.terms.*
import prolog.ast.logic.Clause
import prolog.logic.*

/**
 * [True] when [Term] is a term with [Functor] Name/Arity.
 *
 * If Term is a [Variable] it is unified with a new term whose arguments are all different variables.
 * If Term is [atomic], Arity will be unified with the integer 0, and Name will be unified with Term.
 */
class FunctorOp(private val term: Term, private val functorName: Term, private val functorArity: Term) :
    Structure(Atom("functor"), listOf(term, functorName, functorArity)) {
    override fun satisfy(subs: Substitutions): Answers {
        return when {
            nonvariable(term, subs) -> {
                val t = applySubstitution(term, subs) as Head

                Conjunction(
                    Unify(t.functor.arity, functorArity),
                    Unify(t.functor.name, functorName)
                ).satisfy(subs)
            }

            variable(term, subs) -> {
                require(atomic(functorName, subs) && atomic(functorArity, subs)) {
                    "Arguments are not sufficiently instantiated"
                }

                val name = applySubstitution(functorName, subs) as Atom
                val arity = applySubstitution(functorArity, subs) as Integer
                val result = Structure(name, List(arity.value) { AnonymousVariable.create() })
                sequenceOf(Result.success(mapOf(term to result)))
            }

            else -> throw IllegalStateException()
        }
    }

    override fun applySubstitution(subs: Substitutions): FunctorOp = FunctorOp(
        term.applySubstitution(subs),
        functorName.applySubstitution(subs),
        functorArity.applySubstitution(subs)
    )
}

class Arg(private val arg: Term, private val term: Term, private val value: Term) :
    Structure(Atom("arg"), listOf(arg, term, value)) {
    override fun satisfy(subs: Substitutions): Answers = sequence {
        require(nonvariable(term, subs)) { "Arguments are not sufficiently instantiated" }
        require(compound(term, subs)) {
            val expected = CompoundTerm::class.simpleName?.lowercase()
            val actual = term::class.simpleName?.lowercase()
            "Type error: `$expected' expected, found `$term' ($actual)"
        }

        val t = applySubstitution(term, subs) as Structure

        when {
            variable(arg, subs) -> {
                // Value will be unified with the successive arguments of term.
                // On successful unification, arg is unified with the argument number.
                // Backtracking yields alternative solutions.
                var count = 0
                for (argument in t.arguments) {
                    unifyLazy(value, argument, subs).forEach { result ->
                        result.map {
                            val sub = arg to Integer(count + 1)
                            yield(Result.success(it + sub))
                        }
                    }
                    count++
                }

            }

            else -> {
                val a = applySubstitution(arg, subs) as Integer

                require(0 <= a.value) { "Domain error: not_less_than_zero" }

                // Fail silently if the argument is out of bounds
                if (0 == a.value || t.arguments.size < a.value) {
                    return@sequence
                }

                val argument = t.arguments[a.value - 1]
                yieldAll(unifyLazy(argument, value, subs))
            }
        }
    }
}

/**
 * [True] if [Head] can be unified with a [Clause] and [Body] with the corresponding Clause Body.
 *
 * Gives alternative clauses on backtracking. For facts, Body is unified with the atom [True].
 *
 * When accessing builtins (static predicates, private procedures), the program will act as if the builtins do not
 * exist. Head can only match with dynamic or imported predicates.
 *
 * [SWI-Prolog Operator clause/2](https://www.swi-prolog.org/pldoc/doc_for?object=clause/2)
 */
class ClauseOp(private val head: Head, private val body: Body) :
    Structure(Atom("clause"), listOf(head, body)) {
    override fun satisfy(subs: Substitutions): Answers = sequence {
        require(nonvariable(head, subs)) { "Arguments are not sufficiently instantiated" }

        val predicate = Program.db.predicates[head.functor]

        if (predicate != null) {
            for (clause in predicate.clauses) {
                val clauseHead = clause.head
                val clauseBody = clause.body

                // Unify the head of the clause with the head of the goal
                unifyLazy(clauseHead, head, subs).forEach { result ->
                    result.map { headSubs ->
                        // Unify the body of the clause with the body of the goal
                        unifyLazy(clauseBody, body, headSubs).forEach { bodyResult ->
                            bodyResult.map { bodySubs ->
                                // Combine the substitutions from the head and body
                                val combinedSubs = headSubs + bodySubs
                                yield(Result.success(combinedSubs))
                            }
                        }
                    }
                }
            }
        } else {
            yield(Result.success(emptyMap()))
        }
    }
}