Data.Logic.ATP.Unif

Unification for first order terms.

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

Documentation

class (TermOf a ~ TermOf b) => Unify a b where

Main unification procedure.

Methods

unify :: a -> b -> StateT (Map (TVarOf (TermOf a)) (TermOf a)) Failing ()

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

Instances

Unify SkAtom SkAtom

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

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, v ~ TVarOf term) => lit1 -> lit2 -> StateT (Map v term) Failing ()

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) => (atom1, atom2) -> StateT (Map v term) Failing ()

unify_atoms_eq :: (HasEquate atom1, term ~ TermOf atom1, HasEquate atom2, term ~ TermOf atom2, PredOf atom1 ~ PredOf atom2, v ~ TVarOf term) => atom1 -> atom2 -> 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