A substitution: which logic variables are bound to which terms so
far, opaque outside this module. unify/4 is the whole unification
algorithm -- standard, recursive, structural unification with no
occurs-check (matches ISO Prolog's own default: X = f(X) succeeds,
building a cyclic term, rather than failing or looping to detect the
cycle -- occurs-check is opt-in in real Prolog too, via unify_with_occurs_check/2,
never the default).
Every function takes a term_module argument (an
Ichor.Backtrack.Term implementation) explicitly, so this module
never needs to know what a caller's own term representation looks
like.
Summary
Functions
Extends bindings, binding var_id to value.
An empty substitution.
Follows variable bindings until reaching either an unbound variable
or a non-variable term -- shallow dereferencing only (never recurses
into a compound term's own arguments), matching Prolog's own deref.
Unifies a and b under bindings, extending them on success.
Two distinct (by var_id/1) unbound variables unify by binding one
to the other; an unbound variable and anything else unify by binding
the variable; two compound terms unify when their functor and arity
match and every argument pairwise unifies; anything else unifies with
plain ==/2.
Like unify/4, but with an occurs-check: a variable is never allowed
to bind to a compound term containing itself, which would otherwise
silently build an infinite term (X = f(X)). unify/4's own absence
of this matches ISO Prolog's own default, not what a type checker
needs -- Ichor.Toolkit.TypeScheme is built on this variant
specifically because unifying two types this way must fail (not loop
forever, not silently accept an infinite type) when one contains a
variable already bound to (or literally equal to) the other.
Types
Functions
Extends bindings, binding var_id to value.
@spec new() :: t()
An empty substitution.
Follows variable bindings until reaching either an unbound variable
or a non-variable term -- shallow dereferencing only (never recurses
into a compound term's own arguments), matching Prolog's own deref.
Unifies a and b under bindings, extending them on success.
Two distinct (by var_id/1) unbound variables unify by binding one
to the other; an unbound variable and anything else unify by binding
the variable; two compound terms unify when their functor and arity
match and every argument pairwise unifies; anything else unifies with
plain ==/2.
Like unify/4, but with an occurs-check: a variable is never allowed
to bind to a compound term containing itself, which would otherwise
silently build an infinite term (X = f(X)). unify/4's own absence
of this matches ISO Prolog's own default, not what a type checker
needs -- Ichor.Toolkit.TypeScheme is built on this variant
specifically because unifying two types this way must fail (not loop
forever, not silently accept an infinite type) when one contains a
variable already bound to (or literally equal to) the other.