| Copyright | (c) 2010-2011 Patrick Bahr |
|---|---|
| License | BSD3 |
| Maintainer | Patrick Bahr <[email protected]> |
| Stability | experimental |
| Portability | non-portable (GHC Extensions) |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Comp.Unification
Description
This module implements a simple unification algorithm using compositional data types.
Synopsis
- type Equation (f :: Type -> Type) = (Term f, Term f)
- type Equations (f :: Type -> Type) = [Equation f]
- data UnifError (f :: Type -> Type) v
- = FailedOccursCheck v (Term f)
- | HeadSymbolMismatch (Term f) (Term f)
- | UnifError String
- failedOccursCheck :: forall (f :: Type -> Type) v m a. MonadError (UnifError f v) m => v -> Term f -> m a
- headSymbolMismatch :: forall (f :: Type -> Type) v m a. MonadError (UnifError f v) m => Term f -> Term f -> m a
- appSubstEq :: forall v (f :: Type -> Type). (Ord v, HasVars f v, Traversable f) => Subst f v -> Equation f -> Equation f
- unify :: forall (f :: Type -> Type) v m. (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => Equations f -> m (Subst f v)
- data UnifyState (f :: Type -> Type) v = UnifyState {}
- type UnifyM (f :: Type -> Type) v (m :: Type -> Type) a = StateT (UnifyState f v) m a
- runUnifyM :: forall (f :: Type -> Type) v m a. MonadError (UnifError f v) m => UnifyM f v m a -> Equations f -> m (Subst f v)
- withNextEq :: forall (m :: Type -> Type) (f :: Type -> Type) v. Monad m => (Equation f -> UnifyM f v m ()) -> UnifyM f v m ()
- putEqs :: forall (m :: Type -> Type) (f :: Type -> Type) v. Monad m => Equations f -> UnifyM f v m ()
- putBinding :: forall (m :: Type -> Type) v (f :: Type -> Type). (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m ()
- runUnify :: forall (f :: Type -> Type) v (m :: Type -> Type). (MonadError (UnifError f v) m, Decompose f v, Ord v, Eq (Const f), Traversable f) => UnifyM f v m ()
- unifyStep :: forall (f :: Type -> Type) v (m :: Type -> Type). (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 :: Type -> Type) = (Term f, Term f) Source #
This type represents equations between terms over a specific signature.
data UnifError (f :: Type -> Type) v Source #
This type represents errors that might occur during the unification.
Constructors
| FailedOccursCheck v (Term f) | |
| HeadSymbolMismatch (Term f) (Term f) | |
| UnifError String |
failedOccursCheck :: forall (f :: Type -> Type) v m a. 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 :: forall (f :: Type -> Type) v m a. 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 :: forall v (f :: Type -> Type). (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 :: forall (f :: Type -> Type) v m. (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 :: Type -> Type) v Source #
This type represents the state for the unification algorithm.
Constructors
| UnifyState | |
type UnifyM (f :: Type -> Type) v (m :: Type -> Type) a = StateT (UnifyState f v) m a Source #
This is the unification monad that is used to run the unification algorithm.
runUnifyM :: forall (f :: Type -> Type) v m a. 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 :: forall (m :: Type -> Type) (f :: Type -> Type) v. Monad m => (Equation f -> UnifyM f v m ()) -> UnifyM f v m () Source #
putEqs :: forall (m :: Type -> Type) (f :: Type -> Type) v. Monad m => Equations f -> UnifyM f v m () Source #
putBinding :: forall (m :: Type -> Type) v (f :: Type -> Type). (Monad m, Ord v, HasVars f v, Traversable f) => (v, Term f) -> UnifyM f v m () Source #