Safe Haskell	Safe-Inferred
Language	Haskell2010

CoALP.Unify

Description

Unification and matching

Synopsis

Documentation

match :: (Eq a, Eq b, Eq c, Ord c) => Term a b c -> Term a b c -> Maybe (Subst a b c)

Compute the most general matcher θ for

	t1 match t2

s.t.

	θt1 = t2

unify :: (Eq a, Eq c) => Term a b c -> Term a b c -> Maybe (Subst a b c)

Compute the most general unifier θ for

t1 `unify` t2

s.t.

	θt1 = θt2

applySubst :: Eq c => Subst a b c -> Term a b c -> Term a b c

Apply substitutuon θ to a term t:

	t' = θ t

composeSubst :: (Eq a, Eq b, Eq c) => Subst a b c -> Subst a b c -> Subst a b c

Compose substitutuons σ and θ:

	 σ (θ t) = (σ composeSubst  θ) t

stripVars :: Eq c => Subst a b c -> Term a b c -> Subst a b c

Strip substitution of variables in the term

the term is usualy the head of a clause