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

git.iko.soy/Idris-dev

Use the pprint library to insert line breaks

The "Sized" class is not deleted because it is useful in other contexts, such as eliding parts of error messages. The "show" instances assume an absurdly wide monitor so as to not break interactive editing.

commit41d3dafce46948c71ead29f08e5292a3a7fbebe4 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateFri 31 Jan 2014, 21:00 (13 years ago) parentda24632

4 files changed+48−112

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+39−76 src/Idris/Core/ProofState.hs+6−21 src/Idris/Core/TT.hs+2−10 src/Util/Pretty.hs+1−5

src/Idris/AbsSyntaxTree.hs+39−76

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

2222import Control.Monad.Trans.State.Strict

2323import Control.Monad.Trans.Error

2424

25−import Data.List

25+import Data.List hiding (group)

2626import Data.Char

2727import qualified Data.Map as M

2828import qualified Data.Text as T

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

696696deriving instance Binary PTactic'

697697deriving instance NFData PTactic'

698698!-}

699−

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

701700 size (Intro nms) = 1 + size nms

702701 size Intros = 1

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

10151014

10161015-- Pretty-printing declarations and terms

10171016

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

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

1019+

10181020instance Show PTerm where

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

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

10201022

10211023instance Show PDecl where

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

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

10231025

10241026instance Show PClause where

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

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

10261028

10271029instance Show PData where

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

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

10291031

10301032instance Pretty PTerm OutputAnnotation where

10311033 pretty = prettyImp False

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

10651067 where

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

10671069 prettySe p bnd (PQuote r) =

1068− if size r > breakingSize then

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

1070− else

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

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

10731072 prettySe p bnd e

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

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

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

10771076 prettySe p bnd (PLam n ty sc) =

1078− bracket p 2 $

1079− if size sc > breakingSize then

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

1077+ bracket p 2 . group . hang 2 $

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

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

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

10841081 bracket p 2 $

1085− if size sc > breakingSize then

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

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

1088− else

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

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

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

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

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

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

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

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

1094− bracket p 2 $

1095− if size sc > breakingSize then

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

1088+ bracket p 2 . group $

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

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

11011091 | otherwise =

1102− bracket p 2 $

1103− if size sc > breakingSize then

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

1105− else

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

1092+ bracket p 2 . group $

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

11071094 where

11081095 st =

11091096 case s of

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

11131100 | impl =

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

11151102 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 <+>

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

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

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

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

11231106 where

11241107 st =

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

11271110 _ -> empty

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

11291112 bracket p 2 $

1130− if size sc > breakingSize then

1131− 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

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

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

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

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

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

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

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

11431119 | not impl = prettyName impl bnd f

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

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

11481124 , not (tnull nm) &&

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

11501126 let [l, r] = getExps args in

1151− bracket p 1 $

1152− if size r > breakingSize then

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

1127+ bracket p 1 . align . group $

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

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

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

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

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

11601133 let args = getExps as

11611134 fp = prettySe 1 bnd f

11621135 in

1163− bracket p 1 $

1164− hsep (if impl

1165− then fp : map (prettyArgS bnd) as

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

1136+ bracket p 1 . group $

1137+ if impl

1138+ then if null as

1139+ then fp

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

1141+ else if null args

1142+ then fp

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

11671144 prettySe p bnd (PCase _ scr opts) =

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

11691146 where

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

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

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

11781155 prettySe p bnd (PEq _ l r) =

1179− bracket p 2 $

1180− if size r > breakingSize then

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

1182− else

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

1156+ bracket p 2 . align . group $

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

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

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

11861160 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

11911162 prettySe p bnd (PTyped l r) =

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

11931164 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

11991166 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

12051168 prettySe p bnd (PAlternative a as) =

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

12071170 where

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

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

115115

116116instance Pretty ProofState OutputAnnotation where

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

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

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

124121 let wkEnv = premises g in

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

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

129126 where

130127 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

136129 prettyGoal ps b = prettyEnv ps $ binderTy b

137130

138131 prettyPs env [] = empty

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

140133 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 <+>

147− nest nestingSize (prettyPs env bs))

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

135+ nest nestingSize (prettyPs env bs))

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

153− nest nestingSize (prettyPs env bs))

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

138+ nest nestingSize (prettyPs env bs))

154139

155140same Nothing n = True

156141same (Just x) n = x == n

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

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

191191instance Pretty Err OutputAnnotation where

192192 pretty (Msg m) = text m

193193 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

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

201196 pretty (ProviderError msg) = text msg

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

203198 pretty _ = text "Error"

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

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

211206 pretty (OK ok) = pretty ok

212207 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

217209

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

219211 show (OK x) = show x

src/Util/Pretty.hs+1−5

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

11module Util.Pretty (

22 module Text.PrettyPrint.Annotated.Leijen,

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

3+ Sized(..), nestingSize,

44 Pretty(..)

55) where

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

1717instance Sized a => Sized [a] where

1818 size = sum . map size

1919

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

21−breakingSize :: Int

22−breakingSize = 15

23−

2420nestingSize :: Int

2521nestingSize = 1

2622