A Pretty Expressive Printer (with Appendices)
Sorawee Porncharoenwase, Justin Pombrio, Emina Torlak

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, , that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of is better than many existing pretty printers. When choosing among different ways to lay out a document, consults a user-supplied cost factory, which determines the optimality objective, giving a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of , and implement concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty…
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsArtificial Intelligence in Games · Data Visualization and Analytics · Video Analysis and Summarization
