At the moment we have essentially two copies of the "unification" algorithm in the booster:

https://github.com/runtimeverification/hs-backend-booster/blob/754e6ca645d96b0460355a4d61bdf42b3b4f6ff2/library/Booster/Pattern/Unify.hs#L172
https://github.com/runtimeverification/hs-backend-booster/blob/754e6ca645d96b0460355a4d61bdf42b3b4f6ff2/library/Booster/Pattern/Match.hs#L120

However, I would argue that our "unification" when applying rewrite rules is just a slightly different version of the matching algorithm we use for applying function and simplification rules. Namely, we expressly forbid any overlap of variables in the two terms and expressly check at the end of the unification algorithm that we in fact obtained a matching substitution, such that we have subst(rule_LHS) = current_configuration. Since there is no significant algorithmic difference between our "unification" and matching (match1 is a copy of unify1 with various tweaks), it would be better to merge the two as it will be much easier to see what exactly the differences between the two algorithms are. E.g. match1 allows matching two terms f1(...) where f1 isn't a constructor, whereas unify1 does not allow this. Conversely, unify1 works for a subset of map/set/list problems, whereas support for these is lacking in match1.

This issue has been raised before, but is more pertinent now that we are tackling the implication endpoint in the booster, which requires tweaks to either versions to e.g. lift the restriction that the variables in the two terms are completely disjoint. Instead of making yet another copy of essentially the same code, we should instead merge unify1/match1 and put the differences between rule/function/implication matching in a single place, such that it is easy to see what the subtle differences (if any) are between these versions.