
18 Jul
2008
18 Jul
'08
5:25 a.m.
Since a term can occur both as a pattern on the left-hand side of the equation and also as expression on the right-hand side, I need to keep track of this, too.
So in fact, I have to anti-unify the patterns, 'translate' the resulting state (Data.Map [Pat] Pat) to (Data.Map [Body] Body) and pass it to the state transformer for anti-unifying the bodies. Similarly, from Body to Exp.
Don't you need to do this translation anyway, because Pat and Exp use different constructors? Perhaps you can reduce some of the lookup cases to looking up just Pat and Exp (eg, looking up in a Body or Clause or Pat or Exp could always give antiunifiers in terms of either Pat or Exp, so you need only one type of Map)? Claus