← All papers
A Pretty Expressive Printer (with Appendices)
cs.PL
Oct 2, 2023 · v1
TL;DR
Uses Lean to formally verify correctness and optimality of the pretty printing algorithm.
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 that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, its time complexity is better than many existing pretty printers. When choosing among different ways to lay out a document, the printer consults a user-supplied cost factory, which determines the optimality objective, giving it a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of the algorithm, and implement it concretely as a pretty printer called PrettyExpressive that has seen real-world adoption as a foundation of a code formatter for Racket.
Problem
Pretty printers must balance expressiveness of their layout language, optimality of the chosen layout, and algorithmic performance. No existing pretty printer simultaneously maximizes expressiveness while provably minimizing an optimality objective with competitive time complexity.
Approach
The authors present a pretty printer that is strictly more expressive than all prior pretty printers and provably minimizes a user-supplied cost factory objective. Correctness (validity and optimality) of the algorithm is verified using the Lean theorem prover.
Results
The resulting pretty printer, PrettyExpressive, has better time complexity than many existing pretty printers and has seen real-world adoption as the foundation of a code formatter for Racket.