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

Instances

Error (UnifError f v)

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

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

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

unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const 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

Constructors

UnifyState

Fields

usEqs :: Equations f

usSubst :: Subst f v

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

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

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, Functor f) => (v, Term f) -> UnifyM f v m ()

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

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