1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
(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 i64)
(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 -1) b)))
;; (rewrite (Div a b) (Mul a (Pow b (Const -1))) :when ((is-not-zero b)))
(rewrite (Add a (Const 0)) a)
(rewrite (Mul a (Const 0)) (Const 0))
(rewrite (Mul a (Const 1)) a)
(rewrite (Sub a a) (Const 0))
(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 1)) x)
(rewrite (Pow x (Const 2)) (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 -1) (Sin x)))
(rewrite (Integral (Const 1) x) x)
(rewrite (Integral (Cos x) x) (Sin x))
(rewrite (Integral (Sin x) x) (Mul (Const -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 1) (Mul (Const 2) (Var "x"))))
(Diff (Var "x") (Sub (Pow (Var "x") (Const 3)) (Mul (Const 7) (Pow (Var "x") (Const 2)))))
(Add (Mul (Var "y") (Add (Var "x") (Var "y"))) (Sub (Add (Var "x") (Const 2)) (Add (Var "x") (Var "x"))))
(Div (Const 1)
(Sub (Div (Add (Const 1)
(Sqrt (Var "five")))
(Const 2))
(Div (Sub (Const 1)
(Sqrt (Var "five")))
(Const 2))))
(run 11)
(print-size Add)
(print-size Mul)
(print-size)
(print-stats)