Data.Comp.Unification

This module implements a simple unification algorithm using compositional data types.

Documentation

type Equation f = (Term f, Term f)

This type represents equations between terms over a specific signature.

type Equations f = [Equation f]

This type represents list of equations.

data UnifError f v

This type represents errors that might occur during the unification.

Constructors

FailedOccursCheck v (Term f)

HeadSymbolMismatch (Term f) (Term f)

UnifError String

failedOccursCheck :: MonadError (UnifError f v) m => v -> Term f -> m a

This is used in order to signal a failed occurs check during unification.

headSymbolMismatch :: MonadError (UnifError f v) m => Term f -> Term f -> m a

This is used in order to signal a head symbol mismatch during unification.

appSubstEq :: (Ord v, HasVars f v, Traversable f) => Subst f v -> Equation f -> Equation f

This function applies a substitution to each term in a list of equations.

unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => Equations f -> m (Subst f v)

This function returns the most general unifier of the given equations using the algorithm of Martelli and Montanari.

data UnifyState f v

This type represents the state for the unification algorithm.

Constructors

UnifyState

Fields

• usEqs :: Equations f
• usSubst :: Subst f v

type UnifyM f v m a = StateT (UnifyState f v) m a

This is the unification monad that is used to run the unification algorithm.

runUnifyM :: MonadError (UnifError f v) m => UnifyM f v m a -> Equations f -> m (Subst f v)

This function runs a unification monad with the given initial list of equations.

withNextEq :: Monad m => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()

putEqs :: Monad m => Equations f -> UnifyM f v m ()

putBinding :: (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m ()

runUnify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => UnifyM f v m ()

unifyStep :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => Equation f -> UnifyM f v m ()