compdata-0.13.1: Compositional Data Types
Copyright(c) 2010-2011 Patrick Bahr
LicenseBSD3
MaintainerPatrick Bahr <paba@diku.dk>
Stabilityexperimental
Portabilitynon-portable (GHC Extensions)
Safe HaskellSafe-Inferred
LanguageHaskell2010

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.

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

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

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

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

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

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 #