# Int division

Roman Leshchinskiy rl at cse.unsw.edu.au
Fri Dec 14 21:11:55 EST 2007

```Simon Marlow wrote:
> Roman Leshchinskiy wrote:
>>
>> Yes, but I'd also like to have the rule divInt# x# 1# = x#. With the
>> current definition of divInt#, just inlining it and having the rule
>> quotInt# x# 1# = x# (which I'd like to add, too) wouldn't be quite
>> enough, I think.
>
> It ought to be enough :)  With an extra simplification (described
> below), we could do it.
>
> divInt# :: Int# -> Int# -> Int#
> x# `divInt#` y#
>     | (x# ># 0#) && (y# <# 0#) = ((x# -# 1#) `quotInt#` y#) -# 1#
>     | (x# <# 0#) && (y# ># 0#) = ((x# +# 1#) `quotInt#` y#) -# 1#
>     | otherwise                = x# `quotInt#` y#
>
> so whey y# is 1#, we get
>
> x# `divInt#` 1#
>     | (x# <# 0#) = ((x# +# 1#) `quotInt#` 1#) -# 1#
>     | otherwise  = x# `quotInt#` 1#
>
> and with quotInt# x# 1# == 1#, we get
>
> x# `divInt#` 1#
>     | (x# <# 0#) = (x# +# 1#) -# 1#
>     | otherwise  = x#
>
> GHC doesn't simplify (x# +# 1#) -# 1#, but it should.  If that happened,

Right. In general, we should teach GHC a bit more about arithmetic.

> we'd have
>
> x# `divInt#` 1#
>     | (x# <# 0#) = x#
>     | otherwise  = x#
>
> which simplifies to just x#, and GHC does manage this, I just tried it.

Hmm, I hadn't realised that GHC does this. Is it only for simple rhss?

Roman

```