# Refactor rule for arithmetic operators.

This PR does a bit of refactoring of the rules for binary (arithmetic) operators on integers. This will probably be useful to @paulzhu, and I needed this first step for the handling of right shifts. The changes are the following:

- Define a function
`arith_op_result`

that, given the two operands and the op computes the result. - Define a predicate
`arith_op_sidecond`

that gives the side conditions for a given op. - Use the above functions in the rule
`type_arith_op_int_int`

, and factor in the rules for`/`

and`%`

. - Give more precise side conditions for the right and left shift operators (this is the goal of this PR). Note that the standard leaves it as implementation-define what is the result of right-shifting a negative number. I thing we should consider that UB.

Some further factoring of code is possible with the operational semantics, but we can do that as a second step.