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.

翻译：美化打印机在表达力、布局优化目标及算法性能之间进行权衡。本文提出了一种新型美化打印机 $\Pi_e$，其表达力严格优于现有所有美化打印机，且被证明能最小化优化目标。此外，$\Pi_e$ 的时间复杂度优于许多现有美化打印机。在选择文档布局方案时，$\Pi_e$ 采用用户提供的成本工厂（cost factory）来确定优化目标，从而赋予了 $\Pi_e$ 独特的灵活性。我们使用 Lean 定理证明器验证了 $\Pi_e$ 的正确性（有效性和最优性），并将其具体实现为名为 PrettyExpressive 的美化打印机。为评估该打印机与同类的性能差异，我们构建了用于分析美化打印语言表达力的形式化框架，并对现有文献中的美化打印机进行调研，比较其表达力、最优性、最坏时间复杂度及实际运行时间。评估结果表明，PrettyExpressive 在生成最优布局方面高效且有效。该工具已被实际应用：它作为 Racket 代码格式化工具的基础组件。