# Assistant conversation 37GRNM - Canonical URL: - Resource IRI: - Type: assistant conversation - Mode: chat ## Transcript ### 1. User Import the attached PDF documents. [Uploaded PDFs] - pretty-expressive.pdf: Sheaf file #JNQPZT ### 2. Assistant tool calls #### Tool call: `document_import` ```json { "action": "stage", "file_ids": [ "JNQPZT" ], "name": "Import pretty-expressive.pdf" } ``` ### 3. Tool result: document_import { "status": { "counts": { "pending": 1 }, "files": [ { "error": null, "status": "pending", "file_id": "JNQPZT", "execution_id": null } ] }, "sources": [], "action": "stage", "run_id": "VGNEJT", "file_ids": [ "JNQPZT" ], "run_iri": "https://m.sheaf.less.rest/VGNEJT" } ### 4. Assistant tool calls #### Tool call: `document_import` ```json { "action": "extract", "run_id": "VGNEJT" } ``` ### 5. Tool result: document_import { "status": { "counts": { "completed": 1 }, "files": [ { "error": null, "status": "completed", "file_id": "JNQPZT", "execution_id": "pex_VaH08A7rtlZZ" } ] }, "action": "extract", "completed": 1, "run_id": "VGNEJT", "submitted": 1 } ### 6. Assistant tool calls #### Tool call: `document_import` ```json { "action": "inspect", "run_id": "VGNEJT" } ``` ### 7. Tool result: document_import { "status": { "counts": { "completed": 1 }, "files": [ { "error": null, "status": "completed", "file_id": "JNQPZT", "execution_id": "pex_VaH08A7rtlZZ" } ] }, "action": "inspect", "run_id": "VGNEJT", "files": [ { "status": "completed", "file_id": "JNQPZT", "quality": { "blocks": 478, "pages": 34, "math_expressions": 890, "page_continuations": 4, "block_types": { "Caption": 24, "Equation": 11, "Figure": 5, "Footnote": 21, "ListGroup": 17, "PageFooter": 33, "PageHeader": 67, "SectionHeader": 43, "Table": 6, "Text": 251 }, "empty_equation_blocks": 0, "equation_blocks": 11, "pages_with_math": 32 }, "output_path": "/home/mbrock/sheaf.mikael/var/datalab/VGNEJT/JNQPZT.datalab.json" } ] } ### 8. Assistant tool calls #### Tool call: `document_import` ```json { "action": "import", "run_id": "VGNEJT" } ``` ### 9. Tool result: document_import { "next": "Resolve metadata and validate reader pages. Search indexing is continuing in the background.", "action": "import", "documents": [ { "status": "imported", "title": null, "file_id": "JNQPZT", "document_id": "F3YZ79", "document_iri": "https://m.sheaf.less.rest/F3YZ79" } ], "run_id": "VGNEJT" } ### 10. Assistant tool calls #### Tool call: `document_import` ```json { "action": "metadata", "run_id": "VGNEJT" } ``` ### 11. Tool result: document_import { "action": "metadata", "documents": [ { "match": { "reason": "title match accepted for Crossref type journal-article", "source": "doi", "identifier": "10.1145/3622837", "doi": "10.1145/3622837", "score": 1.0, "accept?": true, "crossref_title": "A Pretty Expressive Printer", "crossref_type": "journal-article" }, "metadata": { "title": "A Pretty Expressive Printer (with Appendices)", "usage": { "cost": { "total": 0.001425, "tokens": 0.001425, "tools": 0.0, "storage": 0.0, "images": 0.0, "input_cost": 0.001182, "output_cost": 2.43e-4, "reasoning_cost": 0.0, "line_items": [ { "count": 4728, "id": "token.input", "kind": "tokens", "component": "token.input", "cost": 0.001182, "quantity": 4728 }, { "count": 162, "id": "token.output", "kind": "tokens", "component": "token.output", "cost": 2.43e-4, "quantity": 162 } ] }, "output_tokens": 162, "input_tokens": 4728, "total_cost": 0.001425, "reasoning_tokens": 0, "input_cost": 0.001182, "output_cost": 2.43e-4, "reasoning_cost": 0.0, "cached_tokens": 0, "total_tokens": 4890, "tool_usage": {}, "image_usage": {}, "cache_creation_tokens": 0 }, "year": "2023", "model": "google:gemini-3.1-flash-lite-preview", "notes": "Published October 2023", "issue": "OOPSLA2", "pages": "Article 261", "authors": [ "Sorawee Porncharoenwase", "Justin Pombrio", "Emina Torlak" ], "doi": "10.1145/3622837", "volume": "7", "isbn": null, "source_filename": null, "publication": "Proc. ACM Program. Lang.", "confidence": "high" }, "document_id": "F3YZ79", "wrote": true } ], "run_id": "VGNEJT" } ### 12. Assistant tool calls #### Tool call: `document_import` ```json { "action": "validate", "run_id": "VGNEJT" } ``` ### 13. Tool result: document_import { "action": "validate", "documents": [ { "title": "A Pretty Expressive Printer", "valid": true, "document_id": "F3YZ79", "readable_chunks": 374, "reader_path": "/F3YZ79", "source_pages": 34 } ], "search_index_status": "search", "run_id": "VGNEJT", "embedding_status": "updating", "embedding_errors": 0, "search_index_message": "Updating text search · another refresh is queued · another refresh is queued" } ### 14. Assistant Imported and validated **A Pretty Expressive Printer** by Sorawee Porncharoenwase, Justin Pombrio, and Emina Torlak (2023). - Document: #F3YZ79 - DOI: `10.1145/3622837` - 34 pages; 374 readable chunks - Search indexing is updating in the background. ### 15. User great let's give it a cool cover art and a micro abstract too ### 16. Assistant tool calls #### Tool call: `get_document` ```json { "id": "F3YZ79" } ``` ### 17. Tool result: get_document DOCUMENT #F3YZ79 Title: A Pretty Expressive Printer Outline: - 1 #QBL3FX A Pretty Expressive Printer (with Appendices) - 1.1 #P22H2B ACM Reference Format: - 1.2 #JMLCZ2 1 INTRODUCTION - 1.3 #ZVVSF8 2 RELATED WORK - 1.3.1 #J2HRAG 2.1 Traditional Printers - 1.3.2 #82ME5U 2.2 Arbitrary-Choice Printers - 1.3.3 #WMC7GF 2.3 Other Printers - 1.4 #XYLN59 3 AN OVERVIEW OF \Pi_e - 1.4.1 #JMZ2NM 3.2 Cost Factory - 1.4.2 #KNV5KS 3.3 \mathcal{W}, the Computation Width Limit - 1.5 #89N59D 4 THE SEMANTICS OF \Sigma_e - 1.5.1 #AE2PYX 4.1 Layouts - 1.5.2 #SSVNFP 4.2 The Formal Semantics of \Sigma_e - 1.6 #T4R6VJ 5 A FRAMEWORK TO REASON ABOUT EXPRESSIVENESS - 1.6.1 #VJC9GT 5.1 The Extended Semantics - 1.6.2 #4MZNU8 5.2 Functional Completeness - 1.6.3 #M4EULF 5.3 Definability - 1.7 #XE9QFA 6 OUR PRINTER, \Pi_e - 1.7.1 #MLEC9U 6.1 Overview - 1.7.2 #VLZ4EC 6.2 Measure - 1.7.3 #ELDRZE 6.3 Measure Set - 1.7.4 #HKZMVQ 6.4 The Document Structure - 1.7.5 #QL5RWL 6.5 The Resolver - 1.7.6 #WEESMY 6.6 Correctness of \Pi_e - 1.7.7 #9NTX7Y 6.7 Handling Flattening - 1.8 #FWYL7E 7 IMPLEMENTATION - 1.9 #UF75XA 8 EVALUATION - 1.9.1 #BZPCRM 8.1 Comparison of Printers - 1.9.2 #A67QMA 8.2 Racket Code Formatter - 1.9.3 #A3EJM6 8.3 Results - 1.10 #35Q3DM 9 CONCLUSION - 1.11 #2AAR7Z DATA-AVAILABILITY STATEMENT - 1.12 #JT5SHP ACKNOWLEDGMENTS - 1.13 #UYECAF A AN ANALYSIS OF PRINTERS - 1.14 #Y93RME B SELECTED PROOF SKETCHES - 1.15 #F6MBTZ C DISCUSSION - 1.15.1 #8L2AHS C.1 Additional Constructs - 1.15.2 #2SM3PJ C.2 Safety - 1.15.3 #FG8E7U C.3 Memoization - 1.15.4 #L2W8KZ C.4 Fusing Resolving and Rendering - 1.15.5 #CZJ9CG C.5 Handling Bias in the Presence of Taintedness - 1.15.6 #ERNNJN C.6 Partial Evaluation - 1.16 #S4HGC5 REFERENCES ### 18. Assistant tool calls #### Tool call: `read` ```json { "blocks": [ "JMLCZ2" ], "expand": true } ``` #### Tool call: `read` ```json { "blocks": [ "35Q3DM" ], "expand": true } ``` ### 19. Tool result: read DOCUMENT #F3YZ79 A Pretty Expressive Printer SECTION #JMLCZ2 1 INTRODUCTION EXCERPT #9LTW6L p. 0 General-purpose pretty printers (or, simply, printers ) are widely used to convert structured data—typically an AST—into human-readable text. Their applications include code reformatting, software reengineering, and synthesized code printing [De Jonge 2002; Prettier 2016; Torlak and Bodik 2014; Yelland 2015]. These printers take as inputs (1) a document in a pretty printing language (PPL), which encodes the structured data along with formatting choices, and (2) a page width limit. Choices in the document can yield exponentially many possible layouts. The task of the printers is then to efficiently choose an optimal layout from all possible layouts. Existing printers use a variety of built-in optimality objectives. A good objective reflects the informal notion of “prettiness,” such as not overflowing past the page width limit whenever possible, while having as few lines as possible. EXCERPT #VF6N2D p. 0 Authors’ addresses: Sorawee Porncharoenwase, Paul G. Allen School of Computer Science & Engineering, University of Washington, Seattle, WA, USA, sorawee@cs.washington.edu; Justin Pombrio, Unaffiliated, Cambridge, MA, USA, jpombrio@cs.brown.edu; Emina Torlak, Paul G. Allen School of Computer Science & Engineering, University of Washington, Seattle, WA, USA, emina@cs.washington.edu. EXCERPT #4Z52DY p. 0 Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for third-party components of this work must be honored. For all other uses, contact the owner/author(s). EXCERPT #G5HJAP p. 0 © 2023 Copyright held by the owner/author(s). EXCERPT #YVSCPH p. 0 2475-1421/2023/10-ART261 EXCERPT #E43QJQ p. 0 https://doi.org/10.1145/3622837 EXCERPT #HBJQTT p. 0 EXCERPT #6BAPG9 p. 0 EXCERPT #DMW5NK p. 1 EXCERPT #LVJ3WU p. 1 EXCERPT #NQXPXH p. 1 Different printers make different trade-offs in the expressiveness of the PPL, the optimality objective, and the performance . This paper presents a printer that we call \Pi_e . It targets \Sigma_e , a PPL that is strictly more expressive than all published PPLs. This can be shown via our formal framework for reasoning about the expressiveness of PPLs. \Pi_e is parameterized by a cost factory , which enables users to specify an optimality objective for \Pi_e to minimize. The cost factory is versatile. For example, it can express non-linear costs and define concepts such as soft page width limits [Yelland 2016]. As a result, the optimal layout that \Pi_e chooses can have higher quality compared to existing printers. The time complexity of \Pi_e is O(nW^4) , where n is the size of the document and W is the computation width limit (defined in Section 6). This is better than the time complexity of many printers in the literature, and it is improved to O(nW^3) when \Pi_e is restricted to process documents in some well-known but less expressive PPLs. We prove the correctness of \Pi_e in the Lean theorem prover [Moura and Ullrich 2021], ensuring the validity and optimality of the output layout, and demonstrate \Pi_e 's efficiency by evaluating our implementation of \Pi_e , which we call PRETTYEXPRESSIVE. We believe these attributes make \Pi_e not only a good printer by itself, but also a good building block to construct other derived printers. EXCERPT #SVC2WR p. 1 A Survey of Printers in the Wild. To evaluate \Pi_e , we conducted a broad survey of the literature on pretty printing. Most PPLs, embedded in a host programming language, provide a small set of core constructs that allow users to create a document with text, concatenate documents together, set indentation level, and express formatting choices. High-level constructs can then be built on top of the core constructs. The details of these core constructs can differ from PPL to PPL. We found that there are two main schools of PPLs in the wild, which we call the traditional and arbitrary-choice PPLs. The traditional PPL centers around manipulation of nls (newlines) and current indentation level, while the arbitrary-choice PPL is characterized by the ability to express arbitrary formatting choices and the use of aligned concatenation to supplant the concept of indentation level. Figure 1 illustrate documents in both PPLs that pretty-print the function definition append in a hypothetical programming language with slightly different styling. EXCERPT #FPNGWP p. 1 Expressiveness. The literature contains informal claims about the expressiveness of PPLs [Chitil 2005; Podkopaev and Boulytchev 2015; Wadler 2003]. We develop two formal notions of expressiveness: the ability to express layouts and the ability to express features . The former reflects the functionality of a PPL, while the latter reflects the ease of document construction. Using our framework, we can show that neither the traditional PPL nor the arbitrary-choice PPL is more expressive than the other. For example, the set of layouts in Figure 1b cannot be expressed by any document in the traditional PPL. This is because all layouts due to a particular document in the traditional PPL must be the same modulo whitespace, but one of the layouts in the figure has an extra pair of parentheses. 1 As another example, the document in Figure 1b is awkwardly constructed, because the document structure and the underlying AST structure do not match (Section 5.3). It would be more natural to use unaligned concatenation, but the feature cannot be expressed by any combination of features in the arbitrary-choice PPL. 2 To that end, we develop a PPL called \Sigma_e that is strictly more expressive than both the traditional and arbitrary-choice PPLs, facilitating both functionality and ease of document construction. EXCERPT #MKCMXT p. 1 1 Languages such as Python require an extra pair of parentheses around an expression that spans multiple lines [The Python Language Reference 2010]. Similarly, some styles prefer adding an extra comma (also known as trailing comma) when a function call spans multiple lines [ESLint 2014]. Hence, the ability to express layouts with differing content is desirable. EXCERPT #6CANRK p. 1 2 Different programming language styles prefer different concatenation operators. C-like languages heavily use unaligned concatenation, while aligned concatenation has been used for Haskell, Lisp, R, and Julia. However, there are instances where C-like languages would benefit from aligned concatenation, and Haskell would benefit from unaligned concatenation. EXCERPT #AXJ4ZH p. 1 EXCERPT #YPU5XL p. 2 EXCERPT #8VE893 p. 2 EXCERPT #N5YB96 p. 2 text "function_append(first,second,third){" 1 function append(first,second,third){ <> nest 4 ( 2 return first + let f = text "first_+" in 3 second + let s = text "second_+" in 4 third let t = text "third" in 5 } nl <> text "return_" <> group (nest 4 (f <> nl <> s <> nl <> t)) 1 function append(first,second,third){ ) <> nl <> text "}" } 2 return first + second + third 3 } EXCERPT #9UFA4U p. 2 (a) A document in the traditional PPL and its corresponding layouts. The nest construct increments the current indentation level by some specified amount, causing nl (newline) to insert indentation spaces. <> is the unaligned concatenation operator, which places the right sub-layout after the left sub-layout on the current indentation level. Lastly, the group construct creates a choice between two alternatives: one where the sub-layouts are left alone and one where the sub-layouts are flattened by replacing newlines and indentation spaces due to nls in the group with single spaces. EXCERPT #89YA99 p. 2 text "function_append(first,second,third){" <> 1 function append(first,second,third){ ( let f = text "first_+" in 2 return ( let s = text "second_+" in 3 first + let t = text "third" in 4 second + let sp = text " " in 5 third let ret = text "return_" in 6 ) text "..." <> 7 } (((ret <> text "(") <> (text "..." <> (f <> s <> t)) <> text ")") <> (ret <> f <> sp <> s <> sp <> t)) <> text "}" } 1 function append(first,second,third){ 2 return first + second + third 3 } EXCERPT #YDX7QL p. 2 (b) A document in the arbitrary-choice PPL and its corresponding layouts. <|> is the arbitrary-choice operator, which per its namesake, creates a choice between the layouts of two arbitrary sub-documents. <> is the vertical concatenation operator, which joins two sub-layouts with a newline. Lastly, <>> is the aligned concatenation operator, which joins two sub-layouts horizontally, aligning the whole right sub-layout at the column where it is to be placed in. EXCERPT #FXT5YH p. 2 Fig. 1. The traditional and arbitrary-choice PPLs, embedded in the host language OCaml. Colored regions in a document and corresponding layouts indicate the correspondence between the colored sub-documents and the colored sub-layouts. We use the let construct to make the documents easier to read, even though it is usually not a part of PPLs. Dotted lines illustrate different page width limits at 22 and 36 characters. EXCERPT #28MJKQ p. 2 Optimality. The optimality objective of a printer indicates what it optimizes for when resolving choices. Most printers targeting the traditional PPL minimize overflow past the page width limit line-by-line, preferring a longer line when there is no overflow. For example, given the document in Figure 1a, the first layout is optimal when the page width limit is 22 (red dotted line), while the second layout is optimal when the page width limit is 36 (green dotted line). Contrary to prior claims [Chitil 2005; Wadler 2003], we discovered that this strategy guarantees neither the absence of overflow whenever possible nor the minimality of the number of lines. By contrast, most printers targeting the arbitrary-choice PPL minimize the number of lines among layouts with no overflow. However, they error when all possible layouts have an overflow, resulting in a poor user experience (e.g., when the page width limit is 22 in Figure 1b). Recognizing that unavoidable overflows do occur in practice, we introduce the concept of a cost factory , which allows users to choose a desired objective permitted by its interface, including an objective that tolerates overflow gracefully. EXCERPT #CYAU3K p. 2 EXCERPT #H4NBCL p. 3 EXCERPT #YCN9EH p. 3 EXCERPT #ZEKFVH p. 3 Performance. Printing proceeds in two phases: resolving choices and rendering the optimal choice to text (although many printers fuse these two phases together). Time complexity of printers is best measured against the resolving phase 3 , and it is usually specified with two parameters: the size of the document n and the width limit W , with the preference that the time complexity be polynomial in W and linear in n . Most printers in the literature leave their time complexity unanalyzed, instead opting to show experimental results that their implementations are efficient in practice. We analyze these printers and demonstrate documents that trigger worse than linear time behavior (in n ) on some printers. Further complication arises in printers with the arbitrary choice feature, which gives rise to documents that are structured as DAGs as opposed to trees. We show that many printers that treat the input document as a tree suffer from a combinatorial explosion as the DAG structure is unfolded during the resolving phase, resulting in exponential time complexity. With a combination of proof and experimental results, we show that the time complexity of \Pi_e is linear in the DAG size of the document and that it runs fast in practice. EXCERPT #V7KTQZ p. 3 In summary, this paper makes the following contributions: EXCERPT #Z364AX p. 3 • A new PPL called \Sigma_e that is strictly more expressive than all published PPLs. The constructs in \Sigma_e are not new, but packaging them all in a single PPL has never been done before. • A printer \Pi_e targeting \Sigma_e that utilizes a cost factory to allow a variety of optimality objectives. • A proof of correctness (validity and optimality) for \Pi_e , formalized in the Lean theorem prover. To our knowledge, this is the first time that a printer has been formally verified. • A framework to formally reason about the expressiveness of PPLs. • A survey of printers and an analysis that dispels common misunderstandings about them. • An implementation of \Pi_e , PRETTYEXPRESSIVE, and an evaluation that shows its effectiveness. EXCERPT #6EVTAG p. 3 The rest of this paper is structured as follows. Section 2 surveys the related work. Section 3 provides an overview of \Pi_e from the user’s perspective. Section 4 presents the formal semantics of \Sigma_e . Section 5 introduces a framework to reason about the expressiveness of PPLs. Section 6 formally presents \Pi_e and its analysis. Section 7 discusses PRETTYEXPRESSIVE, an implementation of \Pi_e . Section 8 presents an evaluation of PRETTYEXPRESSIVE that demonstrates its effectiveness. Lastly, Section 9 concludes the paper. ### 20. Tool result: read DOCUMENT #F3YZ79 A Pretty Expressive Printer SECTION #35Q3DM 9 CONCLUSION EXCERPT #H6FRCG p. 25 We have described \Pi_e , an expressive printer that supports a variety of optimality objectives and is practically efficient. We developed a framework for reasoning about the expressiveness of PPLs, and we used this framework to guide the design of the PPL that \Pi_e targets. By surveying existing pretty printers, we have shown that \Pi_e is well-placed in the design space of printers. \Pi_e is proven correct in the Lean theorem prover and implemented as a practical printer PRETTYEXPRESSIVE, which powers a real-world code formatter for the Racket programming language. Our results show that PRETTYEXPRESSIVE (and \Pi_e ) is both pretty and fast. ### 21. Assistant tool calls #### Tool call: `generate_image` ```json { "prompt": "Portrait-format editorial cover art for a computer science research paper titled “A Pretty Expressive Printer.” Create an elegant, futuristic visualization of structured code transforming into beautifully formatted text: on the left, a dense branching abstract syntax tree made of fine luminous cyan and violet lines; through the center, multiple alternative layout paths fan out like ribbons and are evaluated by subtle geometric cost contours; on the right, they resolve into crisp, harmonious columns and lines on an implied page. Include a restrained visual hint of formal verification through precise theorem-like symbols and a faint proof-grid, but no readable formulas and no logos. Deep charcoal-black background, electric cyan, violet, magenta, and warm white accents; sophisticated generative geometry, high contrast, clean Swiss editorial composition, subtle paper texture, premium academic-tech aesthetic. Leave generous breathing room near the top for interface title overlay. No embedded title, no words, no watermarks, no photorealistic printer hardware." } ``` ### 22. Tool result: generate_image GENERATED IMAGE #Y4V6LW URL: /images/Y4V6LW Model: gpt-image-2 Prompt: Portrait-format editorial cover art for a computer science research paper titled “A Pretty Expressive Printer.” Create an elegant, futuristic visualization of structured code transforming into beautifully formatted text: on the left, a dense branching abstract syntax tree made of fine luminous cyan and violet lines; through the center, multiple alternative layout paths fan out like ribbons and are evaluated by subtle geometric cost contours; on the right, they resolve into crisp, harmonious columns and lines on an implied page. Include a restrained visual hint of formal verification through precise theorem-like symbols and a faint proof-grid, but no readable formulas and no logos. Deep charcoal-black background, electric cyan, violet, magenta, and warm white accents; sophisticated generative geometry, high contrast, clean Swiss editorial composition, subtle paper texture, premium academic-tech aesthetic. Leave generous breathing room near the top for interface title overlay. No embedded title, no words, no watermarks, no photorealistic printer hardware. ### 23. Assistant tool calls #### Tool call: `update_document_metadata` ```json { "cover_image_id": "Y4V6LW", "document_id": "F3YZ79", "micro_abstract": "Introduces an expressive pretty-printing language and a formally verified, practical printer that selects optimal layouts using customizable cost objectives while remaining efficient on real-world formatters." } ``` ### 24. Tool result: update_document_metadata Updated metadata for #F3YZ79: cover_image_id, micro_abstract ### 25. Assistant Updated **A Pretty Expressive Printer** #F3YZ79 with: - New generated cover art #Y4V6LW - Micro abstract: “Introduces an expressive pretty-printing language and a formally verified, practical printer that selects optimal layouts using customizable cost objectives while remaining efficient on real-world formatters.”