verification of ghc folding rules

ver.py

equations = '''x    :++: (y :++: v)          -> (x+y)   `add` v
x    :++: (y :-: v)           -> (x+y)   `sub` v
x    :++: (v   :-: y)         -> (x-y)   `add` v
x  :-:  (y :++: v)            -> (x-y)   `sub` v
x  :-:  (y :-: v)             -> (x-y)   `add` v
x  :-:  (v   :-: y)         -> (x+y)   `sub` v
(y :++: v)    :-: x           -> (y-x)   `add` v
(y :-: v)     :-: x           -> (y-x)   `sub` v
(v   :-: y) :-: x           -> (0-y-x) `add` v
(x :++: w)  :+: (y :++: v)    -> (x+y)   `add` (w `add` v)
(w :-: x) :+: (y :-: v)   -> (y-x)   `add` (w `sub` v)
(w :-: x) :+: (v   :-: y) -> (0-x-y) `add` (w `add` v)
(x :-: w) :+: (y :-: v)   -> (x+y)   `sub` (w `add` v)
(x :-: w) :+: (v   :-: y) -> (x-y)   `add` (v `sub` w)
(w :-: x) :+: (y :++: v)    -> (y-x)   `add` (w `add` v)
(x :-: w) :+: (y :++: v)    -> (x+y)   `add` (v `sub` w)
(y :++: v)  :+: (w :-: x)   -> (y-x)   `add` (w `add` v)
(y :++: v)  :+: (x :-: w)   -> (x+y)   `add` (v `sub` w)
(v   :-: y) :-: (w :-: x) -> (x-y)   `add` (v `sub` w)
(v   :-: y) :-: (x :-: w) -> (0-x-y) `add` (v `add` w)
(y :-: v) :-: (w :-: x) -> (x+y)   `sub` (v `add` w)
(y :-: v) :-: (x :-: w) -> (y-x)   `add` (w `add` v)
(x :++: w)    :-: (y :++: v)  -> (x-y)   `add` (w `sub` v)
(w :-: x)   :-: (y :++: v)  -> (0-y-x) `add` (w `sub` v)
(x :-: w)   :-: (y :++: v)  -> (x-y)   `sub` (v `add` w)
(y :++: v)    :-: (w :-: x) -> (y+x)   `add` (v `sub` w)
(y :++: v)    :-: (x :-: w) -> (y-x)   `add` (v `add` w)
x :**: (y :**: v)             -> (x*y)   `mul` v
(x :**: w) :*: (y :**: v)     -> (x*y)   `mul` (w `mul` v)
x :**: (y :++: v)             -> (x*y)   `add` (x `mul` v)
x :**: (y :-: v)            -> (x*y)   `sub` (x `mul` v)
x :**: (v   :-: y)          -> (x `mul` v) `sub` (x*y)
v :+: v                       -> 2       `mul` v
v :+: (y :**: v)              -> (1+y)   `mul` v
v :-: (y :**: v)              -> (1-y)   `mul` v
(y :**: v) :+: v              -> (y+1)   `mul` v
(y :**: v) :-: v              -> (y-1)   `mul` v
(x :**: v) :+: (y :**: v)     -> (x+y)   `mul` v
(x :**: v) :-: (y :**: v)     -> (x-y)   `mul` v
w  :+: (y :++: v)             -> y `add` (w `add` v)
(y :++: v) :+: w              -> y       `add` (w `add` v)
w  :-: (y :++: v)             -> (w `sub` v) `sub` y
(y :++: v) :-: w              -> y       `add` (v `sub` w)
w    :-: (y :-: v)          -> (w `add` v) `sub` y
(y :-: v) :-: w             -> y       `sub` (w `add` v)
w    :+: (y :-: v)          -> y       `add` (w `sub` v)
w    :+: (v :-: y)          -> (w `add` v) `sub` y
(y :-: v) :+: w             -> y       `add` (w `sub` v)
(v :-: y) :+: w             -> (w `add` v) `sub` y
(y :-:   v) :-: (x :-: w) -> (y-x)   `add` (w `sub` v)'''.splitlines()

from sympy import *

x, y, v, w = symbols('x y v w')

for e in equations:
    left, right = e.split('->')
    rules = [
            (':**:', '*'),
            (':++:', '+'),
            (':-:',  '-'),
            (':+:',  '+'),
            (':*:',  '*'),
            ('`add`', '+'),
            ('`sub`', '-'),
            ('`mul`', '*'),
            ]
    for a, b in rules:
        left = left.replace(a, b)
        right = right.replace(a, b)

    left = left.strip()
    right = right.strip()

    diff = simplify(eval(left) - eval(right))
    if diff == 0:
        print('OK', left, '=', right)
    else:
        print('WRONG', left, '=', right)
        print('simplifies to %s' % diff)