git.iko.soy/Idris-dev
on master help sign in
Replace the string-slinging show with pretty-print

The built-in show for PTerms has been completely removed. This reduces code duplication, but it also ensures that semantics last longer - a step towards better IDE support.

commitdc4ce0cfa73246fec6d7c9052d4f53601215da98 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 27 Jan 2014, 03:25 (13 years ago) parent5f0c449
13 files changed+498−622
compare with master
unifiedsplit
src/Idris/AbsSyntax.hs+1−305 src/Idris/AbsSyntaxTree.hs+394−196 src/Idris/CaseSplit.hs+3−3 src/Idris/Core/TT.hs+2 src/Idris/Coverage.hs+3−3 src/Idris/Delaborate.hs+36−49 src/Idris/ElabDecls.hs+32−32 src/Idris/Parser.hs+1−1 src/Idris/REPL.hs+16−23 src/Util/Pretty.hs+1−1 test/reg007/expected+4−4 test/reg007/run+1−1 test/test037/expected+4−4
src/Idris/AbsSyntax.hs+1−305
@@ -688,90 +688,6 @@ setTypeCase t = do i <- getIState
688688 putIState $ i { idris_options = opt' }
689689
690690
691−-- For inferring types of things
692−
693−bi = fileFC "builtin"
694−
695−inferTy = sMN 0 "__Infer"
696−inferCon = sMN 0 "__infer"
697−inferDecl = PDatadecl inferTy
698− PType
699− [("", inferCon, PPi impl (sMN 0 "iType") PType (
700− PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
701− (PRef bi inferTy)), bi, [])]
702−inferOpts = []
703−
704−infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
705−infP = P (TCon 6 0) inferTy (TType (UVal 0))
706−
707−getInferTerm, getInferType :: Term -> Term
708−getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
709−getInferTerm (App (App _ _) tm) = tm
710−getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
711−
712−getInferType (Bind n b sc) = Bind n b $ getInferType sc
713−getInferType (App (App _ ty) _) = ty
714−
715−-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
716−
717−primNames = [unitTy, unitCon,
718− falseTy, pairTy, pairCon,
719− eqTy, eqCon, inferTy, inferCon]
720−
721−unitTy = sMN 0 "__Unit"
722−unitCon = sMN 0 "__II"
723−unitDecl = PDatadecl unitTy PType
724− [("", unitCon, PRef bi unitTy, bi, [])]
725−unitOpts = [DefaultEliminator]
726−
727−falseTy = sMN 0 "__False"
728−falseDecl = PDatadecl falseTy PType []
729−falseOpts = []
730−
731−pairTy = sMN 0 "__Pair"
732−pairCon = sMN 0 "__MkPair"
733−pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
734− [("", pairCon, PPi impl (n "A") PType (
735− PPi impl (n "B") PType (
736− PPi expl (n "a") (PRef bi (n "A")) (
737− PPi expl (n "b") (PRef bi (n "B"))
738− (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
739− pexp (PRef bi (n "B"))])))), bi, [])]
740− where n a = sMN 0 a
741−pairOpts = []
742−
743−eqTy = sUN "="
744−eqCon = sUN "refl"
745−eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
746− (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
747− PType)
748− [("", eqCon, PPi impl (n "A") PType (
749− PPi impl (n "x") (PRef bi (n "A"))
750− (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
751− pimp (n "B") Placeholder False,
752− pexp (PRef bi (n "x")),
753− pexp (PRef bi (n "x"))])), bi, [])]
754− where n a = sMN 0 a
755−eqOpts = []
756−
757−elimName = sUN "__Elim"
758−elimMethElimTy = sUN "__elimTy"
759−elimMethElim = sUN "elim"
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−
764−-- Defined in builtins.idr
765−sigmaTy = sUN "Exists"
766−existsCon = sUN "Ex_intro"
767−
768−piBind :: [(Name, PTerm)] -> PTerm -> PTerm
769−piBind = piBindp expl
770−
771−piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
772−piBindp p [] t = t
773−piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
774−
775691-- Dealing with parameters
776692
777693expandParams :: (Name -> Name) -> [(Name, PTerm)] ->
@@ -1438,7 +1354,7 @@ mkPApp fc a f as = let rest = drop a as in
14381354-- FIXME: It's possible that this really has to happen after elaboration
14391355
14401356findStatics :: IState -> PTerm -> (PTerm, [Bool])
1441−findStatics ist tm = trace (showImp Nothing True False tm) $
1357+findStatics ist tm = trace (show tm) $
14421358 let (ns, ss) = fs tm in
14431359 runState (pos ns ss tm) []
14441360 where fs (PPi p n t sc)
@@ -1723,223 +1639,3 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where
17231639 mkUniq t = return t
17241640
17251641
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+394−196
@@ -892,60 +892,412 @@ expandNS syn n = case syn_namespace syn of
892892 xs -> sNS n xs
893893
894894
895−--- Pretty printing declarations and terms
895+-- For inferring types of things
896+
897+bi = fileFC "builtin"
898+
899+inferTy = sMN 0 "__Infer"
900+inferCon = sMN 0 "__infer"
901+inferDecl = PDatadecl inferTy
902+ PType
903+ [("", inferCon, PPi impl (sMN 0 "iType") PType (
904+ PPi expl (sMN 0 "ival") (PRef bi (sMN 0 "iType"))
905+ (PRef bi inferTy)), bi, [])]
906+inferOpts = []
907+
908+infTerm t = PApp bi (PRef bi inferCon) [pimp (sMN 0 "iType") Placeholder True, pexp t]
909+infP = P (TCon 6 0) inferTy (TType (UVal 0))
910+
911+getInferTerm, getInferType :: Term -> Term
912+getInferTerm (Bind n b sc) = Bind n b $ getInferTerm sc
913+getInferTerm (App (App _ _) tm) = tm
914+getInferTerm tm = tm -- error ("getInferTerm " ++ show tm)
915+
916+getInferType (Bind n b sc) = Bind n b $ getInferType sc
917+getInferType (App (App _ ty) _) = ty
918+
919+
920+
921+-- Handy primitives: Unit, False, Pair, MkPair, =, mkForeign, Elim type class
922+
923+primNames = [unitTy, unitCon,
924+ falseTy, pairTy, pairCon,
925+ eqTy, eqCon, inferTy, inferCon]
926+
927+unitTy = sMN 0 "__Unit"
928+unitCon = sMN 0 "__II"
929+unitDecl = PDatadecl unitTy PType
930+ [("", unitCon, PRef bi unitTy, bi, [])]
931+unitOpts = [DefaultEliminator]
932+
933+falseTy = sMN 0 "__False"
934+falseDecl = PDatadecl falseTy PType []
935+falseOpts = []
936+
937+pairTy = sMN 0 "__Pair"
938+pairCon = sMN 0 "__MkPair"
939+pairDecl = PDatadecl pairTy (piBind [(n "A", PType), (n "B", PType)] PType)
940+ [("", pairCon, PPi impl (n "A") PType (
941+ PPi impl (n "B") PType (
942+ PPi expl (n "a") (PRef bi (n "A")) (
943+ PPi expl (n "b") (PRef bi (n "B"))
944+ (PApp bi (PRef bi pairTy) [pexp (PRef bi (n "A")),
945+ pexp (PRef bi (n "B"))])))), bi, [])]
946+ where n a = sMN 0 a
947+pairOpts = []
948+
949+eqTy = sUN "="
950+eqCon = sUN "refl"
951+eqDecl = PDatadecl eqTy (piBind [(n "A", PType), (n "B", PType),
952+ (n "x", PRef bi (n "A")), (n "y", PRef bi (n "B"))]
953+ PType)
954+ [("", eqCon, PPi impl (n "A") PType (
955+ PPi impl (n "x") (PRef bi (n "A"))
956+ (PApp bi (PRef bi eqTy) [pimp (n "A") Placeholder False,
957+ pimp (n "B") Placeholder False,
958+ pexp (PRef bi (n "x")),
959+ pexp (PRef bi (n "x"))])), bi, [])]
960+ where n a = sMN 0 a
961+eqOpts = []
962+
963+elimName = sUN "__Elim"
964+elimMethElimTy = sUN "__elimTy"
965+elimMethElim = sUN "elim"
966+elimDecl = PClass "Type class for eliminators" defaultSyntax bi [] elimName [(sUN "scrutineeType", PType)]
967+ [PTy "" defaultSyntax bi [TotalFn] elimMethElimTy PType,
968+ PTy "" defaultSyntax bi [TotalFn] elimMethElim (PRef bi elimMethElimTy)]
969+
970+-- Defined in builtins.idr
971+sigmaTy = sUN "Exists"
972+existsCon = sUN "Ex_intro"
973+
974+piBind :: [(Name, PTerm)] -> PTerm -> PTerm
975+piBind = piBindp expl
976+
977+piBindp :: Plicity -> [(Name, PTerm)] -> PTerm -> PTerm
978+piBindp p [] t = t
979+piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)
980+
981+
982+-- Pretty-printing declarations and terms
896983
897984instance Show PTerm where
898− show tm = showImp Nothing False False tm
899−
985+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm
900986
901987instance Show PDecl where
902− show d = showDeclImp False d
988+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d
903989
904990instance Show PClause where
905− show c = showCImp True c
991+ showsPrec _ c = (displayS . renderCompact . showCImp True) c
906992
907993instance Show PData where
908− show d = showDImp False d
994+ showsPrec _ d = (displayS . renderCompact . showDImp False) d
995+
996+instance Pretty PTerm OutputAnnotation where
997+ pretty = prettyImp False
998+
999+-- | Colourise annotations according to an Idris state. It ignores the names
1000+-- in the annotation, as there's no good way to show extended information on a
1001+-- terminal.
1002+consoleDecorate :: IState -> OutputAnnotation -> String -> String
1003+consoleDecorate ist _ | not (idris_colourRepl ist) = id
1004+consoleDecorate ist AnnConstData = let theme = idris_colourTheme ist
1005+ in colouriseData theme
1006+consoleDecorate ist AnnConstType = let theme = idris_colourTheme ist
1007+ in colouriseType theme
1008+consoleDecorate ist (AnnBoundName _ True) = colouriseImplicit (idris_colourTheme ist)
1009+consoleDecorate ist (AnnBoundName _ False) = colouriseBound (idris_colourTheme ist)
1010+consoleDecorate ist (AnnName n _ _) = let ctxt = tt_ctxt ist
1011+ theme = idris_colourTheme ist
1012+ in case () of
1013+ _ | isDConName n ctxt -> colouriseData theme
1014+ _ | isFnName n ctxt -> colouriseFun theme
1015+ _ | isTConName n ctxt -> colouriseType theme
1016+ _ | otherwise -> id -- don't colourise unknown names
1017+
1018+-- | Pretty-print a high-level closed Idris term
1019+prettyImp :: Bool -- ^^ whether to show implicits
1020+ -> PTerm -- ^^ the term to pretty-print
1021+ -> Doc OutputAnnotation
1022+prettyImp impl = pprintPTerm impl []
1023+
1024+-- | Pretty-print a high-level Idris term in some bindings context
1025+pprintPTerm :: Bool -- ^^ whether to show implicits
1026+ -> [(Name, Bool)] -- ^^ the currently-bound names and whether they are implicit
1027+ -> PTerm -- ^^ the term to pretty-print
1028+ -> Doc OutputAnnotation
1029+pprintPTerm impl bnd = prettySe 10 bnd
1030+ where
1031+ prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation
1032+ prettySe p bnd (PQuote r) =
1033+ if size r > breakingSize then
1034+ text "![" <> line <> pretty r <> text "]"
1035+ else
1036+ text "![" <> pretty r <> text "]"
1037+ prettySe p bnd (PPatvar fc n) = pretty n
1038+ prettySe p bnd e
1039+ | Just str <- slist p bnd e = str
1040+ | Just n <- snat p e = annotate AnnConstData (text (show n))
1041+ prettySe p bnd (PRef fc n) = prettyName impl bnd n
1042+ prettySe p bnd (PLam n ty sc) =
1043+ bracket p 2 $
1044+ if size sc > breakingSize then
1045+ text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc
1046+ else
1047+ text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc
1048+ prettySe p bnd (PLet n ty v sc) =
1049+ bracket p 2 $
1050+ if size sc > breakingSize then
1051+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>
1052+ nest nestingSize (prettySe 10 ((n, False):bnd) sc)
1053+ else
1054+ text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>
1055+ prettySe 10 ((n, False):bnd) sc
1056+ prettySe p bnd (PPi (Exp l s _ _) n ty sc)
1057+ | n `elem` allNamesIn sc || impl =
1058+ let open = (if l then text "|" else empty) <> lparen in
1059+ bracket p 2 $
1060+ if size sc > breakingSize then
1061+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1062+ st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
1063+ else
1064+ enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>
1065+ st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
1066+ | otherwise =
1067+ bracket p 2 $
1068+ if size sc > breakingSize then
1069+ prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc
1070+ else
1071+ prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc
1072+ where
1073+ st =
1074+ case s of
1075+ Static -> text "[static]" <> space
1076+ _ -> empty
1077+ prettySe p bnd (PPi (Imp l s _ _) n ty sc)
1078+ | impl =
1079+ let open = if l then text "|" <> lbrace else lbrace in
1080+ bracket p 2 $
1081+ if size sc > breakingSize then
1082+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1083+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1084+ else
1085+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>
1086+ st <> text "->" <+> prettySe 10 ((n, True):bnd) sc
1087+ | otherwise = prettySe 10 ((n, True):bnd) sc
1088+ where
1089+ st =
1090+ case s of
1091+ Static -> text "[static]" <> space
1092+ _ -> empty
1093+ prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =
1094+ bracket p 2 $
1095+ if size sc > breakingSize then
1096+ prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc
1097+ else
1098+ prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc
1099+ prettySe p bnd (PPi (TacImp _ _ s _) n ty sc) =
1100+ bracket p 2 $
1101+ if size sc > breakingSize then
1102+ lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>
1103+ rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc
1104+ else
1105+ lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>
1106+ rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc
1107+ prettySe p bnd (PApp _ (PRef _ f) [])
1108+ | not impl = prettyName impl bnd f
1109+ prettySe p bnd (PAppBind _ (PRef _ f) [])
1110+ | not impl = text "!" <> prettyName impl bnd f
1111+ prettySe p bnd (PApp _ (PRef _ op@(UN nm)) args)
1112+ | not (tnull nm) &&
1113+ length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =
1114+ let [l, r] = getExps args in
1115+ bracket p 1 $
1116+ if size r > breakingSize then
1117+ prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r
1118+ else
1119+ prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r
1120+ prettySe p bnd (PApp _ f as) =
1121+ let args = getExps as
1122+ fp = prettySe 1 bnd f
1123+ in
1124+ bracket p 1 $
1125+ hsep (if impl
1126+ then fp : map (prettyArgS bnd) as
1127+ else fp : map (prettyArgSe bnd) args)
1128+ prettySe p bnd (PCase _ scr opts) =
1129+ text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody
1130+ where
1131+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
1132+
1133+ sc (l, r) = nest nestingSize $ prettySe 10 bnd l <+> text "=>" <+> prettySe 10 bnd r
1134+ prettySe p bnd (PHidden tm) = text "." <> prettySe 0 bnd tm
1135+ prettySe p bnd (PRefl _ _) = annotate (AnnName eqCon Nothing Nothing) $ text "refl"
1136+ prettySe p bnd (PResolveTC _) = text "resolvetc"
1137+ prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"
1138+ prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"
1139+ prettySe p bnd (PEq _ l r) =
1140+ bracket p 2 $
1141+ if size r > breakingSize then
1142+ prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)
1143+ else
1144+ prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r
1145+ where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")
1146+ prettySe p bnd (PRewrite _ l r _) =
1147+ bracket p 2 $
1148+ if size r > breakingSize then
1149+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)
1150+ else
1151+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r
1152+ prettySe p bnd (PTyped l r) =
1153+ lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen
1154+ prettySe p bnd (PPair _ l r) =
1155+ if size r > breakingSize then
1156+ lparen <> prettySe 10 bnd l <> text "," <>
1157+ line <> prettySe 10 bnd r <> rparen
1158+ else
1159+ lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen
1160+ prettySe p bnd (PDPair _ l t r) =
1161+ if size r > breakingSize then
1162+ lparen <> prettySe 10 bnd l <+> text "**" <>
1163+ line <> prettySe 10 bnd r <> rparen
1164+ else
1165+ lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen
1166+ prettySe p bnd (PAlternative a as) =
1167+ lparen <> text "|" <> prettyAs <> text "|" <> rparen
1168+ where
1169+ prettyAs =
1170+ foldr (\l -> \r -> l <+> text "," <+> r) empty $ map (prettySe 10 bnd) as
1171+ prettySe p bnd PType = text "Type"
1172+ prettySe p bnd (PConstant c) = annotate (annot c) (text (show c))
1173+ where annot (AType _) = AnnConstType
1174+ annot StrType = AnnConstType
1175+ annot PtrType = AnnConstType
1176+ annot VoidType = AnnConstType
1177+ annot _ = AnnConstData
1178+ -- XXX: add pretty for tactics
1179+ prettySe p bnd (PProof ts) =
1180+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1181+ prettySe p bnd (PTactics ts) =
1182+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
1183+ prettySe p bnd (PMetavar n) = text "?" <> pretty n
1184+ prettySe p bnd (PReturn f) = text "return"
1185+ prettySe p bnd PImpossible = text "impossible"
1186+ prettySe p bnd Placeholder = text "_"
1187+ prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"
1188+ prettySe p bnd (PElabError s) = pretty s
1189+
1190+ prettySe p bnd _ = text "test"
1191+
1192+ prettyArgS bnd (PImp _ _ _ n tm _) = prettyArgSi bnd (n, tm)
1193+ prettyArgS bnd (PExp _ _ tm _) = prettyArgSe bnd tm
1194+ prettyArgS bnd (PConstraint _ _ tm _) = prettyArgSc bnd tm
1195+ prettyArgS bnd (PTacImplicit _ _ n _ tm _) = prettyArgSti bnd (n, tm)
1196+
1197+ prettyArgSe bnd arg = prettySe 0 bnd arg
1198+ prettyArgSi bnd (n, val) = lbrace <> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
1199+ prettyArgSc bnd val = lbrace <> lbrace <> prettySe 10 bnd val <> rbrace <> rbrace
1200+ prettyArgSti bnd (n, val) = lbrace <> text "auto" <+> pretty n <+> text "=" <+> prettySe 10 bnd val <> rbrace
9091201
910−showDecls :: Bool -> [PDecl] -> String
911−showDecls _ [] = ""
912−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds
9131202
914−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops
915−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t
916−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)
917−showDeclImp _ (PData _ _ _ _ d) = showDImp True d
918−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"
919−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"
920−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn
921−showDeclImp i (PClass _ _ _ cs n ps ds)
922− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds
923−showDeclImp i (PInstance _ _ cs n _ t _ ds)
924− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds
925−showDeclImp _ _ = "..."
926−-- showDeclImp (PImport i) = "import " ++ i
1203+ slist' p bnd (PApp _ (PRef _ nil) _)
1204+ | not impl && nsroot nil == sUN "Nil" = Just []
1205+ slist' p bnd (PApp _ (PRef _ cons) args)
1206+ | nsroot cons == sUN "::",
1207+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1208+ all isImp imps,
1209+ Just tl' <- slist' p bnd tl
1210+ = Just (hd:tl')
1211+ where
1212+ isImp (PImp {}) = True
1213+ isImp _ = False
1214+ slist' _ _ _ = Nothing
1215+
1216+ slist p bnd e | Just es <- slist' p bnd e = Just $
1217+ case es of [] -> annotate AnnConstData $ text "[]"
1218+ [x] -> enclose left
1219+ right
1220+ (prettySe p bnd x)
1221+ xs -> (enclose left right . hsep . punctuate comma . map (prettySe p bnd)) xs
1222+ where left = (annotate AnnConstData (text "["))
1223+ right = (annotate AnnConstData (text "]"))
1224+ comma = (annotate AnnConstData (text ","))
1225+ slist _ _ _ = Nothing
9271226
1227+ natns = "Prelude.Nat."
1228+
1229+ snat p (PRef _ z)
1230+ | show z == (natns++"Z") || show z == "Z" = Just 0
1231+ snat p (PApp _ s [PExp {getTm=n}])
1232+ | show s == (natns++"S") || show s == "S",
1233+ Just n' <- snat p n
1234+ = Just $ 1 + n'
1235+ snat _ _ = Nothing
9281236
929−showCImp :: Bool -> PClause -> String
1237+ bracket outer inner doc
1238+ | inner > outer = lparen <> doc <> rparen
1239+ | otherwise = doc
1240+
1241+-- | Pretty-printer helper for the binding site of a name
1242+bindingOf :: Name -- ^^ the bound name
1243+ -> Bool -- ^^ whether the name is implicit
1244+ -> Doc OutputAnnotation
1245+bindingOf n imp = annotate (AnnBoundName n imp) (text (show n))
1246+
1247+-- | Pretty-printer helper for names that attaches the correct annotations
1248+prettyName :: Bool -- ^^ whether to show namespaces
1249+ -> [(Name, Bool)] -- ^^ the current bound variables and whether they are implicit
1250+ -> Name -- ^^ the name to pprint
1251+ -> Doc OutputAnnotation
1252+prettyName showNS bnd n | Just imp <- lookup n bnd = annotate (AnnBoundName n imp) (text (strName n))
1253+ | otherwise = annotate (AnnName n Nothing Nothing) (text (strName n))
1254+ where strName (UN n) = T.unpack n
1255+ strName (NS n ns) | showNS = (concatMap (++ ".") . map T.unpack . reverse) ns ++ strName n
1256+ | otherwise = strName n
1257+ strName (MN i s) = T.unpack s
1258+ strName other = show other
1259+
1260+
1261+showCImp :: Bool -> PClause -> Doc OutputAnnotation
9301262showCImp impl (PClause _ n l ws r w)
931− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r
932− ++ " where " ++ show w
1263+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r
1264+ <+> text "where" <+> text (show w)
9331265 where
934− showWs [] = ""
935− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
1266+ showWs [] = empty
1267+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
9361268showCImp impl (PWith _ n l ws r w)
937− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r
938− ++ " { " ++ show w ++ " } "
1269+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r
1270+ <+> braces (text (show w))
9391271 where
940− showWs [] = ""
941− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs
1272+ showWs [] = empty
1273+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs
9421274
9431275
944−showDImp :: Bool -> PData -> String
1276+showDImp :: Bool -> PData -> Doc OutputAnnotation
9451277showDImp impl (PDatadecl n ty cons)
946− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"
947− ++ showSep "\n\t| "
948− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False t) cons)
1278+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>
1279+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))
1280+
1281+showDecls :: Bool -> [PDecl] -> Doc OutputAnnotation
1282+showDecls i ds = vsep (map (showDeclImp i) ds)
1283+
1284+showDeclImp _ (PFix _ f ops) = text (show f) <+> cat (punctuate (text ",") (map text ops))
1285+showDeclImp i (PTy _ _ _ _ n t) = text "tydecl" <+> text (showCG n) <+> colon <+> prettyImp i t
1286+showDeclImp i (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\t" <+>
1287+ indent 2 (vsep (map (showCImp i) cs))
1288+showDeclImp _ (PData _ _ _ _ d) = showDImp True d
1289+showDeclImp i (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls i ps <> line)
1290+showDeclImp i (PNamespace n ps) = text "namespace" <+> text n <> braces (line <> showDecls i ps <> line)
1291+showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)
1292+showDeclImp i (PClass _ _ _ cs n ps ds)
1293+ = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls i ds
1294+showDeclImp i (PInstance _ _ cs n _ t _ ds)
1295+ = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp i t <> line <> showDecls i ds
1296+showDeclImp _ _ = text "..."
1297+-- showDeclImp (PImport i) = "import " ++ i
1298+
1299+instance Show (Doc OutputAnnotation) where
1300+ show = flip (displayS . renderCompact) ""
9491301
9501302getImps :: [PArg] -> [(Name, PTerm)]
9511303getImps [] = []
@@ -995,168 +1347,14 @@ showName ist bnd impl colour n = case ist of
9951347 -- (like error messages). Thus, unknown vars are colourised as implicits.
9961348 | otherwise -> colouriseImplicit t name
9971349
998−-- | Show Idris term
999−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours
1000− -> Bool -- ^^ whether to show implicits
1001− -> Bool -- ^^ whether to colourise
1002− -> PTerm -- ^^ the term to show
1003− -> String
1004−showImp ist impl colour tm = se 10 [] tm where
1005− perhapsColourise :: (ColourTheme -> String -> String) -> String -> String
1006− perhapsColourise col str = case ist of
1007− Just i -> if colour then col (idris_colourTheme i) str else str
1008− Nothing -> str
1009−
1010− se :: Int -> [(Name, Bool)] -> PTerm -> String
1011− se p bnd (PQuote r) = "![" ++ show r ++ "]"
1012− se p bnd (PPatvar fc n) = if impl then show n ++ "[p]" else show n
1013− se p bnd (PInferRef fc n) = "!" ++ show n -- ++ "[" ++ show fc ++ "]"
1014− se p bnd e
1015− | Just str <- slist p bnd e = str
1016− | Just num <- snat p e = perhapsColourise colouriseData (show num)
1017− se p bnd (PRef fc n) = showName ist bnd impl colour n
1018− se p bnd (PLam n ty sc) = bracket p 2 $ "\\ " ++ perhapsColourise colouriseBound (show n) ++
1019− (if impl then " : " ++ se 10 bnd ty else "") ++ " => "
1020− ++ se 10 ((n, False):bnd) sc
1021− se p bnd (PLet n ty v sc) = bracket p 2 $ "let " ++ perhapsColourise colouriseBound (show n) ++
1022− " = " ++ se 10 bnd v ++
1023− " in " ++ se 10 ((n, False):bnd) sc
1024− se p bnd (PPi (Exp l s _ param) n ty sc)
1025− | n `elem` allNamesIn sc || impl
1026− = bracket p 2 $
1027− (if l then "|(" else "(") ++
1028− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1029− ") " ++
1030− (if (impl && param) then "P" else "") ++
1031− st ++
1032− "-> " ++ se 10 ((n, False):bnd) sc
1033− | otherwise = bracket p 2 $ se 0 bnd ty ++ " " ++ st ++ "-> " ++ se 10 bnd sc
1034− where st = case s of
1035− Static -> "[static] "
1036− _ -> ""
1037− se p bnd (PPi (Imp l s _ _) n ty sc)
1038− | impl = bracket p 2 $ (if l then "|{" else "{") ++
1039− perhapsColourise colouriseBound (show n) ++ " : " ++ se 10 bnd ty ++
1040− "} " ++ st ++ "-> " ++ se 10 ((n, True):bnd) sc
1041− | otherwise = se 10 ((n, True):bnd) sc
1042− where st = case s of
1043− Static -> "[static] "
1044− _ -> ""
1045− se p bnd (PPi (Constraint _ _ _) n ty sc)
1046− = bracket p 2 $ se 10 bnd ty ++ " => " ++ se 10 bnd sc
1047− se p bnd (PPi (TacImp _ _ s _) n ty sc)
1048− = bracket p 2 $
1049− "{tacimp " ++ (perhapsColourise colouriseBound (show n)) ++ " : " ++ se 10 bnd ty ++ "} -> " ++
1050− se 10 ((n, False):bnd) sc
1051− se p bnd (PMatchApp _ f) = "match " ++ show f
1052− se p bnd (PApp _ hd@(PRef _ f) [])
1053− | not impl = se p bnd hd
1054− se p bnd (PAppBind _ hd@(PRef _ f) [])
1055− | not impl = "!" ++ se p bnd hd
1056− se p bnd (PApp _ op@(PRef _ (UN nm)) args)
1057− | not (tnull nm) &&
1058− length (getExps args) == 2 && not impl && not (isAlpha (thead nm))
1059− = let [l, r] = getExps args in
1060− bracket p 1 $ se 1 bnd l ++ " " ++ se p bnd op ++ " " ++ se 0 bnd r
1061− se p bnd (PApp _ f as)
1062− = -- let args = getExps as in
1063− bracket p 1 $ se 1 bnd f ++
1064− if impl then concatMap (sArg bnd) as
1065− else concatMap (suiArg impl bnd) as
1066− se p bnd (PAppBind _ f as)
1067− = let args = getExps as in
1068− "!" ++ (bracket p 1 $ se 1 bnd f ++ if impl then concatMap (sArg bnd) as
1069− else concatMap (seArg bnd) args)
1070− se p bnd (PCase _ scr opts) = "case " ++ se 10 bnd scr ++ " of " ++ showSep " | " (map sc opts)
1071− where sc (l, r) = se 10 bnd l ++ " => " ++ se 10 bnd r
1072− se p bnd (PHidden tm) = "." ++ se 0 bnd tm
1073− se p bnd (PRefl _ t)
1074− | not impl = perhapsColourise colouriseData "refl"
1075− | otherwise = perhapsColourise colouriseData $ "refl {" ++ se 10 bnd t ++ "}"
1076− se p bnd (PResolveTC _) = "resolvetc"
1077− se p bnd (PTrue _) = perhapsColourise colouriseType "()"
1078− se p bnd (PFalse _) = perhapsColourise colouriseType "_|_"
1079− se p bnd (PEq _ l r) = bracket p 2 $ se 10 bnd l ++ perhapsColourise colouriseType " = " ++ se 10 bnd r
1080− se p bnd (PRewrite _ l r _) = bracket p 2 $ "rewrite " ++ se 10 bnd l ++ " in " ++ se 10 bnd r
1081− se p bnd (PTyped l r) = "(" ++ se 10 bnd l ++ " : " ++ se 10 bnd r ++ ")"
1082− se p bnd (PPair _ l r) = "(" ++ se 10 bnd l ++ ", " ++ se 10 bnd r ++ ")"
1083− se p bnd (PDPair _ l t r) = "(" ++ se 10 bnd l ++ " ** " ++ se 10 bnd r ++ ")"
1084− se p bnd (PAlternative a as) = "(|" ++ showSep " , " (map (se 10 bnd) as) ++ "|)"
1085− se p bnd PType = perhapsColourise colouriseType "Type"
1086− se p bnd (PConstant c) = perhapsColourise (cfun c) (show c)
1087− where cfun (AType _) = colouriseType
1088− cfun StrType = colouriseType
1089− cfun PtrType = colouriseType
1090− cfun VoidType = colouriseType
1091− cfun _ = colouriseData
1092− se p bnd (PProof ts) = "proof { " ++ show ts ++ "}"
1093− se p bnd (PTactics ts) = "tactics { " ++ show ts ++ "}"
1094− se p bnd (PMetavar n) = "?" ++ show n
1095− se p bnd (PReturn f) = "return"
1096− se p bnd PImpossible = "impossible"
1097− se p bnd Placeholder = "_"
1098− se p bnd (PDoBlock _) = "do block show not implemented"
1099− se p bnd (PElabError s) = show s
1100− se p bnd (PCoerced t) = se p bnd t
1101− se p bnd (PUnifyLog t) = "%unifyLog " ++ se p bnd t
1102− se p bnd (PDisamb ns t) = "%disamb " ++ show ns ++ se p bnd t
1103− se p bnd (PNoImplicits t) = "%noimplicit " ++ se p bnd t
1104−-- se p bnd x = "Not implemented"
1105−
1106− slist' p bnd (PApp _ (PRef _ nil) _)
1107− | not impl && nsroot nil == sUN "Nil" = Just []
1108− slist' p bnd (PApp _ (PRef _ cons) args)
1109− | nsroot cons == sUN "::",
1110− (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,
1111− all isImp imps,
1112− Just tl' <- slist' p bnd tl
1113− = Just (hd:tl')
1114− where
1115− isImp (PImp {}) = True
1116− isImp _ = False
1117− slist' _ _ _ = Nothing
1118−
1119− slist p bnd e | Just es <- slist' p bnd e = Just $
1120− case es of [] -> "[]"
1121− [x] -> "[" ++ se p bnd x ++ "]"
1122− xs -> "[" ++ intercalate "," (map (se p bnd ) xs) ++ "]"
1123− slist _ _ _ = Nothing
1124−
1125− -- since Prelude is always imported, S & Z are unqualified iff they're the
1126− -- Nat ones.
1127− snat p (PRef _ o)
1128− | show o == (natns++"Z") || show o == "Z" = Just 0
1129− snat p (PApp _ s [PExp {getTm=n}])
1130− | show s == (natns++"S") || show s == "S",
1131− Just n' <- snat p n
1132− = Just $ 1 + n'
1133− snat _ _ = Nothing
1134−
1135− natns = "Prelude.Nat."
1350+showTm :: IState -- ^^ the Idris state, for information about identifiers and colours
1351+ -> PTerm -- ^^ the term to show
1352+ -> String
1353+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))
11361354
1137− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)
1138− sArg bnd (PExp _ _ tm _) = seArg bnd tm
1139− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm
1140− sArg bnd (PTacImplicit _ _ n _ tm _) = stiArg bnd (n, tm)
1141−
1142− -- show argument, implicits given by the user also shown
1143− suiArg impl bnd (PImp _ mi _ n tm _)
1144− | impl || not mi = siArg bnd (n, tm)
1145− suiArg impl bnd (PExp _ _ tm _) = seArg bnd tm
1146− suiArg impl bnd _ = ""
1147−
1148− seArg bnd arg = " " ++ se 0 bnd arg
1149− siArg bnd (n, val) =
1150− let n' = show n
1151− val' = se 10 bnd val in
1152− if (n' == val')
1153− then " {" ++ n' ++ "}"
1154− else " {" ++ n' ++ " = " ++ val' ++ "}"
1155− scArg bnd val = " {{" ++ se 10 bnd val ++ "}}"
1156− stiArg bnd (n, val) = " {auto " ++ show n ++ " = " ++ se 10 bnd val ++ "}"
1157−
1158− bracket outer inner str | inner > outer = "(" ++ str ++ ")"
1159− | otherwise = str
1355+-- | Show a term with implicits, no colours
1356+showTmImpls :: PTerm -> String
1357+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""
11601358
11611359
11621360instance Sized PTerm where
src/Idris/CaseSplit.hs+3−3
@@ -62,11 +62,11 @@ split n t'
6262 Just ty ->
6363 do let splits = findPats ist ty
6464 iLOG ("New patterns " ++ showSep ", "
65− (map (showImp Nothing True False) splits))
65+ (map showTmImpls splits))
6666 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)
6767 logLvl 4 ("Working from " ++ show t)
6868 logLvl 4 ("Trying " ++ showSep "\n"
69− (map (showImp Nothing True False) newPats_in))
69+ (map (showTmImpls) newPats_in))
7070 newPats <- mapM elabNewPat newPats_in
7171 logLvl 3 ("Original:\n" ++ show t)
7272 logLvl 3 ("Split:\n" ++
@@ -237,7 +237,7 @@ splitOnLine l n fn = do
237237-- let (before, later) = splitAt (l-1) (lines inp)
238238-- i <- getIState
239239 cl <- getInternalApp fn l
240− logLvl 3 ("Working with " ++ showImp Nothing True False cl)
240+ logLvl 3 ("Working with " ++ showTmImpls cl)
241241 tms <- split n cl
242242-- iputStrLn (showSep "\n" (map show tms))
243243 return tms -- "" -- not yet done...
src/Idris/Core/TT.hs+2
@@ -83,6 +83,8 @@ data NameOutput = TypeOutput | FunOutput | DataOutput
8383-- | Output annotations for pretty-printing
8484data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)
8585 | AnnBoundName Name Bool
86+ | AnnConstData
87+ | AnnConstType
8688
8789-- | Used for error reflection
8890data ErrorReportPart = TextPart String
src/Idris/Coverage.hs+3−3
@@ -50,7 +50,7 @@ genClauses fc n xs given
5050 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)
5151 logLvl 10 $ show argss ++ "\n" ++ show all_args
5252 logLvl 10 $ "Original: \n" ++
53− showSep "\n" (map (\t -> showImp Nothing True False (delab' i t True True)) xs)
53+ showSep "\n" (map (\t -> showTm i (delab' i t True True)) xs)
5454 -- add an infinite supply of explicit arguments to update the possible
5555 -- cases for (the return type may be variadic, or function type, sp
5656 -- there may be more case splitting that the idris_implicits record
@@ -60,10 +60,10 @@ genClauses fc n xs given
6060 _ -> repeat (pexp Placeholder)
6161 let tryclauses = mkClauses parg all_args
6262 logLvl 2 $ show (length tryclauses) ++ " initially to check"
63− logLvl 5 $ showSep "\n" (map (showImp Nothing True False) tryclauses)
63+ logLvl 5 $ showSep "\n" (map (showTm i) tryclauses)
6464 let new = filter (noMatch i) (nub tryclauses)
6565 logLvl 1 $ show (length new) ++ " clauses to check for impossibility"
66− logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showImp Nothing True False) new)
66+ logLvl 5 $ "New clauses: \n" ++ showSep "\n" (map (showTm i) new)
6767-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)
6868 return new
6969-- return (map (\t -> PClause n t [] PImpossible []) new)
src/Idris/Delaborate.hs+36−49
@@ -125,60 +125,48 @@ pshow i (Msg s) = s
125125pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++
126126 "\nThis is probably a bug, or a missing error message.\n" ++
127127 "Please consider reporting at " ++ bugaddr
128−pshow i (CantUnify _ x y e sc s)
129− = let imps = opt_showimp (idris_options i) in
130− let colour = idris_colourRepl i in
131− "Can't unify" ++ indented (showImp (Just i) imps colour (delab i x))
132− ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++
133−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++
134− case e of
135− Msg "" -> ""
136− _ -> "\nSpecifically:" ++
137− indented (pshow i e) ++
138− if (opt_errContext (idris_options i)) then showSc i sc else ""
139−pshow i (CantConvert x y env)
140− = let imps = opt_showimp (idris_options i) in
141− let colour = idris_colourRepl i in
142− "Can't convert" ++ indented (showImp (Just i) imps colour (delab i x)) ++ "with"
143− ++ indented (showImp (Just i) imps colour (delab i y)) ++
144− if (opt_errContext (idris_options i)) then showSc i env else ""
145−pshow i (UnifyScope n out tm env)
146− = let imps = opt_showimp (idris_options i) in
147− let colour = idris_colourRepl i in
148− "Can't unify" ++ indented (show n) ++ "with"
149− ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++
150− indented (show out) ++ "is not in scope" ++
151− if (opt_errContext (idris_options i)) then showSc i env else ""
152−pshow i (CantInferType t)
153− = "Can't infer type for " ++ t
154−pshow i (NonFunctionType f ty)
155− = let imps = opt_showimp (idris_options i) in
156− let colour = idris_colourRepl i in
157− showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("
158− ++ showImp (Just i) imps colour (delab i ty) ++ ")"
159−pshow i (NotEquality tm ty)
160− = let imps = opt_showimp (idris_options i) in
161− let colour = idris_colourRepl i in
162− showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("
163− ++ showImp (Just i) imps colour (delab i ty) ++ ")"
164−pshow i (TooManyArguments f)
165− = "Too many arguments for " ++ show f
166−pshow i (CantIntroduce ty)
167− = let imps = opt_showimp (idris_options i) in
168− let colour = idris_colourRepl i in
169− "Can't use lambda here: type is " ++ showImp (Just i) imps colour (delab i ty)
128+pshow i (CantUnify _ x y e sc s) =
129+ "Can't unify" ++ indented (showTm i (delab i x)) ++
130+ "with" ++ indented (showTm i (delab i y)) ++
131+ case e of
132+ Msg "" -> ""
133+ _ -> "\nSpecifically:" ++
134+ indented (pshow i e) ++
135+ if (opt_errContext (idris_options i)) then showSc i sc else ""
136+pshow i (CantConvert x y env) =
137+ "Can't convert" ++ indented (showTm i (delab i x)) ++
138+ "with" ++ indented (showTm i (delab i y)) ++
139+ if (opt_errContext (idris_options i)) then showSc i env else ""
140+pshow i (UnifyScope n out tm env) =
141+ "Can't unify" ++ indented (show n) ++
142+ "with" ++ indented (showTm i (delab i tm)) ++
143+ "as" ++ indented (show out) ++ "is not in scope" ++
144+ if (opt_errContext (idris_options i)) then showSc i env else ""
145+pshow i (CantInferType t) = "Can't infer type for " ++ t
146+pshow i (NonFunctionType f ty) =
147+ showTm i (delab i f) ++
148+ " does not have a function type (" ++
149+ showTm i (delab i ty) ++ ")"
150+pshow i (NotEquality tm ty) =
151+ showTm i (delab i tm) ++
152+ " does not have an equality type (" ++
153+ showTm i (delab i ty) ++ ")"
154+pshow i (TooManyArguments f) = "Too many arguments for " ++ show f
155+pshow i (CantIntroduce ty) =
156+ "Can't use lambda here: type is " ++ showTm i (delab i ty)
170157pshow i (InfiniteUnify x tm env)
171− = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++
158+ = "Unifying " ++ showbasic x ++ " and " ++ showTm i (delab i tm) ++
172159 " would lead to infinite value" ++
173160 if (opt_errContext (idris_options i)) then showSc i env else ""
174−pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++
175− " when unifying " ++ show (delab i x) ++ " and " ++
176− show (delab i y)
161+pshow i (NotInjective p x y) =
162+ "Can't verify injectivity of " ++ showTm i (delab i p) ++
163+ " when unifying " ++ showTm i (delab i x) ++ " and " ++
164+ showTm i (delab i y)
177165pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)
178166pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as
179167pshow i (NoTypeDecl n) = "No type declaration for " ++ show n
180168pshow i (NoSuchVariable n) = "No such variable " ++ show n
181−pshow i (IncompleteTerm t) = "Incomplete term " ++ showImp Nothing True False (delab i t)
169+pshow i (IncompleteTerm t) = "Incomplete term " ++ showTm i (delab i t)
182170pshow i UniverseError = "Universe inconsistency"
183171pshow i ProgramLineComment = "Program line next to comment"
184172pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"
@@ -199,8 +187,7 @@ pshow i (ReflectionError parts orig) = let parts' = map (concat . intersperse "
199187 showPart (TextPart str) = str
200188 showPart (NamePart n) = let colour = idris_colourRepl i in
201189 showName (Just i) [] False colour n
202− showPart (TermPart tm) = let colour = idris_colourRepl i
203− in showImp (Just i) False colour (delab i tm)
190+ showPart (TermPart tm) = showTm i (delab i tm)
204191 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs
205192pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++
206193 indented (pshow i err) ++
src/Idris/ElabDecls.hs+32−32
@@ -67,12 +67,12 @@ elabType' norm info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty
6767 ctxt <- getContext
6868 i <- getIState
6969
70− logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'
70+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'
7171 ty' <- addUsingConstraints syn fc ty'
7272 ty' <- implicit syn n ty'
7373
7474 let ty = addImpl i ty'
75− logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty
75+ logLvl 2 $ show n ++ " type " ++ showTmImpls ty
7676 ((tyT, defer, is), log) <-
7777 tclift $ elaborate ctxt n (TType (UVal 0)) []
7878 (errAt "type of " n (erun fc (build i info False [] n ty)))
@@ -325,10 +325,10 @@ elabEliminator paramPos n ty cons info = do
325325 let clauseConsElimArgs = map getPiName consTerms
326326 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
327327 let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
328− let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
328+ let elimSig = "-- eliminator signature: " ++ showTmImpls eliminatorTy
329329 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
330330 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
331− elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
331+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef
332332 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
333333 -- Do not elaborate clauses if there aren't any
334334 case eliminatorClauses of
@@ -813,7 +813,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)
813813 i <- getIState
814814 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)
815815 let t = addImpl i t_in
816− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ showImp Nothing True False t
816+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t
817817 ((t', defer, is), log) <-
818818 tclift $ elaborate ctxt n (TType (UVal 0)) []
819819 (errAt "constructor " n (erun fc (build i info False [] n t)))
@@ -957,9 +957,9 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
957957 missing' <- filterM (checkPossible info fc True n) missing
958958 let clhs = map getLHS pdef
959959 logLvl 2 $ "Must be unreachable:\n" ++
960− showSep "\n" (map (showImp Nothing True False) missing') ++
960+ showSep "\n" (map showTmImpls missing') ++
961961 "\nAgainst: " ++
962− showSep "\n" (map (\t -> showImp Nothing True False (delab ist t)) (map getLHS pdef))
962+ showSep "\n" (map (\t -> showTmImpls (delab ist t)) (map getLHS pdef))
963963 -- filter out anything in missing' which is
964964 -- matched by any of clhs. This might happen since
965965 -- unification may force a variable to take a
@@ -1123,8 +1123,8 @@ elabPE info fc caller r =
11231123 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
11241124 showSep "\n"
11251125 (map (\ (lhs, rhs) ->
1126− (showImp Nothing True False lhs ++ " = " ++
1127− showImp Nothing True False rhs)) pats)
1126+ (showTmImpls lhs ++ " = " ++
1127+ showTmImpls rhs)) pats)
11281128 elabType info defaultSyntax "" fc opts newnm specTy
11291129 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
11301130 elabClauses info fc opts newnm def
@@ -1178,7 +1178,7 @@ elabValBind info aspat tm_in
11781178 = do ctxt <- getContext
11791179 i <- getIState
11801180 let tm = addImpl i tm_in
1181− logLvl 10 (showImp Nothing True False tm)
1181+ logLvl 10 (showTmImpls tm)
11821182 -- try:
11831183 -- * ordinary elaboration
11841184 -- * elaboration as a Type
@@ -1269,7 +1269,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12691269 let params = getParamsInType i [] fn_is fn_ty
12701270 let lhs = stripUnmatchable i $
12711271 addImplPat i (propagateParams params (stripLinear i lhs_in))
1272− logLvl 5 ("LHS: " ++ show fc ++ " " ++ showImp Nothing True False lhs)
1272+ logLvl 5 ("LHS: " ++ show fc ++ " " ++ showTmImpls lhs)
12731273 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))
12741274
12751275 ((lhs', dlhs, []), _) <-
@@ -1284,7 +1284,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
12841284 (clhs_c, clhsty) <- recheckC fc [] lhs_tm
12851285 let clhs = normalise ctxt [] clhs_c
12861286
1287− logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))
1287+ logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))
12881288
12891289 rep <- useREPL
12901290 when rep $ do
@@ -1310,10 +1310,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
13101310 mapM_ (elabDecl' EAll info) wbefore
13111311 -- Now build the RHS, using the type of the LHS as the goal.
13121312 i <- getIState -- new implicits from where block
1313− logLvl 5 (showImp Nothing True False (expandParams decorate newargs defs (defs \\ decls) rhs_in))
1313+ logLvl 5 (showTmImpls (expandParams decorate newargs defs (defs \\ decls) rhs_in))
13141314 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)
13151315 (expandParams decorate newargs defs (defs \\ decls) rhs_in)
1316− logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs
1316+ logLvl 2 $ "RHS: " ++ showTmImpls rhs
13171317 ctxt <- getContext -- new context with where block added
13181318 logLvl 5 "STARTING CHECK"
13191319 ((rhs', defer, is), _) <-
@@ -1452,7 +1452,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14521452 -- pattern bindings
14531453 i <- getIState
14541454 let lhs = addImplPat i (stripLinear i lhs_in)
1455− logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)
1455+ logLvl 5 ("LHS: " ++ showTmImpls lhs)
14561456 ((lhs', dlhs, []), _) <-
14571457 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []
14581458 (errAt "left hand side of with in " fname
@@ -1465,7 +1465,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
14651465 logLvl 5 ("Checked " ++ show clhs)
14661466 let bargs = getPBtys lhs_tm
14671467 let wval = addImplBound i (map fst bargs) wval_in
1468− logLvl 5 ("Checking " ++ showImp Nothing True False wval)
1468+ logLvl 5 ("Checking " ++ showTmImpls wval)
14691469 -- Elaborate wval in this context
14701470 ((wval', defer, is), _) <-
14711471 tclift $ elaborate ctxt (sMN 0 "withRHS")
@@ -1529,7 +1529,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15291529 (map (pexp . (PRef fc) . fst) bargs_pre ++
15301530 pexp wval :
15311531 (map (pexp . (PRef fc) . fst) bargs_post))
1532− logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)
1532+ logLvl 5 ("New RHS " ++ showTmImpls rhs)
15331533 ctxt <- getContext -- New context with block added
15341534 i <- getIState
15351535 ((rhs', defer, is), _) <-
@@ -1560,8 +1560,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15601560 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)
15611561 = do i <- getIState
15621562 let tm = addImplPat i tm_in
1563− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1564− showImp Nothing True False toplhs)
1563+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1564+ showTmImpls toplhs)
15651565 case matchClause i toplhs tm of
15661566 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")
15671567 Right mvars ->
@@ -1571,8 +1571,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)
15711571 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)
15721572 = do i <- getIState
15731573 let tm = addImplPat i tm_in
1574− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++
1575− showImp Nothing True False toplhs)
1574+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++
1575+ showTmImpls toplhs)
15761576 withs' <- mapM (mkAuxC wname toplhs ns ns') withs
15771577 case matchClause i toplhs tm of
15781578 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")
@@ -1639,7 +1639,7 @@ elabClass info syn doc fc constraints tn ps ds
16391639 constraint
16401640 let cons = [("", cn, cty, fc, [])]
16411641 let ddecl = PDatadecl tn tty cons
1642− logLvl 5 $ "Class data " ++ showDImp True ddecl
1642+ logLvl 5 $ "Class data " ++ show (showDImp True ddecl)
16431643 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
16441644 -- for each constraint, build a top level function to chase it
16451645 logLvl 5 $ "Building functions"
@@ -1681,7 +1681,7 @@ elabClass info syn doc fc constraints tn ps ds
16811681 getMName (PTy _ _ _ _ n _) = nsroot n
16821682 tdecl allmeths (PTy doc syn _ o n t)
16831683 = do t' <- implicit' syn allmeths n t
1684− logLvl 5 $ "Method " ++ show n ++ " : " ++ showImp Nothing True False t'
1684+ logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'
16851685 return ( (n, (toExp (map fst ps) Exp t')),
16861686 (n, (doc, o, (toExp (map fst ps) Imp t'))),
16871687 (n, (syn, o, t) ) )
@@ -1718,8 +1718,8 @@ elabClass info syn doc fc constraints tn ps ds
17181718 let lhs = PApp fc (PRef fc cfn) [pconst capp]
17191719 let rhs = PResolveTC (fileFC "HACK")
17201720 let ty = PPi constraint (sMN 0 "pc") c con
1721− iLOG (showImp Nothing True False ty)
1722− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1721+ iLOG (showTmImpls ty)
1722+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
17231723 i <- getIState
17241724 let conn = case con of
17251725 PRef _ n -> n
@@ -1743,9 +1743,9 @@ elabClass info syn doc fc constraints tn ps ds
17431743 let anames = map (\x -> sMN x "arg") [0..]
17441744 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)
17451745 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)
1746− iLOG (showImp Nothing True False ty)
1746+ iLOG (showTmImpls ty)
17471747 iLOG (show (m, ty', capp, margs))
1748− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)
1748+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)
17491749 return [PTy doc syn fc o m ty',
17501750 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]
17511751
@@ -1833,7 +1833,7 @@ elabInstance info syn what fc cs n ps t expn ds = do
18331833 let wbTys = map mkTyDecl mtys
18341834 let wbVals = map (decorateid (decorate ns iname)) ds'
18351835 let wb = wbTys ++ wbVals
1836− logLvl 3 $ "Method types " ++ showSep "\n" (map (showDeclImp True . mkTyDecl) mtys)
1836+ logLvl 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp True . mkTyDecl) mtys)
18371837 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++
18381838 show (concat (nub wparams))
18391839 let lhs = PRef fc iname
@@ -2140,8 +2140,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)
21402140
21412141checkInferred :: FC -> PTerm -> PTerm -> Idris ()
21422142checkInferred fc inf user =
2143− do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++
2144− showImp Nothing True False user
2143+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++
2144+ showTmImpls user
21452145 logLvl 10 $ "Checking match"
21462146 i <- getIState
21472147 tclift $ case matchClause' True i user inf of
@@ -2158,8 +2158,8 @@ checkInferred fc inf user =
21582158inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool
21592159inferredDiff fc inf user =
21602160 do i <- getIState
2161− logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++
2162− showImp Nothing True False user
2161+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++
2162+ showTmImpls user
21632163 tclift $ case matchClause' True i user inf of
21642164 Right vs -> return False
21652165 Left (x, y) -> return True
src/Idris/Parser.hs+1−1
@@ -1060,7 +1060,7 @@ loadSource h lidr f
10601060 f file pos
10611061 unless (null ds') $ do
10621062 let ds = namespaces mname ds'
1063− logLvl 3 (showDecls True ds)
1063+ logLvl 3 (show $ showDecls True ds)
10641064 i <- getIState
10651065 logLvl 10 (show (toAlist (idris_implicits i)))
10661066 logLvl 3 (show (idris_infixes i))
src/Idris/REPL.hs+16−23
@@ -448,10 +448,8 @@ process h fn (Eval t)
448448 ist <- getIState
449449 logLvl 3 $ "Raw: " ++ show (tm', ty')
450450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'
451− imp <- impShow
452− c <- colourise
453− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++
454− showImp (Just ist) imp c (delab ist ty'))
451+ ihPrintResult h (showTm ist (delab ist tm') ++ " : " ++
452+ showTm ist (delab ist ty'))
455453process h fn (ExecVal t)
456454 = do ctxt <- getContext
457455 ist <- getIState
@@ -459,10 +457,8 @@ process h fn (ExecVal t)
459457-- let tm' = normaliseAll ctxt [] tm
460458 let ty' = normaliseAll ctxt [] ty
461459 res <- execute tm
462− imp <- impShow
463− c <- colourise
464− ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++
465− showImp (Just ist) imp c (delab ist ty'))
460+ ihPrintResult h (showTm ist (delab ist res) ++ " : " ++
461+ showTm ist (delab ist ty'))
466462process h fn (Check (PRef _ n))
467463 = do ctxt <- getContext
468464 ist <- getIState
@@ -474,7 +470,7 @@ process h fn (Check (PRef _ n))
474470 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)
475471 Nothing -> ihPrintResult h $
476472 concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++
477− showImp (Just ist) imp c (delabTy ist n)) $ ts
473+ showTm ist (delabTy ist n)) $ ts
478474 [] -> ihPrintError h $ "No such variable " ++ show n
479475 where
480476 showMetavarInfo c imp ist n i
@@ -487,27 +483,25 @@ process h fn (Check (PRef _ n))
487483 MN _ _ -> "_"
488484 UN nm | ('_':'_':_) <- str nm -> "_"
489485 _ -> showName (Just ist) [] False c n) ++
490− " : " ++ showImp (Just ist) imp c t ++ "\n"
486+ " : " ++ showTm ist t ++ "\n"
491487 in
492488 current ++ putTy c imp ist (i-1) sc
493489 putTy c imp ist _ sc = putGoal c imp ist sc
494490 putGoal c imp ist g
495491 = "--------------------------------------\n" ++
496492 showName (Just ist) [] False c n ++ " : " ++
497− showImp (Just ist) imp c g
493+ showTm ist g
498494
499495
500496process h fn (Check t)
501497 = do (tm, ty) <- elabVal toplevel False t
502498 ctxt <- getContext
503499 ist <- getIState
504− imp <- impShow
505− c <- colourise
506500 let ty' = normaliseC ctxt [] ty
507501 case tm of
508502 TType _ -> ihPrintResult h ("Type : Type 1")
509− _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++
510− showImp (Just ist) imp c (delab ist ty))
503+ _ -> ihPrintResult h (showTm ist (delab ist tm) ++ " : " ++
504+ showTm ist (delab ist ty))
511505
512506process h fn (DocStr n)
513507 = do i <- getIState
@@ -540,9 +534,9 @@ process h fn (Defn n)
540534 [t] -> iputStrLn (showTotal t i)
541535 _ -> return ()
542536 where printCase i (_, lhs, rhs)
543− = do c <- colourise
544− iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++
545− showImp (Just i) True c (delab i rhs))
537+ = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
538+ in iputStrLn (showTm i' (delab i lhs) ++ " = " ++
539+ showTm i' (delab i rhs))
546540process h fn (TotCheck n)
547541 = do i <- getIState
548542 case lookupNameTotal n (tt_ctxt i) of
@@ -848,7 +842,7 @@ process h fn (TestInline t)
848842 let tm' = inlineTerm ist tm
849843 imp <- impShow
850844 c <- colourise
851− iPrintResult (showImp (Just ist) imp c (delab ist tm'))
845+ iPrintResult (showTm ist (delab ist tm'))
852846process h fn Execute
853847 = do (m, _) <- elabVal toplevel False
854848 (PApp fc
@@ -876,11 +870,11 @@ process h fn (Pattelab t)
876870
877871process h fn (Missing n)
878872 = do i <- getIState
879− c <- colourise
873+ let i' = i { idris_options = (idris_options i) { opt_showimp = True } }
880874 case lookupCtxt n (idris_patdefs i) of
881875 [] -> return ()
882876 [(_, tms)] ->
883− iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))
877+ iPrintResult (showSep "\n" (map (showTm i') tms))
884878 _ -> iPrintError $ "Ambiguous name"
885879process h fn (DynamicLink l)
886880 = do i <- getIState
@@ -949,9 +943,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t
949943dumpInstance :: Name -> Idris ()
950944dumpInstance n = do i <- getIState
951945 ctxt <- getContext
952− imp <- impShow
953946 case lookupTy n ctxt of
954− ts -> mapM_ (\t -> iputStrLn $ showImp Nothing imp False (delab i t)) ts
947+ ts -> mapM_ (\t -> iputStrLn $ showTm i (delab i t)) ts
955948
956949showTotal :: Totality -> IState -> String
957950showTotal t@(Partial (Other ns)) i
src/Util/Pretty.hs+1−1
@@ -1,5 +1,4 @@
11module Util.Pretty (
2− --module Text.PrettyPrint.HughesPJ,
32 module Text.PrettyPrint.Annotated.Leijen,
43 Sized(..), breakingSize, nestingSize,
54 Pretty(..)
@@ -28,3 +27,4 @@ nestingSize = 1
2827class Pretty a ty where
2928 pretty :: a -> Doc ty
3029
30+
test/reg007/expected+4−4
@@ -1,13 +1,13 @@
11reg007.lidr:8:1:A.n is already defined
22reg007.lidr:12:9:When elaborating right hand side of hurrah:
33Can't unify
4− n = lala
4+ n = lala
55with
6− 0 = 1
6+ 0 = 1
77
88Specifically:
99 Can't unify
10− 1
10+ 1
1111 with
12− 0
12+ 0
1313
test/reg007/run+1−1
@@ -1,3 +1,3 @@
11#!/usr/bin/env bash
2−idris --check $@ reg007.lidr
2+idris --nocolour --check $@ reg007.lidr
33rm -f *.ibc
test/test037/expected+4−4
@@ -6,13 +6,13 @@ Original error:
66
77 ErrorReflection.idr:78:5:When elaborating right hand side of bad:
88 Can't unify
9− Tm [] (Main.TFun t' t')
9+ Tm [] (TFun t' t')
1010 with
11− Tm [] Main.TUnit
11+ Tm [] TUnit
1212
1313 Specifically:
1414 Can't unify
15− Main.TFun t' t'
15+ TFun t' t'
1616 with
17− Main.TUnit
17+ TUnit
1818