Text.PrettyPrint.Prettyprinter.Doc


   0 | module Text.PrettyPrint.Prettyprinter.Doc
   1 | 
   2 | import Data.List
   3 | import public Data.List1
   4 | import Data.Maybe
   5 | import Data.String
   6 | import public Data.String.Extra
   7 | 
   8 | %default total
   9 | 
  10 | export
  11 | textSpaces : Int -> String
  12 | textSpaces n = replicate (integerToNat $ cast n) ' '
  13 | 
  14 | ||| Maximum number of characters that fit in one line.
  15 | public export
  16 | data PageWidth : Type where
  17 |   ||| The `Int` is the number of characters, including whitespace, that fit in a line.
  18 |   ||| The `Double` is the ribbon, the fraction of the toal page width that can be printed on.
  19 |   AvailablePerLine : Int -> Double -> PageWidth
  20 |   ||| The layouters should not introduce line breaks.
  21 |   Unbounded : PageWidth
  22 | 
  23 | data FlattenResult : Type -> Type where
  24 |   Flattened : a -> FlattenResult a
  25 |   AlreadyFlat : FlattenResult a
  26 |   NeverFlat : FlattenResult a
  27 | 
  28 | Functor FlattenResult where
  29 |   map f (Flattened a) = Flattened (f a)
  30 |   map _ AlreadyFlat = AlreadyFlat
  31 |   map _ NeverFlat = NeverFlat
  32 | 
  33 | ||| Fusion depth parameter.
  34 | public export
  35 | data FusionDepth : Type where
  36 |   ||| Do not dive deep into nested documents.
  37 |   Shallow : FusionDepth
  38 |   ||| Recurse into all parts of the `Doc`. May impact performace.
  39 |   Deep : FusionDepth
  40 | 
  41 | ||| This data type represents pretty documents that have
  42 | ||| been annotated with an arbitrary data type `ann`.
  43 | public export
  44 | data Doc : Type -> Type where
  45 |   Empty : Doc ann
  46 |   Chara : (c : Char) -> Doc ann                         -- Invariant: not '\n'
  47 |   Text : (len : Int) -> (text : String) -> Doc ann      -- Invariant: at least two characters long and no '\n'
  48 |   Line : Doc ann
  49 |   FlatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
  50 |   Cat : Doc ann -> Doc ann -> Doc ann
  51 |   Nest : (i : Int) -> Doc ann -> Doc ann
  52 |   Union : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann   -- Invariant: the first line of the first document should be
  53 |                                                         -- longer than the first lines of the second one
  54 |   Column : (Int -> Doc ann) -> Doc ann
  55 |   WithPageWidth : (PageWidth -> Doc ann) -> Doc ann
  56 |   Nesting : (Int -> Doc ann) -> Doc ann
  57 |   Annotated : ann -> Doc ann -> Doc ann
  58 | 
  59 | export
  60 | Semigroup (Doc ann) where
  61 |   (<+>) = Cat
  62 | 
  63 | export
  64 | Monoid (Doc ann) where
  65 |   neutral = Empty
  66 | 
  67 | ||| Layout a document depending on which column it starts at.
  68 | export
  69 | column : (Int -> Doc ann) -> Doc ann
  70 | column = Column
  71 | 
  72 | ||| Lays out a document with the current nesting level increased by `i`.
  73 | export
  74 | nest : Int -> Doc ann -> Doc ann
  75 | nest 0 x = x
  76 | nest i x = Nest i x
  77 | 
  78 | ||| Layout a document depending on the current nesting level.
  79 | export
  80 | nesting : (Int -> Doc ann) -> Doc ann
  81 | nesting = Nesting
  82 | 
  83 | ||| Lays out a document, and makes the column width of it available to a function.
  84 | export
  85 | width : Doc ann -> (Int -> Doc ann) -> Doc ann
  86 | width doc f = column (\colStart => doc <+> column (\colEnd => f (colEnd - colStart)))
  87 | 
  88 | ||| Layout a document depending on the page width, if one has been specified.
  89 | export
  90 | pageWidth : (PageWidth -> Doc ann) -> Doc ann
  91 | pageWidth = WithPageWidth
  92 | 
  93 | ||| Lays out a document with the nesting level set to the current column.
  94 | export
  95 | align : Doc ann -> Doc ann
  96 | align d = column (\k => nesting (\i => nest (k - i) d))
  97 | 
  98 | ||| Lays out a document with a nesting level set to the current column plus `i`.
  99 | ||| Negative values are allowed, and decrease the nesting level accordingly.
 100 | export
 101 | hang : Int -> Doc ann -> Doc ann
 102 | hang i d = align (nest i d)
 103 | 
 104 | ||| Insert a number of spaces.
 105 | export
 106 | spaces : Int -> Doc ann
 107 | spaces n = if n <= 0
 108 |               then Empty
 109 |               else if n == 1
 110 |                       then Chara ' '
 111 |                       else Text n (textSpaces n)
 112 | 
 113 | ||| Indents a document with `i` spaces, starting from the current cursor position.
 114 | export
 115 | indent : Int -> Doc ann -> Doc ann
 116 | indent i d = hang i (spaces i <+> d)
 117 | 
 118 | ||| Lays out a document. It then appends spaces until the width is equal to `i`.
 119 | ||| If the width is already larger, nothing is appended.
 120 | export
 121 | fill : Int -> Doc ann -> Doc ann
 122 | fill n doc = width doc (\w => spaces $ n - w)
 123 | 
 124 | export infixr 6 <++>
 125 | ||| Concatenates two documents with a space in between.
 126 | export
 127 | (<++>) : Doc ann -> Doc ann -> Doc ann
 128 | x <++> y = x <+> Chara ' ' <+> y
 129 | 
 130 | ||| The empty document behaves like `pretty ""`, so it has a height of 1.
 131 | export
 132 | emptyDoc : Doc ann
 133 | emptyDoc = Empty
 134 | 
 135 | ||| Behaves like `space` if the resulting output fits the page, otherwise like `line`.
 136 | export
 137 | softline : Doc ann
 138 | softline = Union (Chara ' ') Line
 139 | 
 140 | ||| Like `softline`, but behaves like `neutral` if the resulting output does not fit
 141 | ||| on the page.
 142 | export
 143 | softline' : Doc ann
 144 | softline' = Union neutral Line
 145 | 
 146 | ||| A line break, even when grouped.
 147 | export
 148 | hardline : Doc ann
 149 | hardline = Line
 150 | 
 151 | flatten : Doc ann -> Doc ann
 152 | flatten Empty = Empty
 153 | flatten (Chara x) = Chara x
 154 | flatten (Text len x) = Text len x
 155 | flatten Line = Empty
 156 | flatten (FlatAlt _ y) = flatten y
 157 | flatten (Cat x y) = Cat (flatten x) (flatten y)
 158 | flatten (Nest i x) = Nest i (flatten x)
 159 | flatten (Union x _) = flatten x
 160 | flatten (Column f) = Column (\x => flatten $ f x)
 161 | flatten (WithPageWidth f) = WithPageWidth (\x => flatten $ f x)
 162 | flatten (Nesting f) = Nesting (\x => flatten $ f x)
 163 | flatten (Annotated ann x) = Annotated ann (flatten x)
 164 | 
 165 | changesUponFlattening : Doc ann -> FlattenResult (Doc ann)
 166 | changesUponFlattening Empty = AlreadyFlat
 167 | changesUponFlattening (Chara x) = AlreadyFlat
 168 | changesUponFlattening (Text x y) = AlreadyFlat
 169 | changesUponFlattening Line = NeverFlat
 170 | changesUponFlattening (FlatAlt _ y) = Flattened (flatten y)
 171 | changesUponFlattening (Cat x y) = case (changesUponFlattening x, changesUponFlattening y) of
 172 |   (NeverFlat, _) => NeverFlat
 173 |   (_, NeverFlat) => NeverFlat
 174 |   (Flattened x', Flattened y') => Flattened (Cat x' y')
 175 |   (Flattened x', AlreadyFlat) => Flattened (Cat x' y)
 176 |   (AlreadyFlat , Flattened y') => Flattened (Cat x y')
 177 |   (AlreadyFlat , AlreadyFlat) => AlreadyFlat
 178 | changesUponFlattening (Nest i x) = map (Nest i) (changesUponFlattening x)
 179 | changesUponFlattening (Union x _) = Flattened x
 180 | changesUponFlattening (Column f) = Flattened (Column (flatten . f))
 181 | changesUponFlattening (WithPageWidth f) = Flattened (WithPageWidth (flatten . f))
 182 | changesUponFlattening (Nesting f) = Flattened (Nesting (flatten . f))
 183 | changesUponFlattening (Annotated ann x) = map (Annotated ann) (changesUponFlattening x)
 184 | 
 185 | ||| Tries laying out a document into a single line by removing the contained
 186 | ||| line breaks; if this does not fit the page, or has an `hardline`, the document
 187 | ||| is laid out without changes.
 188 | export
 189 | group : Doc ann -> Doc ann
 190 | group (Union x y) = Union x y
 191 | group (FlatAlt x y) = case changesUponFlattening y of
 192 |   Flattened y' => Union y' x
 193 |   AlreadyFlat => Union y x
 194 |   NeverFlat => x
 195 | group x = case changesUponFlattening x of
 196 |   Flattened x' => Union x' x
 197 |   AlreadyFlat => x
 198 |   NeverFlat => x
 199 | 
 200 | ||| By default renders the first document, When grouped renders the second, with
 201 | ||| the first as fallback when there is not enough space.
 202 | export
 203 | flatAlt : Lazy (Doc ann) -> Lazy (Doc ann) -> Doc ann
 204 | flatAlt = FlatAlt
 205 | 
 206 | ||| Advances to the next line and indents to the current nesting level.
 207 | export
 208 | line : Doc ann
 209 | line = FlatAlt Line (Chara ' ')
 210 | 
 211 | ||| Like `line`, but behaves like `neutral` if the line break is undone by `group`.
 212 | export
 213 | line' : Doc ann
 214 | line' = FlatAlt Line Empty
 215 | 
 216 | ||| First lays out the document. It then appends spaces until the width is equal to `i`.
 217 | ||| If the width is already larger than `i`, the nesting level is decreased by `i`
 218 | ||| and a line is appended.
 219 | export
 220 | fillBreak : Int -> Doc ann -> Doc ann
 221 | fillBreak f x  = width x (\w => if w > f
 222 |                                    then nest f line'
 223 |                                    else spaces $ f - w)
 224 | 
 225 | ||| Concatenate all documents element-wise with a binary function.
 226 | export
 227 | concatWith : (Doc ann -> Doc ann -> Doc ann) -> List (Doc ann) -> Doc ann
 228 | concatWith f [] = neutral
 229 | concatWith f (x :: xs) = foldl f x xs
 230 | 
 231 | ||| Concatenates all documents horizontally with `(<++>)`.
 232 | export
 233 | hsep : List (Doc ann) -> Doc ann
 234 | hsep = concatWith (<++>)
 235 | 
 236 | ||| Concatenates all documents above each other. If a `group` undoes the line breaks,
 237 | ||| the documents are separated with a space instead.
 238 | export
 239 | vsep : List (Doc ann) -> Doc ann
 240 | vsep = concatWith (\x, y => x <+> line <+> y)
 241 | 
 242 | ||| Concatenates the documents horizontally with `(<++>)` as long as it fits the page,
 243 | ||| then inserts a line and continues.
 244 | export
 245 | fillSep : List (Doc ann) -> Doc ann
 246 | fillSep = concatWith (\x, y => x <+> softline <+> y)
 247 | 
 248 | ||| Tries laying out the documents separated with spaces and if this does not fit,
 249 | ||| separates them with newlines.
 250 | export
 251 | sep : List (Doc ann) -> Doc ann
 252 | sep = group . vsep
 253 | 
 254 | ||| Concatenates all documents horizontally with `(<+>)`.
 255 | export
 256 | hcat : List (Doc ann) -> Doc ann
 257 | hcat = concatWith (<+>)
 258 | 
 259 | ||| Vertically concatenates the documents. If it is grouped, the line breaks are removed.
 260 | export
 261 | vcat : List (Doc ann) -> Doc ann
 262 | vcat = concatWith (\x, y => x <+> line' <+> y)
 263 | 
 264 | ||| Concatenates documents horizontally with `(<+>)` as log as it fits the page, then
 265 | ||| inserts a line and continues.
 266 | export
 267 | fillCat : List (Doc ann) -> Doc ann
 268 | fillCat = concatWith (\x, y => x <+> softline' <+> y)
 269 | 
 270 | ||| Tries laying out the documents separated with nothing, and if it does not fit the page,
 271 | ||| separates them with newlines.
 272 | export
 273 | cat : List (Doc ann) -> Doc ann
 274 | cat = group . vcat
 275 | 
 276 | ||| Appends `p` to all but the last document.
 277 | export
 278 | punctuate : Doc ann -> List (Doc ann) -> List (Doc ann)
 279 | punctuate _ [] = []
 280 | punctuate _ [d] = [d]
 281 | punctuate p (d :: ds) = (d <+> p) :: punctuate p ds
 282 | 
 283 | export
 284 | plural : Num amount => Eq amount => doc -> doc -> amount -> doc
 285 | plural one multiple n = if n == 1 then one else multiple
 286 | 
 287 | ||| Encloses the document between two other documents using `(<+>)`.
 288 | export
 289 | enclose : Doc ann -> Doc ann -> Doc ann -> Doc ann
 290 | enclose l r x = l <+> x <+> r
 291 | 
 292 | ||| Reordering of `encloses`.
 293 | ||| Example: concatWith (surround (pretty ".")) [pretty "Text", pretty "PrettyPrint", pretty "Doc"]
 294 | |||          Text.PrettyPrint.Doc
 295 | export
 296 | surround : Doc ann -> Doc ann -> Doc ann -> Doc ann
 297 | surround x l r = l <+> x <+> r
 298 | 
 299 | ||| Concatenates the documents separated by `s` and encloses the resulting document by `l` and `r`.
 300 | export
 301 | encloseSep : Doc ann -> Doc ann -> Doc ann -> List (Doc ann) -> Doc ann
 302 | encloseSep l r s []  = l <+> r
 303 | encloseSep l r s [d] = l <+> d <+> r
 304 | encloseSep l r s ds  = cat (zipWith (<+>) (l :: replicate (length ds `minus` 1) s) ds) <+> r
 305 | 
 306 | unsafeTextWithoutNewLines : String -> Doc ann
 307 | unsafeTextWithoutNewLines str = case strM str of
 308 |   StrNil => Empty
 309 |   StrCons c cs => if cs == ""
 310 |                      then Chara c
 311 |                      else Text (cast $ length str) str
 312 | 
 313 | ||| Adds an annotation to a document.
 314 | export
 315 | annotate : ann -> Doc ann -> Doc ann
 316 | annotate = Annotated
 317 | 
 318 | ||| Changes the annotations of a document. Individual annotations can be removed,
 319 | ||| changed, or replaced by multiple ones.
 320 | export
 321 | alterAnnotations : (ann -> List ann') -> Doc ann -> Doc ann'
 322 | alterAnnotations re Empty = Empty
 323 | alterAnnotations re (Chara c) = Chara c
 324 | alterAnnotations re (Text l t) = Text l t
 325 | alterAnnotations re Line = Line
 326 | alterAnnotations re (FlatAlt x y) = FlatAlt (alterAnnotations re x) (alterAnnotations re y)
 327 | alterAnnotations re (Cat x y) = Cat (alterAnnotations re x) (alterAnnotations re y)
 328 | alterAnnotations re (Nest i x) = Nest i (alterAnnotations re x)
 329 | alterAnnotations re (Union x y) = Union (alterAnnotations re x) (alterAnnotations re y)
 330 | alterAnnotations re (Column f) = Column (\x => alterAnnotations re $ f x)
 331 | alterAnnotations re (WithPageWidth f) = WithPageWidth (\x => alterAnnotations re $ f x)
 332 | alterAnnotations re (Nesting f) = Nesting (\x => alterAnnotations re $ f x)
 333 | alterAnnotations re (Annotated ann x) = foldr Annotated (alterAnnotations re x) (re ann)
 334 | 
 335 | ||| Removes all annotations.
 336 | export
 337 | unAnnotate : Doc ann -> Doc xxx
 338 | unAnnotate = alterAnnotations (const [])
 339 | 
 340 | ||| Changes the annotations of a document.
 341 | export
 342 | reAnnotate : (ann -> ann') -> Doc ann -> Doc ann'
 343 | reAnnotate re = alterAnnotations (pure . re)
 344 | 
 345 | ||| Alter the document's annotations.
 346 | export
 347 | Functor Doc where
 348 |   map = reAnnotate
 349 | 
 350 | ||| Overloaded conversion to `Doc`.
 351 | public export
 352 | interface Pretty a where
 353 |   pretty : a -> Doc ann
 354 |   pretty x = prettyPrec Open x
 355 | 
 356 |   prettyPrec : Prec -> a -> Doc ann
 357 |   prettyPrec _ x = pretty x
 358 | 
 359 | export
 360 | Pretty String where
 361 |   pretty str = let str' = if "\n" `isSuffixOf` str then dropLast 1 str else str in
 362 |                    vsep $ map unsafeTextWithoutNewLines $ lines str'
 363 | 
 364 | public export
 365 | FromString (Doc ann) where
 366 |   fromString = pretty
 367 | 
 368 | ||| Variant of `encloseSep` with braces and comma as separator.
 369 | export
 370 | list : List (Doc ann) -> Doc ann
 371 | list = group . encloseSep (flatAlt (pretty "[ ") (pretty "["))
 372 |                           (flatAlt (pretty " ]") (pretty "]"))
 373 |                           (pretty ", ")
 374 | 
 375 | ||| Variant of `encloseSep` with parentheses and comma as separator.
 376 | export
 377 | tupled : List (Doc ann) -> Doc ann
 378 | tupled = group . encloseSep (flatAlt (pretty "( ") (pretty "("))
 379 |                             (flatAlt (pretty " )") (pretty ")"))
 380 |                             (pretty ", ")
 381 | 
 382 | export
 383 | Pretty a => Pretty (List a) where
 384 |   pretty = align . list . map pretty
 385 | 
 386 | export
 387 | Pretty a => Pretty (List1 a) where
 388 |   pretty = pretty . forget
 389 | 
 390 | export
 391 | [prettyListMaybe] Pretty a => Pretty (List (Maybe a)) where
 392 |   pretty = pretty . catMaybes
 393 |     where catMaybes : List (Maybe a) -> List a
 394 |           catMaybes [] = []
 395 |           catMaybes (Nothing :: xs) = catMaybes xs
 396 |           catMaybes ((Just x) :: xs) = x :: catMaybes xs
 397 | 
 398 | export
 399 | Pretty () where
 400 |   pretty _ = pretty "()"
 401 | 
 402 | export
 403 | Pretty Bool where
 404 |   pretty True = pretty "True"
 405 |   pretty False = pretty "False"
 406 | 
 407 | export
 408 | Pretty Char where
 409 |   pretty '\n' = line
 410 |   pretty c = Chara c
 411 | 
 412 | export Pretty Nat where pretty = unsafeTextWithoutNewLines . show
 413 | export Pretty Int where pretty = unsafeTextWithoutNewLines . show
 414 | export Pretty Integer where pretty = unsafeTextWithoutNewLines . show
 415 | export Pretty Double where pretty = unsafeTextWithoutNewLines . show
 416 | export Pretty Bits8 where pretty = unsafeTextWithoutNewLines . show
 417 | export Pretty Bits16 where pretty = unsafeTextWithoutNewLines . show
 418 | export Pretty Bits32 where pretty = unsafeTextWithoutNewLines . show
 419 | export Pretty Bits64 where pretty = unsafeTextWithoutNewLines . show
 420 | export Pretty Int8 where pretty = unsafeTextWithoutNewLines . show
 421 | export Pretty Int16 where pretty = unsafeTextWithoutNewLines . show
 422 | export Pretty Int32 where pretty = unsafeTextWithoutNewLines . show
 423 | export Pretty Int64 where pretty = unsafeTextWithoutNewLines . show
 424 | 
 425 | export
 426 | (Pretty a, Pretty b) => Pretty (a, b) where
 427 |   pretty (x, y) = tupled [pretty x, pretty y]
 428 | 
 429 | export
 430 | Pretty a => Pretty (Maybe a) where
 431 |   pretty = maybe neutral pretty
 432 | 
 433 | ||| Combines text nodes so they can be rendered more efficiently.
 434 | export
 435 | fuse : FusionDepth -> Doc ann -> Doc ann
 436 | fuse depth (Cat Empty x) = fuse depth x
 437 | fuse depth (Cat x Empty) = fuse depth x
 438 | fuse depth (Cat (Chara c1) (Chara c2)) = Text 2 (strCons c1 (strCons c2 ""))
 439 | fuse depth (Cat (Text lt t) (Chara c)) = Text (lt + 1) (t ++ singleton c)
 440 | fuse depth (Cat (Chara c) (Text lt t)) = Text (lt + 1) (strCons c t)
 441 | fuse depth (Cat (Text l1 t1) (Text l2 t2)) = Text (l1 + l2) (t1 ++ t2)
 442 | fuse depth (Cat (Chara x) (Cat (Chara y) z)) =
 443 |   let sub = Text 2 (strCons x (strCons y "")) in
 444 |       fuse depth $ assert_smaller (Cat (Chara x) (Cat (Chara y) z)) (Cat sub z)
 445 | fuse depth (Cat (Text lx x) (Cat (Chara y) z)) =
 446 |   let sub = Text (lx + 1) (x ++ singleton y) in
 447 |       fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Chara y) z)) (Cat sub z)
 448 | fuse depth (Cat (Chara x) (Cat (Text ly y) z)) =
 449 |   let sub = Text (ly + 1) (strCons x y) in
 450 |       fuse depth $ assert_smaller (Cat (Chara x) (Cat (Text ly y) z)) (Cat sub z)
 451 | fuse depth (Cat (Text lx x) (Cat (Text ly y) z)) =
 452 |   let sub = Text (lx + ly) (x ++ y) in
 453 |       fuse depth $ assert_smaller (Cat (Text lx x) (Cat (Text ly y) z)) (Cat sub z)
 454 | fuse depth (Cat (Cat x (Chara y)) z) =
 455 |   let sub = fuse depth (Cat (Chara y) z) in
 456 |       assert_total $ fuse depth (Cat x sub)
 457 | fuse depth (Cat (Cat x (Text ly y)) z) =
 458 |   let sub = fuse depth (Cat (Text ly y) z) in
 459 |       assert_total $ fuse depth (Cat x sub)
 460 | fuse depth (Cat x y) = Cat (fuse depth x) (fuse depth y)
 461 | fuse depth (Nest i (Nest j x)) = fuse depth $ assert_smaller (Nest i (Nest j x)) (Nest (i + j) x)
 462 | fuse depth (Nest _ Empty) = Empty
 463 | fuse depth (Nest _ (Text lx x)) = Text lx x
 464 | fuse depth (Nest _ (Chara x)) = Chara x
 465 | fuse depth (Nest 0 x) = fuse depth x
 466 | fuse depth (Nest i x) = Nest i (fuse depth x)
 467 | fuse depth (Annotated ann x) = Annotated ann (fuse depth x)
 468 | fuse depth (FlatAlt x y) = FlatAlt (fuse depth x) (fuse depth y)
 469 | fuse depth (Union x y) = Union (fuse depth x) (fuse depth y)
 470 | fuse Shallow (Column f) = Column f
 471 | fuse depth (Column f) = Column (\x => fuse depth $ f x)
 472 | fuse Shallow (WithPageWidth f) = WithPageWidth f
 473 | fuse depth (WithPageWidth f) = WithPageWidth (\x => fuse depth $ f x)
 474 | fuse Shallow (Nesting f) = Nesting f
 475 | fuse depth (Nesting f) = Nesting (\x => fuse depth $ f x)
 476 | fuse depth x = x
 477 | 
 478 | ||| This data type represents laid out documents and is used by the display functions.
 479 | public export
 480 | data SimpleDocStream : Type -> Type where
 481 |   SEmpty : SimpleDocStream ann
 482 |   SChar : (c : Char) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
 483 |   SText : (len : Int) -> (text : String) -> (rest : Lazy (SimpleDocStream ann)) -> SimpleDocStream ann
 484 |   SLine : (i : Int) -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
 485 |   SAnnPush : ann -> (rest : SimpleDocStream ann) -> SimpleDocStream ann
 486 |   SAnnPop : (rest : SimpleDocStream ann) -> SimpleDocStream ann
 487 | 
 488 | internalError : SimpleDocStream ann
 489 | internalError = let msg = "<internal pretty printing error>" in
 490 |                     SText (cast $ length msg) msg SEmpty
 491 | 
 492 | data AnnotationRemoval = Remove | DontRemove
 493 | 
 494 | ||| Changes the annotation of a document to a different annotation or none.
 495 | export
 496 | alterAnnotationsS : (ann -> Maybe ann') -> SimpleDocStream ann -> SimpleDocStream ann'
 497 | alterAnnotationsS re = fromMaybe internalError . go []
 498 |   where
 499 |     go : List AnnotationRemoval -> SimpleDocStream ann -> Maybe (SimpleDocStream ann')
 500 |     go stack SEmpty = pure SEmpty
 501 |     go stack (SChar c rest) = SChar c . delay <$> go stack rest
 502 |     go stack (SText l t rest) = SText l t . delay <$> go stack rest
 503 |     go stack (SLine l rest) = SLine l <$> go stack rest
 504 |     go stack (SAnnPush ann rest) = case re ann of
 505 |       Nothing => go (Remove :: stack) rest
 506 |       Just ann' => SAnnPush ann' <$> go (DontRemove :: stack) rest
 507 |     go stack (SAnnPop rest) = case stack of
 508 |       [] => Nothing
 509 |       DontRemove :: stack' => SAnnPop <$> go stack' rest
 510 |       Remove :: stack' => go stack' rest
 511 | 
 512 | ||| Removes all annotations.
 513 | export
 514 | unAnnotateS : SimpleDocStream ann -> SimpleDocStream xxx
 515 | unAnnotateS SEmpty = SEmpty
 516 | unAnnotateS (SChar c rest) = SChar c (unAnnotateS rest)
 517 | unAnnotateS (SText l t rest) = SText l t (unAnnotateS rest)
 518 | unAnnotateS (SLine l rest) = SLine l (unAnnotateS rest)
 519 | unAnnotateS (SAnnPush ann rest) = unAnnotateS rest
 520 | unAnnotateS (SAnnPop rest) = unAnnotateS rest
 521 | 
 522 | ||| Changes the annotation of a document.
 523 | export
 524 | reAnnotateS : (ann -> ann') -> SimpleDocStream ann -> SimpleDocStream ann'
 525 | reAnnotateS re SEmpty = SEmpty
 526 | reAnnotateS re (SChar c rest) = SChar c (reAnnotateS re rest)
 527 | reAnnotateS re (SText l t rest) = SText l t (reAnnotateS re rest)
 528 | reAnnotateS re (SLine l rest) = SLine l (reAnnotateS re rest)
 529 | reAnnotateS re (SAnnPush ann rest) = SAnnPush (re ann) (reAnnotateS re rest)
 530 | reAnnotateS re (SAnnPop rest) = SAnnPop (reAnnotateS re rest)
 531 | 
 532 | export
 533 | Functor SimpleDocStream where
 534 |   map = reAnnotateS
 535 | 
 536 | ||| Collects all annotations from a document.
 537 | export
 538 | collectAnnotations : Monoid m => (ann -> m) -> SimpleDocStream ann -> m
 539 | collectAnnotations f SEmpty = neutral
 540 | collectAnnotations f (SChar c rest) = collectAnnotations f rest
 541 | collectAnnotations f (SText l t rest) = collectAnnotations f rest
 542 | collectAnnotations f (SLine l rest) = collectAnnotations f rest
 543 | collectAnnotations f (SAnnPush ann rest) = f ann <+> collectAnnotations f rest
 544 | collectAnnotations f (SAnnPop rest) = collectAnnotations f rest
 545 | 
 546 | ||| Transform a document based on its annotations.
 547 | export
 548 | traverse : Applicative f => (ann -> f ann') -> SimpleDocStream ann -> f (SimpleDocStream ann')
 549 | traverse f SEmpty = pure SEmpty
 550 | traverse f (SChar c rest) = SChar c . delay <$> traverse f rest
 551 | traverse f (SText l t rest) = SText l t . delay <$> traverse f rest
 552 | traverse f (SLine l rest) = SLine l <$> traverse f rest
 553 | traverse f (SAnnPush ann rest) = SAnnPush <$> f ann <*> traverse f rest
 554 | traverse f (SAnnPop rest) = SAnnPop <$> traverse f rest
 555 | 
 556 | data WhitespaceStrippingState = AnnotationLevel Int | RecordedWithespace (List Int) Int
 557 | 
 558 | dropWhileEnd : (a -> Bool) -> List a -> List a
 559 | dropWhileEnd p = foldr (\x, xs => if p x && isNil xs then [] else x :: xs) []
 560 | 
 561 | ||| Removes all trailing space characters.
 562 | export
 563 | removeTrailingWhitespace : SimpleDocStream ann -> SimpleDocStream ann
 564 | removeTrailingWhitespace = fromMaybe internalError . go (RecordedWithespace [] 0)
 565 |   where
 566 |     prependEmptyLines : List Int -> SimpleDocStream ann -> SimpleDocStream ann
 567 |     prependEmptyLines is sds0 = foldr (\_, sds => SLine 0 sds) sds0 is
 568 | 
 569 |     commitWhitespace : List Int -> Int -> SimpleDocStream ann -> SimpleDocStream ann
 570 |     commitWhitespace [] 0 sds = sds
 571 |     commitWhitespace [] 1 sds = SChar ' ' sds
 572 |     commitWhitespace [] n sds = SText n (textSpaces n) sds
 573 |     commitWhitespace (i :: is) n sds = prependEmptyLines is (SLine (i + n) sds)
 574 | 
 575 |     go : WhitespaceStrippingState -> SimpleDocStream ann -> Maybe (SimpleDocStream ann)
 576 |     go (AnnotationLevel _) SEmpty = pure SEmpty
 577 |     go l@(AnnotationLevel _) (SChar c rest) = SChar c . delay <$> go l rest
 578 |     go l@(AnnotationLevel _) (SText lt text rest) = SText lt text . delay <$> go l rest
 579 |     go l@(AnnotationLevel _) (SLine i rest) = SLine i <$> go l rest
 580 |     go (AnnotationLevel l) (SAnnPush ann rest) = SAnnPush ann <$> go (AnnotationLevel (l + 1)) rest
 581 |     go (AnnotationLevel l) (SAnnPop rest) =
 582 |       if l > 1
 583 |          then SAnnPop <$> go (AnnotationLevel (l - 1)) rest
 584 |          else SAnnPop <$> go (RecordedWithespace [] 0) rest
 585 |     go (RecordedWithespace _ _) SEmpty = pure SEmpty
 586 |     go (RecordedWithespace lines spaces) (SChar ' ' rest) = go (RecordedWithespace lines (spaces + 1)) rest
 587 |     go (RecordedWithespace lines spaces) (SChar c rest) =
 588 |       do rest' <- go (RecordedWithespace [] 0) rest
 589 |          pure $ commitWhitespace lines spaces (SChar c rest')
 590 |     go (RecordedWithespace lines spaces) (SText l text rest) =
 591 |       let stripped = pack $ dropWhileEnd (== ' ') $ unpack text
 592 |           strippedLength = cast $ length stripped
 593 |           trailingLength = l - strippedLength in
 594 |           if strippedLength == 0
 595 |              then go (RecordedWithespace lines (spaces + l)) rest
 596 |              else do rest' <- go (RecordedWithespace [] trailingLength) rest
 597 |                      pure $ commitWhitespace lines spaces (SText strippedLength stripped rest')
 598 |     go (RecordedWithespace lines spaces) (SLine i rest) = go (RecordedWithespace (i :: lines) 0) rest
 599 |     go (RecordedWithespace lines spaces) (SAnnPush ann rest) =
 600 |       do rest' <- go (AnnotationLevel 1) rest
 601 |          pure $ commitWhitespace lines spaces (SAnnPush ann rest')
 602 |     go (RecordedWithespace lines spaces) (SAnnPop _) = Nothing
 603 | 
 604 | public export
 605 | FittingPredicate : Type -> Type
 606 | FittingPredicate ann = Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
 607 | 
 608 | data LayoutPipeline ann = Nil | Cons Int (Doc ann) (LayoutPipeline ann) | UndoAnn (LayoutPipeline ann)
 609 | 
 610 | export
 611 | defaultPageWidth : PageWidth
 612 | defaultPageWidth = AvailablePerLine 80 1
 613 | 
 614 | round : Double -> Int
 615 | round x = if x > 0
 616 |              then if x - floor x < 0.5 then cast $ floor x else cast $ ceiling x
 617 |              else if ceiling x - x < 0.5 then cast $ ceiling x else cast $ floor x
 618 | 
 619 | ||| The remaining width on the current line.
 620 | remainingWidth : Int -> Double -> Int -> Int -> Int
 621 | remainingWidth lineLength ribbonFraction lineIndent currentColumn =
 622 |   let columnsLeftInLine = lineLength - currentColumn
 623 |       ribbonWidth = (max 0 . min lineLength . round) (cast lineLength * ribbonFraction)
 624 |       columnsLeftInRibbon = lineIndent + ribbonWidth - currentColumn in
 625 |       min columnsLeftInLine columnsLeftInRibbon
 626 | 
 627 | public export
 628 | record LayoutOptions where
 629 |   constructor MkLayoutOptions
 630 |   layoutPageWidth : PageWidth
 631 | 
 632 | export
 633 | defaultLayoutOptions : LayoutOptions
 634 | defaultLayoutOptions = MkLayoutOptions defaultPageWidth
 635 | 
 636 | ||| The Wadler/Leijen layout algorithm.
 637 | export
 638 | layoutWadlerLeijen : FittingPredicate ann -> PageWidth -> Doc ann -> SimpleDocStream ann
 639 | layoutWadlerLeijen fits pageWidth_ doc = best 0 0 (Cons 0 doc Nil)
 640 |   where
 641 |     initialIndentation : SimpleDocStream ann -> Maybe Int
 642 |     initialIndentation (SLine i _) = Just i
 643 |     initialIndentation (SAnnPush _ s) = initialIndentation s
 644 |     initialIndentation (SAnnPop s) = initialIndentation s
 645 |     initialIndentation _ = Nothing
 646 | 
 647 |     selectNicer : Int -> Int -> SimpleDocStream ann -> Lazy (SimpleDocStream ann) -> SimpleDocStream ann
 648 |     selectNicer lineIndent currentColumn x y =
 649 |       if fits lineIndent currentColumn (initialIndentation y) x then x else y
 650 | 
 651 |     best : Int -> Int -> LayoutPipeline ann -> SimpleDocStream ann
 652 |     best _ _ Nil = SEmpty
 653 |     best nl cc (UndoAnn ds) = SAnnPop (best nl cc ds)
 654 |     best nl cc (Cons i Empty ds) = best nl cc ds
 655 |     best nl cc (Cons i (Chara c) ds) = SChar c (best nl (cc + 1) ds)
 656 |     best nl cc (Cons i (Text l t) ds) = SText l t (best nl (cc + l) ds)
 657 |     best nl cc (Cons i Line ds) = let x = best i i ds
 658 |                                       i' = case x of
 659 |                                                 SEmpty => 0
 660 |                                                 SLine _ _ => 0
 661 |                                                 _ => i in
 662 |                                       SLine i' x
 663 |     best nl cc c@(Cons i (FlatAlt x y) ds) = best nl cc $ assert_smaller c (Cons i x ds)
 664 |     best nl cc (Cons i (Cat x y) ds) = assert_total $ best nl cc (Cons i x (Cons i y ds))
 665 |     best nl cc c@(Cons i (Nest j x) ds) = best nl cc $ assert_smaller c (Cons (i + j) x ds)
 666 |     best nl cc c@(Cons i (Union x y) ds) = let x' = best nl cc $ assert_smaller c (Cons i x ds)
 667 |                                                y' = delay $ best nl cc $ assert_smaller c (Cons i y ds) in
 668 |                                                selectNicer nl cc x' y'
 669 |     best nl cc c@(Cons i (Column f) ds) = best nl cc $ assert_smaller c (Cons i (f cc) ds)
 670 |     best nl cc c@(Cons i (WithPageWidth f) ds) = best nl cc $ assert_smaller c (Cons i (f pageWidth_) ds)
 671 |     best nl cc c@(Cons i (Nesting f) ds) = best nl cc $ assert_smaller c (Cons i (f i) ds)
 672 |     best nl cc c@(Cons i (Annotated ann x) ds) = SAnnPush ann $ best nl cc $ assert_smaller c (Cons i x (UndoAnn ds))
 673 | 
 674 | ||| Layout a document with unbounded page width.
 675 | export
 676 | layoutUnbounded : Doc ann -> SimpleDocStream ann
 677 | layoutUnbounded = layoutWadlerLeijen (\_, _, _, sdoc => True) Unbounded
 678 | 
 679 | fits : Int -> SimpleDocStream ann -> Bool
 680 | fits w s = if w < 0 then False
 681 |   else case s of
 682 |             SEmpty => True
 683 |             SChar _ x => fits (w - 1) x
 684 |             SText l _ x => fits (w - l) x
 685 |             SLine i x => True
 686 |             SAnnPush _ x => fits w x
 687 |             SAnnPop x => fits w x
 688 | 
 689 | ||| The default layout algorithm.
 690 | export
 691 | layoutPretty : LayoutOptions -> Doc ann -> SimpleDocStream ann
 692 | layoutPretty (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
 693 |     layoutWadlerLeijen (\lineIndent, currentColumn, _, sdoc =>
 694 |       fits (remainingWidth lineLength ribbonFraction lineIndent currentColumn) sdoc) pageWidth_
 695 | layoutPretty (MkLayoutOptions Unbounded) = layoutUnbounded
 696 | 
 697 | ||| Layout algorithm with more lookahead than layoutPretty.
 698 | export
 699 | layoutSmart : LayoutOptions -> Doc ann -> SimpleDocStream ann
 700 | layoutSmart (MkLayoutOptions pageWidth_@(AvailablePerLine lineLength ribbonFraction)) =
 701 |     layoutWadlerLeijen fits pageWidth_
 702 |   where
 703 |     fits : Int -> Int -> Maybe Int -> SimpleDocStream ann -> Bool
 704 |     fits lineIndent currentColumn initialIndentY sdoc = go availableWidth sdoc
 705 |       where
 706 |         availableWidth : Int
 707 |         availableWidth = remainingWidth lineLength ribbonFraction lineIndent currentColumn
 708 | 
 709 |         minNestingLevel : Int
 710 |         minNestingLevel = case initialIndentY of
 711 |                                Just i => min i currentColumn
 712 |                                Nothing => currentColumn
 713 | 
 714 |         go : Int -> SimpleDocStream ann -> Bool
 715 |         go w s = if w < 0
 716 |           then False
 717 |           else case s of
 718 |                     SEmpty => True
 719 |                     SChar _ x => go (w - 1) $ assert_smaller s x
 720 |                     SText l _ x => go (w - l) $ assert_smaller s x
 721 |                     SLine i x => if minNestingLevel < i
 722 |                                     then go (lineLength - i) $ assert_smaller s x
 723 |                                     else True
 724 |                     SAnnPush _ x => go w x
 725 |                     SAnnPop x => go w x
 726 | layoutSmart (MkLayoutOptions Unbounded) = layoutUnbounded
 727 | 
 728 | ||| Lays out the document without adding any indentation. This layouter is very fast.
 729 | export
 730 | layoutCompact : Doc ann -> SimpleDocStream ann
 731 | layoutCompact doc = scan 0 [doc]
 732 |   where
 733 |     scan : Int -> List (Doc ann) -> SimpleDocStream ann
 734 |     scan _ [] = SEmpty
 735 |     scan col (Empty :: ds) = scan col ds
 736 |     scan col ((Chara c) :: ds) = SChar c (scan (col + 1) ds)
 737 |     scan col ((Text l t) :: ds) = SText l t (scan (col + l) ds)
 738 |     scan col s@((FlatAlt x _) :: ds) = scan col $ assert_smaller s (x :: ds)
 739 |     scan col (Line :: ds) = SLine 0 (scan 0 ds)
 740 |     scan col s@((Cat x y) :: ds) = scan col $ assert_smaller s (x :: y :: ds)
 741 |     scan col s@((Nest _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
 742 |     scan col s@((Union _ y) :: ds) = scan col $ assert_smaller s (y :: ds)
 743 |     scan col s@((Column f) :: ds) = scan col $ assert_smaller s (f col :: ds)
 744 |     scan col s@((WithPageWidth f) :: ds) = scan col $ assert_smaller s (f Unbounded :: ds)
 745 |     scan col s@((Nesting f) :: ds) = scan col $ assert_smaller s (f 0 :: ds)
 746 |     scan col s@((Annotated _ x) :: ds) = scan col $ assert_smaller s (x :: ds)
 747 | 
 748 | export
 749 | renderShow : SimpleDocStream ann -> (String -> String)
 750 | renderShow SEmpty = id
 751 | renderShow (SChar c x) = (strCons c) . renderShow x
 752 | renderShow (SText _ t x) = (t ++) . renderShow x
 753 | renderShow (SLine i x) = ((strCons '\n' $ textSpaces i) ++) . renderShow x
 754 | renderShow (SAnnPush _ x) = renderShow x
 755 | renderShow (SAnnPop x) = renderShow x
 756 | 
 757 | export
 758 | Show (Doc ann) where
 759 |   show doc = renderShow (layoutPretty defaultLayoutOptions doc) ""
 760 |