Safe Haskell | None |
---|---|
Language | Haskell98 |
Unification for first order terms.
Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)
- class (Monad m, IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify m a where
- type UTermOf a
- unify :: (Unify m a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a))
- unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) => [(term, term)] -> StateT (Map v term) m ()
- unify_literals :: forall lit1 lit2 atom1 atom2 v term m. (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) m ()
- unify_atoms :: (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) => (atom1, atom2) -> StateT (Map v term) m ()
- unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) => atom1 -> atom2 -> StateT (Map v term) m ()
- solve :: (IsTerm term, v ~ TVarOf term) => Map v term -> Map v term
- fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => [(term, term)] -> m (Map v term)
- unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => [(term, term)] -> m [(term, term)]
- testUnif :: Test
Documentation
class (Monad m, IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify m a where Source #
Main unification procedure. The result of unification is a mapping of variables to terms, so although we can unify two dissimilar types, they must at least have the same term type (which means the variable type will also match.) The result of unifying the two arguments is added to the state, while failure is signalled in the Failing monad.
One might think that Unify should take two type parameters, the
types of two values to be unified, but there are instances where a
single type contains both - for example, in template-haskell we
want to unify a and b in a predicate such as this: (AppT (AppT
EqualityT a) b)
.
unify :: (Unify m a, Monad m) => a -> Map (TVarOf (UTermOf a)) (UTermOf a) -> m (Map (TVarOf (UTermOf a)) (UTermOf a)) Source #
unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) => [(term, term)] -> StateT (Map v term) m () Source #
unify_literals :: forall lit1 lit2 atom1 atom2 v term m. (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify m (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) m () Source #
Unify literals, perhaps of different types, but sharing term and
variable type. Note that only one needs to be JustLiteral
, if
the unification succeeds the other must have been too, if it fails,
who cares.
unify_atoms :: (JustApply atom1, term ~ TermOf atom1, JustApply atom2, term ~ TermOf atom2, v ~ TVarOf term, PredOf atom1 ~ PredOf atom2, Monad m) => (atom1, atom2) -> StateT (Map v term) m () Source #
unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term, Monad m) => atom1 -> atom2 -> StateT (Map v term) m () Source #
solve :: (IsTerm term, v ~ TVarOf term) => Map v term -> Map v term Source #
Solve to obtain a single instantiation.
fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => [(term, term)] -> m (Map v term) Source #
Unification reaching a final solved form (often this isn't needed).