git.iko.soy/Idris-dev
on master help sign in
Colouring support in the prover
commit5f0c4494a817bfdd0f6d065191858522b138a28b authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 26 Jan 2014, 23:51 (13 years ago) parent13f3c29
4 files changed+252−207
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+223−2 src/Idris/AbsSyntaxTree.hs−182 src/Idris/Core/TT.hs+7−6 src/Idris/Prover.hs+22−17
src/Idris/AbsSyntax.hs+223−2
@@ -424,7 +424,7 @@ ideslavePutSExp cmd info = do i <- getIState
424424iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
425425iputGoal g = do i <- getIState
426426 case idris_outputmode i of
427− RawOutput -> runIO $ displayIO stdout g >> putStrLn ""
427+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)
428428 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n
429429
430430isetPrompt :: String -> Idris ()
@@ -757,7 +757,7 @@ eqOpts = []
757757elimName = sUN "__Elim"
758758elimMethElimTy = sUN "__elimTy"
759759elimMethElim = sUN "elim"
760−elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
760+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
761761 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
762762 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
763763
@@ -1722,3 +1722,224 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17221722 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)
17231723 mkUniq t = return t
17241724
1725+
1726+---------------------------------------------------------
1727+-- Pretty-printing
1728+---------------------------------------------------------
1729+
1730+instance Pretty PTerm OutputAnnotation where
1731+ pretty = prettyImp False
1732+
1733+-- | Colourise annotations according to an Idris state. It ignores the names
1734+-- in the annotation, as there's no good way to show extended information on a
1735+-- terminal.
1736+consoleDecorate :: IState -> OutputAnnotation -> String -> String
1737+consoleDecorate ist _ | not (idris_colourRepl ist) = id
1738+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1739+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1740+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
1741+ theme = idris_colourTheme ist
1742+ in case () of
1743+ _ | isDConName n ctxt -> colouriseData theme
1744+ _ | isFnName n ctxt -> colouriseFun theme
1745+ _ | isTConName n ctxt -> colouriseType theme
1746+ _ | otherwise -> id -- don't colourise unknown names
1747+
1748+-- | Pretty-print a high-level closed Idris term
1749+prettyImp :: Bool -- ^^ whether to show implicits
1750+ -> PTerm -- ^^ the term to pretty-print
1751+ -> Doc OutputAnnotation
1752+prettyImp impl = pprintPTerm impl []
1753+
1754+-- | Pretty-print a high-level Idris term in some bindings context
1755+pprintPTerm :: Bool -- ^^ whether to show implicits
1756+ -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1757+ -> PTerm -- ^^ the term to pretty-print
1758+ -> Doc OutputAnnotation
1759+pprintPTerm impl bnd = prettySe 10 bnd
1760+ where
1761+ prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1762+ prettySe p bnd (PQuote r) =
1763+ if size r > breakingSize then
1764+ text "![" <> line <> pretty r <> text "]"
1765+ else
1766+ text "![" <> pretty r <> text "]"
1767+ prettySe p bnd (PPatvar fc n) = pretty n
1768+ prettySe p bnd (PRef fc n) = prettyName impl bnd n
1769+ prettySe p bnd (PLam n ty sc) =
1770+ bracket p 2 $
1771+ if size sc > breakingSize then
1772+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc
1773+ else
1774+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc
1775+ prettySe p bnd (PLet n ty v sc) =
1776+ bracket p 2 $
1777+ if size sc > breakingSize then
1778+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
1779+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)
1780+ else
1781+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
1782+ prettySe 10 ((n, False):bnd) sc
1783+ prettySe p bnd (PPi (Exp l s _ _) n ty sc)
1784+ | n `elem` allNamesIn sc || impl =
1785+ let open = (if l then text "|" else empty) <> lparen in
1786+ bracket p 2 $
1787+ if size sc > breakingSize then
1788+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1789+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
1790+ else
1791+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1792+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
1793+ | otherwise =
1794+ bracket p 2 $
1795+ if size sc > breakingSize then
1796+ prettySe 0 bnd ty <+> st <+> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
1797+ else
1798+ prettySe 0 bnd ty <+> st <+> text "->" <+> prettySe 10 ((n, False):bnd) sc
1799+ where
1800+ st =
1801+ case s of
1802+ Static -> text "[static]" <> space
1803+ _ -> empty
1804+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)
1805+ | impl =
1806+ let open = if l then text "|" <> lbrace else lbrace in
1807+ bracket p 2 $
1808+ if size sc > breakingSize then
1809+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1810+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1811+ else
1812+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1813+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1814+ | otherwise = prettySe 10 ((n, True):bnd) sc
1815+ where
1816+ st =
1817+ case s of
1818+ Static -> text "[static]" <> space
1819+ _ -> empty
1820+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
1821+ bracket p 2 $
1822+ if size sc > breakingSize then
1823+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc
1824+ else
1825+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc
1826+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
1827+ bracket p 2 $
1828+ if size sc > breakingSize then
1829+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>
1830+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc
1831+ else
1832+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1833+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
1834+ prettySe p bnd (PApp _ (PRef _ f) [])
1835+ | not impl = pretty f
1836+ prettySe p bnd (PAppBind _ (PRef _ f) [])
1837+ | not impl = text "!" <+> pretty f
1838+ prettySe p bnd (PApp _ (PRef _ op@(UN nm)) args)
1839+ | not (tnull nm) &&
1840+ length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1841+ let [l, r] = getExps args in
1842+ bracket p 1 $
1843+ if size r > breakingSize then
1844+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r
1845+ else
1846+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r
1847+ prettySe p bnd (PApp _ f as) =
1848+ let args = getExps as in
1849+ bracket p 1 $
1850+ prettySe 1 bnd f <+>
1851+ align (hsep (if impl
1852+ then map (prettyArgS bnd) as
1853+ else map (prettyArgSe bnd) args))
1854+ prettySe p bnd (PCase _ scr opts) =
1855+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
1856+ where
1857+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1858+
1859+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1860+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1861+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
1862+ prettySe p bnd (PResolveTC _) = text "resolvetc"
1863+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
1864+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
1865+ prettySe p bnd (PEq _ l r) =
1866+ bracket p 2 $
1867+ if size r > breakingSize then
1868+ prettySe 10 bnd l <+> eq <> nest nestingSize (prettySe 10 bnd r)
1869+ else
1870+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
1871+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
1872+ prettySe p bnd (PRewrite _ l r _) =
1873+ bracket p 2 $
1874+ if size r > breakingSize then
1875+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)
1876+ else
1877+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1878+ prettySe p bnd (PTyped l r) =
1879+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1880+ prettySe p bnd (PPair _ l r) =
1881+ if size r > breakingSize then
1882+ lparen <> prettySe 10 bnd l <> text "," <>
1883+ line <> prettySe 10 bnd r <> rparen
1884+ else
1885+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
1886+ prettySe p bnd (PDPair _ l t r) =
1887+ if size r > breakingSize then
1888+ lparen <> prettySe 10 bnd l <+> text "**" <>
1889+ line <> prettySe 10 bnd r <> rparen
1890+ else
1891+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1892+ prettySe p bnd (PAlternative a as) =
1893+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
1894+ where
1895+ prettyAs =
1896+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1897+ prettySe p bnd PType = text "Type"
1898+ prettySe p bnd (PConstant c) = pretty c
1899+ -- XXX: add pretty for tactics
1900+ prettySe p bnd (PProof ts) =
1901+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1902+ prettySe p bnd (PTactics ts) =
1903+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1904+ prettySe p bnd (PMetavar n) = text "?" <> pretty n
1905+ prettySe p bnd (PReturn f) = text "return"
1906+ prettySe p bnd PImpossible = text "impossible"
1907+ prettySe p bnd Placeholder = text "_"
1908+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1909+ prettySe p bnd (PElabError s) = pretty s
1910+
1911+ prettySe p bnd _ = text "test"
1912+
1913+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)
1914+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm
1915+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm
1916+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)
1917+
1918+ prettyArgSe bnd arg = prettySe 0 bnd arg
1919+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1920+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1921+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1922+
1923+
1924+ bracket outer inner doc
1925+ | inner > outer = lparen <> doc <> rparen
1926+ | otherwise = doc
1927+
1928+-- | Pretty-printer helper for the binding site of a name
1929+bindingOf :: Name -- ^^ the bound name
1930+ -> Bool -- ^^ whether the name is implicit
1931+ -> Doc OutputAnnotation
1932+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1933+
1934+-- | Pretty-printer helper for names that attaches the correct annotations
1935+prettyName :: Bool -- ^^ whether to show namespaces
1936+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1937+ -> Name -- ^^ the name to pprint
1938+ -> Doc OutputAnnotation
1939+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1940+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
1941+ where strName (UN n) = T.unpack n
1942+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1943+ | otherwise = strName n
1944+ strName (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"
1945+ strName other = show other
src/Idris/AbsSyntaxTree.hs−182
@@ -897,8 +897,6 @@ expandNS syn n = case syn_namespace syn of
897897instance Show PTerm where
898898 show tm = showImp Nothing False False tm
899899
900−instance Pretty PTerm OutputAnnotation where
901− pretty = prettyImp False
902900
903901instance Show PDecl where
904902 show d = showDeclImp False d
@@ -968,186 +966,6 @@ getAll :: [PArg] -> [PTerm]
968966getAll = map getTm
969967
970968
971−-- | Pretty-print a high-level Idris term
972−prettyImp :: Bool -- ^^ whether to show implicits
973− -> PTerm -- ^^ the term to pretty-print
974− -> Doc OutputAnnotation
975−prettyImp impl = prettySe 10
976− where
977− prettySe :: Int -> PTerm -> Doc OutputAnnotation
978− prettySe p (PQuote r) =
979− if size r > breakingSize then
980− text "![" <> line <> pretty r <> text "]"
981− else
982− text "![" <> pretty r <> text "]"
983− prettySe p (PPatvar fc n) = pretty n
984− prettySe p (PRef fc n) =
985− if impl then
986− pretty n
987− else
988− prettyBasic n
989− where
990− prettyBasic n@(UN _) = pretty n
991− prettyBasic (MN _ s) = text (str s)
992− prettyBasic (NS n s) = (foldr (<>) empty (intersperse (text ".") (map (text.str) $ reverse s))) <> prettyBasic n
993− prettyBasic (SN sn) = text (show sn)
994− prettySe p (PLam n ty sc) =
995− bracket p 2 $
996− if size sc > breakingSize then
997− text "λ" <> pretty n <+> text "=>" <> line <> pretty sc
998− else
999− text "λ" <> pretty n <+> text "=>" <+> pretty sc
1000− prettySe p (PLet n ty v sc) =
1001− bracket p 2 $
1002− if size sc > breakingSize then
1003− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <>
1004− nest nestingSize (prettySe 10 sc)
1005− else
1006− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
1007− prettySe 10 sc
1008− prettySe p (PPi (Exp l s _ _) n ty sc)
1009− | n `elem` allNamesIn sc || impl =
1010− let open = (if l then text "|" else empty) <> lparen in
1011− bracket p 2 $
1012− if size sc > breakingSize then
1013− enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>
1014− st <> text "->" <> line <> prettySe 10 sc
1015− else
1016− enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>
1017− st <> text "->" <+> prettySe 10 sc
1018− | otherwise =
1019− bracket p 2 $
1020− if size sc > breakingSize then
1021− prettySe 0 ty <+> st <+> text "->" <> line <> prettySe 10 sc
1022− else
1023− prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
1024− where
1025− st =
1026− case s of
1027− Static -> text "[static]" <> space
1028− _ -> empty
1029− prettySe p (PPi (Imp l s _ _) n ty sc)
1030− | impl =
1031− let open = if l then text "|" <> lbrace else lbrace in
1032− bracket p 2 $
1033− if size sc > breakingSize then
1034− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1035− st <> text "->" <+> prettySe 10 sc
1036− else
1037− open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1038− st <> text "->" <+> prettySe 10 sc
1039− | otherwise = prettySe 10 sc
1040− where
1041− st =
1042− case s of
1043− Static -> text "[static]" <> space
1044− _ -> empty
1045− prettySe p (PPi (Constraint _ _ _) n ty sc) =
1046− bracket p 2 $
1047− if size sc > breakingSize then
1048− prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
1049− else
1050− prettySe 10 ty <+> text "=>" <> line <> prettySe 10 sc
1051− prettySe p (PPi (TacImp _ _ s _) n ty sc) =
1052− bracket p 2 $
1053− if size sc > breakingSize then
1054− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1055− rbrace <+> text "->" <> line <> prettySe 10 sc
1056− else
1057− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1058− rbrace <+> text "->" <+> prettySe 10 sc
1059− prettySe p (PApp _ (PRef _ f) [])
1060− | not impl = pretty f
1061− prettySe p (PAppBind _ (PRef _ f) [])
1062− | not impl = text "!" <+> pretty f
1063− prettySe p (PApp _ (PRef _ op@(UN nm)) args)
1064− | not (tnull nm) &&
1065− length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1066− let [l, r] = getExps args in
1067− bracket p 1 $
1068− if size r > breakingSize then
1069− prettySe 1 l <+> pretty op <> line <> prettySe 0 r
1070− else
1071− prettySe 1 l <+> pretty op <+> prettySe 0 r
1072− prettySe p (PApp _ f as) =
1073− let args = getExps as in
1074− bracket p 1 $
1075− prettySe 1 f <+>
1076− align (hsep (if impl
1077− then map prettyArgS as
1078− else map prettyArgSe args))
1079− prettySe p (PCase _ scr opts) =
1080− text "case" <+> prettySe 10 scr <+> text "of" <> prettyBody
1081− where
1082− prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1083−
1084− sc (l, r) = nest nestingSize $ prettySe 10 l <+> text "=>" <+> prettySe 10 r
1085− prettySe p (PHidden tm) = text "." <> prettySe 0 tm
1086− prettySe p (PRefl _ _) = text "refl"
1087− prettySe p (PResolveTC _) = text "resolvetc"
1088− prettySe p (PTrue _) = text "()"
1089− prettySe p (PFalse _) = text "_|_"
1090− prettySe p (PEq _ l r) =
1091− bracket p 2 $
1092− if size r > breakingSize then
1093− prettySe 10 l <+> text "=" <> nest nestingSize (prettySe 10 r)
1094− else
1095− prettySe 10 l <+> text "=" <+> prettySe 10 r
1096− prettySe p (PRewrite _ l r _) =
1097− bracket p 2 $
1098− if size r > breakingSize then
1099− text "rewrite" <+> prettySe 10 l <+> text "in" <> nest nestingSize (prettySe 10 r)
1100− else
1101− text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
1102− prettySe p (PTyped l r) =
1103− lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
1104− prettySe p (PPair _ l r) =
1105− if size r > breakingSize then
1106− lparen <> prettySe 10 l <> text "," <>
1107− line <> prettySe 10 r <> rparen
1108− else
1109− lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
1110− prettySe p (PDPair _ l t r) =
1111− if size r > breakingSize then
1112− lparen <> prettySe 10 l <+> text "**" <>
1113− line <> prettySe 10 r <> rparen
1114− else
1115− lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
1116− prettySe p (PAlternative a as) =
1117− lparen <> text "|" <> prettyAs <> text "|" <> rparen
1118− where
1119− prettyAs =
1120− foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10) as
1121− prettySe p PType = text "Type"
1122− prettySe p (PConstant c) = pretty c
1123− -- XXX: add pretty for tactics
1124− prettySe p (PProof ts) =
1125− text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1126− prettySe p (PTactics ts) =
1127− text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1128− prettySe p (PMetavar n) = text "?" <> pretty n
1129− prettySe p (PReturn f) = text "return"
1130− prettySe p PImpossible = text "impossible"
1131− prettySe p Placeholder = text "_"
1132− prettySe p (PDoBlock _) = text "do block pretty not implemented"
1133− prettySe p (PElabError s) = pretty s
1134−
1135− prettySe p _ = text "test"
1136−
1137− prettyArgS (PImp _ _ _ n tm _) = prettyArgSi (n, tm)
1138− prettyArgS (PExp _ _ tm _) = prettyArgSe tm
1139− prettyArgS (PConstraint _ _ tm _) = prettyArgSc tm
1140− prettyArgS (PTacImplicit _ _ n _ tm _) = prettyArgSti (n, tm)
1141−
1142− prettyArgSe arg = prettySe 0 arg
1143− prettyArgSi (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1144− prettyArgSc val = lbrace <> lbrace <> prettySe 10 val <> rbrace <> rbrace
1145− prettyArgSti (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 val <> rbrace
1146−
1147− bracket outer inner doc
1148− | inner > outer = lparen <> doc <> rparen
1149− | otherwise = doc
1150−
1151969-- | Show Idris name
1152970showName :: Maybe IState -- ^^ the Idris state, for information about names and colours
1153971 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit
src/Idris/Core/TT.hs+7−6
@@ -78,10 +78,11 @@ instance Show FC where
7878 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
7979
8080-- | Output annotation for pretty-printed name - decides colour
81−data NameOutput = TypeOutput | FunOutput | DataOutput | BoundOutput Bool
81+data NameOutput = TypeOutput | FunOutput | DataOutput
8282
8383-- | Output annotations for pretty-printing
84−data OutputAnnotation = OutName Name (Maybe NameOutput) (Maybe Type)
84+data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)
85+ | AnnBoundName Name Bool
8586
8687-- | Used for error reflection
8788data ErrorReportPart = TextPart String
@@ -294,11 +295,11 @@ instance Sized Name where
294295 size _ = 1
295296
296297instance Pretty Name OutputAnnotation where
297− pretty n@(UN n') = annotate (OutName n Nothing Nothing) $ text (T.unpack n')
298− pretty n@(NS un s) = annotate (OutName n Nothing Nothing) . noAnnotate $ pretty n
299− pretty n@(MN i s) = annotate (OutName n Nothing Nothing) $
298+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')
299+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un
300+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $
300301 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
301− pretty n@(SN s) = annotate (OutName n Nothing Nothing) $ text (show s)
302+ pretty n@(SN s) = annotate (AnnName n Nothing Nothing) $ text (show s)
302303
303304instance Pretty [Name] OutputAnnotation where
304305 pretty = encloseSep empty empty comma . map pretty
src/Idris/Prover.hs+22−17
@@ -89,47 +89,52 @@ elabStep st e = do case runStateT e st of
8989
9090dumpState :: IState -> ProofState -> Idris ()
9191dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
92− iputGoal . renderPretty 0.7 breakingSize $ pretty nm <> colon <+> text "No more goals."
92+ iputGoal . renderPretty 0.7 breakingSize $
93+ prettyName False [] nm <> colon <+> text "No more goals."
9394dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
9495 let OK ty = goalAtFocus ps
9596 let OK env = envAtFocus ps
9697 iputGoal . renderPretty 0.7 breakingSize $
9798 prettyOtherGoals hs <> line <>
9899 prettyAssumptions env <> line <>
99− prettyGoal ty
100+ prettyGoal (zip (assumptionNames env) (repeat False)) ty
100101 where
101102 -- XXX
102− tPretty t = pretty $ delab ist t
103+ tPretty bnd t = pprintPTerm True bnd $ delab ist t
104+
105+ assumptionNames :: Env -> [Name]
106+ assumptionNames = map fst
103107
104− prettyPs [] = empty
105− prettyPs ((MN _ r, _) : bs)
106− | r == txt "rewrite_rule" = prettyPs bs
107− prettyPs ((n, Let t v) : bs) =
108− nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
109− tPretty t <> line <> prettyPs bs)
110− prettyPs ((n, b) : bs) =
111− line <> pretty n <+> colon <+> tPretty (binderTy b) <> prettyPs bs
108+ prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation
109+ prettyPs bnd [] = empty
110+ prettyPs bnd ((n@(MN _ r), _) : bs)
111+ | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs
112+ prettyPs bnd ((n, Let t v) : bs) =
113+ nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>
114+ tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)
115+ prettyPs bnd ((n, b) : bs) =
116+ line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs
112117
113− prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
114− prettyG b = tPretty $ binderTy b
118+ prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v
119+ prettyG bnd b = tPretty bnd $ binderTy b
115120
116− prettyGoal ty =
121+ prettyGoal bnd ty =
117122 text "---------- Goal: ----------" <$$>
118− pretty h <+> colon <+> nest nestingSize (prettyG ty)
123+ bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)
119124
120125 prettyAssumptions env =
121126 if length env == 0 then
122127 empty
123128 else
124129 text "---------- Assumptions: ----------" <>
125− nest nestingSize (prettyPs $ reverse env)
130+ nest nestingSize (prettyPs [] $ reverse env)
126131
127132 prettyOtherGoals hs =
128133 if length hs == 0 then
129134 empty
130135 else
131136 text "---------- Other goals: ----------" <$$>
132− nest nestingSize (align . cat . punctuate (text ",") . map pretty $ hs)
137+ nest nestingSize (align . cat . punctuate (text ",") . map (flip bindingOf False) $ hs)
133138
134139lifte :: ElabState [PDecl] -> ElabD a -> Idris a
135140lifte st e = do (v, _) <- elabStep st e