9702474 · Idris-dev · git.iko.soy

1275 -> [FixDecl] -- ^^ Fixity declarations

1276 -> PTerm -- ^^ the term to pretty-print

1277 -> Doc OutputAnnotation

1278−pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

1278+pprintPTerm ppo bnd docArgs infixes = prettySe startPrec bnd

1279 where

1280+ startPrec = 0

1281+ funcAppPrec = 10

1280 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1282 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1281 prettySe p bnd (PQuote r) =

1283 prettySe p bnd (PQuote r) =

1282 text "![" <> pretty r <> text "]"

1284 text "![" <> pretty r <> text "]"

1286 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1288 | Just n <- snat p e = annotate (AnnData "Nat" "") (text (show n))

1287 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1289 prettySe p bnd (PRef fc n) = prettyName True (ppopt_impl ppo) bnd n

1288 prettySe p bnd (PLam fc n ty sc) =

1290 prettySe p bnd (PLam fc n ty sc) =

1289− bracket p 2 . group . align . hang 2 $

1291+ bracket p startPrec . group . align . hang 2 $

1290 text "\\" <> bindingOf n False <+> text "=>" <$>

1292 text "\\" <> bindingOf n False <+> text "=>" <$>

1291− prettySe 10 ((n, False):bnd) sc

1293+ prettySe startPrec ((n, False):bnd) sc

1292 prettySe p bnd (PLet fc n ty v sc) =

1294 prettySe p bnd (PLet fc n ty v sc) =

1293− bracket p 2 . group . align $

1295+ bracket p startPrec . group . align $

1294− kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe 10 bnd v) </>

1296+ kwd "let" <+> (group . align . hang 2 $ bindingOf n False <+> text "=" <$> prettySe startPrec bnd v) </>

1295− kwd "in" <+> (group . align . hang 2 $ prettySe 10 ((n, False):bnd) sc)

1297+ kwd "in" <+> (group . align . hang 2 $ prettySe startPrec ((n, False):bnd) sc)

1296 prettySe p bnd (PPi (Exp l s _) n ty sc)

1298 prettySe p bnd (PPi (Exp l s _) n ty sc)

1297 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1299 | n `elem` allNamesIn sc || ppopt_impl ppo || n `elem` docArgs =

1298− bracket p 2 . group $

1300+ bracket p startPrec . group $

1299− enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1301+ enclose lparen rparen (group . align $ bindingOf n False <+> colon <+> prettySe startPrec bnd ty) <+>

1300− st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1302+ st <> text "->" <$> prettySe startPrec ((n, False):bnd) sc

1301 | otherwise =

1303 | otherwise =

1302− bracket p 2 . group $

1304+ bracket p startPrec . group $

1303− group (prettySe 1 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1305+ group (prettySe (startPrec + 1) bnd ty <+> st) <> text "->" <$> group (prettySe startPrec ((n, False):bnd) sc)

1304 where

1306 where

1305 st =

1307 st =

1306 case s of

1308 case s of

1308 _ -> empty

1310 _ -> empty

1309 prettySe p bnd (PPi (Imp l s _) n ty sc)

1311 prettySe p bnd (PPi (Imp l s _) n ty sc)

1310 | ppopt_impl ppo =

1312 | ppopt_impl ppo =

1311− bracket p 2 $

1313+ bracket p startPrec $

1312− lbrace <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1314+ lbrace <> bindingOf n True <+> colon <+> prettySe startPrec bnd ty <> rbrace <+>

1313− st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1315+ st <> text "->" </> prettySe startPrec ((n, True):bnd) sc

1314− | otherwise = prettySe 10 ((n, True):bnd) sc

1316+ | otherwise = prettySe startPrec ((n, True):bnd) sc

1315 where

1317 where

1316 st =

1318 st =

1317 case s of

1319 case s of

1318 Static -> text "[static]" <> space

1320 Static -> text "[static]" <> space

1319 _ -> empty

1321 _ -> empty

1320 prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1322 prettySe p bnd (PPi (Constraint _ _) n ty sc) =

1321− bracket p 2 $

1323+ bracket p startPrec $

1322− prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1324+ prettySe (startPrec + 1) bnd ty <+> text "=>" </> prettySe startPrec ((n, True):bnd) sc

1323 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1325 prettySe p bnd (PPi (TacImp _ _ s) n ty sc) =

1324− bracket p 2 $

1326+ bracket p startPrec $

1325− lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

1327+ lbrace <> kwd "tacimp" <+> pretty n <+> colon <+> prettySe startPrec bnd ty <>

1326− rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1328+ rbrace <+> text "->" </> prettySe startPrec ((n, True):bnd) sc

1327 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1329 prettySe p bnd (PApp _ (PRef _ f) args) -- normal names, no explicit args

1328 | UN nm <- basename f

1330 | UN nm <- basename f

1329 , not (ppopt_impl ppo) && null (getShowArgs args) =

1331 , not (ppopt_impl ppo) && null (getShowArgs args) =

1336 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1338 (not (ppopt_impl ppo)) && (not $ isAlpha (thead nm)) =

1337 case getShowArgs args of

1339 case getShowArgs args of

1338 [] -> opName True

1340 [] -> opName True

1339− [x] -> group (opName True <$> group (prettySe 0 bnd (getTm x)))

1341+ [x] -> group (opName True <$> group (prettySe startPrec bnd (getTm x)))

1340− [l,r] -> let precedence = fromMaybe 20 (fmap prec f)

1342+ [l,r] -> let precedence = maybe (startPrec - 1) prec f

1341 in bracket p precedence $ inFix (getTm l) (getTm r)

1343 in bracket p precedence $ inFix (getTm l) (getTm r)

1342 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1344 (l@(PExp _ _ _ _) : r@(PExp _ _ _ _) : rest) ->

1343− bracket p 1 $

1345+ bracket p funcAppPrec $

1344 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1346 enclose lparen rparen (inFix (getTm l) (getTm r)) <+>

1345 align (group (vsep (map (prettyArgS bnd) rest)))

1347 align (group (vsep (map (prettyArgS bnd) rest)))

1346 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1348 as -> opName True <+> align (vsep (map (prettyArgS bnd) as))

1347 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1349 where opName isPrefix = prettyName isPrefix (ppopt_impl ppo) bnd op

1348 f = getFixity (opStr op)

1350 f = getFixity (opStr op)

1349− left l = case f of

1351+ left = case f of

1350− Nothing -> prettySe (-1) bnd l

1352+ Nothing -> funcAppPrec + 1

1351− Just (Infixl p') -> prettySe p' bnd l

1353+ Just (Infixl p') -> p'

1352− Just f' -> prettySe (prec f'-1) bnd l

1354+ Just f' -> prec f' + 1

1353− right r = case f of

1355+ right = case f of

1354− Nothing -> prettySe (-1) bnd r

1356+ Nothing -> funcAppPrec + 1

1355− Just (Infixr p') -> prettySe p' bnd r

1357+ Just (Infixr p') -> p'

1356− Just f' -> prettySe (prec f'-1) bnd r

1358+ Just f' -> prec f' + 1

1357 inFix l r = align . group $

1359 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)

1359 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1362 prettySe p bnd (PApp _ hd@(PRef fc f) [tm]) -- symbols, like 'foo

1360 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1363 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1361 f == sUN "Symbol_" = annotate (AnnType ("'" ++ str) ("The symbol " ++ str)) $

1364 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))

1363 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1366 prettySe p bnd (PApp _ f as) = -- Normal prefix applications

1364 let args = getShowArgs as

1367 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

1366 in

1370 in

1367− bracket p 1 . group $

1371+ bracket p funcAppPrec . group $

1368− if ppopt_impl ppo

1369− then if null as

1372+ if null shownArgs

1370− then fp

1373+ then fp

1371− else fp <+> align (vsep (map (prettyArgS bnd) as))

1374+ else fp <+> align (vsep (map (prettyArgS bnd) shownArgs))

1372− else if null args

1373− then fp

1374− else fp <+> align (vsep (map (prettyArgS bnd) args))

1375 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" <$>

1377 indent 2 (vsep (map ppcase cases))

1378 where

1379+ ppcase (l, r) = let prettyCase = prettySe startPrec

1380+ ([(n, False) | n <- vars l] ++ bnd)

1379− ppcase (l, r) = nest nestingSize $

1381+ in nest nestingSize $

1380− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) l <+>

1382+ prettyCase l <+> text "=>" <+> prettyCase r

1381− text "=>" <+>

1382− prettySe 10 ([(n, False) | n <- vars l] ++ bnd) r

1383 -- Warning: this is a bit of a hack. At this stage, we don't have the

1384 -- global context, so we can't determine which names are constructors,

1385 -- which are types, and which are pattern variables on the LHS of the

1394 noNS (NS _ _) = False

1395 noNS _ = True

1396

1397− prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm

1397+ prettySe p bnd (PHidden tm) = text "." <> prettySe funcAppPrec bnd tm

1398 prettySe p bnd (PRefl _ _) = annName eqCon $ text "Refl"

1399 prettySe p bnd (PResolveTC _) = text "resolvetc"

1400 prettySe p bnd (PTrue _ IsType) = annName unitTy $ text "()"

1402 prettySe p bnd (PTrue _ TypeOrTerm) = text "()"

1403 prettySe p bnd (PEq _ lt rt l r)

1404 | ppopt_impl ppo =

1405− bracket p 1 $

1405+ bracket p eqPrec $

1406 enclose lparen rparen eq <+>

1407 align (group (vsep (map (prettyArgS bnd)

1408 [PImp 0 False [] (sUN "A") lt,

1410 PExp 0 [] (sUN "x") l,

1411 PExp 0 [] (sUN "y") r])))

1412 | otherwise =

1413− bracket p 2 . align . group $

1413+ bracket p eqPrec . align . group $

1414− prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1414+ prettyTerm l <+> eq <$> group (prettyTerm r)

1415 where eq = annName eqTy (text "=")

1416+ eqPrec = startPrec

1417+ prettyTerm = prettySe (eqPrec + 1) bnd

1416 prettySe p bnd (PRewrite _ l r _) =

1418 prettySe p bnd (PRewrite _ l r _) =

1417− bracket p 2 $

1419+ bracket p startPrec $

1418− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1420+ text "rewrite" <+> prettySe (startPrec + 1) bnd l <+> text "in" <+> prettySe startPrec bnd r

1419 prettySe p bnd (PTyped l r) =

1421 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

1421 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

1423 prettySe p bnd pair@(PPair _ pun _ _) -- flatten tuples to the right, like parser

1422 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .

1424 | Just elts <- pairElts pair = enclose (ann lparen) (ann rparen) .

1423 align . group . vsep . punctuate (ann comma) $

1425 align . group . vsep . punctuate (ann comma) $

1424− map (prettySe 10 bnd) elts

1426+ map (prettySe startPrec bnd) elts

1425 where ann = case pun of

1427 where ann = case pun of

1426 TypeOrTerm -> id

1428 TypeOrTerm -> id

1427 IsType -> annName pairTy

1429 IsType -> annName pairTy

1428 IsTerm -> annName pairCon

1430 IsTerm -> annName pairCon

1429− prettySe p bnd (PDPair _ TypeOrTerm l t r) =

1431+ prettySe p bnd (PDPair _ pun l t r) =

1430− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

1432+ annotated lparen <>

1431− prettySe p bnd (PDPair _ IsType (PRef _ n) t r) =

1433+ left <+>

1432− annName sigmaTy lparen <>

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

1433− bindingOf n False <+>

1442+ (PRef _ n, IsType) -> (bindingOf n False, ((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 <>

1443+ _ -> (prettySe startPrec bnd l, id )

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

1449 prettySe p bnd (PAlternative a as) =

1444 prettySe p bnd (PAlternative a as) =

1450 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1445 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1451 where

1446 where

1452 prettyAs =

1447 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

1454 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1449 prettySe p bnd PType = annotate (AnnType "Type" "The type of types") $ text "Type"

1455 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1450 prettySe p bnd (PUniverse u) = annotate (AnnType (show u) "The type of unique types") $ text (show u)

1456 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1451 prettySe p bnd (PConstant c) = annotate (AnnConst c) (text (show c))

1478 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1473 prettyArgS bnd (PConstraint _ _ _ tm) = prettyArgSc bnd tm

1479 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1474 prettyArgS bnd (PTacImplicit _ _ n _ tm) = prettyArgSti bnd (n, tm)

1480

1475

1481− prettyArgSe bnd arg = prettySe 0 bnd arg

1476+ prettyArgSe bnd arg = prettySe (funcAppPrec + 1) bnd arg

1482− prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1477+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

1483− prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace

1478+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe startPrec bnd val <> rbrace <> rbrace

1484− prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace

1479+ prettyArgSti bnd (n, val) = lbrace <> kwd "auto" <+> pretty n <+> text "=" <+> prettySe startPrec bnd val <> rbrace

1485

1480

1486 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1481 annName :: Name -> Doc OutputAnnotation -> Doc OutputAnnotation

1487 annName n = annotate (AnnName n Nothing Nothing Nothing)

1482 annName n = annotate (AnnName n Nothing Nothing Nothing)

1538 snat _ _ = Nothing

1533 snat _ _ = Nothing

1539

1534

1540 bracket outer inner doc

1535 bracket outer inner doc

1541− | inner > outer = lparen <> doc <> rparen

1536+ | outer > inner = lparen <> doc <> rparen

1542 | otherwise = doc

1537 | otherwise = doc

1543

1538

1544 kwd = annotate AnnKeyword . text

1539 kwd = annotate AnnKeyword . text