0 | module Idris.Pretty

  2 | import Core.Metadata

  3 | import Data.String

  5 | import public Idris.Pretty.Annotations

  6 | import public Idris.Pretty.Render

  8 | import public Libraries.Text.PrettyPrint.Prettyprinter

  9 | import public Libraries.Text.PrettyPrint.Prettyprinter.Util

 11 | import Idris.REPL.Opts

 12 | import Idris.Syntax

 14 | %default covering

 16 | %hide Symbols.equals

 17 | %hide Symbols.semi

 20 | syntaxToDecoration : IdrisSyntax -> Maybe Decoration

 21 | syntaxToDecoration Hole     = Nothing

 22 | syntaxToDecoration (TCon {}) = pure Typ

 23 | syntaxToDecoration (DCon {}) = pure Data

 24 | syntaxToDecoration (Fun {})  = pure Function

 25 | syntaxToDecoration Bound    = pure Bound

 26 | syntaxToDecoration Keyword  = pure Keyword

 27 | syntaxToDecoration Pragma   = Nothing

 30 | kindAnn : KindedName -> Maybe IdrisSyntax

 31 | kindAnn (MkKindedName mcat fn nm) = do

 32 |     cat <- mcat

 33 |     pure $ case cat of

 34 |       Bound      => Bound

 35 |       Func       => Fun fn

 36 |       DataCon {} => DCon (Just fn)

 37 |       TyCon {}   => TCon (Just fn)

 40 | showCategory : (IdrisSyntax -> ann) -> GlobalDef -> Doc ann -> Doc ann

 41 | showCategory embed def = annotateM (embed <$> kindAnn (gDefKindedName def))

 43 | public export

 44 | data IdrisAnn

 45 |   = Warning

 46 |   | Error

 47 |   | ErrorDesc

 48 |   | FileCtxt

 49 |   | Code

 50 |   | Meta

 51 |   | Syntax IdrisSyntax

 52 |   | UserDocString

 55 | annToDecoration : IdrisAnn -> Maybe Decoration

 56 | annToDecoration (Syntax syn) = syntaxToDecoration syn

 57 | annToDecoration _ = Nothing

 60 | syntaxAnn : IdrisSyntax -> AnsiStyle

 61 | syntaxAnn Hole = color BrightGreen

 62 | syntaxAnn (TCon {}) = color BrightBlue

 63 | syntaxAnn (DCon {}) = color BrightRed

 64 | syntaxAnn (Fun {})  = color BrightGreen

 65 | syntaxAnn Bound    = italic

 66 | syntaxAnn Keyword  = color BrightWhite

 67 | syntaxAnn Pragma   = color BrightMagenta

 70 | colorAnn : IdrisAnn -> AnsiStyle

 71 | colorAnn Warning = color Yellow <+> bold

 72 | colorAnn Error = color BrightRed <+> bold

 73 | colorAnn ErrorDesc = bold

 74 | colorAnn FileCtxt = color BrightBlue

 75 | colorAnn Code = color Magenta

 76 | colorAnn Meta = color Green

 77 | colorAnn (Syntax syn) = syntaxAnn syn

 78 | colorAnn UserDocString = []

 81 | warning : Doc IdrisAnn -> Doc IdrisAnn

 82 | warning = annotate Warning

 85 | error : Doc IdrisAnn -> Doc IdrisAnn

 86 | error = annotate Error

 89 | errorDesc : Doc IdrisAnn -> Doc IdrisAnn

 90 | errorDesc = annotate ErrorDesc

 93 | fileCtxt : Doc IdrisAnn -> Doc IdrisAnn

 94 | fileCtxt = annotate FileCtxt

 97 | meta : Doc IdrisAnn -> Doc IdrisAnn

 98 | meta = annotate Meta

101 | code : Doc IdrisAnn -> Doc IdrisAnn

102 | code = annotate Code

104 | Pretty i a => Pretty i (WithFC a) where

105 |   pretty x = pretty x.val

109 |   prettyAlt : PClause' KindedName -> Doc IdrisSyntax

110 |   prettyAlt (MkPatClause _ lhs rhs _) =

111 |       space <+> pipe <++> pretty lhs <++> fatArrow <++> pretty rhs <+> semi

112 |   prettyAlt (MkWithClause _ lhs wps flags cs) =

113 |       space <+> pipe <++> angles (angles (reflow "with alts not possible")) <+> semi

114 |   prettyAlt (MkImpossible _ lhs) =

115 |       space <+> pipe <++> pretty lhs <++> impossible_ <+> semi

117 |   prettyPClause : PClause' KindedName -> Doc IdrisSyntax

118 |   prettyPClause (MkPatClause _ lhs rhs _) =

119 |       pretty lhs <++> fatArrow <++> pretty rhs

120 |   prettyPClause (MkWithClause _ lhs wps flags _) =

121 |       space <+> pipe <++> angles (angles (reflow "with alts not possible"))

122 |   prettyPClause (MkImpossible _ lhs) =

123 |       pretty lhs <++> impossible_

125 |   prettyPStr : PStr' KindedName -> Doc IdrisSyntax

126 |   prettyPStr (StrLiteral _ str) = pretty0 str

127 |   prettyPStr (StrInterp _ tm) = pretty tm

129 |   prettyPDo : PDo' KindedName -> Doc IdrisSyntax

130 |   prettyPDo (DoExp _ tm) = pretty tm

131 |   prettyPDo (DoBind _ _ n rig (Just ty) tm) =

132 |       prettyRig rig <+> pretty0 n <++> colon <++> pretty ty <++> keyword "<-" <++> pretty tm

133 |   prettyPDo (DoBind _ _ n rig Nothing tm) =

134 |       prettyRig rig <+> pretty0 n <++> keyword "<-" <++> pretty tm

135 |   prettyPDo (DoBindPat _ l (Just ty) tm alts) =

136 |       pretty l <++> colon <++> keyword "<-" <++> pretty tm <+> hang 4 (fillSep $ prettyAlt <$> alts)

137 |   prettyPDo (DoBindPat _ l Nothing tm alts) =

138 |       pretty l <++> keyword "<-" <++> pretty tm <+> hang 4 (fillSep $ prettyAlt <$> alts)

139 |   prettyPDo (DoLet _ _ l rig _ tm) =

140 |       let_ <++> prettyRig rig <+> pretty0 l <++> equals <++> pretty tm

141 |   prettyPDo (DoLetPat _ l _ tm alts) =

142 |       let_ <++> pretty l <++> equals <++> pretty tm <+> hang 4 (fillSep $ prettyAlt <$> alts)

143 |   prettyPDo (DoLetLocal _ ds) =

144 |       let_ <++> braces (angles (angles "definitions"))

145 |   prettyPDo (DoRewrite _ rule) = rewrite_ <+> pretty rule

147 |   export

148 |   prettyFieldPath : List String -> Doc IdrisSyntax

149 |   prettyFieldPath flds = concatWith (surround $ keyword "->") (pretty0 <$> flds)

151 |   prettyPFieldUpdate : PFieldUpdate' KindedName -> Doc IdrisSyntax

152 |   prettyPFieldUpdate (PSetField path v) =

153 |       prettyFieldPath path <++> equals <++> pretty v

154 |   prettyPFieldUpdate (PSetFieldApp path v) =

155 |       prettyFieldPath path <++> keyword "$=" <++> pretty v

157 |   prettyBinder : Name -> Doc IdrisSyntax

158 |   prettyBinder = annotate Bound . pretty0

160 |   startPrec : Prec

161 |   startPrec = Open

162 |   appPrec : Prec

163 |   appPrec = App

164 |   leftAppPrec : Prec

165 |   leftAppPrec = Open

167 |   prettyOp : KindedName -> Doc IdrisSyntax

168 |   prettyOp op@(MkKindedName _ _ nm) = if isOpName nm

169 |       then annotateM (kindAnn op) $ pretty0 nm

170 |       else Chara '`' <+> annotateM (kindAnn op) (pretty0 nm) <+> Chara '`'

172 |   Pretty IdrisSyntax (BasicMultiBinder' KindedName) where

173 |     pretty (MkBasicMultiBinder rig names type)

174 |       = prettyRig rig <++> commaSep (forget $ map (prettyBinder . val) names)

175 |       <++> colon <++> pretty type

177 |   Pretty IdrisSyntax (PBinder' KindedName) where

178 |     prettyPrec d (MkPBinder Implicit bind) =

179 |       lcurly <+> pretty bind <+> rcurly

180 |     prettyPrec d (MkPBinder Explicit bind) =

181 |       lparen <+> pretty bind <+> rparen

182 |     prettyPrec d (MkPBinder AutoImplicit bind)  =

183 |       lcurly <+> auto_ <++> pretty bind <+> rcurly

184 |     prettyPrec d (MkPBinder (DefImplicit x) bind)  =

185 |       lcurly <+> default_ <++> prettyPrec appPrec x <+> rcurly

187 |   export

188 |   Pretty IdrisSyntax IPTerm where

189 |     prettyPrec d (PRef _ nm) = annotateM (kindAnn nm) $ cast $ prettyOp False nm.rawName

190 |     prettyPrec d (NewPi (MkWithData fc (MkPBinderScope binder scope))) =

191 |       prettyPrec d binder <++> arrow <++> prettyPrec d scope

192 |     prettyPrec d (Forall (MkWithData fc (names, scope))) =

193 |       parenthesise (d > startPrec) $ group $

194 |         forall_ <++> commaSep (map (prettyBinder . val) (forget names)) <++> dot <++> pretty scope

195 |     prettyPrec d (PPi _ rig Explicit Nothing arg ret) =

196 |       parenthesise (d > startPrec) $ group $

197 |         branchVal

198 |           (pretty arg <++> arrow <++> pretty ret)

199 |           (parens (prettyRig rig <+> "_" <++> colon <++> pretty arg)

200 |                   <++> arrow <+> softline <+> pretty ret)

201 |           rig

202 |     prettyPrec d (PPi _ rig Explicit (Just n) arg ret) =

203 |       parenthesise (d > startPrec) $ group $

204 |         parens (prettyRig rig <+> prettyBinder n

205 |              <++> colon <++> pretty arg)

206 |              <++> arrow <+> softline <+> pretty ret

207 |     prettyPrec d (PPi _ rig Implicit Nothing arg ret) =

208 |       parenthesise (d > startPrec) $ group $

209 |         braces (prettyRig rig <+> pretty0 Underscore

210 |              <++> colon <++> pretty arg)

211 |              <++> arrow <+> softline <+> pretty ret

212 |     prettyPrec d (PPi _ rig Implicit (Just n) arg ret) =

213 |       parenthesise (d > startPrec) $ group $

214 |         braces (prettyRig rig <+> prettyBinder n

215 |              <++> colon <++> pretty arg)

216 |              <++> arrow <+> softline <+> pretty ret

217 |     prettyPrec d (PPi _ rig AutoImplicit Nothing arg ret) =

218 |       parenthesise (d > startPrec) $ group $

219 |         branchVal

220 |           (pretty arg <++> fatArrow <+> softline <+> pretty ret)

221 |           (braces (auto_ <++> prettyRig rig <+> "_"

222 |                 <++> colon <++> pretty arg)

223 |                 <++> arrow <+> softline <+> pretty ret)

224 |           rig

225 |     prettyPrec d (PPi _ rig AutoImplicit (Just n) arg ret) =

226 |       parenthesise (d > startPrec) $ group $

227 |         braces (auto_ <++> prettyRig rig <+> prettyBinder n

228 |              <++> colon <++> pretty arg)

229 |              <++> arrow <+> softline <+> pretty ret

230 |     prettyPrec d (PPi _ rig (DefImplicit t) Nothing arg ret) =

231 |       parenthesise (d > startPrec) $ group $

232 |         braces (default_ <++> prettyPrec appPrec t <++> prettyRig rig <+> "_"

233 |              <++> colon <++> pretty arg)

234 |              <++> arrow <+> softline <+> pretty ret

235 |     prettyPrec d (PPi _ rig (DefImplicit t) (Just n) arg ret) =

236 |       parenthesise (d > startPrec) $ group $

237 |         braces (default_ <++> prettyPrec appPrec t

238 |              <++> prettyRig rig <+> prettyBinder n

239 |              <++> colon <++> pretty arg)

240 |              <++> arrow <+> softline <+> pretty ret

241 |     prettyPrec d (PLam _ rig _ n ty sc) =

242 |       let (ns, sc) = getLamNames [(rig, n, ty)] sc in

243 |           parenthesise (d > startPrec) $ group $

244 |             backslash <+> prettyBindings ns <++> fatArrow <+> softline <+> pretty sc

245 |       where

246 |       getLamNames : List (RigCount, IPTerm, IPTerm) ->

247 |                     IPTerm ->

248 |                     (List (RigCount, IPTerm, IPTerm), IPTerm)

249 |       getLamNames acc (PLam _ rig _ n ty sc) = getLamNames ((rig, n, ty) :: acc) sc

250 |       getLamNames acc sc = (reverse acc, sc)

252 |       prettyBindings : List (RigCount, IPTerm, IPTerm) -> Doc IdrisSyntax

253 |       prettyBindings [] = neutral

254 |       prettyBindings [(rig, n, (PImplicit _))] = prettyRig rig <+> pretty n

255 |       prettyBindings [(rig, n, ty)] = prettyRig rig <+> pretty n <++> colon <++> pretty ty

256 |       prettyBindings ((rig, n, (PImplicit _)) :: ns) = prettyRig rig <+> pretty n

257 |                                               <+> comma <+> line <+> prettyBindings ns

258 |       prettyBindings ((rig, n, ty) :: ns) = prettyRig rig <+> pretty n <++> colon <++> pretty ty

259 |                                               <+> comma <+> line <+> prettyBindings ns

260 |     prettyPrec d (PLet _ rig n (PImplicit _) val sc alts) =

261 |       -- Hide uninformative lets

262 |       -- (Those that look like 'let x = x in ...')

263 |       -- Makes printing the types of names bound in where clauses a lot

264 |       -- more readable

265 |       fromMaybe fullLet $ do

266 |         nName   <- getPRefName n

267 |         valName <- getPRefName val

268 |         guard (show nName == show valName)

269 |         pure continuation

271 |      -- Hide lets that bind to underscore

272 |      -- That is, 'let _ = x in ...'

273 |      -- Those end up polluting the types of let bound variables in some

274 |      -- occasions

275 |       <|> do

276 |         nName <- getPRefName n

277 |         guard (isUnderscoreName nName)

278 |         pure continuation

280 |     where

282 |       continuation : Doc IdrisSyntax

283 |       continuation = pretty sc

285 |       fullLet : Doc IdrisSyntax

286 |       fullLet = parenthesise (d > startPrec) $ group $ align $

287 |         let_ <++> (group $ align $ hang 2 $ prettyRig rig <+> pretty n <++> equals <+> line <+> pretty val) <+> line

288 |           <+> in_ <++> (group $ align $ hang 2 $ continuation)

290 |       getPRefName : IPTerm -> Maybe Name

291 |       getPRefName (PRef _ n) = Just (rawName n)

292 |       getPRefName _ = Nothing

294 |     prettyPrec d (PLet _ rig n ty val sc alts) =

295 |       parenthesise (d > startPrec) $ group $ align $

296 |         let_ <++> (group $ align $ hang 2 $

297 |                       prettyRig rig <+> pretty n <++> colon <++> pretty ty

298 |                       <++> equals <+> line <+> pretty val)

299 |         <+> case alts of

300 |              { [] => in_ <+> softline

301 |              ; _ => hardline <+> indent 4 (vsep (prettyAlt <$> alts)) <+> hardline <+> in_

302 |              }

303 |         <+> group (align $ hang 2 $ pretty sc)

304 |     prettyPrec d (PCase _ _ tm cs) =

305 |       parenthesise (d > startPrec) $

306 |         case_ <++> pretty tm <++> of_ <+> nest 2 (

307 |         let punctuation = lcurly :: (semi <$ fromMaybe [] (tail' [1..length cs])) in

308 |         line <+> (vsep $ zipWith (<++>) punctuation (prettyPClause <$> cs) ++ [rcurly]))

309 |     prettyPrec d (PLocal _ ds sc) =

310 |       parenthesise (d > startPrec) $ group $ align $

311 |         let_ <++> braces (angles (angles "definitions")) <+> line <+> in_ <++> pretty sc

312 |     prettyPrec d (PUpdate _ fs) =

313 |       parenthesise (d > startPrec) $ group $

314 |         record_ <++> braces (vsep $ punctuate comma (prettyPFieldUpdate <$> fs))

315 |     prettyPrec d (PApp _ f a) =

316 |       let catchall : Lazy (Doc IdrisSyntax)

317 |            := prettyPrec leftAppPrec f <++> prettyPrec appPrec a

319 |       in parenthesise (d >= appPrec) $ group $ case f of

320 |         (PRef _ n) =>

321 |           if isJust (isRF $ rawName n)

322 |           then prettyPrec leftAppPrec a <++> prettyPrec appPrec f

323 |           else catchall

324 |         _ => catchall

325 |     prettyPrec d (PWithApp _ f a) = prettyPrec d f <++> pipe <++> prettyPrec d a

326 |     prettyPrec d (PDelayed _ LInf ty) = parenthesise (d > startPrec) $ "Inf" <++> prettyPrec appPrec ty

327 |     prettyPrec d (PDelayed _ _ ty) = parenthesise (d > startPrec) $ "Lazy" <++> prettyPrec appPrec ty

328 |     prettyPrec d (PDelay _ tm) = parenthesise (d > startPrec) $ "Delay" <++> prettyPrec appPrec tm

329 |     prettyPrec d (PForce _ tm) = parenthesise (d > startPrec) $ "Force" <++> prettyPrec appPrec tm

330 |     prettyPrec d (PAutoApp _ f a) =

331 |       parenthesise (d > startPrec) $ group $ prettyPrec leftAppPrec f <++> "@" <+> braces (pretty a)

332 |     prettyPrec d (PNamedApp _ f n (PRef _ a)) =

333 |       parenthesise (d > startPrec) $ group $

334 |         if n == rawName a

335 |            then prettyPrec leftAppPrec f <++> braces (pretty0 n)

336 |            else prettyPrec leftAppPrec f <++> braces (pretty0 n <++> equals <++> pretty0 a.rawName)

337 |     prettyPrec d (PNamedApp _ f n a) =

338 |       parenthesise (d > startPrec) $ group $

339 |         prettyPrec leftAppPrec f <++> braces (pretty0 n <++> equals <++> prettyPrec d a)

340 |     prettyPrec d (PSearch {}) = pragma "%search"

341 |     prettyPrec d (PQuote _ tm) = parenthesise (d > startPrec) $ "`" <+> parens (pretty tm)

342 |     prettyPrec d (PQuoteName _ n) = parenthesise (d > startPrec) $ "`" <+> braces (pretty0 n)

343 |     prettyPrec d (PQuoteDecl _ tm) =

344 |       parenthesise (d > startPrec) $

345 |          "`" <+> brackets (angles (angles "declaration"))

346 |     prettyPrec d (PUnquote _ tm) = parenthesise (d > startPrec) $ "~" <+> parens (pretty tm)

347 |     prettyPrec d (PRunElab _ tm) = parenthesise (d > startPrec) $ pragma "%runElab" <++> pretty tm

348 |     prettyPrec d (PPrimVal _ c) = pretty c

349 |     prettyPrec d (PHole _ _ n) = hole (pretty0 (strCons '?' n))

350 |     prettyPrec d (PType _) = annotate (TCon Nothing) "Type"

351 |     prettyPrec d (PAs _ _ n p) = pretty0 n <+> "@" <+> prettyPrec d p

352 |     prettyPrec d (PDotted _ p) = dot <+> prettyPrec d p

353 |     prettyPrec d (PImplicit _) = "_"

354 |     prettyPrec d (PInfer _) = annotate Hole $ "?"

355 |     prettyPrec d (POp _ (MkWithData _ $ BindType nm left) op right) =

356 |         group $ parens (prettyPrec d nm <++> ":" <++> pretty left)

357 |            <++> prettyOp op.val.toName

358 |            <++> pretty right

359 |     prettyPrec d (POp _ (MkWithData _ $ BindExpr nm left) op right) =

360 |         group $ parens (prettyPrec d nm <++> "<-" <++> pretty left)

361 |            <++> prettyOp op.val.toName

362 |            <++> pretty right

363 |     prettyPrec d (POp _ (MkWithData _ $ BindExplicitType nm ty left) op right) =

364 |         group $ parens (prettyPrec d nm <++> ":" <++> pretty ty <++> "<-" <++> pretty left)

365 |            <++> prettyOp op.val.toName

366 |            <++> pretty right

367 |     prettyPrec d (POp _ (MkWithData _ $ NoBinder x) op y) =

368 |       parenthesise (d >= App) $

369 |         group $ pretty x

370 |            <++> prettyOp op.val.toName

371 |            <++> pretty y

372 |     prettyPrec d (PPrefixOp _ op x) = parenthesise (d > startPrec) $ prettyOp op.val.toName <+> pretty x

373 |     prettyPrec d (PSectionL _ op x) = parens (prettyOp op.val.toName <++> pretty x)

374 |     prettyPrec d (PSectionR _ x op) = parens (pretty x <++> prettyOp op.val.toName)

375 |     prettyPrec d (PEq fc l r) = parenthesise (d > startPrec) $ prettyPrec Equal l <++> equals <++> prettyPrec Equal r

376 |     prettyPrec d (PBracketed _ tm) = parens (pretty tm)

377 |     prettyPrec d (PString _ _ xs) = parenthesise (d > startPrec) $ hsep $ punctuate "++" (prettyPStr <$> xs)

378 |     prettyPrec d (PMultiline _ _ indent xs) =

379 |       "multiline" <++>

380 |         (parenthesise (d > startPrec) $

381 |            hsep $ punctuate "++" (prettyPStr <$> concat xs))

382 |     prettyPrec d (PDoBlock _ ns ds) =

383 |       parenthesise (d > startPrec) $ group $ align $ hang 2 $

384 |         do_ <++> (vsep $ punctuate semi (prettyPDo <$> ds))

385 |     prettyPrec d (PBang _ tm) = "!" <+> prettyPrec d tm

386 |     prettyPrec d (PIdiom _ Nothing tm) = enclose (keyword "[|") (keyword "|]") (pretty tm)

387 |     prettyPrec d (PIdiom _ (Just ns) tm) = enclose (pretty0 ns <+> keyword ".[|") (keyword "|]") (pretty tm)

388 |     prettyPrec d (PList _ _ xs) = brackets (group $ align $ vsep $ punctuate comma (pretty . snd <$> xs))

389 |     prettyPrec d (PSnocList _ _ xs)

390 |       = brackets {ldelim = "[<"}

391 |       $ group $ align $ vsep $ punctuate comma

392 |       $ pretty . snd <$> (xs <>> [])

393 |     prettyPrec d (PPair _ l r) = group $ parens (pretty l <+> comma <+> line <+> pretty r)

394 |     prettyPrec d (PDPair _ _ l (PImplicit _) r) = group $ parens (pretty l <++> keyword "**" <+> line <+> pretty r)

395 |     prettyPrec d (PDPair _ _ l ty r) =

396 |       group $ parens (pretty l <++> colon <++> pretty ty <++> keyword "**" <+> line <+> pretty r)

397 |     prettyPrec d (PUnit _) = "()"

398 |     prettyPrec d (PIfThenElse _ x t e) =

399 |       parenthesise (d > startPrec) $ group $ align $ hang 2 $ vsep

400 |         [ keyword "if" <++> pretty x

401 |         , keyword "then" <++> pretty t

402 |         , keyword "else" <++> pretty e]

403 |     prettyPrec d (PComprehension _ ret es) =

404 |       group $ brackets (pretty (dePure ret) <++> pipe <++> vsep (punctuate comma (prettyPDo . deGuard <$> es)))

405 |       where

406 |       dePure : IPTerm -> IPTerm

407 |       dePure tm@(PApp _ (PRef _ n) arg)

408 |         = if dropNS (rawName n) == UN (Basic "pure") then arg else tm

409 |       dePure tm = tm

411 |       deGuard : PDo' KindedName -> PDo' KindedName

412 |       deGuard tm@(DoExp fc (PApp _ (PRef _ n) arg))

413 |         = if dropNS (rawName n) == UN (Basic "guard") then DoExp fc arg else tm

414 |       deGuard tm = tm

415 |     prettyPrec d (PRewrite _ rule tm) =

416 |       parenthesise (d > startPrec) $ group $

417 |         rewrite_ <++> pretty rule <+> line <+> in_ <++> pretty tm

418 |     prettyPrec d (PRange _ start Nothing end) =

419 |       brackets (pretty start <++> keyword ".." <++> pretty end)

420 |     prettyPrec d (PRange _ start (Just next) end) =

421 |       brackets (pretty start <+> comma <++> pretty next <++> keyword ".." <++> pretty end)

422 |     prettyPrec d (PRangeStream _ start Nothing) = brackets (pretty start <++> keyword "..")

423 |     prettyPrec d (PRangeStream _ start (Just next)) =

424 |       brackets (pretty start <+> comma <++> pretty next <++> keyword "..")

425 |     prettyPrec d (PUnifyLog _ lvl tm) = prettyPrec d tm

426 |     prettyPrec d (PPostfixApp fc rec fields) =

427 |       parenthesise (d > startPrec) $

428 |         pretty rec <++> dot <+> concatWith (surround dot) (map (pretty0 . snd) fields)

429 |     prettyPrec d (PPostfixAppPartial fc fields) =

430 |       parens (dot <+> concatWith (surround dot) (map (pretty0 . snd) fields))

431 |     prettyPrec d (PWithUnambigNames fc ns rhs) =

432 |       parenthesise (d > startPrec) $ group $

433 |         with_ <++> cast (prettyList $ map snd ns) <+> line <+> pretty rhs

436 | render : {auto o : Ref ROpts REPLOpts} -> Doc IdrisAnn -> Core String

437 | render = render colorAnn

440 | renderWithDecorations :

441 |   {auto o : Ref ROpts REPLOpts} ->

442 |   (ann -> Maybe ann') ->

443 |   Doc ann ->

444 |   Core (String, List (Span ann'))

445 | renderWithDecorations f doc =

446 |   do (str, mspans) <- Render.renderWithSpans doc

447 |      let spans = mapMaybe (traverse f) mspans

448 |      pure (str, spans)

451 | prettyImport : Import -> Doc IdrisSyntax

452 | prettyImport (MkImport loc reexport path nameAs)

453 |   = keyword "import"

454 |     <+> ifThenElse reexport (space <+> keyword "public") ""

455 |     <++> pretty0 path

456 |     <+> ifThenElse (miAsNamespace path /= nameAs) (space <+> keyword "as" <++> pretty0 nameAs) ""