5f0c449 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Colouring support in the prover

5f0c449David Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+223−2

compare with master

unifiedsplit

@@ -424,7 +424,7 @@ ideslavePutSExp cmd info = do i <- getIState

424iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

425iputGoal g = do i <- getIState

426 case idris_outputmode i of

427− RawOutput -> runIO $ displayIO stdout g >> putStrLn ""

427+ RawOutput -> runIO $ putStrLn (displayDecorated (consoleDecorate i) g)

428 IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n

429

430isetPrompt :: String -> Idris ()

@@ -757,7 +757,7 @@ eqOpts = []

757elimName = sUN "__Elim"

758elimMethElimTy = sUN "__elimTy"

759elimMethElim = 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)]

761 [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,

762 PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]

763

@@ -1722,3 +1722,224 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1722 mkUniq (PTactics ts) = liftM PTactics (mapM mkUniqT ts)

1723 mkUniq t = return t

1724

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

897instance Show PTerm where

898 show tm = showImp Nothing False False tm

899

900−instance Pretty PTerm OutputAnnotation where

901− pretty = prettyImp False

902

900

903instance Show PDecl where

901instance Show PDecl where

904 show d = showDeclImp False d

902 show d = showDeclImp False d

@@ -968,186 +966,6 @@ getAll :: [PArg] -> [PTerm]

968getAll = map getTm

966getAll = map getTm

969

967

970

968

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−

1151-- | Show Idris name

969-- | Show Idris name

1152showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

970showName :: Maybe IState -- ^^ the Idris state, for information about names and colours

1153 -> [(Name, Bool)] -- ^^ the bound variables and whether they're implicit

971 -> [(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

78 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

80-- | Output annotation for pretty-printed name - decides colour

81−data NameOutput = TypeOutput | FunOutput | DataOutput | BoundOutput Bool

81+data NameOutput = TypeOutput | FunOutput | DataOutput

83-- | 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

86-- | Used for error reflection

87-- | Used for error reflection

87data ErrorReportPart = TextPart String

88data ErrorReportPart = TextPart String

@@ -294,11 +295,11 @@ instance Sized Name where

294 size _ = 1

295 size _ = 1

295

296

296instance Pretty Name OutputAnnotation where

297instance Pretty Name OutputAnnotation where

297− pretty n@(UN n') = annotate (OutName n Nothing Nothing) $ text (T.unpack n')

298+ pretty n@(UN n') = annotate (AnnName n Nothing Nothing) $ text (T.unpack n')

298− pretty n@(NS un s) = annotate (OutName n Nothing Nothing) . noAnnotate $ pretty n

299+ pretty n@(NS un s) = annotate (AnnName n Nothing Nothing) . noAnnotate $ pretty un

299− pretty n@(MN i s) = annotate (OutName n Nothing Nothing) $

300+ pretty n@(MN i s) = annotate (AnnName n Nothing Nothing) $

300 lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

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

302

303

303instance Pretty [Name] OutputAnnotation where

304instance Pretty [Name] OutputAnnotation where

304 pretty = encloseSep empty empty comma . map pretty

305 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

90dumpState :: IState -> ProofState -> Idris ()

91dumpState 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."

93dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do

94 let OK ty = goalAtFocus ps

95 let OK ty = goalAtFocus ps

95 let OK env = envAtFocus ps

96 let OK env = envAtFocus ps

96 iputGoal . renderPretty 0.7 breakingSize $

97 iputGoal . renderPretty 0.7 breakingSize $

97 prettyOtherGoals hs <> line <>

98 prettyOtherGoals hs <> line <>

98 prettyAssumptions env <> line <>

99 prettyAssumptions env <> line <>

99− prettyGoal ty

100+ prettyGoal (zip (assumptionNames env) (repeat False)) ty

100 where

101 where

101 -- XXX

102 -- 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

103

107

104− prettyPs [] = empty

108+ prettyPs :: [(Name, Bool)] -> Env -> Doc OutputAnnotation

109+ prettyPs bnd [] = empty

105− prettyPs ((MN _ r, _) : bs)

110+ prettyPs bnd ((n@(MN _ r), _) : bs)

106− | r == txt "rewrite_rule" = prettyPs bs

111+ | r == txt "rewrite_rule" = prettyPs ((n, False):bnd) bs

107− prettyPs ((n, Let t v) : bs) =

112+ prettyPs bnd ((n, Let t v) : bs) =

108− nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>

113+ nest nestingSize (bindingOf n False <+> text "=" <+> tPretty bnd v <> colon <+>

109− tPretty t <> line <> prettyPs bs)

114+ tPretty ((n, False):bnd) t <> line <> prettyPs ((n, False):bnd) bs)

110− prettyPs ((n, b) : bs) =

115+ prettyPs bnd ((n, b) : bs) =

111− line <> pretty n <+> colon <+> tPretty (binderTy b) <> prettyPs bs

116+ line <> bindingOf n False <+> colon <+> tPretty bnd (binderTy b) <> prettyPs ((n, False):bnd) bs

112

117

113− prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v

118+ prettyG bnd (Guess t v) = tPretty bnd t <+> text "=?=" <+> tPretty bnd v

114− prettyG b = tPretty $ binderTy b

119+ prettyG bnd b = tPretty bnd $ binderTy b

115

120

116− prettyGoal ty =

121+ prettyGoal bnd ty =

117 text "---------- Goal: ----------" <$$>

122 text "---------- Goal: ----------" <$$>

118− pretty h <+> colon <+> nest nestingSize (prettyG ty)

123+ bindingOf h False <+> colon <+> nest nestingSize (prettyG bnd ty)

119

124

120 prettyAssumptions env =

125 prettyAssumptions env =

121 if length env == 0 then

126 if length env == 0 then

122 empty

127 empty

123 else

128 else

124 text "---------- Assumptions: ----------" <>

129 text "---------- Assumptions: ----------" <>

125− nest nestingSize (prettyPs $ reverse env)

130+ nest nestingSize (prettyPs [] $ reverse env)

126

131

127 prettyOtherGoals hs =

132 prettyOtherGoals hs =

128 if length hs == 0 then

133 if length hs == 0 then

129 empty

134 empty

130 else

135 else

131 text "---------- Other goals: ----------" <$$>

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

133

138

134lifte :: ElabState [PDecl] -> ElabD a -> Idris a

139lifte :: ElabState [PDecl] -> ElabD a -> Idris a

135lifte st e = do (v, _) <- elabStep st e

140lifte st e = do (v, _) <- elabStep st e