| File | unification.str |
| Author | unknown |
| Since | unknown |
Syntactic unification, no variable bindings are taken into account.
| General | |
| Lines of code | 95 |
| Stratego | |
| Module number | 1 (100% documented) |
| Constructor number | 0 |
| Overlay number | 0 |
| Strategy number | 6 (33% documented) |
| Rule number | 6 (0% documented) |
| DynamicRule number | 0 |
Strategy summary |
||
| diff | n/a | unification.str |
| equal | n/a | unification.str |
| equal(Strategy fltr) | n/a | unification.str |
| equal(Strategy fltr1, Strategy fltr2) | The following equality strategy has an additional filter that can be used for checking equality modulo alpha renaming | unification.str |
| pattern-match(Strategy isvar) | n/a | unification.str |
| unify(Strategy isvar) | The strategy unify unifies a list of pairs of terms and creates the most general unifier for them | unification.str |
Rule summary |
||
| MatchVar(Strategy isvar) | n/a | unification.str |
| UfDecompose | n/a | unification.str |
| UfIdem | n/a | unification.str |
| UfShift | n/a | unification.str |
| UfSwap(Strategy isvar) | n/a | unification.str |
| UfVar(Strategy isvar) | n/a | unification.str |
Strategy details |
|||||||||
| ATerm | equal(Strategy fltr1, Strategy fltr2) | ||||||||
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. |
|||||||||
| ATerm | unify(Strategy isvar) | ||||||||
The strategy unify unifies a list of pairs of terms and creates themost general unifier for them. The strategy is parameterizedby a strategy \verb|isvar| that determines the shape of variables. The result is a list of pairs \verb|(x1,p1)|, where \verb|x1| isa term for which \verb|isvar| succeeds and \verb|p1| is the termit should be substituted with to unify the terms. E.g. <unify(isvar)> [(t1,t2),(t3,t4),...] => [(x1,p1),(x2,p2),...] |
|||||||||