Copyright | (c) 2010-2011 Patrick Bahr |
---|---|
License | BSD3 |
Maintainer | Patrick Bahr <paba@diku.dk> |
Stability | experimental |
Portability | non-portable (GHC Extensions) |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
This module implements a simple unification algorithm using compositional data types.
Synopsis
- type Equation f = (Term f, Term f)
- type Equations f = [Equation f]
- data UnifError f v
- = FailedOccursCheck v (Term f)
- | HeadSymbolMismatch (Term f) (Term f)
- | UnifError String
- 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, Traversable f) => Subst f v -> Equation f -> Equation f
- unify :: (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => Equations f -> m (Subst f v)
- data UnifyState f v = UnifyState {}
- 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, 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 ()
Documentation
type Equation f = (Term f, Term f) Source #
This type represents equations between terms over a specific signature.
This type represents errors that might occur during the unification.
FailedOccursCheck v (Term f) | |
HeadSymbolMismatch (Term f) (Term f) | |
UnifError String |
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.
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.
putBinding :: (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m () Source #