Bug: Miscompilation of operator precedence
Closed this issue · 4 comments
JonathanBrouwer commented
When compiling this code:
module Testing where
open import Haskell.Prelude
infix 8 _^_ -- Higher priority than +, the usual precedence
_^_ : Nat -> Nat -> Nat
_^_ b zero = 1
_^_ b (suc e) = b * (b ^ e)
{-# COMPILE AGDA2HS _^_ #-}
x = 2 ^ (2 + 3)
{-# COMPILE AGDA2HS x #-}
The following haskell is generated
module Testing where
import Numeric.Natural (Natural)
(^) :: Natural -> Natural -> Natural
b ^ zero = 1
b ^ suc e = b * b ^ e
x :: Natural
x = 2 ^ 2 + 3
Note that there is nothing funky going on with the precedence, it's exactly as would be expected, yet it generates wrong code.
In fact, I can never get agda2hs to generate parentheses in infix sequences, no matter the parentheses used in the agda code
JonathanBrouwer commented
Update: You don't even need a custom operator definition, even 10 - (2 + 3)
does not compile correctly
omelkonian commented
jespercockx commented
Even without using explicit operator precedences, shouldn't at least an expression such as 10 - (2 + 3)
(with all parenthesis included) be compiled to an equivalent expression in Haskell?
UlfNorell commented
Yes, handling the default fixities is a slightly different issue than handling user-given ones.