dc4ce0c · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Replace the string-slinging show with pretty-print

dc4ce0cDavid Raymond Christiansen13 years ago

src/Idris/AbsSyntax.hs+1−305

compare with master

unifiedsplit

@@ -688,90 +688,6 @@ setTypeCase t = do i <- getIState

688 putIState $ i { idris_options = opt' }

689

690

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−

775-- Dealing with parameters

691-- Dealing with parameters

776

692

777expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

693expandParams :: (Name -> Name) -> [(Name, PTerm)] ->

@@ -1438,7 +1354,7 @@ mkPApp fc a f as = let rest = drop a as in

1438-- FIXME: It's possible that this really has to happen after elaboration

1354-- FIXME: It's possible that this really has to happen after elaboration

1439

1355

1440findStatics :: IState -> PTerm -> (PTerm, [Bool])

1356findStatics :: IState -> PTerm -> (PTerm, [Bool])

1441−findStatics ist tm = trace (showImp Nothing True False tm) $

1357+findStatics ist tm = trace (show tm) $

1442 let (ns, ss) = fs tm in

1358 let (ns, ss) = fs tm in

1443 runState (pos ns ss tm) []

1359 runState (pos ns ss tm) []

1444 where fs (PPi p n t sc)

1360 where fs (PPi p n t sc)

@@ -1723,223 +1639,3 @@ mkUniqueNames env tm = evalState (mkUniq tm) env where

1723 mkUniq t = return t

1639 mkUniq t = return t

1724

1640

1725

1641

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

892 xs -> sNS n xs

893

894

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+

895−--- Pretty printing declarations and terms

982+-- Pretty-printing declarations and terms

896

983

897instance Show PTerm where

984instance Show PTerm where

898− show tm = showImp Nothing False False tm

985+ showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

899−

900

986

901instance Show PDecl where

987instance Show PDecl where

902− show d = showDeclImp False d

988+ showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

903

989

904instance Show PClause where

990instance Show PClause where

905− show c = showCImp True c

991+ showsPrec _ c = (displayS . renderCompact . showCImp True) c

906

992

907instance Show PData where

993instance 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

909

1201

910−showDecls :: Bool -> [PDecl] -> String

911−showDecls _ [] = ""

912−showDecls i (d:ds) = showDeclImp i d ++ "\n" ++ showDecls i ds

913

1202

914−showDeclImp _ (PFix _ f ops) = show f ++ " " ++ showSep ", " ops

1203+ slist' p bnd (PApp _ (PRef _ nil) _)

915−showDeclImp i (PTy _ _ _ _ n t) = "tydecl " ++ showCG n ++ " : " ++ showImp Nothing i False t

1204+ | not impl && nsroot nil == sUN "Nil" = Just []

916−showDeclImp i (PClauses _ _ n cs) = "pat " ++ showCG n ++ "\t" ++ showSep "\n\t" (map (showCImp i) cs)

1205+ slist' p bnd (PApp _ (PRef _ cons) args)

917−showDeclImp _ (PData _ _ _ _ d) = showDImp True d

1206+ | nsroot cons == sUN "::",

918−showDeclImp i (PParams _ ns ps) = "params {" ++ show ns ++ "\n" ++ showDecls i ps ++ "}\n"

1207+ (PExp {getTm=tl}):(PExp {getTm=hd}):imps <- reverse args,

919−showDeclImp i (PNamespace n ps) = "namespace {" ++ n ++ "\n" ++ showDecls i ps ++ "}\n"

1208+ all isImp imps,

920−showDeclImp _ (PSyntax _ syn) = "syntax " ++ show syn

1209+ Just tl' <- slist' p bnd tl

921−showDeclImp i (PClass _ _ _ cs n ps ds)

1210+ = Just (hd:tl')

922− = "class " ++ show cs ++ " " ++ show n ++ " " ++ show ps ++ "\n" ++ showDecls i ds

1211+ where

923−showDeclImp i (PInstance _ _ cs n _ t _ ds)

1212+ isImp (PImp {}) = True

924− = "instance " ++ show cs ++ " " ++ show n ++ " " ++ show t ++ "\n" ++ showDecls i ds

1213+ isImp _ = False

925−showDeclImp _ _ = "..."

1214+ slist' _ _ _ = Nothing

926−-- showDeclImp (PImport i) = "import " ++ i

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

927

1226

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

928

1236

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+

929−showCImp :: Bool -> PClause -> String

1261+showCImp :: Bool -> PClause -> Doc OutputAnnotation

930showCImp impl (PClause _ n l ws r w)

1262showCImp impl (PClause _ n l ws r w)

931− = showImp Nothing impl False l ++ showWs ws ++ " = " ++ showImp Nothing impl False r

1263+ = prettyImp impl l <+> showWs ws <+> text "=" <+> prettyImp impl r

932− ++ " where " ++ show w

1264+ <+> text "where" <+> text (show w)

933 where

1265 where

934− showWs [] = ""

1266+ showWs [] = empty

935− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

1267+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

936showCImp impl (PWith _ n l ws r w)

1268showCImp impl (PWith _ n l ws r w)

937− = showImp Nothing impl False l ++ showWs ws ++ " with " ++ showImp Nothing impl False r

1269+ = prettyImp impl l <+> showWs ws <+> text "with" <+> prettyImp impl r

938− ++ " { " ++ show w ++ " } "

1270+ <+> braces (text (show w))

939 where

1271 where

940− showWs [] = ""

1272+ showWs [] = empty

941− showWs (x : xs) = " | " ++ showImp Nothing impl False x ++ showWs xs

1273+ showWs (x : xs) = text "|" <+> prettyImp impl x <+> showWs xs

942

1274

943

1275

944−showDImp :: Bool -> PData -> String

1276+showDImp :: Bool -> PData -> Doc OutputAnnotation

945showDImp impl (PDatadecl n ty cons)

1277showDImp impl (PDatadecl n ty cons)

946− = "data " ++ show n ++ " : " ++ showImp Nothing impl False ty ++ " where\n\t"

1278+ = text "data" <+> text (show n) <+> colon <+> prettyImp impl ty <+> text "where" <$>

947− ++ showSep "\n\t| "

1279+ (indent 2 $ vsep (map (\ (_, n, t, _, _) -> pipe <+> prettyName False [] n <+> colon <+> prettyImp impl t) cons))

948− (map (\ (_, n, t, _, _) -> show n ++ " : " ++ showImp Nothing impl False 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) ""

949

1301

950getImps :: [PArg] -> [(Name, PTerm)]

1302getImps :: [PArg] -> [(Name, PTerm)]

951getImps [] = []

1303getImps [] = []

@@ -995,168 +1347,14 @@ showName ist bnd impl colour n = case ist of

995 -- (like error messages). Thus, unknown vars are colourised as implicits.

1347 -- (like error messages). Thus, unknown vars are colourised as implicits.

996 | otherwise -> colouriseImplicit t name

1348 | otherwise -> colouriseImplicit t name

997

1349

998−-- | Show Idris term

999−showImp :: Maybe IState -- ^^ the Idris state, for information about identifiers and colours

1350+showTm :: 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

1351+ -> PTerm -- ^^ the term to show

1003− -> String

1352+ -> String

1004−showImp ist impl colour tm = se 10 [] tm where

1353+showTm ist = displayDecorated (consoleDecorate ist) . renderCompact . prettyImp (opt_showimp (idris_options ist))

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

1136

1354

1137− sArg bnd (PImp _ _ _ n tm _) = siArg bnd (n, tm)

1355+-- | Show a term with implicits, no colours

1138− sArg bnd (PExp _ _ tm _) = seArg bnd tm

1356+showTmImpls :: PTerm -> String

1139− sArg bnd (PConstraint _ _ tm _) = scArg bnd tm

1357+showTmImpls = flip (displayS . renderCompact . prettyImp True) ""

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

1160

1358

1161

1359

1162instance Sized PTerm where

1360instance Sized PTerm where

src/Idris/CaseSplit.hs+3−3

@@ -62,11 +62,11 @@ split n t'

62 Just ty ->

63 do let splits = findPats ist ty

64 iLOG ("New patterns " ++ showSep ", "

65− (map (showImp Nothing True False) splits))

65+ (map showTmImpls splits))

66 let newPats_in = zipWith (replaceVar ctxt n) splits (repeat t)

67 logLvl 4 ("Working from " ++ show t)

68 logLvl 4 ("Trying " ++ showSep "\n"

69− (map (showImp Nothing True False) newPats_in))

69+ (map (showTmImpls) newPats_in))

70 newPats <- mapM elabNewPat newPats_in

71 logLvl 3 ("Original:\n" ++ show t)

72 logLvl 3 ("Split:\n" ++

@@ -237,7 +237,7 @@ splitOnLine l n fn = do

237-- let (before, later) = splitAt (l-1) (lines inp)

238-- i <- getIState

239 cl <- getInternalApp fn l

240− logLvl 3 ("Working with " ++ showImp Nothing True False cl)

240+ logLvl 3 ("Working with " ++ showTmImpls cl)

241 tms <- split n cl

242-- iputStrLn (showSep "\n" (map show tms))

243 return tms -- "" -- not yet done...

src/Idris/Core/TT.hs+2

@@ -83,6 +83,8 @@ data NameOutput = TypeOutput | FunOutput | DataOutput

83-- | Output annotations for pretty-printing

84data OutputAnnotation = AnnName Name (Maybe NameOutput) (Maybe Type)

85 | AnnBoundName Name Bool

86+ | AnnConstData

87+ | AnnConstType

87-- | Used for error reflection

89-- | Used for error reflection

88data ErrorReportPart = TextPart String

90data ErrorReportPart = TextPart String

src/Idris/Coverage.hs+3−3

@@ -50,7 +50,7 @@ genClauses fc n xs given

50 logLvl 5 $ show (map length argss) ++ "\n" ++ show (map length all_args)

51 logLvl 10 $ show argss ++ "\n" ++ show all_args

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

54 -- add an infinite supply of explicit arguments to update the possible

55 -- cases for (the return type may be variadic, or function type, sp

56 -- there may be more case splitting that the idris_implicits record

@@ -60,10 +60,10 @@ genClauses fc n xs given

60 _ -> repeat (pexp Placeholder)

61 let tryclauses = mkClauses parg all_args

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

64 let new = filter (noMatch i) (nub tryclauses)

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

67-- ++ " from:\n" ++ showSep "\n" (map (showImp True) tryclauses)

68 return new

69-- return (map (\t -> PClause n t [] PImpossible []) new)

src/Idris/Delaborate.hs+36−49

@@ -125,60 +125,48 @@ pshow i (Msg s) = s

125pshow i (InternalMsg s) = "INTERNAL ERROR: " ++ show s ++

126 "\nThis is probably a bug, or a missing error message.\n" ++

127 "Please consider reporting at " ++ bugaddr

128−pshow i (CantUnify _ x y e sc s)

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

129+ "Can't unify" ++ indented (showTm i (delab i x)) ++

132− ++ "with" ++ indented (showImp (Just i) imps colour (delab i y)) ++

130+ "with" ++ indented (showTm i (delab i y)) ++

133−-- " (" ++ show x ++ " and " ++ show y ++ ") " ++

134− case e of

131+ case e of

135− Msg "" -> ""

132+ Msg "" -> ""

136− _ -> "\nSpecifically:" ++

133+ _ -> "\nSpecifically:" ++

137− indented (pshow i e) ++

134+ indented (pshow i e) ++

138− if (opt_errContext (idris_options i)) then showSc i sc else ""

135+ if (opt_errContext (idris_options i)) then showSc i sc else ""

139−pshow i (CantConvert x y env)

136+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"

137+ "Can't convert" ++ indented (showTm i (delab i x)) ++

143− ++ indented (showImp (Just i) imps colour (delab i y)) ++

138+ "with" ++ indented (showTm i (delab i y)) ++

144− if (opt_errContext (idris_options i)) then showSc i env else ""

139+ if (opt_errContext (idris_options i)) then showSc i env else ""

145−pshow i (UnifyScope n out tm env)

140+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"

141+ "Can't unify" ++ indented (show n) ++

149− ++ indented (showImp (Just i) imps colour (delab i tm)) ++ "as" ++

142+ "with" ++ indented (showTm i (delab i tm)) ++

150− indented (show out) ++ "is not in scope" ++

143+ "as" ++ indented (show out) ++ "is not in scope" ++

151− if (opt_errContext (idris_options i)) then showSc i env else ""

144+ if (opt_errContext (idris_options i)) then showSc i env else ""

152−pshow i (CantInferType t)

145+pshow i (CantInferType t) = "Can't infer type for " ++ t

153− = "Can't infer type for " ++ t

154−pshow i (NonFunctionType f ty)

146+pshow i (NonFunctionType f ty) =

155− = let imps = opt_showimp (idris_options i) in

147+ showTm i (delab i f) ++

156− let colour = idris_colourRepl i in

157− showImp (Just i) imps colour (delab i f) ++ " does not have a function type ("

148+ " does not have a function type (" ++

158− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

149+ showTm i (delab i ty) ++ ")"

159−pshow i (NotEquality tm ty)

150+pshow i (NotEquality tm ty) =

160− = let imps = opt_showimp (idris_options i) in

151+ showTm i (delab i tm) ++

161− let colour = idris_colourRepl i in

162− showImp (Just i) imps colour (delab i tm) ++ " does not have an equality type ("

152+ " does not have an equality type (" ++

163− ++ showImp (Just i) imps colour (delab i ty) ++ ")"

153+ showTm i (delab i ty) ++ ")"

164−pshow i (TooManyArguments f)

165− = "Too many arguments for " ++ show f

154+pshow i (TooManyArguments f) = "Too many arguments for " ++ show f

166−pshow i (CantIntroduce ty)

155+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)

156+ "Can't use lambda here: type is " ++ showTm i (delab i ty)

170pshow i (InfiniteUnify x tm env)

157pshow i (InfiniteUnify x tm env)

171− = "Unifying " ++ showbasic x ++ " and " ++ show (delab i tm) ++

158+ = "Unifying " ++ showbasic x ++ " and " ++ showTm i (delab i tm) ++

172 " would lead to infinite value" ++

159 " would lead to infinite value" ++

173 if (opt_errContext (idris_options i)) then showSc i env else ""

160 if (opt_errContext (idris_options i)) then showSc i env else ""

161+pshow i (NotInjective p x y) =

174−pshow i (NotInjective p x y) = "Can't verify injectivity of " ++ show (delab i p) ++

162+ "Can't verify injectivity of " ++ showTm i (delab i p) ++

175− " when unifying " ++ show (delab i x) ++ " and " ++

163+ " when unifying " ++ showTm i (delab i x) ++ " and " ++

176− show (delab i y)

164+ showTm i (delab i y)

177pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

165pshow i (CantResolve c) = "Can't resolve type class " ++ show (delab i c)

178pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

166pshow i (CantResolveAlts as) = "Can't disambiguate name: " ++ showSep ", " as

179pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

167pshow i (NoTypeDecl n) = "No type declaration for " ++ show n

180pshow i (NoSuchVariable n) = "No such variable " ++ show n

168pshow 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)

182pshow i UniverseError = "Universe inconsistency"

170pshow i UniverseError = "Universe inconsistency"

183pshow i ProgramLineComment = "Program line next to comment"

171pshow i ProgramLineComment = "Program line next to comment"

184pshow i (Inaccessible n) = show n ++ " is not an accessible pattern variable"

172pshow 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 "

199 showPart (TextPart str) = str

187 showPart (TextPart str) = str

200 showPart (NamePart n) = let colour = idris_colourRepl i in

188 showPart (NamePart n) = let colour = idris_colourRepl i in

201 showName (Just i) [] False colour n

189 showName (Just i) [] False colour n

202− showPart (TermPart tm) = let colour = idris_colourRepl i

190+ showPart (TermPart tm) = showTm i (delab i tm)

203− in showImp (Just i) False colour (delab i tm)

204 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

191 showPart (SubReport rs) = indented . concat . intersperse " " . map showPart $ rs

205pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

192pshow i (ReflectionFailed msg err) = "When attempting to perform error reflection, the following internal error occurred:\n" ++

206 indented (pshow i err) ++

193 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

67 ctxt <- getContext

68 i <- getIState

70− logLvl 3 $ show n ++ " pre-type " ++ showImp Nothing True False ty'

70+ logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

71 ty' <- addUsingConstraints syn fc ty'

72 ty' <- implicit syn n ty'

74 let ty = addImpl i ty'

75− logLvl 2 $ show n ++ " type " ++ showImp Nothing True False ty

75+ logLvl 2 $ show n ++ " type " ++ showTmImpls ty

76 ((tyT, defer, is), log) <-

77 tclift $ elaborate ctxt n (TType (UVal 0)) []

78 (errAt "type of " n (erun fc (build i info False [] n ty)))

@@ -325,10 +325,10 @@ elabEliminator paramPos n ty cons info = do

325 let clauseConsElimArgs = map getPiName consTerms

326 let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs

327 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

329 eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)

330 let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses

331− elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef

331+ elimLog $ "-- eliminator definition: " ++ (show . showDeclImp True) eliminatorDef

332 State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())

333 -- Do not elaborate clauses if there aren't any

334 case eliminatorClauses of

@@ -813,7 +813,7 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

813 i <- getIState

814 t_in <- implicit syn n (if codata then mkLazy t_in else t_in)

815 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

817 ((t', defer, is), log) <-

818 tclift $ elaborate ctxt n (TType (UVal 0)) []

819 (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

957 missing' <- filterM (checkPossible info fc True n) missing

958 let clhs = map getLHS pdef

959 logLvl 2 $ "Must be unreachable:\n" ++

960− showSep "\n" (map (showImp Nothing True False) missing') ++

960+ showSep "\n" (map showTmImpls missing') ++

961 "\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))

963 -- filter out anything in missing' which is

964 -- matched by any of clhs. This might happen since

965 -- unification may force a variable to take a

@@ -1123,8 +1123,8 @@ elabPE info fc caller r =

1123 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++

1124 showSep "\n"

1125 (map (\ (lhs, rhs) ->

1126− (showImp Nothing True False lhs ++ " = " ++

1126+ (showTmImpls lhs ++ " = " ++

1127− showImp Nothing True False rhs)) pats)

1127+ showTmImpls rhs)) pats)

1128 elabType info defaultSyntax "" fc opts newnm specTy

1129 let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats

1130 elabClauses info fc opts newnm def

@@ -1178,7 +1178,7 @@ elabValBind info aspat tm_in

1178 = do ctxt <- getContext

1179 i <- getIState

1180 let tm = addImpl i tm_in

1181− logLvl 10 (showImp Nothing True False tm)

1181+ logLvl 10 (showTmImpls tm)

1182 -- try:

1183 -- * ordinary elaboration

1184 -- * elaboration as a Type

@@ -1269,7 +1269,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1269 let params = getParamsInType i [] fn_is fn_ty

1270 let lhs = stripUnmatchable i $

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

1273 logLvl 4 ("Fixed parameters: " ++ show params ++ " from " ++ show (fn_ty, fn_is))

1274

1275 ((lhs', dlhs, []), _) <-

@@ -1284,7 +1284,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1284 (clhs_c, clhsty) <- recheckC fc [] lhs_tm

1285 let clhs = normalise ctxt [] clhs_c

1286

1287− logLvl 3 ("Normalised LHS: " ++ showImp Nothing True False (delabMV i clhs))

1287+ logLvl 3 ("Normalised LHS: " ++ showTmImpls (delabMV i clhs))

1288

1289 rep <- useREPL

1290 when rep $ do

@@ -1310,10 +1310,10 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1310 mapM_ (elabDecl' EAll info) wbefore

1311 -- Now build the RHS, using the type of the LHS as the goal.

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

1314 let rhs = addImplBoundInf i (map fst newargs) (defs \\ decls)

1315 (expandParams decorate newargs defs (defs \\ decls) rhs_in)

1316− logLvl 2 $ "RHS: " ++ showImp Nothing True False rhs

1316+ logLvl 2 $ "RHS: " ++ showTmImpls rhs

1317 ctxt <- getContext -- new context with where block added

1318 logLvl 5 "STARTING CHECK"

1319 ((rhs', defer, is), _) <-

@@ -1452,7 +1452,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1452 -- pattern bindings

1453 i <- getIState

1454 let lhs = addImplPat i (stripLinear i lhs_in)

1455− logLvl 5 ("LHS: " ++ showImp Nothing True False lhs)

1455+ logLvl 5 ("LHS: " ++ showTmImpls lhs)

1456 ((lhs', dlhs, []), _) <-

1457 tclift $ elaborate ctxt (sMN 0 "patLHS") infP []

1458 (errAt "left hand side of with in " fname

@@ -1465,7 +1465,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1465 logLvl 5 ("Checked " ++ show clhs)

1466 let bargs = getPBtys lhs_tm

1467 let wval = addImplBound i (map fst bargs) wval_in

1468− logLvl 5 ("Checking " ++ showImp Nothing True False wval)

1468+ logLvl 5 ("Checking " ++ showTmImpls wval)

1469 -- Elaborate wval in this context

1470 ((wval', defer, is), _) <-

1471 tclift $ elaborate ctxt (sMN 0 "withRHS")

@@ -1529,7 +1529,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1529 (map (pexp . (PRef fc) . fst) bargs_pre ++

1530 pexp wval :

1531 (map (pexp . (PRef fc) . fst) bargs_post))

1532− logLvl 5 ("New RHS " ++ showImp Nothing True False rhs)

1532+ logLvl 5 ("New RHS " ++ showTmImpls rhs)

1533 ctxt <- getContext -- New context with block added

1534 i <- getIState

1535 ((rhs', defer, is), _) <-

@@ -1560,8 +1560,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1560 mkAux wname toplhs ns ns' (PClause fc n tm_in (w:ws) rhs wheres)

1561 = do i <- getIState

1562 let tm = addImplPat i tm_in

1563− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1563+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1564− showImp Nothing True False toplhs)

1564+ showTmImpls toplhs)

1565 case matchClause i toplhs tm of

1566 Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

1567 Right mvars ->

@@ -1571,8 +1571,8 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1571 mkAux wname toplhs ns ns' (PWith fc n tm_in (w:ws) wval withs)

1572 = do i <- getIState

1573 let tm = addImplPat i tm_in

1574− logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1574+ logLvl 2 ("Matching " ++ showTmImpls tm ++ " against " ++

1575− showImp Nothing True False toplhs)

1575+ showTmImpls toplhs)

1576 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

1577 case matchClause i toplhs tm of

1578 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

1639 constraint

1640 let cons = [("", cn, cty, fc, [])]

1641 let ddecl = PDatadecl tn tty cons

1642− logLvl 5 $ "Class data " ++ showDImp True ddecl

1642+ logLvl 5 $ "Class data " ++ show (showDImp True ddecl)

1643 elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl

1644 -- for each constraint, build a top level function to chase it

1645 logLvl 5 $ "Building functions"

@@ -1681,7 +1681,7 @@ elabClass info syn doc fc constraints tn ps ds

1681 getMName (PTy _ _ _ _ n _) = nsroot n

1682 tdecl allmeths (PTy doc syn _ o n t)

1683 = 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'

1685 return ( (n, (toExp (map fst ps) Exp t')),

1686 (n, (doc, o, (toExp (map fst ps) Imp t'))),

1687 (n, (syn, o, t) ) )

@@ -1718,8 +1718,8 @@ elabClass info syn doc fc constraints tn ps ds

1718 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1719 let rhs = PResolveTC (fileFC "HACK")

1720 let ty = PPi constraint (sMN 0 "pc") c con

1721− iLOG (showImp Nothing True False ty)

1721+ iLOG (showTmImpls ty)

1722− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1722+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1723 i <- getIState

1724 let conn = case con of

1725 PRef _ n -> n

@@ -1743,9 +1743,9 @@ elabClass info syn doc fc constraints tn ps ds

1743 let anames = map (\x -> sMN x "arg") [0..]

1744 let lhs = PApp fc (PRef fc m) (pconst capp : lhsArgs margs anames)

1745 let rhs = PApp fc (getMeth mnames all m) (rhsArgs margs anames)

1746− iLOG (showImp Nothing True False ty)

1746+ iLOG (showTmImpls ty)

1747 iLOG (show (m, ty', capp, margs))

1748− iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

1748+ iLOG (showTmImpls lhs ++ " = " ++ showTmImpls rhs)

1749 return [PTy doc syn fc o m ty',

1750 PClauses fc [Inlinable] m [PClause fc m lhs [] rhs []]]

1751

@@ -1833,7 +1833,7 @@ elabInstance info syn what fc cs n ps t expn ds = do

1833 let wbTys = map mkTyDecl mtys

1834 let wbVals = map (decorateid (decorate ns iname)) ds'

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

1837 logLvl 3 $ "Instance is " ++ show ps ++ " implicits " ++

1838 show (concat (nub wparams))

1839 let lhs = PRef fc iname

@@ -2140,8 +2140,8 @@ elabCaseBlock info opts d@(PClauses f o n ps)

2140

2141checkInferred :: FC -> PTerm -> PTerm -> Idris ()

2142checkInferred fc inf user =

2143− do logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n\nFROM\n\n" ++

2143+ do logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n\nFROM\n\n" ++

2144− showImp Nothing True False user

2144+ showTmImpls user

2145 logLvl 10 $ "Checking match"

2146 i <- getIState

2147 tclift $ case matchClause' True i user inf of

@@ -2158,8 +2158,8 @@ checkInferred fc inf user =

2158inferredDiff :: FC -> PTerm -> PTerm -> Idris Bool

2159inferredDiff fc inf user =

2160 do i <- getIState

2161− logLvl 6 $ "Checked to\n" ++ showImp Nothing True False inf ++ "\n" ++

2161+ logLvl 6 $ "Checked to\n" ++ showTmImpls inf ++ "\n" ++

2162− showImp Nothing True False user

2162+ showTmImpls user

2163 tclift $ case matchClause' True i user inf of

2164 Right vs -> return False

2165 Left (x, y) -> return True

src/Idris/Parser.hs+1−1

@@ -1060,7 +1060,7 @@ loadSource h lidr f

1060 f file pos

1061 unless (null ds') $ do

1062 let ds = namespaces mname ds'

1063− logLvl 3 (showDecls True ds)

1063+ logLvl 3 (show $ showDecls True ds)

1064 i <- getIState

1065 logLvl 10 (show (toAlist (idris_implicits i)))

1066 logLvl 3 (show (idris_infixes i))

src/Idris/REPL.hs+16−23

@@ -448,10 +448,8 @@ process h fn (Eval t)

448 ist <- getIState

449 logLvl 3 $ "Raw: " ++ show (tm', ty')

450 logLvl 10 $ "Debug: " ++ showEnvDbg [] tm'

451− imp <- impShow

452− c <- colourise

453− ihPrintResult h (showImp (Just ist) imp c (delab ist tm') ++ " : " ++

451+ ihPrintResult h (showTm ist (delab ist tm') ++ " : " ++

454− showImp (Just ist) imp c (delab ist ty'))

452+ showTm ist (delab ist ty'))

455process h fn (ExecVal t)

453process h fn (ExecVal t)

456 = do ctxt <- getContext

454 = do ctxt <- getContext

457 ist <- getIState

455 ist <- getIState

@@ -459,10 +457,8 @@ process h fn (ExecVal t)

459-- let tm' = normaliseAll ctxt [] tm

457-- let tm' = normaliseAll ctxt [] tm

460 let ty' = normaliseAll ctxt [] ty

458 let ty' = normaliseAll ctxt [] ty

461 res <- execute tm

459 res <- execute tm

462− imp <- impShow

463− c <- colourise

464− ihPrintResult h (showImp (Just ist) imp c (delab ist res) ++ " : " ++

460+ ihPrintResult h (showTm ist (delab ist res) ++ " : " ++

465− showImp (Just ist) imp c (delab ist ty'))

461+ showTm ist (delab ist ty'))

466process h fn (Check (PRef _ n))

462process h fn (Check (PRef _ n))

467 = do ctxt <- getContext

463 = do ctxt <- getContext

468 ist <- getIState

464 ist <- getIState

@@ -474,7 +470,7 @@ process h fn (Check (PRef _ n))

474 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

470 Just (_, i, _) -> ihPrintResult h (showMetavarInfo c imp ist n i)

475 Nothing -> ihPrintResult h $

471 Nothing -> ihPrintResult h $

476 concat . intersperse "\n" . map (\n -> showName (Just ist) [] False c n ++ " : " ++

472 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

478 [] -> ihPrintError h $ "No such variable " ++ show n

474 [] -> ihPrintError h $ "No such variable " ++ show n

479 where

475 where

480 showMetavarInfo c imp ist n i

476 showMetavarInfo c imp ist n i

@@ -487,27 +483,25 @@ process h fn (Check (PRef _ n))

487 MN _ _ -> "_"

483 MN _ _ -> "_"

488 UN nm | ('_':'_':_) <- str nm -> "_"

484 UN nm | ('_':'_':_) <- str nm -> "_"

489 _ -> showName (Just ist) [] False c n) ++

485 _ -> showName (Just ist) [] False c n) ++

490− " : " ++ showImp (Just ist) imp c t ++ "\n"

486+ " : " ++ showTm ist t ++ "\n"

491 in

487 in

492 current ++ putTy c imp ist (i-1) sc

488 current ++ putTy c imp ist (i-1) sc

493 putTy c imp ist _ sc = putGoal c imp ist sc

489 putTy c imp ist _ sc = putGoal c imp ist sc

494 putGoal c imp ist g

490 putGoal c imp ist g

495 = "--------------------------------------\n" ++

491 = "--------------------------------------\n" ++

496 showName (Just ist) [] False c n ++ " : " ++

492 showName (Just ist) [] False c n ++ " : " ++

497− showImp (Just ist) imp c g

493+ showTm ist g

498

494

499

495

500process h fn (Check t)

496process h fn (Check t)

501 = do (tm, ty) <- elabVal toplevel False t

497 = do (tm, ty) <- elabVal toplevel False t

502 ctxt <- getContext

498 ctxt <- getContext

503 ist <- getIState

499 ist <- getIState

504− imp <- impShow

505− c <- colourise

506 let ty' = normaliseC ctxt [] ty

500 let ty' = normaliseC ctxt [] ty

507 case tm of

501 case tm of

508 TType _ -> ihPrintResult h ("Type : Type 1")

502 TType _ -> ihPrintResult h ("Type : Type 1")

509− _ -> ihPrintResult h (showImp (Just ist) imp c (delab ist tm) ++ " : " ++

503+ _ -> ihPrintResult h (showTm ist (delab ist tm) ++ " : " ++

510− showImp (Just ist) imp c (delab ist ty))

504+ showTm ist (delab ist ty))

511

505

512process h fn (DocStr n)

506process h fn (DocStr n)

513 = do i <- getIState

507 = do i <- getIState

@@ -540,9 +534,9 @@ process h fn (Defn n)

540 [t] -> iputStrLn (showTotal t i)

534 [t] -> iputStrLn (showTotal t i)

541 _ -> return ()

535 _ -> return ()

542 where printCase i (_, lhs, rhs)

536 where printCase i (_, lhs, rhs)

543− = do c <- colourise

537+ = let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

544− iputStrLn (showImp (Just i) True c (delab i lhs) ++ " = " ++

538+ in iputStrLn (showTm i' (delab i lhs) ++ " = " ++

545− showImp (Just i) True c (delab i rhs))

539+ showTm i' (delab i rhs))

546process h fn (TotCheck n)

540process h fn (TotCheck n)

547 = do i <- getIState

541 = do i <- getIState

548 case lookupNameTotal n (tt_ctxt i) of

542 case lookupNameTotal n (tt_ctxt i) of

@@ -848,7 +842,7 @@ process h fn (TestInline t)

848 let tm' = inlineTerm ist tm

842 let tm' = inlineTerm ist tm

849 imp <- impShow

843 imp <- impShow

850 c <- colourise

844 c <- colourise

851− iPrintResult (showImp (Just ist) imp c (delab ist tm'))

845+ iPrintResult (showTm ist (delab ist tm'))

852process h fn Execute

846process h fn Execute

853 = do (m, _) <- elabVal toplevel False

847 = do (m, _) <- elabVal toplevel False

854 (PApp fc

848 (PApp fc

@@ -876,11 +870,11 @@ process h fn (Pattelab t)

876

870

877process h fn (Missing n)

871process h fn (Missing n)

878 = do i <- getIState

872 = do i <- getIState

879− c <- colourise

873+ let i' = i { idris_options = (idris_options i) { opt_showimp = True } }

880 case lookupCtxt n (idris_patdefs i) of

874 case lookupCtxt n (idris_patdefs i) of

881 [] -> return ()

875 [] -> return ()

882 [(_, tms)] ->

876 [(_, tms)] ->

883− iPrintResult (showSep "\n" (map (showImp (Just i) True c) tms))

877+ iPrintResult (showSep "\n" (map (showTm i') tms))

884 _ -> iPrintError $ "Ambiguous name"

878 _ -> iPrintError $ "Ambiguous name"

885process h fn (DynamicLink l)

879process h fn (DynamicLink l)

886 = do i <- getIState

880 = do i <- getIState

@@ -949,9 +943,8 @@ dumpDefaultInstance (PInstance _ _ _ _ _ t _ _) = iputStrLn $ show t

949dumpInstance :: Name -> Idris ()

943dumpInstance :: Name -> Idris ()

950dumpInstance n = do i <- getIState

944dumpInstance n = do i <- getIState

951 ctxt <- getContext

945 ctxt <- getContext

952− imp <- impShow

953 case lookupTy n ctxt of

946 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

955

948

956showTotal :: Totality -> IState -> String

949showTotal :: Totality -> IState -> String

957showTotal t@(Partial (Other ns)) i

950showTotal t@(Partial (Other ns)) i

src/Util/Pretty.hs+1−1

@@ -1,5 +1,4 @@

1module Util.Pretty (

2− --module Text.PrettyPrint.HughesPJ,

3 module Text.PrettyPrint.Annotated.Leijen,

2 module Text.PrettyPrint.Annotated.Leijen,

4 Sized(..), breakingSize, nestingSize,

3 Sized(..), breakingSize, nestingSize,

5 Pretty(..)

4 Pretty(..)

@@ -28,3 +27,4 @@ nestingSize = 1

28class Pretty a ty where

27class Pretty a ty where

29 pretty :: a -> Doc ty

28 pretty :: a -> Doc ty

30+

test/reg007/expected+4−4

@@ -1,13 +1,13 @@

1reg007.lidr:8:1:A.n is already defined

2reg007.lidr:12:9:When elaborating right hand side of hurrah:

3Can't unify

4− [92mn[0m[94m = [0m[92mlala[0m

4+ n = lala

5with

6− [91m0[0m[94m = [0m[91m1[0m

6+ 0 = 1

8Specifically:

9 Can't unify

10− [91m1[0m

10+ 1

11 with

12− [91m0[0m

12+ 0

test/reg007/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−idris --check $@ reg007.lidr

2+idris --nocolour --check $@ reg007.lidr

3rm -f *.ibc

test/test037/expected+4−4

@@ -6,13 +6,13 @@ Original error:

7 ErrorReflection.idr:78:5:When elaborating right hand side of bad:

8 Can't unify

9− Tm [] (Main.TFun t' t')

9+ Tm [] (TFun t' t')

10 with

11− Tm [] Main.TUnit

11+ Tm [] TUnit

13 Specifically:

14 Can't unify

15− Main.TFun t' t'

15+ TFun t' t'

16 with

17− Main.TUnit

17+ TUnit