A Pretty Expressive Printer (with Appendices)
| Autor: | Porncharoenwase, Sorawee, Pombrio, Justin, Torlak, Emina |
|---|---|
| Rok vydání: | 2023 |
| Předmět: | |
| Druh dokumentu: | Working Paper |
| Popis: | 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. Comment: 34 pages. This is the full version (with appendices) of the OOPSLA 2023 paper "A Pretty Expressive Printer." |
| Databáze: | arXiv |
| Externí odkaz: |
|