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

Generic unification and matching

moduleUnificationwhereimportMaybe(fromMaybe)importList(nub)importMUtils(mapFst,mapSnd,mapBoth,apBoth)

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

class(Showterm,Eqvar)=>Unifiabletermvar|term->varwheretopMatch::Equationterm->Maybe(Equationsterm)isVar::term->Maybevarsubst::Substitutionvarterm->term->termshowTerm::term->String-- for error reporting with failshowTerm=showtypeEquationt=(t,t)typeEquationst=[Equationt]typeSubstitutionvt=[(v,t)] --mapSubst = mapSndmapSubstfs=[seqy(v,y)|(v,x)<-s,lety=fx]-- more strict to avoid space leaksmapEqns=mapBothunify::(Monadm,Unifiabletv)=>Equationst->m(Substitutionvt)unify=uni[]where-- Invariant: the vars of eqns are not in the domain of s -- s is idempotentunis[]=returnsunis(eqn@(t1,t2):eqns)=casetopMatcheqnofJusteqns'->unis(eqns'++eqns)_->caseapBothisVareqnof(Justv,_)->varBindvt2(_,Justv)->varBindvt1_->mismatch'"(unify)"t1t2where-- Pre: t is not the variable v. (This is ensured by topMatch.)varBindvt=ifoccursvtthenmismatch'"(occurs check)"t1t2elselets1=(v,t)su=subst[s1]inuni(s1:mapSubstsus) (mapEqnssueqns)match::(Monadm,Unifiabletv)=>Equationst->m(Substitutionvt) -- Pre: lhs vars are disjoint from rhs varsmatcheqns=uni[]eqnswherepvars=nub$concatMap(vars.snd)eqns-- Invariant: the vars of the lhss of the eqns are not in the domain of sunis[]=returnsunis(eqn@(t1,t2):eqns)=casetopMatcheqnofJusteqns'->unis(eqns'++eqns)_->caseisVart1ofJustv->varBindvt2_->mismatch'"(match)"t1t2where-- Pre: t is not the variable v. (This is ensured by topMatch.)varBindvt=ifv`elem`pvarsthenmismatch'"(matchvar)"t1t2elselets1=(v,t)su=subst[s1]inuni(s1:mapSubstsus) (mapFstsueqns)mismatcht1t2=mismatch'""t1t2mismatch'st1t2=fail("Mismatch: "++s++"\n "++showTermt1++"\nvs\n "++showTermt2)subtermst=mapfst$fromMaybebug(topMatch(t,t)) -- clumpsy...wherebug=error$"Unification: bug in topMatch: term doesn't match itself:"++showTermtvarst=caseisVartofJustv->[v]_->nub$concatMapvars$subtermstoccursvt=v`elem`varst

Index

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