@@ -1275,8 +1275,10 @@ pprintPTerm :: PPOption -- ^^ pretty printing options
12751275 -> [FixDecl] -- ^^ Fixity declarations
12761276 -> PTerm -- ^^ the term to pretty-print
12771277 -> Doc OutputAnnotation
1278−pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
1278+pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd
12791279 where
1280+ startPrec = 0
1281+ funcAppPrec = 10
12801282 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
12811283 prettySe p bnd (PQuote r) =
12821284 text "![" <> pretty r <> text "]"
@@ -1286,21 +1288,21 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
12861288 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))
12871289 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n
12881290 prettySe p bnd (PLam fc n ty sc) =
1289− bracket p 2 . group . align . hang 2 $
1291+ bracket p startPrec . group . align . hang 2 $
12901292 text "\\" <> bindingOf n False <+> text "=>" <$>
1291− prettySe 10 ((n, False):bnd) sc
1293+ prettySe startPrec ((n, False):bnd) sc
12921294 prettySe p bnd (PLet fc n ty v sc) =
1293− bracket p 2 . group . align $
1294− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>
1295− kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)
1295+ bracket p startPrec . group . align $
1296+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>
1297+ kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)
12961298 prettySe p bnd (PPi (Exp l s _) n ty sc)
12971299 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =
1298− bracket p 2 . group $
1299− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1300− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc
1300+ bracket p startPrec . group $
1301+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>
1302+ st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc
13011303 | otherwise =
1302− bracket p 2 . group $
1303− group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)
1304+ bracket p startPrec . group $
1305+ group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)
13041306 where
13051307 st =
13061308 case s of
@@ -1308,22 +1310,22 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13081310 _ -> empty
13091311 prettySe p bnd (PPi (Imp l s _) n ty sc)
13101312 | ppopt_impl ppo =
1311− bracket p 2 $
1312− lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1313− st <> text "->" </> prettySe 10 ((n, True):bnd) sc
1314− | otherwise = prettySe 10 ((n, True):bnd) sc
1313+ bracket p startPrec $
1314+ lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>
1315+ st <> text "->" </> prettySe startPrec ((n, True):bnd) sc
1316+ | otherwise = prettySe startPrec ((n, True):bnd) sc
13151317 where
13161318 st =
13171319 case s of
13181320 Static -> text "[static]" <> space
13191321 _ -> empty
13201322 prettySe p bnd (PPi (Constraint _ _) n ty sc) =
1321− bracket p 2 $
1322− prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc
1323+ bracket p startPrec $
1324+ prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc
13231325 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =
1324− bracket p 2 $
1325− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1326− rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc
1326+ bracket p startPrec $
1327+ lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>
1328+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc
13271329 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args
13281330 | UN nm <- basename f
13291331 , not (ppopt_impl ppo) && null (getShowArgs args) =
@@ -1336,50 +1338,48 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13361338 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =
13371339 case getShowArgs args of
13381340 [] -> opName True
1339− [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))
1340− [l,r] -> let precedence = fromMaybe 20 (fmap prec f)
1341+ [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))
1342+ [l,r] -> let precedence = maybe (startPrec - 1) prec f
13411343 in bracket p precedence $ inFix (getTm l) (getTm r)
13421344 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->
1343− bracket p 1 $
1345+ bracket p funcAppPrec $
13441346 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>
13451347 align (group (vsep (map (prettyArgS bnd) rest)))
13461348 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))
13471349 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op
13481350 f = getFixity (opStr op)
1349− left l = case f of
1350− Nothing -> prettySe (-1) bnd l
1351− Just (Infixl p') -> prettySe p' bnd l
1352− Just f' -> prettySe (prec f'-1) bnd l
1353− right r = case f of
1354− Nothing -> prettySe (-1) bnd r
1355− Just (Infixr p') -> prettySe p' bnd r
1356− Just f' -> prettySe (prec f'-1) bnd r
1351+ left = case f of
1352+ Nothing -> funcAppPrec + 1
1353+ Just (Infixl p') -> p'
1354+ Just f' -> prec f' + 1
1355+ right = case f of
1356+ Nothing -> funcAppPrec + 1
1357+ Just (Infixr p') -> p'
1358+ Just f' -> prec f' + 1
13571359 inFix l r = align . group $
1358− (left l <+> opName False) <$> group (right r)
1360+ (prettySe left bnd l <+> opName False) <$>
1361+ group (prettySe right bnd r)
13591362 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo
13601363 | PConstant (Idris.Core.TT.Str str) <- getTm tm,
13611364 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $
1362− char '\'' <> prettySe 10 bnd (PRef fc (sUN str))
1365+ char '\'' <> prettySe startPrec bnd (PRef fc (sUN str))
13631366 prettySe p bnd (PApp _ f as) = -- Normal prefix applications
13641367 let args = getShowArgs as
1365− fp = prettySe 1 bnd f
1368+ fp = prettySe (startPrec + 1) bnd f
1369+ shownArgs = if ppopt_impl ppo then as else args
13661370 in
1367− bracket p 1 . group $
1368− if ppopt_impl ppo
1369− then if null as
1370− then fp
1371− else fp <+> align (vsep (map (prettyArgS bnd) as))
1372− else if null args
1373− then fp
1374− else fp <+> align (vsep (map (prettyArgS bnd) args))
1371+ bracket p funcAppPrec . group $
1372+ if null shownArgs
1373+ then fp
1374+ else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))
13751375 prettySe p bnd (PCase _ scr cases) =
1376− align $ kwd "case" <+> prettySe 10 bnd scr <+> kwd "of" <$>
1376+ align $ kwd "case" <+> prettySe startPrec bnd scr <+> kwd "of" <$>
13771377 indent 2 (vsep (map ppcase cases))
13781378 where
1379− ppcase (l, r) = nest nestingSize $
1380− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>
1381− text "=>" <+>
1382− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r
1379+ ppcase (l, r) = let prettyCase = prettySe startPrec
1380+ ([(n, False) | n <- vars l] ++ bnd)
1381+ in nest nestingSize $
1382+ prettyCase l <+> text "=>" <+> prettyCase r
13831383 -- Warning: this is a bit of a hack. At this stage, we don't have the
13841384 -- global context, so we can't determine which names are constructors,
13851385 -- which are types, and which are pattern variables on the LHS of the
@@ -1394,7 +1394,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
13941394 noNS (NS _ _) = False
13951395 noNS _ = True
13961396
1397− prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1397+ prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm
13981398 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"
13991399 prettySe p bnd (PResolveTC _) = text "resolvetc"
14001400 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"
@@ -1402,7 +1402,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
14021402 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"
14031403 prettySe p bnd (PEq _ lt rt l r)
14041404 | ppopt_impl ppo =
1405− bracket p 1 $
1405+ bracket p eqPrec $
14061406 enclose lparen rparen eq <+>
14071407 align (group (vsep (map (prettyArgS bnd)
14081408 [PImp 0 False [] (sUN "A") lt,
@@ -1410,47 +1410,42 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
14101410 PExp 0 [] (sUN "x") l,
14111411 PExp 0 [] (sUN "y") r])))
14121412 | otherwise =
1413− bracket p 2 . align . group $
1414− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)
1413+ bracket p eqPrec . align . group $
1414+ prettyTerm l <+> eq <$> group (prettyTerm r)
14151415 where eq = annName eqTy (text "=")
1416+ eqPrec = startPrec
1417+ prettyTerm = prettySe (eqPrec + 1) bnd
14161418 prettySe p bnd (PRewrite _ l r _) =
1417− bracket p 2 $
1418− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1419+ bracket p startPrec $
1420+ text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r
14191421 prettySe p bnd (PTyped l r) =
1420− lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1422+ lparen <> prettySe startPrec bnd l <+> colon <+> prettySe startPrec bnd r <> rparen
14211423 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser
14221424 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .
14231425 align . group . vsep . punctuate (ann comma) $
1424− map (prettySe 10 bnd) elts
1426+ map (prettySe startPrec bnd) elts
14251427 where ann = case pun of
14261428 TypeOrTerm -> id
14271429 IsType -> annName pairTy
14281430 IsTerm -> annName pairCon
1429− prettySe p bnd (PDPair _ TypeOrTerm l t r) =
1430− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1431− prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =
1432− annName sigmaTy lparen <>
1433− bindingOf n False <+>
1434− annName sigmaTy (text "**") <+>
1435− prettySe 10 ((n, False):bnd) r <>
1436− annName sigmaTy rparen
1437− prettySe p bnd (PDPair _ IsType l t r) =
1438− annName sigmaTy lparen <>
1439− prettySe 10 bnd l <+>
1440− annName sigmaTy (text "**") <+>
1441− prettySe 10 bnd r <>
1442− annName sigmaTy rparen
1443− prettySe p bnd (PDPair _ IsTerm l t r) =
1444− annName existsCon lparen <>
1445− prettySe 10 bnd l <+>
1446− annName existsCon (text "**") <+>
1447− prettySe 10 bnd r <>
1448− annName existsCon rparen
1431+ prettySe p bnd (PDPair _ pun l t r) =
1432+ annotated lparen <>
1433+ left <+>
1434+ annotated (text "**") <+>
1435+ prettySe startPrec (addBinding bnd) r <>
1436+ annotated rparen
1437+ where annotated = case pun of
1438+ IsType -> annName sigmaTy
1439+ IsTerm -> annName existsCon
1440+ TypeOrTerm -> id
1441+ (left, addBinding) = case (l, pun) of
1442+ (PRef _ n, IsType) -> (bindingOf n False, ((n, False) :))
1443+ _ -> (prettySe startPrec bnd l, id )
14491444 prettySe p bnd (PAlternative a as) =
14501445 lparen <> text "|" <> prettyAs <> text "|" <> rparen
14511446 where
14521447 prettyAs =
1453− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1448+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe startPrec bnd) as
14541449 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"
14551450 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)
14561451 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))
@@ -1478,10 +1473,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
14781473 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm
14791474 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)
14801475
1481− prettyArgSe bnd arg = prettySe 0 bnd arg
1482− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1483− prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1484− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1476+ prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg
1477+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
1478+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace
1479+ prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace
14851480
14861481 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation
14871482 annName n = annotate (AnnName n Nothing Nothing Nothing)
@@ -1538,7 +1533,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd
15381533 snat _ _ = Nothing
15391534
15401535 bracket outer inner doc
1541− | inner > outer = lparen <> doc <> rparen
1536+ | outer > inner = lparen <> doc <> rparen
15421537 | otherwise = doc
15431538
15441539 kwd = annotate AnnKeyword . text