agda/agda2hs

Bug: Miscompilation of operator precedence

Closed this issue · 4 comments

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

Update: You don't even need a custom operator definition, even 10 - (2 + 3) does not compile correctly

Yep, this is a feature we do not currently support -- see the un-checked item in the README.

Closing as this is a duplicate of #41.

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?

Yes, handling the default fixities is a slightly different issue than handling user-given ones.