[<<][meta][>>][..]

Wed Feb 10 14:25:46 CET 2010

## Commutation rewrite rule in CPS

termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add Add)
where
add k Zero a = a
add k One a = add k 1 a
add k (Lit a) (Lit b) = Lit (a + b) -- evaluate
add k a@(Lit _) (Add b@(Lit _) c) = Add (add k a b) c -- associate
add k a b = k b a -- commute
If maching fails, add calls its continuation k. The first k passed in
is (add Add). If that version of add fails again it calls its
continuation k = Add which returns the term unevaluated.
With normalization and all association rules:
termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add norm)
where
add k Zero a = a
add k One a = add k (Lit 1) a
add k (Lit a) (Lit b) = Lit (a + b) -- e
add k (Lit a) (Add (Lit b) c) = Add (Lit (a + b)) c -- a1
add k (Add (Lit a) b) (Add (Lit c) d) = Add (Lit (a + c)) (Add b d) -- a2
add k a (Add b@(Lit _) c) = Add b (Add a c) -- a3
add k a b = k b a -- c
norm a b@(Lit _) = Add b a -- n
norm a b = Add a b
I guess starting from equivalences (the algebraic rules) these rewrite
rules could be derived using Knuth - Bendix?
After thinking some more, this is the simplest set of rules I can find:
termAdd :: (Num l) => (Term l) -> (Term l) -> (Term l)
termAdd = add (add Add)
where
add k Zero a = a
add k One a = add k (Lit 1) a
add k (Lit a) (Lit b) = Lit (a + b) -- e
add k (Lit a) (Add (Lit b) c) = Add (Lit (a + b)) c -- ae1
add k (Add (Lit a) b) (Add (Lit c) d) = Add (Lit (a + c)) (Add b d) -- ae2
add k a (Add b@(Lit _) c) = Add b (Add a c) -- an
add k a@(Lit _) b = Add a b -- n
add k a b = k b a -- c
For multiplication, the rules will look almost exactly the same. Now,
the question is: how to abstract over such a pattern match?
Or.. How many combinations of rewrite rules should we allow?
I.e. allowing Signum

[Reply][About]

[<<][meta][>>][..]