;; The canonicalisations.
;;
;; Tier three of `spec/optimizer/13-rewrite-rules.md` section 13.4: the rewrites that put a term
;; into the one shape every other rule is written against. None of them makes the code smaller or
;; faster on its own, and that is the point. A commutative operation with a constant on it can be
;; written two ways round, so every rule about one has to be written twice, and each of those is a
;; separate line to read and a separate proof to discharge. Moving the constant to the right once
;; is what makes the second copy unnecessary, and it is what lets hash consing in
;; `spec/optimizer/12-egraph.md` section 12.1 see `2 + x` and `x + 2` as the same expression rather
;; than as two.
;;
;; What is here is the first of the four things the tier lists: constants to the right on the
;; commutative operators. `x - c` to `x + (-c)` needs a rule to compute a replacement constant
;; from the one it matched, which is issue 523. The comparison normalisations need the pass to
;; build an instruction that carries a predicate and to create a constant at the operand width
;; rather than at the result width, neither of which `crate::simplify` does yet. `!(a < b)` to
;; `a >= b` is about two instructions at once, which needs a plan that expands an operand, and
;; `simplify` uses none. Each of those is its own change and each is written down rather than
;; quietly left out.
;;
;; Section 13.5 asks every rule to strictly decrease a cost measure or to be marked as a
;; canonicalisation with an explicit direction. These are the second kind. The direction is
;; constant on the right, always, and nothing in the rule set moves one back to the left.
;;
;; Termination is not an argument, it is the plan. A rule here is only ever matched with the
;; operands shown as `[Shown::Const, Shown::Var, Shown::Reg]`, which is `crate::simplify::CANONICAL`
;; and which refuses to show a constant right operand at all. So the term a rule leaves behind,
;; with the number now on the right, is a term this table cannot match a second time, and
;; `add c1, c2` is rewritten zero times rather than forever. Written without that plan the rules
;; below are exactly the cycle section 13.6 warns about, where one rule undoes what another did,
;; except that here the rule undoes itself.
;;
;; The claim each rule makes is that its two sides compute the same thing, which for a commutative
;; operation is the commutativity of the operation and nothing more. `rucc-verify` proves it at
;; every width against `canonical.model` rather than taking the word of the name.
;; Adding.
;;
;; The first four, and the shape of every rule below them. The pattern has the number on the left
;; and something that is not a number on the right, the replacement has them the other way round,
;; and the `spec` clause says the two sides are equal. `k` is a variable in a constant position,
;; which binds whatever number was there and writes it back, so one rule covers every constant
;; rather than one rule per constant.
(rule (simplify (add.i8 (iconst.i8 k) (value.i8 x)))
(add.i8 (value.i8 x) (iconst.i8 k))
(spec (= (bvadd k x) (result))))
(rule (simplify (add.i16 (iconst.i16 k) (value.i16 x)))
(add.i16 (value.i16 x) (iconst.i16 k))
(spec (= (bvadd k x) (result))))
(rule (simplify (add.i32 (iconst.i32 k) (value.i32 x)))
(add.i32 (value.i32 x) (iconst.i32 k))
(spec (= (bvadd k x) (result))))
(rule (simplify (add.i64 (iconst.i64 k) (value.i64 x)))
(add.i64 (value.i64 x) (iconst.i64 k))
(spec (= (bvadd k x) (result))))
;; Multiplying.
(rule (simplify (mul.i8 (iconst.i8 k) (value.i8 x)))
(mul.i8 (value.i8 x) (iconst.i8 k))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i16 (iconst.i16 k) (value.i16 x)))
(mul.i16 (value.i16 x) (iconst.i16 k))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i32 (iconst.i32 k) (value.i32 x)))
(mul.i32 (value.i32 x) (iconst.i32 k))
(spec (= (bvmul k x) (result))))
(rule (simplify (mul.i64 (iconst.i64 k) (value.i64 x)))
(mul.i64 (value.i64 x) (iconst.i64 k))
(spec (= (bvmul k x) (result))))
;; And'ing.
(rule (simplify (and.i8 (iconst.i8 k) (value.i8 x)))
(and.i8 (value.i8 x) (iconst.i8 k))
(spec (= (bvand k x) (result))))
(rule (simplify (and.i16 (iconst.i16 k) (value.i16 x)))
(and.i16 (value.i16 x) (iconst.i16 k))
(spec (= (bvand k x) (result))))
(rule (simplify (and.i32 (iconst.i32 k) (value.i32 x)))
(and.i32 (value.i32 x) (iconst.i32 k))
(spec (= (bvand k x) (result))))
(rule (simplify (and.i64 (iconst.i64 k) (value.i64 x)))
(and.i64 (value.i64 x) (iconst.i64 k))
(spec (= (bvand k x) (result))))
;; Or'ing.
(rule (simplify (or.i8 (iconst.i8 k) (value.i8 x)))
(or.i8 (value.i8 x) (iconst.i8 k))
(spec (= (bvor k x) (result))))
(rule (simplify (or.i16 (iconst.i16 k) (value.i16 x)))
(or.i16 (value.i16 x) (iconst.i16 k))
(spec (= (bvor k x) (result))))
(rule (simplify (or.i32 (iconst.i32 k) (value.i32 x)))
(or.i32 (value.i32 x) (iconst.i32 k))
(spec (= (bvor k x) (result))))
(rule (simplify (or.i64 (iconst.i64 k) (value.i64 x)))
(or.i64 (value.i64 x) (iconst.i64 k))
(spec (= (bvor k x) (result))))
;; Exclusive or'ing.
(rule (simplify (xor.i8 (iconst.i8 k) (value.i8 x)))
(xor.i8 (value.i8 x) (iconst.i8 k))
(spec (= (bvxor k x) (result))))
(rule (simplify (xor.i16 (iconst.i16 k) (value.i16 x)))
(xor.i16 (value.i16 x) (iconst.i16 k))
(spec (= (bvxor k x) (result))))
(rule (simplify (xor.i32 (iconst.i32 k) (value.i32 x)))
(xor.i32 (value.i32 x) (iconst.i32 k))
(spec (= (bvxor k x) (result))))
(rule (simplify (xor.i64 (iconst.i64 k) (value.i64 x)))
(xor.i64 (value.i64 x) (iconst.i64 k))
(spec (= (bvxor k x) (result))))