Is there a generic algorithm for translating equational rules into corresponding data structures?

Question

When implementing a term rewriting system, one “optimization” one can do is to represent operators known to have certain equational properties with a more directly representative data structure. For example, one can use lists to represent uses of a binary operator known to be associative, rather than using the naïve syntax tree representation one is forced to use in the absence of any information about an operator.

I thought I recalled a result that stated that there was an algorithm that could take any (finite) set of equational rules about an operator and transform them into a data structure definition specialized for that set of equational rules. However, when I tried to look for this result, I couldn't find anything like it anywhere. Am I not looking hard enough or not in the right places, or did I just imagine this result entirely? If I did imagine it out of thin air, is there any less-powerful result of the same form that is known, or any counter-result that dashes my hopes of such a generic algorithm existing?