@@ -1131,17 +1131,28 @@ pprintPTerm impl bnd = prettySe 10 bnd
1131 bracket p 2 $
1131 bracket p 2 $
1132 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1132 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1133 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1133 rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1134− prettySe p bnd (PApp _ (PRef _ 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 $
1135− | not impl = prettyName impl bnd f
1139+ prettyName impl bnd f
1136 prettySe p bnd (PAppBind _ (PRef _ f) [])
1140 prettySe p bnd (PAppBind _ (PRef _ f) [])
1137 | not impl = text "!" <> prettyName impl bnd f
1141 | not impl = text "!" <> prettyName impl bnd f
1138 prettySe p bnd (PApp _ (PRef _ op) args)
1142 prettySe p bnd (PApp _ (PRef _ op) args)
1139 | UN nm <- basename op
1143 | UN nm <- basename op
1140 , not (tnull nm) &&
1144 , not (tnull nm) &&
1141− length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1145+ (not impl) && (not $ isAlpha (thead nm)) =
1142− let [l, r] = getExps args in
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
1143− bracket p 1 . align . group $
1150+ (l:r:rest) -> bracket p 1 $
1151+ enclose lparen rparen (inFix l r) <+>
1152+ align (group (vsep (map (prettyArgSe bnd) rest)))
1144− (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)
1153+ where opName = prettyName impl bnd op
1154+ inFix l r = align . group $
1155+ (prettySe 1 bnd l <+> opName) <$> group (prettySe 0 bnd r)
1145 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1156 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])
1146 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1157 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
1147 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1158 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
@@ -1179,20 +1190,14 @@ pprintPTerm impl bnd = prettySe 10 bnd
1179 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1190 text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1180 prettySe p bnd (PTyped l r) =
1191 prettySe p bnd (PTyped l r) =
1181 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1192 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> 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
1182− prettySe p bnd (PPair _ TypeOrTerm l r) =
1198+ TypeOrTerm -> id
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
1199+ IsType -> annotate (AnnName pairTy Nothing Nothing)
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 <+>
1200+ IsTerm -> annotate (AnnName pairCon Nothing Nothing)
1194− prettySe 10 bnd r <>
1195− annotate (AnnName pairCon Nothing Nothing) rparen
1196 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1201 prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1197 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1202 lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1198 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1203 prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
@@ -1281,6 +1286,11 @@ pprintPTerm impl bnd = prettySe 10 bnd
1281 comma = (annotate AnnConstData (text ","))
1286 comma = (annotate AnnConstData (text ","))
1282 slist _ _ _ = Nothing
1287 slist _ _ _ = Nothing
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
1284 natns = "Prelude.Nat."
1294 natns = "Prelude.Nat."
1286 snat p (PRef _ z)
1296 snat p (PRef _ z)