LogicProgrammingScopeWithUnification
Adds unification-related DSL sugar to LogicProgrammingScopeWithUnificator: every Unificator operation gets an overload accepting plain Any operands (auto-toTerm-ed, exactly like the rest of the :dsl-core DSL), plus infix aliases mirroring it.unibo.tuprolog.unify.Unificator.Companion's own Term-only infix functions (it.unibo.tuprolog.unify.Unificator.Companion.mguWith, it.unibo.tuprolog.unify.Unificator.Companion.matches, it.unibo.tuprolog.unify.Unificator.Companion.unifyWith) but resolved against this scope's unificator instead of always Unificator.default:
logicProgramming {
val x = varOf("X")
x matches "a" // true -- equivalent to unificator.match(x, atomOf("a"))
val substitution = x mguWith "a" // {X = a}, an [Substitution.Unifier]
x unifyWith "a" // a, the [Term] resulting from applying the mgu to `x`
}All three infix functions, as well as the Any-accepting mgu/match/unify overloads, perform unification with occurs-check enabled; call mgu/match/unify directly (optionally passing occurCheckEnabled = false) for finer control.
Type Parameters
the concrete, self-referential scope type (see it.unibo.tuprolog.dsl.BaseLogicProgrammingScope).
Inheritors
Properties
Functions
Creates a copy of this scope, backed by the same it.unibo.tuprolog.core.Scope, using unificator instead of the current one.
Overload of Unificator.match accepting plain values instead of Terms: term1 and term2 are auto-toTerm-ed before delegating to this scope's unificator.
Overload of Unificator.mgu accepting plain values instead of Terms: term1 and term2 are auto-toTerm-ed before delegating to this scope's unificator, so e.g. raw Strings, numbers or already-built Terms can be mixed freely.
Infix alias of mgu for Any operands: computes the Most General Unifier of this and other (both auto-toTerm-ed), with occurs-check enabled, using this scope's unificator.
Overload of Unificator.unify accepting plain values instead of Terms: term1 and term2 are auto-toTerm-ed before delegating to this scope's unificator.