[RFC] Pretty Printer / Code Formatting

I'm currently looking into improving the pretty printer and would like to hear what you think about how we should format Lean code. This is important for many potential editor features, like automatic code formatting, but also features that want to make changes to a Lean file, like automatically generating match cases or adding unimplemented functions of a class to an instance. Here the code formatting would allow the implementation of the feature to work on the Syntax level rather than on the textual level.

Pretty printing in Lean is implemented in three steps: The first step is called delaboration and transforms fully elaborated Expr terms from the Lean core into surface-level Syntax. After that, in the second step, the Syntax is turned into an output independent Format via formatters. Both of these steps are automatically created for new notation / macros (when possible) and can be customized. The resulting Format contains the string contents of the Expr/Syntax representation, but is not fixed to a specific formatting with a fixed target width. This is done in the last step where the (feel free to suggest a name for this step) decides where line breaks should be inserted to get a compact String representation that fits in the available width (if possible). In addition there is the parenthesizer between the delaborator and the formatter that inserts parantheses into a Syntax object where necessary.

Delaborator: Expr to Syntax

From what I've seen so far, I don't think the delaborators require much work, but feel free to correct me here. This step is also not required for the code formatting use case.

Formatter: Syntax to Format

This is probably the most controversial part, since each of us has different preferences on how to format (Lean) code. But this step needs work nonetheless, because some formatters are broken or output code that we would not want to have in our Lean projects. I hope we can find some clean formatting rules that most people can work with. Feel free to make suggestions on how to format specific Lean syntax and I will also post examples here when I encounter them.

Examples of broken formatters:

def foo (xs : Array Nat) :=
  Id.run do
    -- do
      -- something
    for (i, x) in xs.mapIdx (·, ·)do
      bar i x where
  bar := fun _ _ => ()

Formatters are either implemented as Formatters or (most of the time) automatically generated. To control the automatic formatter, there are formatting primitives that can be used when defining a new notation, such as ppLine, which emits a hard line break, or ppSpace, which emits a soft line break that can be printed as either a space or a line break. I'd also like to change some of the names of these formatting primitives to make it more obvious what their purpose is.

?: Format to String

This step alone is sometimes called pretty printer in literature, so I will use this term here as well. Up until now, I looked into three language independent pretty printers, listed below. All of those are based on an algebra desribing the semantics of their Format combinators. (The relevant data type is usually called Doc instead of Format).

• Hughes' pretty printer, which can be too greedy when processing long lines.
• Wadler/Leijen's pretty printer, which is also greedy, but delivers good results otherwise. This is the one that is currently used in Lean.
• Bernardy's pretty printer, which is not greedy and allows dynamic indentation (example below). Even though it's not greedy, it's supposed to have linear complexity in the input size (after optimizations), but it's still aroumd 6 - 10 times slower than the Wadler/Leijen pretty printer. It is also unclear if we would want to use dynamic indentation in Lean at all.

Example of constant and dynamic indentation:

-- constant indentation (all items have a fixed indentation of 2)
foo [
  a,
  b,
  c]

-- dynamic indentation (all items after the first one are aligned with the beginning of the first item)
foo [a,
     b,
     c]

My current idea is to keep the Wadler/Leijen pretty printer, but refactor it to make it more understandable and extensible. One possible extension could be anchors, which are necessary for the alignment of e.g. match cases.

match x? with
-- align all `=>`s
| .some x => _
| .none   => _

Testing the Pretty Printer

You can easily test the current pretty printer by using the linter API. This will show you an info message with the formatted code for each command.

import Lean.Elab.Command
import Lean.PrettyPrinter

open Lean Lean.Elab.Command Lean.PrettyPrinter

def testPrettyPrinter : Linter := fun stx => do
  let width := 80

  let fmt ← liftCoreM <| ppTerm (TSyntax.mk stx)
  let str := fmt.pretty width

  logInfoAt stx str

initialize addLinter testPrettyPrinter

Start with the Lean.PrettyPrinter API and the formatter primitives described in the issue, then run the provided linter example to inspect current output. Review the formatter and Format-to-String stages, including the existing Wadler/Leijen pretty printer and possible anchor support. Done requires an agreed formatting design and a clearer, extensible implementation.