git.iko.soy/Idris-dev
on master help sign in
Basic functioning with new pretty-printer
commit13f3c296ec3dfe429e818d5e6fdff7db23b7916e authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateSun 26 Jan 2014, 19:27 (13 years ago) parent1dfc8fd
8 files changed+101−103
compare with master
unifiedsplit
idris.cabal+2 src/Idris/AbsSyntax.hs+4−4 src/Idris/AbsSyntaxTree.hs+36−47 src/Idris/Core/Elaborate.hs+1−1 src/Idris/Core/ProofState.hs+12−12 src/Idris/Core/TT.hs+29−19 src/Idris/Prover.hs+11−11 src/Util/Pretty.hs+6−9
idris.cabal+2
@@ -421,6 +421,7 @@ Library
421421
422422 Build-depends: base >=4 && <5
423423 , Cabal
424+ , annotated-wl-pprint
424425 , ansi-terminal
425426 , ansi-wl-pprint
426427 , binary
@@ -450,6 +451,7 @@ Library
450451 , zlib
451452 Extensions: MultiParamTypeClasses
452453 , FunctionalDependencies
454+ , FlexibleContexts
453455 , FlexibleInstances
454456 , TemplateHaskell
455457
src/Idris/AbsSyntax.hs+4−4
@@ -421,11 +421,11 @@ ideslavePutSExp cmd info = do i <- getIState
421421 _ -> return ()
422422
423423-- this needs some typing magic and more structured output towards emacs
424−iputGoal :: String -> Idris ()
425−iputGoal s = do i <- getIState
424+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()
425+iputGoal g = do i <- getIState
426426 case idris_outputmode i of
427− RawOutput -> runIO $ putStrLn s
428− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n
427+ RawOutput -> runIO $ displayIO stdout g >> putStrLn ""
428+ IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" (displayS g "") n
429429
430430isetPrompt :: String -> Idris ()
431431isetPrompt p = do i <- getIState
src/Idris/AbsSyntaxTree.hs+36−47
@@ -30,6 +30,8 @@ import Data.Word (Word)
3030
3131import Debug.Trace
3232
33+import Text.PrettyPrint.Annotated.Leijen
34+
3335data IOption = IOption { opt_logLevel :: Int,
3436 opt_typecase :: Bool,
3537 opt_typeintype :: Bool,
@@ -895,7 +897,7 @@ expandNS syn n = case syn_namespace syn of
895897instance Show PTerm where
896898 show tm = showImp Nothing False False tm
897899
898−instance Pretty PTerm where
900+instance Pretty PTerm OutputAnnotation where
899901 pretty = prettyImp False
900902
901903instance Show PDecl where
@@ -965,15 +967,17 @@ getConsts (_ : xs) = getConsts xs
965967getAll :: [PArg] -> [PTerm]
966968getAll = map getTm
967969
970+
968971-- | Pretty-print a high-level Idris term
969972prettyImp :: Bool -- ^^ whether to show implicits
970973 -> PTerm -- ^^ the term to pretty-print
971− -> Doc
974+ -> Doc OutputAnnotation
972975prettyImp impl = prettySe 10
973976 where
977+ prettySe :: Int -> PTerm -> Doc OutputAnnotation
974978 prettySe p (PQuote r) =
975979 if size r > breakingSize then
976− text "![" $$ pretty r <> text "]"
980+ text "![" <> line <> pretty r <> text "]"
977981 else
978982 text "![" <> pretty r <> text "]"
979983 prettySe p (PPatvar fc n) = pretty n
@@ -990,37 +994,37 @@ prettyImp impl = prettySe 10
990994 prettySe p (PLam n ty sc) =
991995 bracket p 2 $
992996 if size sc > breakingSize then
993− text "λ" <> pretty n <+> text "=>" $+$ pretty sc
997+ text "λ" <> pretty n <+> text "=>" <> line <> pretty sc
994998 else
995999 text "λ" <> pretty n <+> text "=>" <+> pretty sc
9961000 prettySe p (PLet n ty v sc) =
9971001 bracket p 2 $
9981002 if size sc > breakingSize then
999− text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" $+$
1003+ text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <>
10001004 nest nestingSize (prettySe 10 sc)
10011005 else
10021006 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>
10031007 prettySe 10 sc
10041008 prettySe p (PPi (Exp l s _ _) n ty sc)
10051009 | n `elem` allNamesIn sc || impl =
1006− let open = if l then text "|" <> lparen else lparen in
1010+ let open = (if l then text "|" else empty) <> lparen in
10071011 bracket p 2 $
10081012 if size sc > breakingSize then
1009− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1010− st <+> text "->" $+$ prettySe 10 sc
1013+ enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>
1014+ st <> text "->" <> line <> prettySe 10 sc
10111015 else
1012− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>
1013− st <+> text "->" <+> prettySe 10 sc
1016+ enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>
1017+ st <> text "->" <+> prettySe 10 sc
10141018 | otherwise =
10151019 bracket p 2 $
10161020 if size sc > breakingSize then
1017− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc
1021+ prettySe 0 ty <+> st <+> text "->" <> line <> prettySe 10 sc
10181022 else
10191023 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc
10201024 where
10211025 st =
10221026 case s of
1023− Static -> text "[static]"
1027+ Static -> text "[static]" <> space
10241028 _ -> empty
10251029 prettySe p (PPi (Imp l s _ _) n ty sc)
10261030 | impl =
@@ -1028,27 +1032,27 @@ prettyImp impl = prettySe 10
10281032 bracket p 2 $
10291033 if size sc > breakingSize then
10301034 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1031− st <+> text "->" <+> prettySe 10 sc
1035+ st <> text "->" <+> prettySe 10 sc
10321036 else
10331037 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>
1034− st <+> text "->" <+> prettySe 10 sc
1038+ st <> text "->" <+> prettySe 10 sc
10351039 | otherwise = prettySe 10 sc
10361040 where
10371041 st =
10381042 case s of
1039− Static -> text $ "[static]"
1043+ Static -> text "[static]" <> space
10401044 _ -> empty
10411045 prettySe p (PPi (Constraint _ _ _) n ty sc) =
10421046 bracket p 2 $
10431047 if size sc > breakingSize then
10441048 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc
10451049 else
1046− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc
1050+ prettySe 10 ty <+> text "=>" <> line <> prettySe 10 sc
10471051 prettySe p (PPi (TacImp _ _ s _) n ty sc) =
10481052 bracket p 2 $
10491053 if size sc > breakingSize then
10501054 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
1051− rbrace <+> text "->" $+$ prettySe 10 sc
1055+ rbrace <+> text "->" <> line <> prettySe 10 sc
10521056 else
10531057 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>
10541058 rbrace <+> text "->" <+> prettySe 10 sc
@@ -1062,37 +1066,22 @@ prettyImp impl = prettySe 10
10621066 let [l, r] = getExps args in
10631067 bracket p 1 $
10641068 if size r > breakingSize then
1065− prettySe 1 l <+> pretty op $+$ prettySe 0 r
1069+ prettySe 1 l <+> pretty op <> line <> prettySe 0 r
10661070 else
10671071 prettySe 1 l <+> pretty op <+> prettySe 0 r
10681072 prettySe p (PApp _ f as) =
10691073 let args = getExps as in
10701074 bracket p 1 $
10711075 prettySe 1 f <+>
1072− if impl then
1073− foldl' fS empty as
1074− -- foldr (<+>) empty $ map prettyArgS as
1075− else
1076− foldl' fSe empty args
1077− -- foldr (<+>) empty $ map prettyArgSe args
1078− where
1079− fS l r =
1080− if size r > breakingSize then
1081− l $+$ nest nestingSize (prettyArgS r)
1082− else
1083− l <+> prettyArgS r
1084−
1085− fSe l r =
1086− if size r > breakingSize then
1087− l $+$ nest nestingSize (prettyArgSe r)
1088− else
1089− l <+> prettyArgSe r
1076+ align (hsep (if impl
1077+ then map prettyArgS as
1078+ else map prettyArgSe args))
10901079 prettySe p (PCase _ scr opts) =
1091− text "case" <+> prettySe 10 scr <+> text "of" $+$ nest nestingSize prettyBody
1080+ text "case" <+> prettySe 10 scr <+> text "of" <> prettyBody
10921081 where
1093− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts
1082+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts
10941083
1095− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r
1084+ sc (l, r) = nest nestingSize $ prettySe 10 l <+> text "=>" <+> prettySe 10 r
10961085 prettySe p (PHidden tm) = text "." <> prettySe 0 tm
10971086 prettySe p (PRefl _ _) = text "refl"
10981087 prettySe p (PResolveTC _) = text "resolvetc"
@@ -1101,27 +1090,27 @@ prettyImp impl = prettySe 10
11011090 prettySe p (PEq _ l r) =
11021091 bracket p 2 $
11031092 if size r > breakingSize then
1104− prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)
1093+ prettySe 10 l <+> text "=" <> nest nestingSize (prettySe 10 r)
11051094 else
11061095 prettySe 10 l <+> text "=" <+> prettySe 10 r
11071096 prettySe p (PRewrite _ l r _) =
11081097 bracket p 2 $
11091098 if size r > breakingSize then
1110− text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)
1099+ text "rewrite" <+> prettySe 10 l <+> text "in" <> nest nestingSize (prettySe 10 r)
11111100 else
11121101 text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r
11131102 prettySe p (PTyped l r) =
11141103 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen
11151104 prettySe p (PPair _ l r) =
11161105 if size r > breakingSize then
1117− lparen <> prettySe 10 l <> text "," $+$
1118− prettySe 10 r <> rparen
1106+ lparen <> prettySe 10 l <> text "," <>
1107+ line <> prettySe 10 r <> rparen
11191108 else
11201109 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen
11211110 prettySe p (PDPair _ l t r) =
11221111 if size r > breakingSize then
1123− lparen <> prettySe 10 l <+> text "**" $+$
1124− prettySe 10 r <> rparen
1112+ lparen <> prettySe 10 l <+> text "**" <>
1113+ line <> prettySe 10 r <> rparen
11251114 else
11261115 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen
11271116 prettySe p (PAlternative a as) =
@@ -1133,9 +1122,9 @@ prettyImp impl = prettySe 10
11331122 prettySe p (PConstant c) = pretty c
11341123 -- XXX: add pretty for tactics
11351124 prettySe p (PProof ts) =
1136− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1125+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
11371126 prettySe p (PTactics ts) =
1138− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace
1127+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace
11391128 prettySe p (PMetavar n) = text "?" <> pretty n
11401129 prettySe p (PReturn f) = text "return"
11411130 prettySe p PImpossible = text "impossible"
src/Idris/Core/Elaborate.hs+1−1
@@ -24,7 +24,7 @@ import Data.Char
2424import Data.List
2525import Debug.Trace
2626
27−import Util.Pretty
27+import Util.Pretty hiding (fill)
2828
2929-- I don't really want this here, but it's useful for the test shell
3030data Command = Theorem Name Raw
src/Idris/Core/ProofState.hs+12−12
@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)
1818import Data.List
1919import Debug.Trace
2020
21−import Util.Pretty
21+import Util.Pretty hiding (fill)
2222
2323data ProofState = PS { thname :: Name,
2424 holes :: [Name], -- holes still to be solved
@@ -113,23 +113,23 @@ instance Show ProofState where
113113 " =?= " ++ showEnv ps v
114114 showG ps b = showEnv ps (binderTy b)
115115
116−instance Pretty ProofState where
116+instance Pretty ProofState OutputAnnotation where
117117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
118118 if size nm > breakingSize then
119− pretty nm <> colon $$ nest nestingSize (text " no more goals.")
119+ pretty nm <+> colon <+> nest nestingSize (text " no more goals.")
120120 else
121− pretty nm <> colon <+> text " no more goals."
121+ pretty nm <+> colon <+> text " no more goals."
122122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =
123123 let OK g = goal (Just h) tm in
124124 let wkEnv = premises g in
125− text "Other goals" <+> colon <+> pretty hs $$
126− prettyPs wkEnv (reverse wkEnv) $$
127− text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$
125+ text "Other goals" <+> colon <+> pretty hs <+>
126+ prettyPs wkEnv (reverse wkEnv) <+>
127+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>
128128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)
129129 where
130130 prettyGoal ps (Guess t v) =
131131 if size v > breakingSize then
132− prettyEnv ps t <+> text "=?=" $$
132+ prettyEnv ps t <+> text "=?=" <+>
133133 nest nestingSize (prettyEnv ps v)
134134 else
135135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v
@@ -139,17 +139,17 @@ instance Pretty ProofState where
139139 prettyPs env ((n, Let t v):bs) =
140140 nest nestingSize (pretty n <+> colon <+>
141141 if size v > breakingSize then
142− prettyEnv env t <+> text "=" $$
143− nest nestingSize (prettyEnv env v) $$
142+ prettyEnv env t <+> text "=" <+>
143+ nest nestingSize (prettyEnv env v) <+>
144144 nest nestingSize (prettyPs env bs)
145145 else
146− prettyEnv env t <+> text "=" <+> prettyEnv env v $$
146+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>
147147 nest nestingSize (prettyPs env bs))
148148 prettyPs env ((n, b):bs) =
149149 if size (binderTy b) > breakingSize then
150150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)
151151 else
152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$
152+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>
153153 nest nestingSize (prettyPs env bs))
154154
155155same Nothing n = True
src/Idris/Core/TT.hs+29−19
@@ -77,6 +77,12 @@ instance Sized FC where
7777instance Show FC where
7878 show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c
7979
80+-- | Output annotation for pretty-printed name - decides colour
81+data NameOutput = TypeOutput | FunOutput | DataOutput | BoundOutput Bool
82+
83+-- | Output annotations for pretty-printing
84+data OutputAnnotation = OutName Name (Maybe NameOutput) (Maybe Type)
85+
8086-- | Used for error reflection
8187data ErrorReportPart = TextPart String
8288 | NamePart Name
@@ -170,15 +176,15 @@ instance Show Err where
170176 show (At f e) = show f ++ ":" ++ show e
171177 show _ = "Error"
172178
173−instance Pretty Err where
179+instance Pretty Err OutputAnnotation where
174180 pretty (Msg m) = text m
175181 pretty (CantUnify _ l r e _ i) =
176182 if size l + size r > breakingSize then
177− text "Cannot unify" <+> colon $$
178− nest nestingSize (pretty l <+> text "and" <+> pretty r) $$
183+ text "Cannot unify" <+> colon <+>
184+ nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>
179185 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
180186 else
181− text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$
187+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>
182188 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))
183189 pretty (ProviderError msg) = text msg
184190 pretty err@(LoadingFailed _ _) = text (show err)
@@ -189,11 +195,11 @@ instance Error Err where
189195
190196type TC = TC' Err
191197
192−instance (Pretty a) => Pretty (TC a) where
198+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where
193199 pretty (OK ok) = pretty ok
194200 pretty (Error err) =
195201 if size err > breakingSize then
196− text "Error" <+> colon $$ (nest nestingSize $ pretty err)
202+ text "Error" <+> colon <+> (nest nestingSize $ pretty err)
197203 else
198204 text "Error" <+> colon <+> pretty err
199205
@@ -287,11 +293,15 @@ instance Sized Name where
287293 size (MN i n) = 1
288294 size _ = 1
289295
290−instance Pretty Name where
291− pretty (UN n) = text (T.unpack n)
292− pretty (NS n s) = pretty n
293− pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
294− pretty (SN s) = text (show s)
296+instance Pretty Name OutputAnnotation where
297+ pretty n@(UN n') = annotate (OutName n Nothing Nothing) $ text (T.unpack n')
298+ pretty n@(NS un s) = annotate (OutName n Nothing Nothing) . noAnnotate $ pretty n
299+ pretty n@(MN i s) = annotate (OutName n Nothing Nothing) $
300+ lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace
301+ pretty n@(SN s) = annotate (OutName n Nothing Nothing) $ text (show s)
302+
303+instance Pretty [Name] OutputAnnotation where
304+ pretty = encloseSep empty empty comma . map pretty
295305
296306instance Show Name where
297307 show (UN n) = str n
@@ -408,7 +418,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)
408418data NativeTy = IT8 | IT16 | IT32 | IT64
409419 deriving (Show, Eq, Ord, Enum)
410420
411−instance Pretty NativeTy where
421+instance Pretty NativeTy OutputAnnotation where
412422 pretty IT8 = text "Bits8"
413423 pretty IT16 = text "Bits16"
414424 pretty IT32 = text "Bits32"
@@ -426,7 +436,7 @@ deriving instance NFData NativeTy
426436deriving instance NFData ArithTy
427437!-}
428438
429−instance Pretty ArithTy where
439+instance Pretty ArithTy OutputAnnotation where
430440 pretty (ATInt ITNative) = text "Int"
431441 pretty (ATInt ITBig) = text "BigInt"
432442 pretty (ATInt ITChar) = text "Char"
@@ -462,7 +472,7 @@ deriving instance NFData Const
462472instance Sized Const where
463473 size _ = 1
464474
465−instance Pretty Const where
475+instance Pretty Const OutputAnnotation where
466476 pretty (I i) = text . show $ i
467477 pretty (BI i) = text . show $ i
468478 pretty (Fl f) = text . show $ f
@@ -494,7 +504,7 @@ instance Sized Raw where
494504 size (RForce raw) = 1 + size raw
495505 size (RConstant const) = size const
496506
497−instance Pretty Raw where
507+instance Pretty Raw OutputAnnotation where
498508 pretty = text . show
499509
500510{-!
@@ -604,7 +614,7 @@ deriving instance NFData NameType
604614instance Sized NameType where
605615 size _ = 1
606616
607−instance Pretty NameType where
617+instance Pretty NameType OutputAnnotation where
608618 pretty = text . show
609619
610620instance Eq NameType where
@@ -662,7 +672,7 @@ instance Sized a => Sized (TT a) where
662672 size Erased = 1
663673 size (TType u) = 1 + size u
664674
665−instance Pretty a => Pretty (TT a) where
675+instance Pretty a o => Pretty (TT a) o where
666676 pretty _ = text "test"
667677
668678type EnvTT n = [(n, Binder (TT n))]
@@ -978,7 +988,7 @@ prettyEnv env t = prettyEnv' env t False
978988 prettySe p env (P nt n t) debug =
979989 pretty n <+>
980990 if debug then
981− lbrack <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbrack
991+ lbracket <+> pretty nt <+> colon <+> prettySe 10 env t debug <+> rbracket
982992 else
983993 empty
984994 prettySe p env (V i) debug
@@ -986,7 +996,7 @@ prettyEnv env t = prettyEnv' env t False
986996 if debug then
987997 text . show . fst $ env!!i
988998 else
989− lbrack <+> text (show i) <+> rbrack
999+ lbracket <+> text (show i) <+> rbracket
9901000 | otherwise = text "unbound" <+> text (show i) <+> text "!"
9911001 prettySe p env (Bind n b@(Pi t) sc) debug
9921002 | noOccurrence n sc && not debug =
src/Idris/Prover.hs+11−11
@@ -89,13 +89,13 @@ elabStep st e = do case runStateT e st of
8989
9090dumpState :: IState -> ProofState -> Idris ()
9191dumpState ist (PS nm [] _ _ tm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =
92− iputGoal . render $ pretty nm <> colon <+> text "No more goals."
92+ iputGoal . renderPretty 0.7 breakingSize $ pretty nm <> colon <+> text "No more goals."
9393dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = do
9494 let OK ty = goalAtFocus ps
9595 let OK env = envAtFocus ps
96− iputGoal . render $
97− prettyOtherGoals hs $$
98− prettyAssumptions env $$
96+ iputGoal . renderPretty 0.7 breakingSize $
97+ prettyOtherGoals hs <> line <>
98+ prettyAssumptions env <> line <>
9999 prettyGoal ty
100100 where
101101 -- XXX
@@ -106,30 +106,30 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d
106106 | r == txt "rewrite_rule" = prettyPs bs
107107 prettyPs ((n, Let t v) : bs) =
108108 nest nestingSize (pretty n <+> text "=" <+> tPretty v <> colon <+>
109− tPretty t $$ prettyPs bs)
109+ tPretty t <> line <> prettyPs bs)
110110 prettyPs ((n, b) : bs) =
111− pretty n <+> colon <+> tPretty (binderTy b) $$ prettyPs bs
111+ line <> pretty n <+> colon <+> tPretty (binderTy b) <> prettyPs bs
112112
113113 prettyG (Guess t v) = tPretty t <+> text "=?=" <+> tPretty v
114114 prettyG b = tPretty $ binderTy b
115115
116116 prettyGoal ty =
117− text "---------- Goal: ----------" $$
118− pretty h <> colon $$ nest nestingSize (prettyG ty)
117+ text "---------- Goal: ----------" <$$>
118+ pretty h <+> colon <+> nest nestingSize (prettyG ty)
119119
120120 prettyAssumptions env =
121121 if length env == 0 then
122122 empty
123123 else
124− text "---------- Assumptions: ----------" $$
124+ text "---------- Assumptions: ----------" <>
125125 nest nestingSize (prettyPs $ reverse env)
126126
127127 prettyOtherGoals hs =
128128 if length hs == 0 then
129129 empty
130130 else
131− text "---------- Other goals: ----------" $$
132− pretty hs
131+ text "---------- Other goals: ----------" <$$>
132+ nest nestingSize (align . cat . punctuate (text ",") . map pretty $ hs)
133133
134134lifte :: ElabState [PDecl] -> ElabD a -> Idris a
135135lifte st e = do (v, _) <- elabStep st e
src/Util/Pretty.hs+6−9
@@ -1,10 +1,12 @@
11module Util.Pretty (
2− module Text.PrettyPrint.HughesPJ,
2+ --module Text.PrettyPrint.HughesPJ,
3+ module Text.PrettyPrint.Annotated.Leijen,
34 Sized(..), breakingSize, nestingSize,
45 Pretty(..)
56) where
67
7−import Text.PrettyPrint.HughesPJ
8+--import Text.PrettyPrint.HughesPJ
9+import Text.PrettyPrint.Annotated.Leijen
810
911-- A rough notion of size for pretty printing various types.
1012class Sized a where
@@ -23,11 +25,6 @@ breakingSize = 15
2325nestingSize :: Int
2426nestingSize = 1
2527
26−class Pretty a where
27− pretty :: a -> Doc
28+class Pretty a ty where
29+ pretty :: a -> Doc ty
2830
29−instance Pretty () where
30− pretty () = text "()"
31−
32−instance Pretty a => Pretty [a] where
33− pretty l = foldr ($$) empty $ map pretty l