Skip to content

Commit

Permalink
[ fix agda#317 ] Add parens around infix where left argument is anoth…
Browse files Browse the repository at this point in the history
…er infix with lambda RHS
  • Loading branch information
jespercockx committed Jun 28, 2024
1 parent fdbebb6 commit c006900
Show file tree
Hide file tree
Showing 5 changed files with 29 additions and 3 deletions.
11 changes: 8 additions & 3 deletions src/Agda2Hs/HsUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -251,9 +251,14 @@ insertPars fixs = \case
needParen _ Nothing _ = True -- If we don't know, add parens
needParen _ _ Nothing = True

parL topOp = \case
e@Lambda{} -> Paren () e
e -> par topOp (needParen (AssocLeft () /=)) e
needParenExpr (InfixApp _ _ _ e2) = needParenExpr e2
needParenExpr Lambda{} = True
needParenExpr _ = False

parL topOp e =
if needParenExpr e
then Paren () e
else par topOp (needParen (AssocLeft () /=)) e
parR topOp = par topOp (needParen (AssocRight () /=))

par topOp need e@(InfixApp _ _ op _)
Expand Down
2 changes: 2 additions & 0 deletions test/AllTests.agda
Original file line number Diff line number Diff line change
Expand Up @@ -84,6 +84,7 @@ import Issue301
import Issue305
import Issue302
import Issue309
import Issue317

{-# FOREIGN AGDA2HS
import Issue14
Expand Down Expand Up @@ -165,4 +166,5 @@ import Issue301
import Issue305
import Issue302
import Issue309
import Issue317
#-}
11 changes: 11 additions & 0 deletions test/Issue317.agda
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
open import Haskell.Prelude

record D : Set where
constructor C
field unC : Int
open D public
{-# COMPILE AGDA2HS D #-}

test : D D
test d = C ∘ unC $ d
{-# COMPILE AGDA2HS test #-}
1 change: 1 addition & 0 deletions test/golden/AllTests.hs
Original file line number Diff line number Diff line change
Expand Up @@ -79,4 +79,5 @@ import Issue301
import Issue305
import Issue302
import Issue309
import Issue317

7 changes: 7 additions & 0 deletions test/golden/Issue317.hs
Original file line number Diff line number Diff line change
@@ -0,0 +1,7 @@
module Issue317 where

data D = C{unC :: Int}

test :: D -> D
test d = (C . \ r -> unC r) $ d

0 comments on commit c006900

Please sign in to comment.