Int division

[Roman Leshchinskiy]

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