Implement a custom Unificator

How to change the way two Terms are compared during unification, and how to control occurs-check, using the unify module's Unificator API.

This is a usage recipe; see the Explanation section for the rationale behind pluggable unification strategies.

1. Use a built-in strategy

Unificator's companion object ships two ready-made strategies:

        term1: Term,
        term2: Term,
    ): Boolean = match(term1, term2, true)

• Unificator.default (an alias for strict()) compares terms with plain Term.equals.
• Unificator.naive() behaves like strict(), except it compares numbers by their numeric value rather than their exact representation (so 1 and 1.0 can be considered equal).

val strict = Unificator.strict()
val naive = Unificator.naive()

val substitution = strict.mgu(term1, term2)

Both factory methods accept an optional starting context: Substitution of pre-existing bindings to unify against:

val context: Substitution = Substitution.of(Var.of("X") to Atom.of("a"))
val strictWithContext = Unificator.strict(context)

2. Disable occurs-check for a single call

mgu, match, and unify all accept an occurCheckEnabled: Boolean parameter (true by default):

 *   that same variable (which would otherwise produce an infinite/cyclic term); disabling it trades soundness for
 *   speed, which is safe only when the caller already knows the operands cannot give rise to such a cycle.
 *
 * When the operands have distinct semantic roles, the subject term (such as a goal, query, actual value, or sought
 * item) should be passed first, and the reference term (such as a pattern, rule head, expected value, or stored
 * candidate) second. Calls whose operands have no such roles may retain their natural or mathematical order.
 *

val unificator = Unificator.default
val substitution = unificator.mgu(term1, term2, occurCheckEnabled = false)

The infix operators mguWith, matches, and unifyWith always perform occurs-check, since they delegate to Unificator.default; use the explicit method calls above if you need to disable it.

3. Implement a custom unification strategy

Subclass AbstractUnificator and override checkTermsEquality, which decides whether two terms are considered equal while building the unification equations. For reference, this is how the built-in naive() strategy implements value-based comparison of numbers:

    ): Term? = unify(term1, term2, true)

    /**
     * Merges [substitution1] and [substitution2] into a single [Substitution], as if their bindings had been
     * collected while unifying two terms piecewise (e.g. argument by argument): equal-variable bindings from both
     * sides are unified against each other and, optionally, checked for occurrence, rather than simply overwritten.
     *
     * @return the merged [Substitution], or [Substitution.failed] if [substitution1] and [substitution2] disagree
     * on some variable's binding (or either of them, or [context], is already failed).
     */
    @JsName("mergeWithOccurCheck")
    fun merge(
        substitution1: Substitution,
        substitution2: Substitution,
        occurCheckEnabled: Boolean,
    ): Substitution

Follow the same pattern for your own strategy — for instance, comparing atoms case-insensitively:

import it.unibo.tuprolog.core.Term
import it.unibo.tuprolog.unify.AbstractUnificator

val caseInsensitive =
    object : AbstractUnificator() {
        override fun checkTermsEquality(
            first: Term,
            second: Term,
        ): Boolean =
            when {
                first.isAtom && second.isAtom ->
                    first.castToAtom().value.equals(second.castToAtom().value, ignoreCase = true)
                else -> first == second
            }
    }

caseInsensitive.match(Atom.of("Foo"), Atom.of("foo")) // true

AbstractUnificator() (no-arg) starts from an empty context; pass a Substitution to the constructor if you need a starting context, same as the built-in factories.

4. Add caching, if needed

Any Unificator — built-in or custom — can be wrapped to cache its results (LRU, capacity 32 by default):

        @JsName("unifyWith")
        infix fun Term.unifyWith(other: Term): Term? = default.unify(this, other)

        /** Merges [this] and [other], using the [default] unification strategy. */
        @JvmStatic
        @JsName("mergeWith")
        infix fun Substitution.mergeWith(other: Substitution): Substitution = default.merge(this, other)

        /**
         * Creates a naive unification strategy, with the given starting [context], that checks [Term]s' equality
         * through [Term.equals], except for numeric terms which are compared *by value* rather than by exact

val cached = Unificator.cached(caseInsensitive)
val smallerCache = Unificator.cached(caseInsensitive, capacity = 5)

Wrapping an already-cached Unificator again just re-wraps the original with the new capacity, instead of double-caching.