3d87454 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

TT pretty-printing - also in elab debug

3d87454David Raymond Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs−6

compare with master

unifiedsplit

@@ -1661,12 +1661,6 @@ isHoleName _ = False

1661containsHole :: PTerm -> Bool

1662containsHole pterm = or [isHoleName n | PRef _ n <- take 1000 $ universe pterm]

1663

1664−-- | Pretty-printer helper for the binding site of a name

1665−bindingOf :: Name -- ^^ the bound name

1666− -> Bool -- ^^ whether the name is implicit

1667− -> Doc OutputAnnotation

1668−bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))

1669−

1670-- | Pretty-printer helper for names that attaches the correct annotations

1664-- | Pretty-printer helper for names that attaches the correct annotations

1671prettyName

1665prettyName

1672 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator

1666 :: Bool -- ^^ whether the name should be parenthesised if it is an infix operator

src/Idris/Core/TT.hs+97−1

@@ -30,7 +30,7 @@ import Data.Char

30import Data.Data (Data)

31import Numeric (showIntAtBase)

32import qualified Data.Text as T

33−import Data.List hiding (insert)

33+import Data.List hiding (group, insert)

34import Data.Set(Set, member, fromList, insert)

35import Data.Maybe (listToMaybe)

36import Data.Foldable (Foldable)

@@ -1498,3 +1498,99 @@ allTTNames = nub . allNamesIn

1498 nb t = allNamesIn (binderTy t)

1499 allNamesIn (App f a) = allNamesIn f ++ allNamesIn a

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

src/Idris/Delaborate.hs+3−3

@@ -342,7 +342,7 @@ pprintErr' i (ReflectionFailed msg err) =

342pprintErr' i (ElabDebug msg tm holes) =

343 text "Elaboration halted." <>

344 maybe empty (indented . text) msg <> line <>

345− text "Term: " <> indented (pprintTerm' i [] (delab i tm)) <> line <>

345+ text "Term: " <> indented (pprintTT [] tm) <> line <>

346 text "Holes:" <>

347 indented (vsep (map ppHole holes))

348

@@ -351,13 +351,13 @@ pprintErr' i (ElabDebug msg tm holes) =

351 ppAssumptions [] (reverse env) <>

352 text "----------------------------------" <> line <>

353 bindingOf hn False <+> text ":" <+>

354− pprintTerm' i (zip (map fst env) (repeat False)) (delab i goal) <> line

354+ pprintTT (map fst (reverse env)) goal <> line

355 ppAssumptions :: [Name] -> Env -> Doc OutputAnnotation

356 ppAssumptions ns [] = empty

357 ppAssumptions ns ((n, b) : rest) =

358 bindingOf n False <+>

359 text ":" <+>

360− pprintTerm' i (zip ns (repeat False)) (delab i (binderTy b)) <>

360+ pprintTT ns (binderTy b) <>

361 line <>

362 ppAssumptions (n:ns) rest

363