--Generic unification: module Unification where import Maybe(fromJust) import List(nub) import MUtils(mapFst,mapSnd,mapBoth,apBoth) 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 type Equation t = (t,t) type Equations t = [Equation t] type Substitution v t = [(v,t)] mapSubst = mapSnd 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 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 "++show t1++"\nvs\n "++show t2) subterms t = map fst $ fromJust (topMatch (t,t)) -- clumpsy... vars t = case isVar t of Just v -> [v] _ -> nub $ concatMap vars $ subterms t occurs v t = v `elem` vars t