syntactic anti-unification of TH terms --- best practise?
I am implementing syntactic anti-unification for TH terms (Exp, Pat, Clause, ...). For example anti-unifying the clauses tail (1:xs) = xs tail (1:2:xs) = (2:xs) would yield tail (1:x1) = x1 whereas the anti-instance of last (1:[]) = 1 last (1:xs) = last xs is last (1:x1) = x2 So different subterms are always replaced with the same variable if anti-unified twice. So far, so good, there is nothing complicated. I am using a State Monad to keep track of my variables and defined a type class for anti-unification and implemented instances for Exp, Pat, ... type AU a = State (Data.Map [a] a) a class Antiunifieable t where antiunify :: (Ord t) => [t] -> t antiunify = (\t -> evalState (aunify t) M.empty) aunify :: (Ord t) => [t] -> AU t Problems arise when I come to clauses, defined in TH as Clause [Pat] Body [Dec] where Body is for example NormalB Exp 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. This seems a bit ugly to me, but I have no idea how to solve it more elegantly. I thought about introducing some kind of wrapper type like data Term = TC Clause | TB Body | TP Pat | TE Exp and implement an instance for Eq and Antiunifieable for it. But again, this is not better either and I run into a lot of bookkeeping when processing it. Is there some kind of best practise dealing with such a problem? I am not sure if MonadTransformers would help here, because it is always the same monad but with different parameter. Thanks a lot, Martin
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
Don't you need to do this translation anyway, because Pat and Exp use different constructors?
Yes, somewhere I have to say how to convert Pat to Exp.
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)?
So you mean use a specific (M.Map [Exp] Exp) instead of a general (M.Map [a] a)? Yes, this would make sense. Then I only translate the value I want to lookup (if at all) and not the whole map, which I can pass to the accordant state transformer straight away. I'll try it out. Thanks, Martin
Excerpts from Martin Hofmann's message of Fri Jul 18 12:01:28 +0200 2008:
Don't you need to do this translation anyway, because Pat and Exp use different constructors?
Yes, somewhere I have to say how to convert Pat to Exp.
That's often doable, but you have to deal with patterns like `_', `v@pat', `!v'... -- Nicolas Pouillard
participants (3)
-
Claus Reinke -
Martin Hofmann -
Nicolas Pouillard