AbstractUnificator

Skeletal Unificator implementation, providing a complete, equation-based unification algorithm (in the style of Martelli & Montanari's): both mgu and merge repeatedly decompose their operands into Equations and simplify them (structurally comparing Terms, applying resulting variable assignments to the remaining equations) until either a contradiction is found (failure) or no equation can be simplified further (success).

The only decision left to subclasses is checkTermsEquality, namely how two non-variable Terms are compared while building equations — this is exactly what distinguishes Unificator.strict from Unificator.naive. Subclasses that additionally need to observe or alter the equation-solving process itself (e.g. to reject some equations based on custom criteria, or to inspect the final result) may also override handleEquation and/or handleResult; both default to the identity function and thus have no effect unless overridden.

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

Parameters