# Unification

Plain source file: base/TI/Unification.hs (2004-12-06)

Unification is imported by: TiFunDeps, TiGeneralize, TiInstanceDB, TiKinds, TiSolve.

Generic unification and matching

```module Unification where
import Maybe(fromMaybe)
import List(nub)
import MUtils(mapFst,mapSnd,mapBoth,apBoth)

```

Term types to be unified (or matched) must be instances of the following class:

```class (Show term,Eq var) => Unifiable term var | term -> var where
topMatch :: Equation term -> Maybe (Equations term)
isVar :: term -> Maybe var
subst :: Substitution var term -> term -> term

showTerm :: term -> String -- for error reporting with fail

showTerm = show

type Equation t = (t,t)
type Equations t = [Equation t]

type Substitution v t = [(v,t)]

--mapSubst = mapSnd
mapSubst f s = [seq y (v,y)|(v,x)<-s,let y=f x]-- more strict to avoid space leaks
mapEqns = mapBoth

unify :: (Monad m,Unifiable t v) => Equations t -> m (Substitution v t)
unify = uni []
where
-- Invariant: the vars of eqns are not in the domain of s
--            s is idempotent
uni s [] = return s
uni s (eqn@(t1,t2):eqns) =
case topMatch eqn of
Just eqns' -> uni s (eqns'++eqns)
_ -> case apBoth isVar eqn of
(Just v,_) -> varBind v t2
(_,Just v) -> varBind v t1
_ -> mismatch' "(unify)" t1 t2
where
-- Pre: t is not the variable v. (This is ensured by topMatch.)
varBind v t =
if occurs v t
then mismatch' "(occurs check)" t1 t2
else let s1=(v,t)
su=subst [s1]
in uni (s1:mapSubst su s) (mapEqns su eqns)

match :: (Monad m,Unifiable t v) => Equations t -> m (Substitution v t)
-- Pre: lhs vars are disjoint from rhs vars
match eqns = uni [] eqns
where
pvars = nub \$ concatMap (vars.snd) eqns

-- Invariant: the vars of the lhss of the eqns are not in the domain of s
uni s [] = return s
uni s (eqn@(t1,t2):eqns) =
case topMatch eqn of
Just eqns' -> uni s (eqns'++eqns)
_ -> case isVar t1 of
Just v -> varBind v t2
_ -> mismatch' "(match)" t1 t2
where
-- Pre: t is not the variable v. (This is ensured by topMatch.)
varBind v t =
if v `elem` pvars
then mismatch' "(matchvar)"  t1 t2
else let s1=(v,t)
su=subst [s1]
in uni (s1:mapSubst su s) (mapFst su eqns)

mismatch t1 t2 = mismatch' "" t1 t2
mismatch' s t1 t2 =
fail ("Mismatch: "++s++"\n  "++showTerm t1++"\nvs\n  "++showTerm t2)

subterms t = map fst \$ fromMaybe bug (topMatch (t,t)) -- clumpsy...
where
bug = error \$
"Unification: bug in topMatch: term doesn't match itself:"++showTerm t

vars t =
case isVar t of
Just v -> [v]
_ -> nub \$ concatMap vars \$ subterms t

occurs v t = v `elem` vars t
```

Index

(HTML for this module was generated on 2006-08-12. About the conversion tool.)