(datatype Math
    (Diff Math Math)
    (Integral Math Math)
    
    (Add Math Math)
    (Sub Math Math)
    (Mul Math Math)
    (Div Math Math)
    (Pow Math Math)
    (Ln Math)
    (Sqrt Math)
    
    (Sin Math)
    (Cos Math)
    
    (Const Rational)
    (Var String))

(rewrite (Add a b) (Add b a))
(rewrite (Mul a b) (Mul b a))
(rewrite (Add a (Add b c)) (Add (Add a b) c))
(rewrite (Mul a (Mul b c)) (Mul (Mul a b) c))

(rewrite (Sub a b) (Add a (Mul (Const (rational -1 1)) b)))
;; (rewrite (Div a b) (Mul a (Pow b (Const (rational -1 1)))) :when ((is-not-zero b)))

(rewrite (Add a (Const (rational 0 1))) a)
(rewrite (Mul a (Const (rational 0 1))) (Const (rational 0 1)))
(rewrite (Mul a (Const (rational 1 1))) a)

(rewrite (Sub a a) (Const (rational 0 1)))

(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))
(rewrite (Add (Mul a b) (Mul a c)) (Mul a (Add b c)))

(rewrite (Mul (Pow a b) (Pow a c)) (Pow a (Add b c)))
(rewrite (Pow x (Const (rational 1 1))) x)
(rewrite (Pow x (Const (rational 2 1))) (Mul x x))

(rewrite (Diff x (Add a b)) (Add (Diff x a) (Diff x b)))
(rewrite (Diff x (Mul a b)) (Add (Mul a (Diff x b)) (Mul b (Diff x a))))

(rewrite (Diff x (Sin x)) (Cos x))
(rewrite (Diff x (Cos x)) (Mul (Const (rational -1 1)) (Sin x)))

(rewrite (Integral (Const (rational 1 1)) x) x)
(rewrite (Integral (Cos x) x) (Sin x))
(rewrite (Integral (Sin x) x) (Mul (Const (rational -1 1)) (Cos x)))
(rewrite (Integral (Add f g) x) (Add (Integral f x) (Integral g x)))
(rewrite (Integral (Sub f g) x) (Sub (Integral f x) (Integral g x)))
(rewrite (Integral (Mul a b) x) 
(Sub (Mul a (Integral b x)) 
    (Integral (Mul (Diff x a) (Integral b x)) x)))
(Integral (Ln (Var "x")) (Var "x"))
(Integral (Add (Var "x") (Cos (Var "x"))) (Var "x"))
(Integral (Mul (Cos (Var "x")) (Var "x")) (Var "x"))
(Diff (Var "x") (Add (Const (rational 1 1)) (Mul (Const (rational 2 1)) (Var "x"))))
(Diff (Var "x") (Sub (Pow (Var "x") (Const (rational 3 1))) (Mul (Const (rational 7 1)) (Pow (Var "x") (Const (rational 2 1))))))
(Add (Mul (Var "y") (Add (Var "x") (Var "y"))) (Sub (Add (Var "x") (Const (rational 2 1))) (Add (Var "x") (Var "x"))))
(Div (Const (rational 1 1))
                        (Sub (Div (Add (Const (rational 1 1))
                                    (Sqrt (Var "five")))
                                (Const (rational 2 1)))
                            (Div (Sub (Const (rational 1 1))
                                    (Sqrt (Var "five")))
                                (Const (rational 2 1)))))
(run 11)
(print-size Add)
(print-size Mul)

(print-size)

(print-stats)