@@ -1131,17 +1131,28 @@ pprintPTerm impl bnd = prettySe 10 bnd
11311131 bracket p 2 $
11321132 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
11331133 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1134− prettySe p bnd (PApp _ (PRef _ f) [])
1135− | not impl = prettyName impl bnd f
1134+ prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
1135+ | UN nm <- basename f
1136+ , not impl && null (getExps args) = if isAlpha (thead nm)
1137+ then prettyName impl bnd f
1138+ else enclose lparen rparen $
1139+ prettyName impl bnd f
11361140 prettySe p bnd (PAppBind _ (PRef _ f) [])
11371141 | not impl = text "!" <> prettyName impl bnd f
11381142 prettySe p bnd (PApp _ (PRef _ op) args)
11391143 | UN nm <- basename op
11401144 , not (tnull nm) &&
1141− length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1142− let [l, r] = getExps args in
1143− bracket p 1 . align . group $
1144− (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)
1145+ (not impl) && (not $ isAlpha (thead nm)) =
1146+ case getExps args of
1147+ [] -> enclose lparen rparen opName
1148+ [x] -> group (enclose lparen rparen opName <$> group (prettySe 0 bnd x))
1149+ [l,r] -> bracket p 1 $ inFix l r
1150+ (l:r:rest) -> bracket p 1 $
1151+ enclose lparen rparen (inFix l r) <+>
1152+ align (group (vsep (map (prettyArgSe bnd) rest)))
1153+ where opName = prettyName impl bnd op
1154+ inFix l r = align . group $
1155+ (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)
11451156 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
11461157 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
11471158 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
@@ -1179,20 +1190,14 @@ pprintPTerm impl bnd = prettySe 10 bnd
11791190 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
11801191 prettySe p bnd (PTyped l r) =
11811192 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1182− prettySe p bnd (PPair _ TypeOrTerm l r) =
1183− lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
1184− prettySe p bnd (PPair _ IsType l r) =
1185− annotate (AnnName pairTy Nothing Nothing) lparen <>
1186− prettySe 10 bnd l <>
1187− annotate (AnnName pairTy Nothing Nothing) comma <+>
1188− prettySe 10 bnd r <>
1189− annotate (AnnName pairTy Nothing Nothing) rparen
1190− prettySe p bnd (PPair _ IsTerm l r) =
1191− annotate (AnnName pairCon Nothing Nothing) lparen <>
1192− prettySe 10 bnd l <>
1193− annotate (AnnName pairCon Nothing Nothing) comma <+>
1194− prettySe 10 bnd r <>
1195− annotate (AnnName pairCon Nothing Nothing) rparen
1193+ prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
1194+ | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
1195+ align . group . vsep . punctuate (ann comma) $
1196+ map (prettySe 10 bnd) elts
1197+ where ann = case pun of
1198+ TypeOrTerm -> id
1199+ IsType -> annotate (AnnName pairTy Nothing Nothing)
1200+ IsTerm -> annotate (AnnName pairCon Nothing Nothing)
11961201 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
11971202 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
11981203 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
@@ -1281,6 +1286,11 @@ pprintPTerm impl bnd = prettySe 10 bnd
12811286 comma = (annotate AnnConstData (text ","))
12821287 slist _ _ _ = Nothing
12831288
1289+ pairElts :: PTerm -> Maybe [PTerm]
1290+ pairElts (PPair _ _ x y) | Just elts <- pairElts y = Just (x:elts)
1291+ | otherwise = Just [x, y]
1292+ pairElts _ = Nothing
1293+
12841294 natns = "Prelude.Nat."
12851295
12861296 snat p (PRef _ z)