Data.Logic.ATP.Unif

Unification for first order terms.

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

Documentation

class Unify a v term where

Main unification procedure.

Methods

unify :: a -> a -> StateT (Map v term) Failing ()

Unify the two elements of a pair, collecting variable assignments in the state.

Instances

Unify SkAtom V SkTerm

Unify a v term => Unify [a] v term

Unify a v term => Unify (Seq a) v term

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

unify_literals :: (IsLiteral lit, HasApply atom, Unify atom v term, atom ~ AtomOf lit, term ~ TermOf atom, v ~ TVarOf term) => lit -> lit -> StateT (Map v term) Failing ()

Unify literals

unify_atoms :: (JustApply atom, term ~ TermOf atom, v ~ TVarOf term) => (atom, atom) -> StateT (Map v term) Failing ()

unify_atoms_eq :: (HasEquate atom, term ~ TermOf atom, v ~ TVarOf term) => atom -> atom -> StateT (Map v term) Failing ()

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) => [(term, term)] -> Failing (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) => [(term, term)] -> Failing [(term, term)]

Examples.

testUnif :: Test