Data.Logic.ATP.Unif

Unification for first order terms.

Copyright (c) 2003-2007, John Harrison. (See "LICENSE.txt" for details.)

Documentation

class (IsTerm (UTermOf a), IsVariable (TVarOf (UTermOf a))) => Unify a where

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

Associated Types

type UTermOf a

Methods

unify :: Monad m => a -> StateT (Map (TVarOf (UTermOf a)) (UTermOf a)) m ()

Instances

Unify (SkAtom, SkAtom)

unify_terms :: (IsTerm term, v ~ TVarOf term, Monad m) => [(term, term)] -> StateT (Map v term) m ()

unify_literals :: (IsLiteral lit1, HasApply atom1, atom1 ~ AtomOf lit1, term ~ TermOf atom1, JustLiteral lit2, HasApply atom2, atom2 ~ AtomOf lit2, term ~ TermOf atom2, Unify (atom1, atom2), term ~ UTermOf (atom1, atom2), v ~ TVarOf term, Monad m) => lit1 -> lit2 -> StateT (Map v term) m ()

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

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, f ~ FunOf term) => Map v term -> Map v term

Solve to obtain a single instantiation.

fullunify :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => [(term, term)] -> m (Map v term)

Unification reaching a final solved form (often this isn't needed).

unify_and_apply :: (IsTerm term, v ~ TVarOf term, f ~ FunOf term, Monad m) => [(term, term)] -> m [(term, term)]

Examples.

testUnif :: Test