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 df7978f
Show file tree
Hide file tree
Showing 5 changed files with 30 additions and 5 deletions.
14 changes: 9 additions & 5 deletions src/Agda2Hs/HsUtils.hs
Original file line number Diff line number Diff line change
Expand Up @@ -221,15 +221,14 @@ uses ty = not . null . usedTypesOf ty

-- Ideally, our pretty-printing library should insert parenthesis where needed.
-- However, hs-src-exts does not insert adequate parenthesis for infix
-- operators so we need to insert some by hand (see issues #54 and #273).
-- operators so we need to insert some by hand (see issues #54 and #273 and #317).

-- | Properly parenthesize an expression with regards to the default fixities.
insertParens :: Data a => a -> a
insertParens = everywhere (mkT $ insertPars $ fixityMap baseFixities)
where
fixityMap fxs = Map.fromList [ (q, fx) | fx@(Fixity _ _ q) <- fxs ]


-- | Given fixities of operators, properly parenthesize an expression.
insertPars :: Map (QName ()) Fixity -> Exp () -> Exp ()
insertPars fixs = \case
Expand All @@ -251,9 +250,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 df7978f

Please sign in to comment.