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