1;; rewrites for integer and floating-point arithmetic
2;; eg: `iadd`, `isub`, `ineg`, `imul`, `fadd`, `fsub`, `fmul`
3
4;; x+0 == 0+x == x.
5(rule (simplify (iadd ty
6                      x
7                      (iconst ty (u64_from_imm64 0))))
8      (subsume x))
9(rule (simplify (iadd ty
10                      (iconst ty (u64_from_imm64 0))
11                      x))
12      (subsume x))
13;; x-0 == x.
14(rule (simplify (isub ty
15                      x
16                      (iconst ty (u64_from_imm64 0))))
17      (subsume x))
18;; 0-x == (ineg x).
19(rule (simplify (isub ty
20                      (iconst ty (u64_from_imm64 0))
21                      x))
22      (ineg ty x))
23
24;; ineg(ineg(x)) == x.
25(rule (simplify (ineg ty (ineg ty x))) (subsume x))
26
27;; ineg(x) * ineg(y) == x*y.
28(rule (simplify (imul ty (ineg ty x) (ineg ty y)))
29      (subsume (imul ty x y)))
30
31;; iabs(ineg(x)) == iabs(x).
32(rule (simplify (iabs ty (ineg ty x)))
33      (iabs ty x))
34
35;; iabs(iabs(x)) == iabs(x).
36(rule (simplify (iabs ty inner @ (iabs ty x)))
37      (subsume inner))
38
39;; x-x == 0.
40(rule (simplify (isub (fits_in_64 (ty_int ty)) x x)) (subsume (iconst ty (imm64 0))))
41
42;; x*1 == 1*x == x.
43(rule (simplify (imul ty
44                      x
45                      (iconst ty (u64_from_imm64 1))))
46      (subsume x))
47(rule (simplify (imul ty
48                      (iconst ty (u64_from_imm64 1))
49                      x))
50      (subsume x))
51
52;; x*0 == 0*x == 0.
53(rule (simplify (imul ty
54                      _
55                      zero @ (iconst ty (u64_from_imm64 0))))
56      (subsume zero))
57(rule (simplify (imul ty
58                      zero @ (iconst ty (u64_from_imm64 0))
59                      _))
60      (subsume zero))
61
62;; x*-1 == -1*x == ineg(x).
63(rule (simplify (imul ty x (iconst ty c)))
64      (if-let -1 (i64_sextend_imm64 ty c))
65      (ineg ty x))
66(rule (simplify (imul ty (iconst ty c) x))
67      (if-let -1 (i64_sextend_imm64 ty c))
68      (ineg ty x))
69
70;; (!x) + 1 == 1 + (!x) == !(x) - (-1) == ineg(x)
71(rule (simplify (iadd ty (bnot ty x) (iconst ty (u64_from_imm64 1))))
72      (ineg ty x))
73(rule (simplify (iadd ty (iconst ty (u64_from_imm64 1)) (bnot ty x)))
74      (ineg ty x))
75(rule (simplify (isub ty (bnot ty x) (iconst ty c)))
76      (if-let -1 (i64_sextend_imm64 ty c))
77      (ineg ty x))
78
79;; !(x - 1) == !(x + (-1)) == !((-1) + x) == ineg(x)
80(rule (simplify (bnot ty (isub ty x (iconst ty (u64_from_imm64 1)))))
81      (ineg ty x))
82(rule (simplify (bnot ty (iadd ty x (iconst ty c))))
83      (if-let -1 (i64_sextend_imm64 ty c))
84      (ineg ty x))
85(rule (simplify (bnot ty (iadd ty (iconst ty c) x)))
86      (if-let -1 (i64_sextend_imm64 ty c))
87      (ineg ty x))
88
89;; x/1 == x.
90(rule (simplify (sdiv ty
91                      x
92                      (iconst ty (u64_from_imm64 1))))
93      (subsume x))
94(rule (simplify (udiv ty
95                      x
96                      (iconst ty (u64_from_imm64 1))))
97      (subsume x))
98
99;; TODO: strength reduction: div to shifts
100;; TODO: div/rem by constants -> magic multiplications
101
102;; x*2 == 2*x == x+x.
103(rule (simplify (imul ty x (iconst _ (simm32 2))))
104      (iadd ty x x))
105(rule (simplify (imul ty (iconst _ (simm32 2)) x))
106      (iadd ty x x))
107
108;; x*c == x<<log2(c) when c is a power of two.
109;; Note that the type of `iconst` must be the same as the type of `imul`,
110;; so these rules can only fire in situations where it's safe to construct an
111;; `iconst` of that type.
112(rule (simplify (imul ty x (iconst _ (imm64_power_of_two c))))
113      (ishl ty x (iconst ty (imm64 c))))
114(rule (simplify (imul ty (iconst _ (imm64_power_of_two c)) x))
115      (ishl ty x (iconst ty (imm64 c))))
116
117;; fneg(fneg(x)) == x.
118(rule (simplify (fneg ty (fneg ty x))) (subsume x))
119
120;; If both of the multiplied arguments to an `fma` are negated then remove
121;; both of them since they cancel out.
122(rule (simplify (fma ty (fneg ty x) (fneg ty y) z))
123      (fma ty x y z))
124
125;; If both of the multiplied arguments to an `fmul` are negated then remove
126;; both of them since they cancel out.
127(rule (simplify (fmul ty (fneg ty x) (fneg ty y)))
128      (fmul ty x y))
129