@@ -30,7 +30,7 @@ import Data.Char
3030import Data.Data (Data)
3131import Numeric (showIntAtBase)
3232import qualified Data.Text as T
33−import Data.List hiding (insert)
33+import Data.List hiding (group, insert)
3434import Data.Set(Set, member, fromList, insert)
3535import Data.Maybe (listToMaybe)
3636import Data.Foldable (Foldable)
@@ -1498,3 +1498,99 @@ allTTNames = nub . allNamesIn
14981498 nb t = allNamesIn (binderTy t)
14991499 allNamesIn (App f a) = allNamesIn f ++ allNamesIn a
15001500 allNamesIn _ = []
1501+
1502+
1503+-- | Pretty-print a term
1504+pprintTT :: [Name] -- ^ The bound names (for highlighting and de Bruijn indices)
1505+ -> TT Name -- ^ The term to be printed
1506+ -> Doc OutputAnnotation
1507+pprintTT bound tm = pp startPrec bound tm
1508+
1509+ where
1510+ startPrec = 0
1511+ appPrec = 10
1512+
1513+ pp p bound (P Bound n ty) = annotate (AnnBoundName n False) (text $ show n)
1514+ pp p bound (P nt n ty) = annotate (AnnName n Nothing Nothing Nothing)
1515+ (text $ show n)
1516+ pp p bound (V i)
1517+ | i < length bound = let n = bound !! i
1518+ in annotate (AnnBoundName n False) (text $ show n)
1519+ | otherwise = text ("{{{V" ++ show i ++ "}}}")
1520+ pp p bound (Bind n b sc) = ppb p bound n b $
1521+ pp startPrec (n:bound) sc
1522+ pp p bound (App tm1 tm2) =
1523+ bracket p appPrec . group . hang 2 $
1524+ pp appPrec bound tm1 <> line <>
1525+ pp (appPrec + 1) bound tm2
1526+ pp p bound (Constant c) = annotate (AnnConst c) (text (show c))
1527+ pp p bound (Proj tm i) =
1528+ lparen <> pp startPrec bound tm <> rparen <>
1529+ text "!" <> text (show i)
1530+ pp p bound Erased = text "<<<erased>>>"
1531+ pp p bound Impossible = text "<<<impossible>>>"
1532+ pp p bound (TType ue) = annotate (AnnType "Type" "The type of types") $
1533+ text "Type"
1534+ pp p bound (UType u) = text (show u)
1535+
1536+ ppb p bound n (Lam ty) sc =
1537+ bracket p startPrec . group . align . hang 2 $
1538+ text "λ" <> bindingOf n False <+> text "." <> line <> sc
1539+ ppb p bound n (Pi _ ty k) sc =
1540+ bracket p startPrec . group . align $
1541+ lparen <> (bindingOf n False) <+> colon <+>
1542+ (group . align) (pp startPrec bound ty) <>
1543+ rparen <> mkArrow k <> line <> sc
1544+ where mkArrow (UType UniqueType) = text "⇴"
1545+ mkArrow (UType NullType) = text "⥛"
1546+ mkArrow _ = text "→"
1547+ ppb p bound n (Let ty val) sc =
1548+ bracket p startPrec . group . align $
1549+ (group . hang 2) (annotate AnnKeyword (text "let") <+>
1550+ bindingOf n False <+> colon <+>
1551+ pp startPrec bound ty <+>
1552+ text "=" <> line <>
1553+ pp startPrec bound val) <> line <>
1554+ (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1555+ ppb p bound n (NLet ty val) sc =
1556+ bracket p startPrec . group . align $
1557+ (group . hang 2) (annotate AnnKeyword (text "nlet") <+>
1558+ bindingOf n False <+> colon <+>
1559+ pp startPrec bound ty <+>
1560+ text "=" <> line <>
1561+ pp startPrec bound val) <> line <>
1562+ (group . hang 2) (annotate AnnKeyword (text "in") <+> sc)
1563+ ppb p bound n (Hole ty) sc =
1564+ bracket p startPrec . group . align . hang 2 $
1565+ text "?" <> bindingOf n False <+> text "." <> line <> sc
1566+ ppb p bound n (GHole _ ty) sc =
1567+ bracket p startPrec . group . align . hang 2 $
1568+ text "¿" <> bindingOf n False <+> text "." <> line <> sc
1569+ ppb p bound n (Guess ty val) sc =
1570+ bracket p startPrec . group . align . hang 2 $
1571+ text "?" <> bindingOf n False <+>
1572+ text "≈" <+> pp startPrec bound val <>
1573+ text "." <> line <> sc
1574+ ppb p bound n (PVar ty) sc =
1575+ bracket p startPrec . group . align . hang 2 $
1576+ annotate AnnKeyword (text "pat") <+>
1577+ bindingOf n False <+> colon <+> pp startPrec bound ty <>
1578+ text "." <> line <>
1579+ sc
1580+ ppb p bound n (PVTy ty) sc =
1581+ bracket p startPrec . group . align . hang 2 $
1582+ annotate AnnKeyword (text "patTy") <+>
1583+ bindingOf n False <+> colon <+> pp startPrec bound ty <>
1584+ text "." <> line <>
1585+ sc
1586+
1587+ bracket outer inner doc
1588+ | outer > inner = lparen <> doc <> rparen
1589+ | otherwise = doc
1590+
1591+
1592+-- | Pretty-printer helper for the binding site of a name
1593+bindingOf :: Name -- ^^ the bound name
1594+ -> Bool -- ^^ whether the name is implicit
1595+ -> Doc OutputAnnotation
1596+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))