prose: infix + paren elision + doc-wrap + nested-match (iter 20b)

Eleven binary builtins (+ - * / % == != < <= > >=) render as
lhs op rhs when called with two args (tail-flagged keeps prefix).
Standard Rust-aligned 4-level precedence table elides parens.
not(x) renders as !x. Long /// doc strings wrap at 80 cols on
word boundaries.

bench_list_sum: 'if ==(n, 0)' becomes 'if n == 0', '+(acc, h)'
becomes 'acc + h', tail keyword still visible on tail calls.

19 new unit tests (47 total). 4 snapshots (3 re-rendered + 1 new
bench fixture). Public API unchanged.

crates/ailang-prose/src/lib.rs

@@ -81,15 +81,59 @@ fn write_def(out: &mut String, def: &Def, level: usize) {
 
 fn write_doc(out: &mut String, doc: &Option<String>, level: usize) {
     if let Some(d) = doc {
-        for line in d.split('\n') {
-            indent(out, level);
-            out.push_str("/// ");
-            out.push_str(line);
-            out.push('\n');
+        // Polish 4 (Iter 20b): wrap long lines at 80 columns.
+        // Algorithm: split on explicit '\n' first (each piece is its own
+        // logical line). Then for each piece, greedy-wrap at word
+        // boundaries so that `<indent>/// <text>` fits in 80 cols.
+        // An empty logical line stays a single empty `///` line.
+        let prefix_cols = level * 2 + 4; // `<indent>/// ` width
+        let target = 80usize;
+        // If the prefix already eats the whole budget, fall back to no
+        // wrap (one word per line is worse than overflow).
+        let budget = target.saturating_sub(prefix_cols).max(1);
+        for piece in d.split('\n') {
+            for wrapped in wrap_words(piece, budget) {
+                indent(out, level);
+                out.push_str("/// ");
+                out.push_str(&wrapped);
+                out.push('\n');
+            }
         }
     }
 }
 
+/// Greedy word-boundary wrap. Returns at least one element (possibly
+/// empty when `piece` is empty). Words longer than `budget` are placed
+/// on their own line and overflow — splitting inside a word would
+/// destroy identifiers.
+fn wrap_words(piece: &str, budget: usize) -> Vec<String> {
+    if piece.is_empty() {
+        return vec![String::new()];
+    }
+    let mut out: Vec<String> = Vec::new();
+    let mut current = String::new();
+    for word in piece.split_whitespace() {
+        if current.is_empty() {
+            current.push_str(word);
+        } else if current.len() + 1 + word.len() <= budget {
+            current.push(' ');
+            current.push_str(word);
+        } else {
+            out.push(std::mem::take(&mut current));
+            current.push_str(word);
+        }
+    }
+    if !current.is_empty() {
+        out.push(current);
+    }
+    if out.is_empty() {
+        // `piece` was non-empty but all-whitespace. Preserve as one
+        // empty line rather than dropping it.
+        out.push(String::new());
+    }
+    out
+}
+
 fn write_type_def(out: &mut String, td: &TypeDef, level: usize) {
     write_doc(out, &td.doc, level);
     indent(out, level);
@@ -301,7 +345,116 @@ fn write_type(out: &mut String, t: &Type) {
 
 // ---- terms ----------------------------------------------------------------
 
+// Precedence ladder for paren elision (Iter 20b, Polish 2). Higher = binds
+// tighter; an atomic form (var / literal / call / ctor / lambda / match /
+// if / let / do / clone / reuse-as) sits at PREC_ATOMIC and never needs
+// to wrap itself. PREC_NONE is the top-level (caller asks for no
+// outer parens).
+const PREC_NONE: u8 = 0;
+const PREC_EQ: u8 = 1; //  == !=          (non-assoc)
+const PREC_REL: u8 = 2; // <  <= >  >=    (non-assoc)
+const PREC_ADD: u8 = 3; // +  -           (left-assoc)
+const PREC_MUL: u8 = 4; // *  /  %        (left-assoc)
+const PREC_ATOMIC: u8 = 5;
+
+/// Precedence + associativity of a canonical binary op name. Returns
+/// `None` for any non-canonical name. Three-tuple: (level, left_assoc).
+/// Non-assoc ops report `left_assoc = false`; for them we additionally
+/// bump both sides to `level + 1` so same-level chains always wrap.
+fn binop_info(name: &str) -> Option<(u8, bool)> {
+    Some(match name {
+        "*" | "/" | "%" => (PREC_MUL, true),
+        "+" | "-" => (PREC_ADD, true),
+        "<" | "<=" | ">" | ">=" => (PREC_REL, false),
+        "==" | "!=" => (PREC_EQ, false),
+        _ => return None,
+    })
+}
+
+/// Detect a `Term::App` of a canonical binary operator with exactly two
+/// args and no `tail` flag. Returns the operator name + the two args.
+/// A tail-flagged binary op is rendered the old prefix way so the
+/// `tail ` keyword stays visible — that channel matters for the
+/// reader.
+fn as_binop(t: &Term) -> Option<(&str, &Term, &Term, u8, bool)> {
+    if let Term::App { callee, args, tail } = t {
+        if *tail || args.len() != 2 {
+            return None;
+        }
+        if let Term::Var { name } = callee.as_ref() {
+            if let Some((prec, left_assoc)) = binop_info(name) {
+                return Some((name.as_str(), &args[0], &args[1], prec, left_assoc));
+            }
+        }
+    }
+    None
+}
+
+/// Detect a `Term::App` of unary `not` (one arg, not tail). Returns the
+/// argument.
+fn as_unary_not(t: &Term) -> Option<&Term> {
+    if let Term::App { callee, args, tail } = t {
+        if *tail || args.len() != 1 {
+            return None;
+        }
+        if let Term::Var { name } = callee.as_ref() {
+            if name == "not" {
+                return Some(&args[0]);
+            }
+        }
+    }
+    None
+}
+
+/// Top-level entry into term rendering. The caller's precedence floor
+/// is `PREC_NONE`, so a binary op at the root never wraps itself. All
+/// internal recursion goes through this same fn with the appropriate
+/// `parent_prec` for the sub-position.
 fn write_term(out: &mut String, t: &Term, level: usize) {
+    write_term_prec(out, t, level, PREC_NONE);
+}
+
+fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
+    // Polish 1+2: infix binary operators with paren elision.
+    if let Some((op, lhs, rhs, prec, left_assoc)) = as_binop(t) {
+        let need_parens = prec < parent_prec;
+        if need_parens {
+            out.push('(');
+        }
+        let (lhs_floor, rhs_floor) = if left_assoc {
+            // Left-assoc: same-prec on the left elides; same-prec on the
+            // right wraps. `a - b - c` reads as `(a - b) - c`, so the
+            // right side at the same level is a different parse tree
+            // and must be paren-flagged.
+            (prec, prec + 1)
+        } else {
+            // Non-assoc (==, !=, <, …): same-prec on either side wraps.
+            // `a < b < c` is ambiguous and Rust forbids it; we keep the
+            // parens to avoid implying we accept it.
+            (prec + 1, prec + 1)
+        };
+        write_term_prec(out, lhs, level, lhs_floor);
+        out.push(' ');
+        out.push_str(op);
+        out.push(' ');
+        write_term_prec(out, rhs, level, rhs_floor);
+        if need_parens {
+            out.push(')');
+        }
+        return;
+    }
+
+    // Polish 3: unary `not` → `!arg`. Argument renders at PREC_ATOMIC,
+    // so anything below atomic (i.e. another binary op) wraps.
+    if let Some(arg) = as_unary_not(t) {
+        out.push('!');
+        write_term_prec(out, arg, level, PREC_ATOMIC);
+        return;
+    }
+
+    // Everything below this point is atomic from the precedence pov:
+    // non-binary calls, ctors, literals, vars, control-flow blocks. We
+    // never need outer parens around them — they parse as a single unit.
     match t {
         Term::Lit { lit } => write_lit(out, lit),
         Term::Var { name } => out.push_str(name),
@@ -309,13 +462,17 @@ fn write_term(out: &mut String, t: &Term, level: usize) {
             if *tail {
                 out.push_str("tail ");
             }
-            write_term(out, callee, level);
+            // Callee is rendered at PREC_ATOMIC: a binary op as callee
+            // (rare, but legal) would need parens.
+            write_term_prec(out, callee, level, PREC_ATOMIC);
             out.push('(');
             for (i, a) in args.iter().enumerate() {
                 if i > 0 {
                     out.push_str(", ");
                 }
-                write_term(out, a, level);
+                // Args sit in their own paren context — no outer prec
+                // floor. Pass NONE so binary ops inside don't wrap.
+                write_term_prec(out, a, level, PREC_NONE);
             }
             out.push(')');
         }
@@ -921,4 +1078,337 @@ mod tests {
         write_type_def(&mut out, &td, 0);
         assert_eq!(out, "data IntList = Nil | Cons(Int, IntList)");
     }
+
+    // ======================================================================
+    // Iter 20b: formatting polish
+    // ======================================================================
+
+    /// Convenience: two-arg App of a named callee. Used pervasively in
+    /// the 20b unit tests.
+    fn binop(op: &str, lhs: Term, rhs: Term) -> Term {
+        Term::App {
+            callee: Box::new(Term::Var { name: op.into() }),
+            args: vec![lhs, rhs],
+            tail: false,
+        }
+    }
+
+    fn ivar(name: &str) -> Term {
+        Term::Var { name: name.into() }
+    }
+
+    // ---- Polish 1: infix for each canonical binary operator ----
+
+    #[test]
+    fn binop_renders_infix_for_every_canonical_op() {
+        // All 11 operators must collapse to `lhs op rhs` shape.
+        let ops = ["+", "-", "*", "/", "%", "==", "!=", "<", "<=", ">", ">="];
+        for op in ops {
+            let t = binop(op, ivar("a"), ivar("b"));
+            let expected = format!("a {op} b");
+            assert_eq!(render_term(&t), expected, "op = {op}");
+        }
+    }
+
+    #[test]
+    fn binop_with_tail_flag_keeps_prefix_form() {
+        // `tail +(a, b)` keeps the `tail` keyword visible; collapsing it
+        // to infix would erase the contract that this is a tail call.
+        let t = Term::App {
+            callee: Box::new(ivar("+")),
+            args: vec![ivar("a"), ivar("b")],
+            tail: true,
+        };
+        assert_eq!(render_term(&t), "tail +(a, b)");
+    }
+
+    #[test]
+    fn three_arg_app_of_operator_name_keeps_prefix_form() {
+        // A user-defined `+` with three args must not trigger the infix
+        // renderer — the binary-op detector is arity-2 only.
+        let t = Term::App {
+            callee: Box::new(ivar("+")),
+            args: vec![ivar("a"), ivar("b"), ivar("c")],
+            tail: false,
+        };
+        assert_eq!(render_term(&t), "+(a, b, c)");
+    }
+
+    // ---- Polish 2: paren elision by precedence ----
+
+    #[test]
+    fn higher_prec_subexpr_elides_parens() {
+        // (a * b) + c → a * b + c    (mul binds tighter than add)
+        let t = binop("+", binop("*", ivar("a"), ivar("b")), ivar("c"));
+        assert_eq!(render_term(&t), "a * b + c");
+    }
+
+    #[test]
+    fn lower_prec_subexpr_keeps_parens() {
+        // (a + b) * c → (a + b) * c   (add binds looser than mul)
+        let t = binop("*", binop("+", ivar("a"), ivar("b")), ivar("c"));
+        assert_eq!(render_term(&t), "(a + b) * c");
+    }
+
+    #[test]
+    fn left_assoc_left_chain_elides_parens() {
+        // (a + b) + c is the natural parse for `a + b + c`, so the
+        // left-side parens disappear.
+        let t = binop("+", binop("+", ivar("a"), ivar("b")), ivar("c"));
+        assert_eq!(render_term(&t), "a + b + c");
+    }
+
+    #[test]
+    fn left_assoc_right_chain_keeps_parens() {
+        // `a + (b + c)` is a *different* parse tree from `a + b + c`,
+        // so the right-side parens stay to preserve the AST shape.
+        let t = binop("+", ivar("a"), binop("+", ivar("b"), ivar("c")));
+        assert_eq!(render_term(&t), "a + (b + c)");
+    }
+
+    #[test]
+    fn non_assoc_same_level_keeps_parens_on_both_sides() {
+        // `a < b < c` is forbidden in Rust; we keep parens regardless of
+        // which side carries the same-level sub.
+        let t = binop("<", binop("<", ivar("a"), ivar("b")), ivar("c"));
+        assert_eq!(render_term(&t), "(a < b) < c");
+        let t2 = binop("<", ivar("a"), binop("<", ivar("b"), ivar("c")));
+        assert_eq!(render_term(&t2), "a < (b < c)");
+    }
+
+    #[test]
+    fn atomic_subexpr_never_wraps() {
+        // A var on either side of any op never picks up parens.
+        let t = binop("==", ivar("n"), Term::Lit { lit: Literal::Int { value: 0 } });
+        assert_eq!(render_term(&t), "n == 0");
+    }
+
+    #[test]
+    fn function_call_subexpr_in_binop_does_not_wrap() {
+        // `f(x) + 1` — calls are atomic, so the call doesn't pick up
+        // outer parens even though it sits inside a binop.
+        let call = Term::App {
+            callee: Box::new(ivar("f")),
+            args: vec![ivar("x")],
+            tail: false,
+        };
+        let t = binop("+", call, Term::Lit { lit: Literal::Int { value: 1 } });
+        assert_eq!(render_term(&t), "f(x) + 1");
+    }
+
+    // ---- Polish 3: unary `not` ----
+
+    #[test]
+    fn not_of_var_renders_as_bang_var() {
+        let t = Term::App {
+            callee: Box::new(ivar("not")),
+            args: vec![ivar("x")],
+            tail: false,
+        };
+        assert_eq!(render_term(&t), "!x");
+    }
+
+    #[test]
+    fn not_of_binop_keeps_parens() {
+        // `not(a == b)` → `!(a == b)`. The arg's prec is 1; the unary
+        // floor is PREC_ATOMIC=5; 1 < 5 means wrap.
+        let inner = binop("==", ivar("a"), ivar("b"));
+        let t = Term::App {
+            callee: Box::new(ivar("not")),
+            args: vec![inner],
+            tail: false,
+        };
+        assert_eq!(render_term(&t), "!(a == b)");
+    }
+
+    #[test]
+    fn not_of_call_does_not_wrap() {
+        // `not(f(x))` → `!f(x)`. Calls are atomic.
+        let call = Term::App {
+            callee: Box::new(ivar("f")),
+            args: vec![ivar("x")],
+            tail: false,
+        };
+        let t = Term::App {
+            callee: Box::new(ivar("not")),
+            args: vec![call],
+            tail: false,
+        };
+        assert_eq!(render_term(&t), "!f(x)");
+    }
+
+    #[test]
+    fn not_with_tail_flag_keeps_prefix_form() {
+        // Tail-flagged `not` keeps `tail` visible (mirrors binary-op
+        // policy).
+        let t = Term::App {
+            callee: Box::new(ivar("not")),
+            args: vec![ivar("x")],
+            tail: true,
+        };
+        assert_eq!(render_term(&t), "tail not(x)");
+    }
+
+    // ---- Polish 4: long doc-string wrap ----
+
+    #[test]
+    fn long_doc_string_wraps_at_eighty_cols() {
+        // 110-char single line should wrap into multiple `///` lines,
+        // each ≤ 80 cols, breaking at word boundaries.
+        let long = "This is a deliberately long documentation string designed to overflow eighty \
+                    columns and exercise the wrapping path."
+            .to_string();
+        let td = TypeDef {
+            name: "Foo".into(),
+            vars: vec![],
+            ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
+            doc: Some(long),
+            drop_iterative: false,
+        };
+        let mut out = String::new();
+        write_type_def(&mut out, &td, 0);
+        let doc_lines: Vec<&str> = out.lines().take_while(|l| l.starts_with("///")).collect();
+        assert!(doc_lines.len() >= 2, "expected wrap, got:\n{out}");
+        for line in &doc_lines {
+            assert!(line.len() <= 80, "line over 80 cols: {line:?} ({} cols)", line.len());
+        }
+        // Sanity: re-joining the words should give back the original
+        // content.
+        let rejoined: String = doc_lines
+            .iter()
+            .map(|l| l.trim_start_matches("///").trim())
+            .collect::<Vec<_>>()
+            .join(" ");
+        assert!(
+            rejoined.contains("deliberately long") && rejoined.contains("wrapping path."),
+            "lost content during wrap; rejoined = {rejoined:?}"
+        );
+    }
+
+    #[test]
+    fn short_doc_string_stays_on_one_line() {
+        // Below the 80-col threshold: no wrapping.
+        let td = TypeDef {
+            name: "Foo".into(),
+            vars: vec![],
+            ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
+            doc: Some("Short and snappy.".into()),
+            drop_iterative: false,
+        };
+        let mut out = String::new();
+        write_type_def(&mut out, &td, 0);
+        assert!(out.starts_with("/// Short and snappy.\n"), "got:\n{out}");
+        let doc_count = out.lines().filter(|l| l.starts_with("///")).count();
+        assert_eq!(doc_count, 1);
+    }
+
+    #[test]
+    fn doc_string_explicit_newlines_split_first_then_wrap() {
+        // A two-paragraph doc string: each \n-piece is its own logical
+        // line, then each piece wraps independently.
+        let long_first = "First paragraph that is short.";
+        let long_second = "Second paragraph is intentionally lengthy enough to require wrapping \
+                           at the eighty column boundary.";
+        let doc = format!("{long_first}\n{long_second}");
+        let td = TypeDef {
+            name: "Foo".into(),
+            vars: vec![],
+            ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
+            doc: Some(doc),
+            drop_iterative: false,
+        };
+        let mut out = String::new();
+        write_type_def(&mut out, &td, 0);
+        let doc_lines: Vec<&str> = out.lines().take_while(|l| l.starts_with("///")).collect();
+        // First line = unwrapped first paragraph; the rest = wrapped
+        // second paragraph (≥ 2 lines).
+        assert_eq!(doc_lines[0], "/// First paragraph that is short.");
+        assert!(doc_lines.len() >= 3, "expected at least 3 doc lines, got:\n{out}");
+    }
+
+    // ---- Polish 5: nested match across lines ----
+
+    #[test]
+    fn nested_match_in_arm_body_renders_multi_line() {
+        // The outer arm's body is itself a `Match`. The inner match
+        // must lay out across multiple lines, with the inner `}` at
+        // its own indent — not be collapsed onto the outer arm's line.
+        let inner = Term::Match {
+            scrutinee: Box::new(ivar("a")),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Ctor {
+                        ctor: "MkCell".into(),
+                        fields: vec![Pattern::Var { name: "w1".into() }, Pattern::Wild],
+                    },
+                    body: Term::Lit { lit: Literal::Int { value: 1 } },
+                },
+            ],
+        };
+        let outer = Term::Match {
+            scrutinee: Box::new(ivar("p")),
+            arms: vec![
+                Arm {
+                    pat: Pattern::Ctor {
+                        ctor: "MkPair".into(),
+                        fields: vec![Pattern::Var { name: "a".into() }, Pattern::Var { name: "b".into() }],
+                    },
+                    body: inner,
+                },
+            ],
+        };
+        assert_eq!(
+            render_term(&outer),
+            "match p {\n  \
+               MkPair(a, b) => match a {\n    \
+                 MkCell(w1, _) => 1\n  \
+               }\n\
+             }"
+        );
+    }
+
+    #[test]
+    fn deeply_nested_match_keeps_each_level_at_its_own_indent() {
+        // Three-deep nesting: each level lands one indent step deeper.
+        // This is the case the spec calls out — earlier renderers might
+        // have flattened the inner-inner onto a single line.
+        let innermost = Term::Match {
+            scrutinee: Box::new(ivar("c")),
+            arms: vec![Arm {
+                pat: Pattern::Var { name: "x".into() },
+                body: ivar("x"),
+            }],
+        };
+        let mid = Term::Match {
+            scrutinee: Box::new(ivar("b")),
+            arms: vec![Arm {
+                pat: Pattern::Var { name: "c".into() },
+                body: innermost,
+            }],
+        };
+        let outer = Term::Match {
+            scrutinee: Box::new(ivar("a")),
+            arms: vec![Arm {
+                pat: Pattern::Var { name: "b".into() },
+                body: mid,
+            }],
+        };
+        let rendered = render_term(&outer);
+        // Innermost arm line lands at 6 spaces of indent (3 levels × 2).
+        assert!(
+            rendered.contains("\n      x => x\n"),
+            "innermost arm not at expected 6-space indent, got:\n{rendered}"
+        );
+        // Innermost `}` lands at 4 spaces.
+        assert!(
+            rendered.contains("\n    }\n"),
+            "innermost close brace not at 4-space indent, got:\n{rendered}"
+        );
+        // Mid `}` lands at 2 spaces, outer `}` at 0.
+        assert!(
+            rendered.contains("\n  }\n"),
+            "mid close brace not at 2-space indent, got:\n{rendered}"
+        );
+        assert!(rendered.ends_with("\n}"), "outer close brace at col 0 expected, got:\n{rendered}");
+    }
 }

crates/ailang-prose/tests/snapshot.rs

@@ -62,3 +62,12 @@ fn snapshot_rc_match_arm_partial_drop_leak() {
 fn snapshot_rc_app_let_partial_drop_leak() {
     check_snapshot("rc_app_let_partial_drop_leak");
 }
+
+/// Iter 20b: this fixture exercises the infix renderer + paren elision.
+/// Pre-20b, the body had `if ==(n, 0) { ... }` and `tail sum_acc(-(n,
+/// 1), ICons(-(n, 1), acc))`; after 20b those collapse to `if n == 0`
+/// and `n - 1`. If this regresses, the renderer is broken.
+#[test]
+fn snapshot_bench_list_sum() {
+    check_snapshot("bench_list_sum");
+}

docs/JOURNAL.md

@@ -8964,3 +8964,96 @@ All explicitly out of 20a's scope; pinned for 20b.
 - **Iter 20d** — the round-trip mediator (prose-edit → updated
   AIL via LLM call). Specification + prompt template, not a
   compiler pass.
+
+## 2026-05-08 — Iter 20b: prose formatting polish shipped
+
+The polish pass on top of 20a's renderer skeleton. Four polishes,
+no public-API change.
+
+### Polishes
+
+  1. **Infix binary operators.** Eleven canonical builtins
+     (`+ - * / % == != < <= > >=`) when called via
+     `Term::App { args.len() == 2, tail: false }` render as
+     `lhs op rhs`. Tail-flagged binary ops keep prefix form so the
+     `tail` keyword stays visible.
+  2. **Paren elision by precedence.** Standard 4-level Rust-aligned
+     table: `* / %` (mul) > `+ -` (add) > `< <= > >=` (cmp,
+     non-assoc) > `== !=` (eq, non-assoc). Atomic terms (Var,
+     Lit, Ctor, App-non-binary, etc.) bind tightest. Same-level
+     left-associative left side: no parens; same-level right
+     side: keeps parens. Non-assoc ops always keep parens at
+     same level.
+  3. **Unary `not`.** `App { callee: Var "not", args: [x] }`
+     renders as `!x`. Atomic operand binds at level 5 (tightest);
+     `!(a == b)` keeps parens because the operand is a level-1
+     binary op.
+  4. **Long doc-string wrap.** `///` lines exceeding 80 columns
+     wrap at word boundaries. Explicit newlines split first, then
+     each piece word-wraps independently.
+  5. **Nested-match formatting** (already structurally correct in
+     20a; locked in by a 3-deep test).
+
+### Snapshot impressions
+
+`bench_list_sum.prose.txt` after 20b:
+
+```
+fn cons_n_acc(n: Int, acc: IntList) -> IntList {
+  if n == 0 {
+    acc
+  } else {
+    tail cons_n_acc(n - 1, ICons(n - 1, acc))
+  }
+}
+```
+
+vs. pre-20b `if ==(n, 0) { ... -(n, 1) ... ICons(-(n, 1), acc) }`.
+The infix conversion is the headline win — arithmetic now reads
+as arithmetic.
+
+`rc_own_param_drop.prose.txt` doc string now wraps:
+
+```
+/// Take ownership of an IntList; return its head if Cons, else 0. The tail is
+/// loaded as a pattern binder but never consumed — iter A dec's it at arm
+/// close. The outer cell is dec'd at fn return via iter B's Own-param emission.
+```
+
+### Tests
+
+Test count went from 28 → 47 (19 new unit tests in `lib.rs`),
+plus a fourth snapshot (`examples/bench_list_sum.prose.txt`) that
+exercises infix on a real benchmark fixture. Existing snapshots
+re-rendered to incorporate the wrapping.
+
+### Files
+
+  - `crates/ailang-prose/src/lib.rs` — `write_doc` rewrite,
+    `wrap_words` helper, `PREC_*` constants, `binop_info`,
+    `as_binop`, `as_unary_not` helpers, `write_term_prec`
+    threading `parent_prec` through term recursion.
+  - `crates/ailang-prose/tests/snapshot.rs` — new
+    `snapshot_bench_list_sum`.
+  - `examples/bench_list_sum.prose.txt` — new.
+  - `examples/rc_own_param_drop.prose.txt` — re-rendered.
+
+### Build/test status
+
+- `cargo build --workspace` — green, no warnings.
+- `cargo test --workspace` — 47 prose-unit + 4 prose-snapshot
+  pass; everything else unchanged-green.
+
+### What stays queued
+
+- **Iter 20d** — round-trip mediator. Specification + prompt
+  template (the LLM bundles original .ail.json + edited prose
+  and emits the updated .ail.json). Likely a `ail merge-prose`
+  subcommand that prints a shaped prompt, the user mediates
+  through their LLM, then `ail parse` (or `ail check`) on the
+  re-emitted artefact. Possibly: skip the CLI shim, ship as a
+  documented prompt template under `docs/`.
+- **Let-inlining** — questionable polish; deferred until the
+  corpus shows it's needed.
+- **`do io/print_int(x)` → `print(x)`** — needs type context
+  to be safe; deferred.

examples/bench_list_sum.prose.txt

@@ -0,0 +1,41 @@
+// module bench_list_sum
+
+data IntList = INil | ICons(Int, IntList)
+
+/// Tail-recursive list builder. Result = accumulator-prepended list.
+fn cons_n_acc(n: Int, acc: IntList) -> IntList {
+  if n == 0 {
+    acc
+  } else {
+    tail cons_n_acc(n - 1, ICons(n - 1, acc))
+  }
+}
+
+/// Build [0, 1, ..., n-1] :: IntList. Order doesn't matter for sum.
+fn cons_n(n: Int) -> IntList {
+  cons_n_acc(n, INil)
+}
+
+/// Tail-recursive sum.
+fn sum_acc(xs: IntList, acc: Int) -> Int {
+  match xs {
+    INil => acc,
+    ICons(h, t) => tail sum_acc(t, acc + h)
+  }
+}
+
+/// Sum every element. Calls sum_acc with seed 0.
+fn sum_list(xs: IntList) -> Int {
+  sum_acc(xs, 0)
+}
+
+/// Build a list of length n, sum it, print the sum.
+fn run_one(n: Int) -> Unit with IO {
+  do io/print_int(sum_list(cons_n(n)))
+}
+
+fn main() -> Unit with IO {
+  run_one(100000);
+  run_one(1000000);
+  run_one(3000000)
+}

examples/rc_own_param_drop.prose.txt

@@ -3,7 +3,9 @@
 /// Recursive Int list — boxed.
 data IntList = Nil | Cons(Int, IntList)
 
-/// Take ownership of an IntList; return its head if Cons, else 0. The tail is loaded as a pattern binder but never consumed — iter A dec's it at arm close. The outer cell is dec'd at fn return via iter B's Own-param emission.
+/// Take ownership of an IntList; return its head if Cons, else 0. The tail is
+/// loaded as a pattern binder but never consumed — iter A dec's it at arm
+/// close. The outer cell is dec'd at fn return via iter B's Own-param emission.
 fn head_or_zero(xs: own IntList) -> Int {
   match xs {
     Nil => 0,
@@ -11,7 +13,8 @@ fn head_or_zero(xs: own IntList) -> Int {
   }
 }
 
-/// Build a 5-element IntList; pass to head_or_zero (transferring ownership); print the result.
+/// Build a 5-element IntList; pass to head_or_zero (transferring ownership);
+/// print the result.
 fn main() -> Unit with IO {
   let xs = Cons(11, Cons(22, Cons(33, Cons(44, Cons(55, Nil)))));
   do io/print_int(head_or_zero(xs))