    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Pretty Printing
    -- This module is based on Jean-Philippe Bernardy's functional pearl
    -- "A Pretty But Not Greedy Printer"
    ------------------------------------------------------------------------

    {-# OPTIONS --with-K #-}

    open import Data.Nat.Base using (ℕ)

    module Text.Pretty (width : ℕ) where

    import Level
    open import Data.Char.Base using (Char)
    open import Data.List.Base
      using (List; _∷_; []; [_]; uncons; _++_; map; filter)
    open import Data.List.NonEmpty as List⁺ using (foldr₁)
    open import Data.Maybe.Base using (maybe′)
    open import Data.Product.Base using (uncurry)
    open import Data.String.Base using (String; fromList; replicate)
    open import Function.Base using (_∘_; _∘′_; _$_)

    open import Effect.Monad using (RawMonad)
    import Data.List.Effectful as List
    open RawMonad (List.monad {Level.zero})

    import Data.Nat.Properties as ℕ
    open import Data.List.Extrema.Core ℕ.≤-totalOrder using (⊓ᴸ)

    ------------------------------------------------------------------------
    -- Internal representation of documents and rendering function

    import Text.Pretty.Core as Core

    record Doc : Set where
      constructor mkDoc
      field runDoc : List Core.Block
    open Doc public

    render : Doc → String
    render = Core.render
           ∘ maybe′ (foldr₁ (⊓ᴸ Core.Block.height) ∘′ uncurry List⁺._∷_) Core.empty
           ∘ uncons
           ∘′ runDoc

    ------------------------------------------------------------------------
    -- Basic building blocks

    fail : Doc
    fail = mkDoc []

    text : String → Doc
    text = mkDoc ∘′ filter (Core.valid width) ∘ pure ∘ Core.text

    empty : Doc
    empty = text ""

    char : Char → Doc
    char c = text (fromList (c ∷ []))

    spaces : ℕ → Doc
    spaces n = text (replicate n ' ')

    semi colon comma space dot : Doc
    semi = char ';'; colon = char ':'
    comma = char ','; space = char ' '; dot = char '.'

    backslash forwardslash equal : Doc
    backslash = char '\\'; forwardslash = char '/'; equal = char '='

    squote dquote : Doc
    squote = char '\''; dquote = char '"'

    lparen rparen langle rangle : Doc
    lparen = char '('; rparen = char ')'
    langle = char '<'; rangle = char '>'

    lbrace rbrace llbrace rrbrace : Doc
    lbrace = char '{'; rbrace = char '}'
    llbrace = char '⦃'; rrbrace = char '⦄'

    lbracket rbracket llbracket rrbracket : Doc
    lbracket = char '['; rbracket = char ']'
    llbracket = char '⟦'; rrbracket = char '⟧'

    ------------------------------------------------------------------------
    -- Combining two documents

    infixr 5 _<>_
    _<>_ : Doc → Doc → Doc
    xs <> ys = mkDoc $
      let candidates = Core._<>_ <$> runDoc xs ⊛ runDoc ys in
      filter (Core.valid width) candidates

    flush : Doc → Doc
    flush = mkDoc ∘′ map Core.flush ∘′ runDoc

    infixr 5 _<+>_
    _<+>_ : Doc → Doc → Doc
    x <+> y = x <> space <> y

    infixr 5 _$$_
    _$$_ : Doc → Doc → Doc
    x $$ y = flush x <> y

    infixr 4 _<|>_
    _<|>_ : Doc → Doc → Doc
    x <|> y = mkDoc (runDoc x ++ runDoc y)

    ------------------------------------------------------------------------
    -- Combining lists of documents

    foldDoc : (Doc → Doc → Doc) → List Doc → Doc
    foldDoc _ []       = empty
    foldDoc _ (x ∷ []) = x
    foldDoc f (x ∷ xs) = f x (foldDoc f xs)

    hsep vcat : List Doc → Doc
    hsep = foldDoc _<+>_
    vcat = foldDoc _$$_

    sep : List Doc → Doc
    sep [] = empty
    sep xs = hsep xs <|> vcat xs

    ------------------------------------------------------------------------
    -- Defined combinators

    parens : Doc → Doc
    parens d = lparen <> d <> rparen

    commaSep : List Doc → Doc
    commaSep = foldDoc (λ d e → d <> comma <+> e)

    newline : Doc
    newline = flush empty