compdata-0.6.1.4: Compositional Data Types

Portabilitynon-portable (GHC Extensions)
Stabilityexperimental
MaintainerPatrick Bahr <paba@diku.dk>
Safe HaskellNone

Data.Comp.Unification

Description

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

Synopsis

Documentation

type Equation f = (Term f, Term f)Source

This type represents equations between terms over a specific signature.

type Equations f = [Equation f]Source

This type represents list of equations.

data UnifError f v Source

This type represents errors that might occur during the unification.

Instances

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

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

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

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 fSource

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)Source

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

data UnifyState f v Source

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 aSource

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)Source

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 ()Source

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

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

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

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