tiny.pretty

Overview · API · Code relationships · Verification · Audit

Overview

Pretty is a width-aware document layout and structured output package.

Design rationale and problem model

Pretty printing separates declarative document structure from geometric layout to resolve formatting choices without output backtracking: formatters cannot determine whether an expression fits on a single line until both the expression and its trailing syntactic context are known. An algebraic tree (Doc) defers line-break selection to the renderer.

The package enforces strict separation between construction and rendering:

• Construction: Builder allocates AST nodes using any caller-supplied allocator, while text nodes borrow source slices. Callers bear the obligation of ensuring both allocated nodes and borrowed slices remain valid until rendering finishes.
• Traversal: The layout pass (write, writeWithState) performs zero dynamic allocation, streaming directly to a caller-owned *std.Io.Writer. Callers retain control over output buffering, flush timing, and I/O side effects, trading automated memory management for zero-allocation rendering. Where an owned slice is required, renderAlloc manages an allocating writer.

Continuation-sensitive layout and mode inheritance

Line-break decisions require continuation lookahead: evaluating a group in isolation is insufficient because trailing tokens on the same line (such as closing delimiters or commas) could force an immediate overflow. The renderer therefore tests whether the candidate and its inline sibling continuation fit the saturating remaining width width -| col.

Mode inheritance is deliberately asymmetric:

• A flat parent forces all descendant groups into flat mode, because an inner line break would contradict the parent's single-line commitment.
• A broken parent permits nested groups to choose independently, allowing localized compaction of sub-expressions within an expanded structure.

Lookahead revisits subtrees to measure flat width prior to emission, and recursive descent operates without an explicit stack ceiling. Unconditional breaks (hardline) emit a newline followed by the current nesting indentation in all modes.

Layout metrics, control breaks, and styling

Column advancement strictly measures raw byte length (bytes.len), omitting Unicode scalar, grapheme, and terminal display-width semantics. Raw escape bytes inside text count as bytes. When indivisible text exceeds the margin, it emits across it without error, prioritizing semantic data preservation over rigid column boundaries.

Only carriage returns and line feeds reset the column:

• In text, \r and \n reset column tracking, where CR alone produces zero line feeds. They do not insert structural indentation.
• In soft breaks, alternatives containing CR or LF force broken mode to prevent broken control characters from polluting flat layout.

Semantic styling (styled) emits ANSI sequences under ColorMode.ansi. These escape sequences consume zero layout columns, ensuring monochrome and styled outputs make identical line-break decisions.

Worked example: Why continuation lookahead matters

The trailing-continuation witness from test.zig demonstrates why groups cannot evaluate fit in isolation:

1const grouped = try builder.group(try builder.concat(&.{2    builder.text("abc"),3    pretty.softline,4    builder.text("de"),5}));6const doc = try builder.concat(&.{ grouped, builder.text("XY") });

At width 6, grouped alone has a flat width of 6 ("abc de"). Evaluated in isolation, it would fit flat. However, trailing sibling "XY" shares the same output line without an intervening break, requiring 8 columns total.

Continuation lookahead inspects "XY", detects that $6+2>6$, and forces grouped to break, emitting "abc\ndeXY" instead of overflowing to "abc deXY".

Verification boundary

Evidence is partitioned across formal models and test suites:

• Formal model: The Lean specification in verification/pretty/ proves compositionality and layout properties for finite trees over abstract byte classes (cell, LF, CR) and unbounded natural numbers (Nat). It assumes successful writes and omits continuation lookahead, machine usize saturation, and display width. No formal theorem proves that the Zig implementation refines the Lean specification.
• Empirical and capacity evidence: Automated unit tests in test.zig and Hypothesis property tests in src/properties/ test ANSI neutrality, saturating arithmetic, and position composition, while bounded table capacity contracts are declared in compact/table.zig.

Definitions

Actions

Public operations.

• writeWithState
• write
• renderAlloc

Types and contracts

Public types and contracts.

• Builder
• ColorMode
• Doc
• FlatFitWriter
• LayoutOptions
• Nested
• RenderError
• Style
• Styled
• WriteState
• TextWriter: Adapts incremental text production to the Pretty renderer without allocating.

Namespaces

Public namespaces.

• compact: Bounded tables for compact terminal and agent output.
• json: Deterministic JSON escaping, tree rendering, and allocation-free streaming.
• diagnostic

Values and defaults

Public values and defaults.

• default_width
• hardline
• softbreak
• softline

Code relationships

Direct static dependencies extracted from parsed source by semantic graph analysis.

Uses: tiny.coz, tiny.sdfii, tiny.smg
Used by: tiny.choir, tiny.glom, tiny.smg, tiny.tracy

Verification

No verification records are cataloged for this module in this build.

Audit