package prolog.ast

import io.Logger
import prolog.Answers
import prolog.Substitutions
import prolog.ast.logic.Clause
import prolog.ast.logic.Predicate
import prolog.ast.logic.Resolvent
import prolog.ast.terms.Functor
import prolog.ast.terms.Goal

/**
 * Prolog Program or Database
 */
open class Database(val sourceFile: String) {
    var predicates: Map<Functor, Predicate> = emptyMap()

    /**
     * Initializes the database by running the initialization clauses of that database.
     */
    fun initialize() {
        databases.add(this)

        if (sourceFile !== "") {
            Logger.debug("Moving clauses from $sourceFile to main database")
            predicates.filter { it.key != "/_" }
                .forEach { (_, predicate) -> db.load(predicate, force = true) }
        }

        Logger.info("Initializing database from $sourceFile")
        if (predicates.contains("/_")) {
            Logger.debug("Loading clauses from /_ predicate")
            predicates["/_"]?.clauses?.forEach {
                Logger.debug("Loading clause $it")
                val goal = it.body as Goal
                goal.satisfy(emptyMap()).toList()
            }
        }
    }

    /**
     * Loads a list of clauses into the program.
     *
     * @param clauses The list of clauses to load.
     * @param index The index at which to insert the clause. If null, the clause is added to the end of the list.
     * @param force If true, the clause is added even if the predicate is static.
     */
    fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) {
        for (clause in clauses) {
            val functor = clause.functor
            val predicate = predicates[functor]

            if (predicate != null) {
                // If the predicate already exists, add the clause to it
                predicate.add(clause, index, force)
            } else {
                // If the predicate does not exist, create a new one, usually during Program execution, so dynamic.
                predicates += Pair(functor, Predicate(listOf(clause), dynamic = true))
            }

            Logger.debug("Loaded clause $clause into predicate $functor")
        }
    }

    fun load(predicate: Predicate, force: Boolean = false) {
        val functor = predicate.functor
        val existingPredicate = predicates[functor]

        if (existingPredicate != null) {
            // If the predicate already exists, add the clauses to it
            existingPredicate.addAll(predicate.clauses)
        } else {
            // If the predicate does not exist, create a new one
            predicates += Pair(functor, predicate)
        }
    }

    fun clear() {
        if (sourceFile == "") {
            Logger.debug("Clearing main database")
            predicates = emptyMap()
            return
        }

        Logger.debug("Clearing database $sourceFile")
        // Remove our clauses from the database
        predicates.forEach { (_, predicate) ->
            val dbPredicate = db.predicates[predicate.functor]
            predicate.clauses.forEach { clause -> dbPredicate?.clauses?.remove(clause) }
        }
        databases.remove(this)
    }

    /**
     * Object to handle execution
     *
     * This object is a singleton that manages a list of databases.
     */
    companion object Program : Resolvent {
        var db = Database("")
        var databases: MutableList<Database> = mutableListOf(db)
        var storeNewLine: Boolean = false
        var variableRenamingStart: Int = 0

        /**
         * Queries the program with a goal.
         * @return true if the goal can be proven, false otherwise.
         */
        fun query(goal: Goal): Answers = solve(goal, emptyMap())

        override fun solve(goal: Goal, subs: Substitutions): Answers {
            val functor = goal.functor
            // If the predicate does not exist, return false
            val predicate = db.predicates[functor] ?: return emptySequence()
            // If the predicate exists, evaluate the goal against it
            return predicate.solve(goal, subs)
        }

        fun consult(database: Database) = database.initialize()
        fun disregard(database: Database) = database.clear()

        fun load(clauses: List<Clause>, index: Int? = null, force: Boolean = false) = db.load(clauses, index, force)

        fun reset() {
            databases.toList().map { it.clear() }
            variableRenamingStart = 0
            storeNewLine = false
        }
    }
}