A Pretty Expressive Printer (with Appendices)

TL;DR

This paper introduces PrettyExpressive, a highly expressive pretty printer that guarantees optimal document layout, verified for correctness using the Lean theorem prover, and demonstrates efficiency and practical adoption in Racket code formatting.

Contribution

It presents a new pretty printer, $ Pi_e$, that is more expressive and has better time complexity than existing solutions, with formal correctness guarantees.

Findings

PrettyExpressive is more expressive than existing pretty printers.

It guarantees optimal document layouts based on user-defined cost functions.

It is efficient and has been adopted in real-world Racket code formatting.

Abstract

Pretty printers make trade-offs between the expressiveness of their pretty printing language, the optimality objective that they minimize when choosing between different ways to lay out a document, and the performance of their algorithm. This paper presents a new pretty printer, $\Pi_e$, that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of $\Pi_e$ is better than many existing pretty printers. When choosing among different ways to lay out a document, $\Pi_e$ consults a user-supplied cost factory, which determines the optimality objective, giving $\Pi_e$ a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of $\Pi_e$, and implement $\Pi_e$ concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty printer against others, we develop a formal framework for reasoning about the expressiveness of pretty printing languages, and survey pretty printers in the literature, comparing their expressiveness, optimality, worst-case time complexity, and practical running time. Our evaluation shows that PrettyExpressive is efficient and effective at producing optimal layouts. PrettyExpressive has also seen real-world adoption: it serves as a foundation of a code formatter for Racket.