Data.Rewriting.Substitution.Unify

Documentation

unify :: (Eq f, Ord v) => Term f v -> Term f v -> Maybe (Subst f v)

Unify two terms. If unification succeeds, return a most general unifier of the given terms. We have the following property:

unify t u == Just s   ==>   apply s t == apply s u

O(n log(n)), where n is the apparent size of the arguments. Note that the apparent size of the result may be exponential due to shared subterms.

unifyRef :: (Eq f, Ord v) => Term f v -> Term f v -> Maybe (Subst f v)

Unify two terms. This is a simple implementation for testing purposes, and may be removed in future versions of this library.