13f3c29 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Basic functioning with new pretty-printer

13f3c29David Raymond Christiansen13 years ago

idris.cabal+2

compare with master

unifiedsplit

@@ -421,6 +421,7 @@ Library

421

422 Build-depends: base >=4 && <5

423 , Cabal

424+ , annotated-wl-pprint

424 , ansi-terminal

425 , ansi-terminal

425 , ansi-wl-pprint

426 , ansi-wl-pprint

426 , binary

427 , binary

@@ -450,6 +451,7 @@ Library

450 , zlib

451 , zlib

451 Extensions: MultiParamTypeClasses

452 Extensions: MultiParamTypeClasses

452 , FunctionalDependencies

453 , FunctionalDependencies

454+ , FlexibleContexts

453 , FlexibleInstances

455 , FlexibleInstances

454 , TemplateHaskell

456 , TemplateHaskell

455

457

src/Idris/AbsSyntax.hs+4−4

@@ -421,11 +421,11 @@ ideslavePutSExp cmd info = do i <- getIState

421 _ -> return ()

422

423-- this needs some typing magic and more structured output towards emacs

424−iputGoal :: String -> Idris ()

424+iputGoal :: SimpleDoc OutputAnnotation -> Idris ()

425−iputGoal s = do i <- getIState

425+iputGoal g = do i <- getIState

426 case idris_outputmode i of

427− RawOutput -> runIO $ putStrLn s

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

428− IdeSlave n -> runIO . putStrLn $ convSExp "write-goal" s n

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

429

430isetPrompt :: String -> Idris ()

431isetPrompt p = do i <- getIState

src/Idris/AbsSyntaxTree.hs+36−47

@@ -30,6 +30,8 @@ import Data.Word (Word)

31import Debug.Trace

33+import Text.PrettyPrint.Annotated.Leijen

34+

33data IOption = IOption { opt_logLevel :: Int,

35data IOption = IOption { opt_logLevel :: Int,

34 opt_typecase :: Bool,

36 opt_typecase :: Bool,

35 opt_typeintype :: Bool,

37 opt_typeintype :: Bool,

@@ -895,7 +897,7 @@ expandNS syn n = case syn_namespace syn of

895instance Show PTerm where

897instance Show PTerm where

896 show tm = showImp Nothing False False tm

898 show tm = showImp Nothing False False tm

897

899

898−instance Pretty PTerm where

900+instance Pretty PTerm OutputAnnotation where

899 pretty = prettyImp False

901 pretty = prettyImp False

900

902

901instance Show PDecl where

903instance Show PDecl where

@@ -965,15 +967,17 @@ getConsts (_ : xs) = getConsts xs

965getAll :: [PArg] -> [PTerm]

967getAll :: [PArg] -> [PTerm]

966getAll = map getTm

968getAll = map getTm

967

969

970+

968-- | Pretty-print a high-level Idris term

971-- | Pretty-print a high-level Idris term

969prettyImp :: Bool -- ^^ whether to show implicits

972prettyImp :: Bool -- ^^ whether to show implicits

970 -> PTerm -- ^^ the term to pretty-print

973 -> PTerm -- ^^ the term to pretty-print

971− -> Doc

974+ -> Doc OutputAnnotation

972prettyImp impl = prettySe 10

975prettyImp impl = prettySe 10

973 where

976 where

977+ prettySe :: Int -> PTerm -> Doc OutputAnnotation

974 prettySe p (PQuote r) =

978 prettySe p (PQuote r) =

975 if size r > breakingSize then

979 if size r > breakingSize then

976− text "![" $$ pretty r <> text "]"

980+ text "![" <> line <> pretty r <> text "]"

977 else

981 else

978 text "![" <> pretty r <> text "]"

982 text "![" <> pretty r <> text "]"

979 prettySe p (PPatvar fc n) = pretty n

983 prettySe p (PPatvar fc n) = pretty n

@@ -990,37 +994,37 @@ prettyImp impl = prettySe 10

990 prettySe p (PLam n ty sc) =

994 prettySe p (PLam n ty sc) =

991 bracket p 2 $

995 bracket p 2 $

992 if size sc > breakingSize then

996 if size sc > breakingSize then

993− text "λ" <> pretty n <+> text "=>" $+$ pretty sc

997+ text "λ" <> pretty n <+> text "=>" <> line <> pretty sc

994 else

998 else

995 text "λ" <> pretty n <+> text "=>" <+> pretty sc

999 text "λ" <> pretty n <+> text "=>" <+> pretty sc

996 prettySe p (PLet n ty v sc) =

1000 prettySe p (PLet n ty v sc) =

997 bracket p 2 $

1001 bracket p 2 $

998 if size sc > breakingSize then

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

1000 nest nestingSize (prettySe 10 sc)

1004 nest nestingSize (prettySe 10 sc)

1001 else

1005 else

1002 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

1006 text "let" <+> pretty n <+> text "=" <+> prettySe 10 v <+> text "in" <+>

1003 prettySe 10 sc

1007 prettySe 10 sc

1004 prettySe p (PPi (Exp l s _ _) n ty sc)

1008 prettySe p (PPi (Exp l s _ _) n ty sc)

1005 | n `elem` allNamesIn sc || impl =

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

1007 bracket p 2 $

1011 bracket p 2 $

1008 if size sc > breakingSize then

1012 if size sc > breakingSize then

1009− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1013+ enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>

1010− st <+> text "->" $+$ prettySe 10 sc

1014+ st <> text "->" <> line <> prettySe 10 sc

1011 else

1015 else

1012− open <> pretty n <+> colon <+> prettySe 10 ty <> rparen <+>

1016+ enclose open rparen (pretty n <+> colon <+> prettySe 10 ty) <+>

1013− st <+> text "->" <+> prettySe 10 sc

1017+ st <> text "->" <+> prettySe 10 sc

1014 | otherwise =

1018 | otherwise =

1015 bracket p 2 $

1019 bracket p 2 $

1016 if size sc > breakingSize then

1020 if size sc > breakingSize then

1017− prettySe 0 ty <+> st <+> text "->" $+$ prettySe 10 sc

1021+ prettySe 0 ty <+> st <+> text "->" <> line <> prettySe 10 sc

1018 else

1022 else

1019 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc

1023 prettySe 0 ty <+> st <+> text "->" <+> prettySe 10 sc

1020 where

1024 where

1021 st =

1025 st =

1022 case s of

1026 case s of

1023− Static -> text "[static]"

1027+ Static -> text "[static]" <> space

1024 _ -> empty

1028 _ -> empty

1025 prettySe p (PPi (Imp l s _ _) n ty sc)

1029 prettySe p (PPi (Imp l s _ _) n ty sc)

1026 | impl =

1030 | impl =

@@ -1028,27 +1032,27 @@ prettyImp impl = prettySe 10

1028 bracket p 2 $

1032 bracket p 2 $

1029 if size sc > breakingSize then

1033 if size sc > breakingSize then

1030 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1034 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1031− st <+> text "->" <+> prettySe 10 sc

1035+ st <> text "->" <+> prettySe 10 sc

1032 else

1036 else

1033 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1037 open <> pretty n <+> colon <+> prettySe 10 ty <> rbrace <+>

1034− st <+> text "->" <+> prettySe 10 sc

1038+ st <> text "->" <+> prettySe 10 sc

1035 | otherwise = prettySe 10 sc

1039 | otherwise = prettySe 10 sc

1036 where

1040 where

1037 st =

1041 st =

1038 case s of

1042 case s of

1039− Static -> text $ "[static]"

1043+ Static -> text "[static]" <> space

1040 _ -> empty

1044 _ -> empty

1041 prettySe p (PPi (Constraint _ _ _) n ty sc) =

1045 prettySe p (PPi (Constraint _ _ _) n ty sc) =

1042 bracket p 2 $

1046 bracket p 2 $

1043 if size sc > breakingSize then

1047 if size sc > breakingSize then

1044 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

1048 prettySe 10 ty <+> text "=>" <+> prettySe 10 sc

1045 else

1049 else

1046− prettySe 10 ty <+> text "=>" $+$ prettySe 10 sc

1050+ prettySe 10 ty <+> text "=>" <> line <> prettySe 10 sc

1047 prettySe p (PPi (TacImp _ _ s _) n ty sc) =

1051 prettySe p (PPi (TacImp _ _ s _) n ty sc) =

1048 bracket p 2 $

1052 bracket p 2 $

1049 if size sc > breakingSize then

1053 if size sc > breakingSize then

1050 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1054 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1051− rbrace <+> text "->" $+$ prettySe 10 sc

1055+ rbrace <+> text "->" <> line <> prettySe 10 sc

1052 else

1056 else

1053 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1057 lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 ty <>

1054 rbrace <+> text "->" <+> prettySe 10 sc

1058 rbrace <+> text "->" <+> prettySe 10 sc

@@ -1062,37 +1066,22 @@ prettyImp impl = prettySe 10

1062 let [l, r] = getExps args in

1066 let [l, r] = getExps args in

1063 bracket p 1 $

1067 bracket p 1 $

1064 if size r > breakingSize then

1068 if size r > breakingSize then

1065− prettySe 1 l <+> pretty op $+$ prettySe 0 r

1069+ prettySe 1 l <+> pretty op <> line <> prettySe 0 r

1066 else

1070 else

1067 prettySe 1 l <+> pretty op <+> prettySe 0 r

1071 prettySe 1 l <+> pretty op <+> prettySe 0 r

1068 prettySe p (PApp _ f as) =

1072 prettySe p (PApp _ f as) =

1069 let args = getExps as in

1073 let args = getExps as in

1070 bracket p 1 $

1074 bracket p 1 $

1071 prettySe 1 f <+>

1075 prettySe 1 f <+>

1072− if impl then

1076+ align (hsep (if impl

1073− foldl' fS empty as

1074− -- foldr (<+>) empty $ map prettyArgS as

1077+ then map prettyArgS as

1075− else

1076− foldl' fSe empty args

1077− -- foldr (<+>) empty $ map prettyArgSe args

1078+ else 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

1090 prettySe p (PCase _ scr opts) =

1079 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

1092 where

1081 where

1093− prettyBody = foldr ($$) empty $ intersperse (text "|") $ map sc opts

1082+ prettyBody = foldr (<>) empty $ intersperse (text "|") $ map sc opts

1094

1083

1095− sc (l, r) = prettySe 10 l <+> text "=>" <+> prettySe 10 r

1084+ sc (l, r) = nest nestingSize $ prettySe 10 l <+> text "=>" <+> prettySe 10 r

1096 prettySe p (PHidden tm) = text "." <> prettySe 0 tm

1085 prettySe p (PHidden tm) = text "." <> prettySe 0 tm

1097 prettySe p (PRefl _ _) = text "refl"

1086 prettySe p (PRefl _ _) = text "refl"

1098 prettySe p (PResolveTC _) = text "resolvetc"

1087 prettySe p (PResolveTC _) = text "resolvetc"

@@ -1101,27 +1090,27 @@ prettyImp impl = prettySe 10

1101 prettySe p (PEq _ l r) =

1090 prettySe p (PEq _ l r) =

1102 bracket p 2 $

1091 bracket p 2 $

1103 if size r > breakingSize then

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

1105 else

1094 else

1106 prettySe 10 l <+> text "=" <+> prettySe 10 r

1095 prettySe 10 l <+> text "=" <+> prettySe 10 r

1107 prettySe p (PRewrite _ l r _) =

1096 prettySe p (PRewrite _ l r _) =

1108 bracket p 2 $

1097 bracket p 2 $

1109 if size r > breakingSize then

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

1111 else

1100 else

1112 text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r

1101 text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r

1113 prettySe p (PTyped l r) =

1102 prettySe p (PTyped l r) =

1114 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen

1103 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen

1115 prettySe p (PPair _ l r) =

1104 prettySe p (PPair _ l r) =

1116 if size r > breakingSize then

1105 if size r > breakingSize then

1117− lparen <> prettySe 10 l <> text "," $+$

1106+ lparen <> prettySe 10 l <> text "," <>

1118− prettySe 10 r <> rparen

1107+ line <> prettySe 10 r <> rparen

1119 else

1108 else

1120 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen

1109 lparen <> prettySe 10 l <> text "," <+> prettySe 10 r <> rparen

1121 prettySe p (PDPair _ l t r) =

1110 prettySe p (PDPair _ l t r) =

1122 if size r > breakingSize then

1111 if size r > breakingSize then

1123− lparen <> prettySe 10 l <+> text "**" $+$

1112+ lparen <> prettySe 10 l <+> text "**" <>

1124− prettySe 10 r <> rparen

1113+ line <> prettySe 10 r <> rparen

1125 else

1114 else

1126 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen

1115 lparen <> prettySe 10 l <+> text "**" <+> prettySe 10 r <> rparen

1127 prettySe p (PAlternative a as) =

1116 prettySe p (PAlternative a as) =

@@ -1133,9 +1122,9 @@ prettyImp impl = prettySe 10

1133 prettySe p (PConstant c) = pretty c

1122 prettySe p (PConstant c) = pretty c

1134 -- XXX: add pretty for tactics

1123 -- XXX: add pretty for tactics

1135 prettySe p (PProof ts) =

1124 prettySe p (PProof ts) =

1136− text "proof" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1125+ text "proof" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1137 prettySe p (PTactics ts) =

1126 prettySe p (PTactics ts) =

1138− text "tactics" <+> lbrace $+$ nest nestingSize (text . show $ ts) $+$ rbrace

1127+ text "tactics" <+> lbrace <> nest nestingSize (text . show $ ts) <> rbrace

1139 prettySe p (PMetavar n) = text "?" <> pretty n

1128 prettySe p (PMetavar n) = text "?" <> pretty n

1140 prettySe p (PReturn f) = text "return"

1129 prettySe p (PReturn f) = text "return"

1141 prettySe p PImpossible = text "impossible"

1130 prettySe p PImpossible = text "impossible"

src/Idris/Core/Elaborate.hs+1−1

@@ -24,7 +24,7 @@ import Data.Char

24import Data.List

25import Debug.Trace

27−import Util.Pretty

27+import Util.Pretty hiding (fill)

29-- I don't really want this here, but it's useful for the test shell

30data Command = Theorem Name Raw

src/Idris/Core/ProofState.hs+12−12

@@ -18,7 +18,7 @@ import Control.Applicative hiding (empty)

18import Data.List

19import Debug.Trace

21−import Util.Pretty

21+import Util.Pretty hiding (fill)

23data ProofState = PS { thname :: Name,

24 holes :: [Name], -- holes still to be solved

@@ -113,23 +113,23 @@ instance Show ProofState where

113 " =?= " ++ showEnv ps v

114 showG ps b = showEnv ps (binderTy b)

115

116−instance Pretty ProofState where

116+instance Pretty ProofState OutputAnnotation where

117 pretty (PS nm [] _ _ trm _ _ _ _ _ _ _ _ _ _ _ _ _ _) =

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

120 else

121− pretty nm <> colon <+> text " no more goals."

121+ pretty nm <+> colon <+> text " no more goals."

122 pretty p@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ _ i _ _ ctxt _ _ _) =

123 let OK g = goal (Just h) tm in

124 let wkEnv = premises g in

125− text "Other goals" <+> colon <+> pretty hs $$

125+ text "Other goals" <+> colon <+> pretty hs <+>

126− prettyPs wkEnv (reverse wkEnv) $$

126+ prettyPs wkEnv (reverse wkEnv) <+>

127− text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" $$

127+ text "---------- " <+> text "Focussing on" <> colon <+> pretty nm <+> text " ----------" <+>

128 pretty h <+> colon <+> prettyGoal wkEnv (goalType g)

129 where

130 prettyGoal ps (Guess t v) =

131 if size v > breakingSize then

132− prettyEnv ps t <+> text "=?=" $$

132+ prettyEnv ps t <+> text "=?=" <+>

133 nest nestingSize (prettyEnv ps v)

134 else

135 prettyEnv ps t <+> text "=?=" <+> prettyEnv ps v

@@ -139,17 +139,17 @@ instance Pretty ProofState where

139 prettyPs env ((n, Let t v):bs) =

140 nest nestingSize (pretty n <+> colon <+>

141 if size v > breakingSize then

142− prettyEnv env t <+> text "=" $$

142+ prettyEnv env t <+> text "=" <+>

143− nest nestingSize (prettyEnv env v) $$

143+ nest nestingSize (prettyEnv env v) <+>

144 nest nestingSize (prettyPs env bs)

145 else

146− prettyEnv env t <+> text "=" <+> prettyEnv env v $$

146+ prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

147 nest nestingSize (prettyPs env bs))

148 prettyPs env ((n, b):bs) =

149 if size (binderTy b) > breakingSize then

150 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+> prettyPs env bs)

151 else

152− nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) $$

152+ nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

153 nest nestingSize (prettyPs env bs))

154

155same Nothing n = True

src/Idris/Core/TT.hs+29−19

@@ -77,6 +77,12 @@ instance Sized FC where

77instance Show FC where

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

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

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

82+

83+-- | Output annotations for pretty-printing

84+data OutputAnnotation = OutName Name (Maybe NameOutput) (Maybe Type)

85+

80-- | Used for error reflection

86-- | Used for error reflection

81data ErrorReportPart = TextPart String

87data ErrorReportPart = TextPart String

82 | NamePart Name

88 | NamePart Name

@@ -170,15 +176,15 @@ instance Show Err where

170 show (At f e) = show f ++ ":" ++ show e

176 show (At f e) = show f ++ ":" ++ show e

171 show _ = "Error"

177 show _ = "Error"

172

178

173−instance Pretty Err where

179+instance Pretty Err OutputAnnotation where

174 pretty (Msg m) = text m

180 pretty (Msg m) = text m

175 pretty (CantUnify _ l r e _ i) =

181 pretty (CantUnify _ l r e _ i) =

176 if size l + size r > breakingSize then

182 if size l + size r > breakingSize then

177− text "Cannot unify" <+> colon $$

183+ text "Cannot unify" <+> colon <+>

178− nest nestingSize (pretty l <+> text "and" <+> pretty r) $$

184+ nest nestingSize (pretty l <+> text "and" <+> pretty r) <+>

179 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

185 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

180 else

186 else

181− text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r $$

187+ text "Cannot unify" <+> colon <+> pretty l <+> text "and" <+> pretty r <+>

182 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

188 nest nestingSize (text "where" <+> pretty e <+> text "with" <+> (text . show $ i))

183 pretty (ProviderError msg) = text msg

189 pretty (ProviderError msg) = text msg

184 pretty err@(LoadingFailed _ _) = text (show err)

190 pretty err@(LoadingFailed _ _) = text (show err)

@@ -189,11 +195,11 @@ instance Error Err where

189

195

190type TC = TC' Err

196type TC = TC' Err

191

197

192−instance (Pretty a) => Pretty (TC a) where

198+instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

193 pretty (OK ok) = pretty ok

199 pretty (OK ok) = pretty ok

194 pretty (Error err) =

200 pretty (Error err) =

195 if size err > breakingSize then

201 if size err > breakingSize then

196− text "Error" <+> colon $$ (nest nestingSize $ pretty err)

202+ text "Error" <+> colon <+> (nest nestingSize $ pretty err)

197 else

203 else

198 text "Error" <+> colon <+> pretty err

204 text "Error" <+> colon <+> pretty err

199

205

@@ -287,11 +293,15 @@ instance Sized Name where

287 size (MN i n) = 1

293 size (MN i n) = 1

288 size _ = 1

294 size _ = 1

289

295

290−instance Pretty Name where

296+instance Pretty Name OutputAnnotation where

291− pretty (UN n) = text (T.unpack n)

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

292− pretty (NS n s) = pretty 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) $

293− pretty (MN i s) = lbrace <+> text (T.unpack s) <+> (text . show $ i) <+> rbrace

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

294− pretty (SN s) = text (show s)

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

295

305

296instance Show Name where

306instance Show Name where

297 show (UN n) = str n

307 show (UN n) = str n

@@ -408,7 +418,7 @@ addAlist ((n, tm) : ds) ctxt = addDef n tm (addAlist ds ctxt)

408data NativeTy = IT8 | IT16 | IT32 | IT64

418data NativeTy = IT8 | IT16 | IT32 | IT64

409 deriving (Show, Eq, Ord, Enum)

419 deriving (Show, Eq, Ord, Enum)

410

420

411−instance Pretty NativeTy where

421+instance Pretty NativeTy OutputAnnotation where

412 pretty IT8 = text "Bits8"

422 pretty IT8 = text "Bits8"

413 pretty IT16 = text "Bits16"

423 pretty IT16 = text "Bits16"

414 pretty IT32 = text "Bits32"

424 pretty IT32 = text "Bits32"

@@ -426,7 +436,7 @@ deriving instance NFData NativeTy

426deriving instance NFData ArithTy

436deriving instance NFData ArithTy

427!-}

437!-}

428

438

429−instance Pretty ArithTy where

439+instance Pretty ArithTy OutputAnnotation where

430 pretty (ATInt ITNative) = text "Int"

440 pretty (ATInt ITNative) = text "Int"

431 pretty (ATInt ITBig) = text "BigInt"

441 pretty (ATInt ITBig) = text "BigInt"

432 pretty (ATInt ITChar) = text "Char"

442 pretty (ATInt ITChar) = text "Char"

@@ -462,7 +472,7 @@ deriving instance NFData Const

462instance Sized Const where

472instance Sized Const where

463 size _ = 1

473 size _ = 1

464

474

465−instance Pretty Const where

475+instance Pretty Const OutputAnnotation where

466 pretty (I i) = text . show $ i

476 pretty (I i) = text . show $ i

467 pretty (BI i) = text . show $ i

477 pretty (BI i) = text . show $ i

468 pretty (Fl f) = text . show $ f

478 pretty (Fl f) = text . show $ f

@@ -494,7 +504,7 @@ instance Sized Raw where

494 size (RForce raw) = 1 + size raw

504 size (RForce raw) = 1 + size raw

495 size (RConstant const) = size const

505 size (RConstant const) = size const

496

506

497−instance Pretty Raw where

507+instance Pretty Raw OutputAnnotation where

498 pretty = text . show

508 pretty = text . show

499

509

500{-!

510{-!

@@ -604,7 +614,7 @@ deriving instance NFData NameType

604instance Sized NameType where

614instance Sized NameType where

605 size _ = 1

615 size _ = 1

606

616

607−instance Pretty NameType where

617+instance Pretty NameType OutputAnnotation where

608 pretty = text . show

618 pretty = text . show

609

619

610instance Eq NameType where

620instance Eq NameType where

@@ -662,7 +672,7 @@ instance Sized a => Sized (TT a) where

662 size Erased = 1

672 size Erased = 1

663 size (TType u) = 1 + size u

673 size (TType u) = 1 + size u

664

674

665−instance Pretty a => Pretty (TT a) where

675+instance Pretty a o => Pretty (TT a) o where

666 pretty _ = text "test"

676 pretty _ = text "test"

667

677

668type EnvTT n = [(n, Binder (TT n))]

678type EnvTT n = [(n, Binder (TT n))]

@@ -978,7 +988,7 @@ prettyEnv env t = prettyEnv' env t False

978 prettySe p env (P nt n t) debug =

988 prettySe p env (P nt n t) debug =

979 pretty n <+>

989 pretty n <+>

980 if debug then

990 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

982 else

992 else

983 empty

993 empty

984 prettySe p env (V i) debug

994 prettySe p env (V i) debug

@@ -986,7 +996,7 @@ prettyEnv env t = prettyEnv' env t False

986 if debug then

996 if debug then

987 text . show . fst $ env!!i

997 text . show . fst $ env!!i

988 else

998 else

989− lbrack <+> text (show i) <+> rbrack

999+ lbracket <+> text (show i) <+> rbracket

990 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1000 | otherwise = text "unbound" <+> text (show i) <+> text "!"

991 prettySe p env (Bind n b@(Pi t) sc) debug

1001 prettySe p env (Bind n b@(Pi t) sc) debug

992 | noOccurrence n sc && not debug =

1002 | noOccurrence n sc && not debug =

src/Idris/Prover.hs+11−11

@@ -89,13 +89,13 @@ elabStep st e = do case runStateT e st of

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

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

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

94 let OK ty = goalAtFocus ps

95 let OK env = envAtFocus ps

96− iputGoal . render $

96+ iputGoal . renderPretty 0.7 breakingSize $

97− prettyOtherGoals hs $$

97+ prettyOtherGoals hs <> line <>

98− prettyAssumptions env $$

98+ prettyAssumptions env <> line <>

99 prettyGoal ty

100 where

101 -- XXX

@@ -106,30 +106,30 @@ dumpState ist ps@(PS nm (h:hs) _ _ tm _ _ _ _ _ _ problems i _ _ ctxy _ _ _) = d

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

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

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

109− tPretty t $$ prettyPs bs)

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

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

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

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

112

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

114 prettyG b = tPretty $ binderTy b

115

116 prettyGoal ty =

117− text "---------- Goal: ----------" $$

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

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

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

119

120 prettyAssumptions env =

121 if length env == 0 then

122 empty

123 else

124− text "---------- Assumptions: ----------" $$

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

125 nest nestingSize (prettyPs $ reverse env)

126

127 prettyOtherGoals hs =

128 if length hs == 0 then

129 empty

130 else

131− text "---------- Other goals: ----------" $$

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

132− pretty hs

132+ nest nestingSize (align . cat . punctuate (text ",") . map pretty $ hs)

133

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

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

src/Util/Pretty.hs+6−9

@@ -1,10 +1,12 @@

1module Util.Pretty (

2− module Text.PrettyPrint.HughesPJ,

2+ --module Text.PrettyPrint.HughesPJ,

3+ module Text.PrettyPrint.Annotated.Leijen,

3 Sized(..), breakingSize, nestingSize,

4 Sized(..), breakingSize, nestingSize,

4 Pretty(..)

5 Pretty(..)

5) where

6) where

7−import Text.PrettyPrint.HughesPJ

8+--import Text.PrettyPrint.HughesPJ

9+import Text.PrettyPrint.Annotated.Leijen

9-- A rough notion of size for pretty printing various types.

11-- A rough notion of size for pretty printing various types.

10class Sized a where

12class Sized a where

@@ -23,11 +25,6 @@ breakingSize = 15

23nestingSize :: Int

25nestingSize :: Int

24nestingSize = 1

26nestingSize = 1

26−class Pretty a where

28+class Pretty a ty where

27− pretty :: a -> Doc

29+ pretty :: a -> Doc ty

29−instance Pretty () where

30− pretty () = text "()"

31−

32−instance Pretty a => Pretty [a] where

33− pretty l = foldr ($$) empty $ map pretty l