41d3daf · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Use the pprint library to insert line breaks

41d3dafDavid Raymond Christiansen13 years ago

src/Idris/AbsSyntaxTree.hs+39−76

compare with master

unifiedsplit

@@ -22,7 +22,7 @@ import System.IO

22import Control.Monad.Trans.State.Strict

23import Control.Monad.Trans.Error

25−import Data.List

25+import Data.List hiding (group)

26import Data.Char

27import qualified Data.Map as M

28import qualified Data.Text as T

@@ -696,7 +696,6 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

696deriving instance Binary PTactic'

697deriving instance NFData PTactic'

698!-}

699−

700instance Sized a => Sized (PTactic' a) where

699instance Sized a => Sized (PTactic' a) where

701 size (Intro nms) = 1 + size nms

700 size (Intro nms) = 1 + size nms

702 size Intros = 1

701 size Intros = 1

@@ -1015,17 +1014,20 @@ piBindp p ((n, ty):ns) t = PPi p n ty (piBindp p ns t)

1015

1014

1016-- Pretty-printing declarations and terms

1015-- Pretty-printing declarations and terms

1017

1016

1017+-- These "show" instances render to an absurdly wide screen because inserted line breaks

1018+-- could interfere with interactive editing, which calls "show".

1019+

1018instance Show PTerm where

1020instance Show PTerm where

1019− showsPrec _ tm = (displayS . renderCompact . prettyImp False) tm

1021+ showsPrec _ tm = (displayS . renderPretty 1.0 10000000 . prettyImp False) tm

1020

1022

1021instance Show PDecl where

1023instance Show PDecl where

1022− showsPrec _ d = (displayS . renderCompact . showDeclImp False) d

1024+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDeclImp False) d

1023

1025

1024instance Show PClause where

1026instance Show PClause where

1025− showsPrec _ c = (displayS . renderCompact . showCImp True) c

1027+ showsPrec _ c = (displayS . renderPretty 1.0 10000000 . showCImp True) c

1026

1028

1027instance Show PData where

1029instance Show PData where

1028− showsPrec _ d = (displayS . renderCompact . showDImp False) d

1030+ showsPrec _ d = (displayS . renderPretty 1.0 10000000 . showDImp False) d

1029

1031

1030instance Pretty PTerm OutputAnnotation where

1032instance Pretty PTerm OutputAnnotation where

1031 pretty = prettyImp False

1033 pretty = prettyImp False

@@ -1065,9 +1067,6 @@ pprintPTerm impl bnd = prettySe 10 bnd

1065 where

1067 where

1066 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1068 prettySe :: Int -> [(Name, Bool)] -> PTerm -> Doc OutputAnnotation

1067 prettySe p bnd (PQuote r) =

1069 prettySe p bnd (PQuote r) =

1068− if size r > breakingSize then

1069− text "![" <> line <> pretty r <> text "]"

1070− else

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

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

1072 prettySe p bnd (PPatvar fc n) = pretty n

1071 prettySe p bnd (PPatvar fc n) = pretty n

1073 prettySe p bnd e

1072 prettySe p bnd e

@@ -1075,35 +1074,23 @@ pprintPTerm impl bnd = prettySe 10 bnd

1075 | Just n <- snat p e = annotate AnnConstData (text (show n))

1074 | Just n <- snat p e = annotate AnnConstData (text (show n))

1076 prettySe p bnd (PRef fc n) = prettyName impl bnd n

1075 prettySe p bnd (PRef fc n) = prettyName impl bnd n

1077 prettySe p bnd (PLam n ty sc) =

1076 prettySe p bnd (PLam n ty sc) =

1078− bracket p 2 $

1077+ bracket p 2 . group . hang 2 $

1079− if size sc > breakingSize then

1078+ text "\\" <> bindingOf n False <+> text "=>" <$>

1080− text "\\" <> bindingOf n False <+> text "=>" <> line <> prettySe 10 ((n, False):bnd) sc

1081− else

1082− text "\\" <> bindingOf n False <+> text "=>" <+> prettySe 10 ((n, False):bnd) sc

1079+ prettySe 10 ((n, False):bnd) sc

1083 prettySe p bnd (PLet n ty v sc) =

1080 prettySe p bnd (PLet n ty v sc) =

1084 bracket p 2 $

1081 bracket p 2 $

1085− if size sc > breakingSize then

1086− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <>

1082+ text "let" <+> bindingOf n False <+> text "=" </>

1087− nest nestingSize (prettySe 10 ((n, False):bnd) sc)

1088− else

1089− text "let" <+> bindingOf n False <+> text "=" <+> prettySe 10 bnd v <+> text "in" <+>

1083+ prettySe 10 bnd v <+> text "in" </>

1090− prettySe 10 ((n, False):bnd) sc

1084+ prettySe 10 ((n, False):bnd) sc

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

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

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

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

1093 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1087 let open = if Lazy `elem` l then text "|" <> lparen else lparen in

1094− bracket p 2 $

1088+ bracket p 2 . group $

1095− if size sc > breakingSize then

1089+ enclose open rparen (group . align $ bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1096− enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1097− st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1098− else

1099− enclose open rparen (bindingOf n False <+> colon <+> prettySe 10 bnd ty) <+>

1100− st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1090+ st <> text "->" <$> prettySe 10 ((n, False):bnd) sc

1101 | otherwise =

1091 | otherwise =

1102− bracket p 2 $

1092+ bracket p 2 . group $

1103− if size sc > breakingSize then

1104− prettySe 0 bnd ty <+> st <> text "->" <> line <> prettySe 10 ((n, False):bnd) sc

1093+ group (prettySe 0 bnd ty <+> st) <> text "->" <$> group (prettySe 10 ((n, False):bnd) sc)

1105− else

1106− prettySe 0 bnd ty <+> st <> text "->" <+> prettySe 10 ((n, False):bnd) sc

1107 where

1094 where

1108 st =

1095 st =

1109 case s of

1096 case s of

@@ -1113,12 +1100,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1113 | impl =

1100 | impl =

1114 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1101 let open = if Lazy `elem` l then text "|" <> lbrace else lbrace in

1115 bracket p 2 $

1102 bracket p 2 $

1116− if size sc > breakingSize then

1117− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1118− st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1119− else

1120− open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1103+ open <> bindingOf n True <+> colon <+> prettySe 10 bnd ty <> rbrace <+>

1121− st <> text "->" <+> prettySe 10 ((n, True):bnd) sc

1104+ st <> text "->" </> prettySe 10 ((n, True):bnd) sc

1122 | otherwise = prettySe 10 ((n, True):bnd) sc

1105 | otherwise = prettySe 10 ((n, True):bnd) sc

1123 where

1106 where

1124 st =

1107 st =

@@ -1127,18 +1110,11 @@ pprintPTerm impl bnd = prettySe 10 bnd

1127 _ -> empty

1110 _ -> empty

1128 prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1111 prettySe p bnd (PPi (Constraint _ _ _) n ty sc) =

1129 bracket p 2 $

1112 bracket p 2 $

1130− if size sc > breakingSize then

1131− prettySe 10 bnd ty <+> text "=>" <+> prettySe 10 ((n, True):bnd) sc

1113+ prettySe 10 bnd ty <+> text "=>" </> prettySe 10 ((n, True):bnd) sc

1132− else

1133− prettySe 10 bnd ty <+> text "=>" <> line <> prettySe 10 ((n, True):bnd) sc

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

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

1135 bracket p 2 $

1115 bracket p 2 $

1136− if size sc > breakingSize then

1137− lbrace <> text "tacimp" <+> bindingOf n True <+> colon <+> prettySe 10 bnd ty <>

1138− rbrace <+> text "->" <> line <> prettySe 10 ((n, True):bnd) sc

1139− else

1140− lbrace <> text "tacimp" <+> pretty n <+> colon <+> prettySe 10 bnd ty <>

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

1141− rbrace <+> text "->" <+> prettySe 10 ((n, True):bnd) sc

1117+ rbrace <+> text "->" </> prettySe 10 ((n, True):bnd) sc

1142 prettySe p bnd (PApp _ (PRef _ f) [])

1118 prettySe p bnd (PApp _ (PRef _ f) [])

1143 | not impl = prettyName impl bnd f

1119 | not impl = prettyName impl bnd f

1144 prettySe p bnd (PAppBind _ (PRef _ f) [])

1120 prettySe p bnd (PAppBind _ (PRef _ f) [])

@@ -1148,11 +1124,8 @@ pprintPTerm impl bnd = prettySe 10 bnd

1148 , not (tnull nm) &&

1124 , not (tnull nm) &&

1149 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1125 length (getExps args) == 2 && (not impl) && (not $ isAlpha (thead nm)) =

1150 let [l, r] = getExps args in

1126 let [l, r] = getExps args in

1151− bracket p 1 $

1127+ bracket p 1 . align . group $

1152− if size r > breakingSize then

1128+ (prettySe 1 bnd l <+> prettyName impl bnd op) <$> group (prettySe 0 bnd r)

1153− prettySe 1 bnd l <+> prettyName impl bnd op <> line <> prettySe 0 bnd r

1154− else

1155− prettySe 1 bnd l <+> prettyName impl bnd op <+> prettySe 0 bnd r

1156 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1129 prettySe p bnd (PApp _ hd@(PRef fc f) [tm])

1157 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1130 | PConstant (Idris.Core.TT.Str str) <- getTm tm,

1158 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

1131 f == sUN "Symbol_" = char '\'' <> prettySe 10 bnd (PRef fc (sUN str))

@@ -1160,10 +1133,14 @@ pprintPTerm impl bnd = prettySe 10 bnd

1160 let args = getExps as

1133 let args = getExps as

1161 fp = prettySe 1 bnd f

1134 fp = prettySe 1 bnd f

1162 in

1135 in

1163− bracket p 1 $

1136+ bracket p 1 . group $

1164− hsep (if impl

1137+ if impl

1138+ then if null as

1139+ then fp

1165− then fp : map (prettyArgS bnd) as

1140+ else fp <+> align (vsep (map (prettyArgS bnd) as))

1141+ else if null args

1142+ then fp

1166− else fp : map (prettyArgSe bnd) args)

1143+ else fp <+> align (vsep (map (prettyArgSe bnd) args))

1167 prettySe p bnd (PCase _ scr opts) =

1144 prettySe p bnd (PCase _ scr opts) =

1168 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1145 text "case" <+> prettySe 10 bnd scr <+> text "of" <> prettyBody

1169 where

1146 where

@@ -1176,32 +1153,18 @@ pprintPTerm impl bnd = prettySe 10 bnd

1176 prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1153 prettySe p bnd (PTrue _) = annotate (AnnName unitTy Nothing Nothing) $ text "()"

1177 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1154 prettySe p bnd (PFalse _) = annotate (AnnName falseTy Nothing Nothing) $ text "_|_"

1178 prettySe p bnd (PEq _ l r) =

1155 prettySe p bnd (PEq _ l r) =

1179− bracket p 2 $

1156+ bracket p 2 . align . group $

1180− if size r > breakingSize then

1181− prettySe 10 bnd l <+> eq <$> nest nestingSize (prettySe 10 bnd r)

1157+ prettySe 10 bnd l <+> eq <$> group (prettySe 10 bnd r)

1182− else

1183− prettySe 10 bnd l <+> eq <+> prettySe 10 bnd r

1184 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1158 where eq = annotate (AnnName eqTy Nothing Nothing) (text "=")

1185 prettySe p bnd (PRewrite _ l r _) =

1159 prettySe p bnd (PRewrite _ l r _) =

1186 bracket p 2 $

1160 bracket p 2 $

1187− if size r > breakingSize then

1188− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <> nest nestingSize (prettySe 10 bnd r)

1189− else

1190− text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1161+ text "rewrite" <+> prettySe 10 bnd l <+> text "in" <+> prettySe 10 bnd r

1191 prettySe p bnd (PTyped l r) =

1162 prettySe p bnd (PTyped l r) =

1192 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1163 lparen <> prettySe 10 bnd l <+> colon <+> prettySe 10 bnd r <> rparen

1193 prettySe p bnd (PPair _ l r) =

1164 prettySe p bnd (PPair _ l r) =

1194− if size r > breakingSize then

1195− lparen <> prettySe 10 bnd l <> text "," <>

1196− line <> prettySe 10 bnd r <> rparen

1197− else

1198− lparen <> prettySe 10 bnd l <> text "," <+> prettySe 10 bnd r <> rparen

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

1199 prettySe p bnd (PDPair _ l t r) =

1166 prettySe p bnd (PDPair _ l t r) =

1200− if size r > breakingSize then

1201− lparen <> prettySe 10 bnd l <+> text "**" <>

1202− line <> prettySe 10 bnd r <> rparen

1203− else

1204− lparen <> prettySe 10 bnd l <+> text "**" <+> prettySe 10 bnd r <> rparen

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

1205 prettySe p bnd (PAlternative a as) =

1168 prettySe p bnd (PAlternative a as) =

1206 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1169 lparen <> text "|" <> prettyAs <> text "|" <> rparen

1207 where

1170 where

src/Idris/Core/ProofState.hs+6−21

@@ -115,10 +115,7 @@ instance Show ProofState where

115

116instance 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.")

120− else

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

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

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

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

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

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

124 let wkEnv = premises g in

121 let wkEnv = premises g in

@@ -128,29 +125,17 @@ instance Pretty ProofState OutputAnnotation where

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

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

129 where

126 where

130 prettyGoal ps (Guess t v) =

127 prettyGoal ps (Guess t v) =

131− if size v > breakingSize then

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

133− nest nestingSize (prettyEnv ps v)

134− else

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

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

136 prettyGoal ps b = prettyEnv ps $ binderTy b

129 prettyGoal ps b = prettyEnv ps $ binderTy b

137

130

138 prettyPs env [] = empty

131 prettyPs env [] = empty

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

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

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

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

141− if size v > breakingSize then

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

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

144− nest nestingSize (prettyPs env bs)

145− else

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

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

147− nest nestingSize (prettyPs env bs))

135+ nest nestingSize (prettyPs env bs))

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

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

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

151− else

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

153− nest nestingSize (prettyPs env bs))

138+ nest nestingSize (prettyPs env bs))

154

139

155same Nothing n = True

140same Nothing n = True

156same (Just x) n = x == n

141same (Just x) n = x == n

src/Idris/Core/TT.hs+2−10

@@ -191,13 +191,8 @@ instance Show Err where

191instance Pretty Err OutputAnnotation where

192 pretty (Msg m) = text m

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

194− if size l + size r > breakingSize then

195− text "Cannot unify" <+> colon <+>

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

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

198− else

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

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

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

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

201 pretty (ProviderError msg) = text msg

196 pretty (ProviderError msg) = text msg

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

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

203 pretty _ = text "Error"

198 pretty _ = text "Error"

@@ -210,10 +205,7 @@ type TC = TC' Err

210instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

205instance (Pretty a OutputAnnotation) => Pretty (TC a) OutputAnnotation where

211 pretty (OK ok) = pretty ok

206 pretty (OK ok) = pretty ok

212 pretty (Error err) =

207 pretty (Error err) =

213− if size err > breakingSize then

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

215− else

216− text "Error" <+> colon <+> pretty err

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

217

209

218instance Show a => Show (TC a) where

210instance Show a => Show (TC a) where

219 show (OK x) = show x

211 show (OK x) = show x

src/Util/Pretty.hs+1−5

@@ -1,6 +1,6 @@

1module Util.Pretty (

2 module Text.PrettyPrint.Annotated.Leijen,

3− Sized(..), breakingSize, nestingSize,

3+ Sized(..), nestingSize,

4 Pretty(..)

5) where

@@ -17,10 +17,6 @@ instance (Sized a, Sized b) => Sized (a, b) where

17instance Sized a => Sized [a] where

18 size = sum . map size

20−-- The maximum size before we break on to another line.

21−breakingSize :: Int

22−breakingSize = 15

23−

24nestingSize :: Int

20nestingSize :: Int

25nestingSize = 1

21nestingSize = 1