Library for specifying the unification on first-order terms.
This library implements a general unification algorithm. Because the algorithm is easy to understand, but rather slow, it serves as a specification for more elaborate implementations.
Author: Michael Hanus, Jan-Hendrik Matthes, Jonas Oberschweiber, Bjoern Peemoeller
Version: February 2020
showUnificationError
:: (a -> String) -> UnificationError a -> String
Transforms a unification error into a string representation. |
unify
:: (Eq a, Show a) => [(Term a,Term a)] -> Either (UnificationError a) (Map Int (Term a))
Unifies a list of term equations. |
unifiable
:: (Eq a, Show a) => [(Term a,Term a)] -> Bool
Checks whether a list of term equations can be unified. |
Representation of a unification error, parameterized over the kind of function symbols, e.g., strings.
Constructors:
Clash
:: (Term a) -> (Term a) -> UnificationError a
: The constructor term t1
is supposed to be equal
to the constructor term t2
but has a different
constructor.
OccurCheck
:: VarIdx -> (Term a) -> UnificationError a
: The variable v
is supposed to be equal to the
term t
in which it occurs as a subterm.
Transforms a unification error into a string representation. |