/** * Syntactic unification, no variable bindings are taken into account. */ module strategy/general/unification imports collection/list/- term/common term/properties strategy/general/substitution strategies equal = for(id ,[], UfIdem <+ UfDecompose //<+ debug(!"not equal: "); FAIL ) rules UfIdem : [(x,x) | ps] -> ps UfDecompose : [(f#(xs), f#(ys)) | ps] -> <conc>(<zip(id)>(xs, ys), ps) strategies diff = for(\ ps -> ([],ps) \ , (id,[]), (id, UfIdem <+ UfDecompose) <+ UfShift) rules UfShift : (ps1, [p | ps2]) -> ([p | ps1], ps2) strategies pattern-match(isvar) = for(\ pairs -> (pairs, []) \ ,\ ([], sbs) -> sbs \ ,(UfIdem, id) <+ MatchVar(isvar) + (UfDecompose, id)) rules MatchVar(isvar) : ([(x,y) | ps], sbs) -> (ps, [(x, y) | sbs]) where <isvar> x; <not(fetch({z: ?(x,z); <not(eq)> (y, z)}))> sbs strategies /** * The strategy unify unifies a list of pairs of terms and creates the * most general unifier for them. The strategy is parameterized * by a strategy \verb|isvar| that determines the shape of variables. * * The result is a list of pairs \verb|(x1,p1)|, where \verb|x1| is * a term for which \verb|isvar| succeeds and \verb|p1| is the term * it should be substituted with to unify the terms. * * E.g. <unify(isvar)> [(t1,t2),(t3,t4),...] => [(x1,p1),(x2,p2),...] */ unify(isvar) = for(\ pairs -> (pairs, []) \ ,\ ([], sbs) -> sbs \ ,(UfIdem, id) <+ UfVar(isvar) + UfSwap(isvar) <+ (UfDecompose, id)) rules UfVar(isvar) : ([(x,y) | ps], sbs) -> (ps', [(x, y) | sbs'']) where <isvar> x; <not(is-subterm)>(x,y); <substitute(isvar)> ([(x,y)], (sbs, ps)) => (sbs'', ps') UfSwap(isvar) : ([(x,y) | ps], sbs) -> ([(y,x) | ps], sbs) where <not(isvar)> x; <isvar> y strategies equal(fltr) = for(id ,[], UfIdem <+ try([(fltr,fltr)|id]); UfDecompose //<+ debug(!"not equal: "); FAIL ) strategies /** * The following equality strategy has an additional filter * that can be used for checking equality modulo alpha renaming. * The filter applies to the entire pair and can change something * in one term based on the other term. */ equal(fltr1, fltr2) = for(id ,[], UfIdem <+ [(try(fltr1),try(fltr1)); try(fltr2)|id]; UfDecompose //<+ debug(!"not equal: "); FAIL )