[Haskell] AC-unification libraries?

[Frank Atanassow]

In the near future I expect to have need of an implementation of some 
basic term rewriting system algorithms, most notably:

   - term matching and unification
   - same, modulo associativity
   - same, modulo associativity and commutativity

The first, of course, is easy to do myself; the second, I imagine, is 
not too difficult but, as I hear the last is very difficult to 
implement halfway efficiently, I would be grateful if someone could 
point me to an existing Haskell implementation. (No, I could not find a 
pointer at the Haskell website, or by scouring the web.)

BTW, bonus points if such a framework supports extra things like checks 
for TRS confluence, termination, enumeration of critical pairs, 
Knuth-Bendix completion, etc.

Thanks in advance.

Regards,
Frank