AILang/crates/ailang-prose/src/lib.rs

//! AILang prose projection — human-readable presentation layer.
//!
//! This crate is the form-(B) projection of [`ailang_core::ast::Module`]:
//! a Rust-flavoured, brace-and-comma text rendering optimised for human
//! reading. It is a *one-way* projection — there is no parser. Editing
//! the prose and re-integrating the changes is the round-trip-mediator's
//! job (Iter 20d), not this crate's.
//!
//! The canonical authoring surface remains form (A) (`ailang-surface`)
//! and the canonical hashable artefact remains the JSON-AST
//! (`ailang-core`). Prose is deliberately lossy where the LLM can
//! re-derive the dropped machinery from typecheck context (the `(con T)`
//! wrap, the `(fn-type ...)` wrap, the `(term-ctor T C ...)` collapsing
//! to `C(...)`); every load-bearing semantic detail (mode annotations,
//! effects, `clone`, `reuse-as`, doc strings, type annotations on
//! signatures and lambdas, the `tail` flag) stays visible.
//!
//! See `design/contracts/authoring-surface.md` for the prose-surface
//! invariants this crate must respect.
//!
//! # Public API
//!
//! [`module_to_prose`] is the only entry point. It is deterministic and
//! never fails on a well-formed AST.

use ailang_core::ast::{
    ClassDef, ClassMethod, ConstDef, Ctor, Def, FnDef, Import, InstanceDef, InstanceMethod,
    Literal, Module, ParamMode, Pattern, Suppress, Term, Type, TypeDef,
};

/// Render a [`Module`] as human-readable prose.
///
/// The output is deterministic; identical input AST always yields
/// identical bytes. The renderer never fails on a well-formed AST.
pub fn module_to_prose(m: &Module) -> String {
    let mut out = String::new();
    write_module(&mut out, m);
    out
}

// ---- module ---------------------------------------------------------------

fn write_module(out: &mut String, m: &Module) {
    out.push_str("// module ");
    out.push_str(&m.name);
    out.push('\n');

    if !m.imports.is_empty() {
        out.push('\n');
        for imp in &m.imports {
            write_import(out, imp);
            out.push('\n');
        }
    }

    // The file's own module name is the owner-qualifier that the
    // prose surface trims when it appears on intra-module
    // `Type::Con.name`. Cross-module qualifiers round-trip verbatim.
    // Threaded through every recursive write_* that can reach a
    // `Type::Con`.
    let owning_module = m.name.as_str();

    for def in &m.defs {
        out.push('\n');
        write_def(out, def, 0, owning_module);
        out.push('\n');
    }
}

fn write_import(out: &mut String, imp: &Import) {
    out.push_str("import ");
    out.push_str(&imp.module);
    if let Some(alias) = &imp.alias {
        out.push_str(" as ");
        out.push_str(alias);
    }
}

// ---- defs -----------------------------------------------------------------

fn write_def(out: &mut String, def: &Def, level: usize, owning_module: &str) {
    match def {
        Def::Type(td) => write_type_def(out, td, level, owning_module),
        Def::Fn(fd) => write_fn_def(out, fd, level, owning_module),
        Def::Const(cd) => write_const_def(out, cd, level, owning_module),
        Def::Class(c) => write_class_def(out, c, level, owning_module),
        Def::Instance(i) => write_instance_def(out, i, level, owning_module),
    }
}

/// render the [`FnDef::suppress`] list as one
/// `// @suppress <code>: <reason>` line per entry, indented to
/// `level`. Multiple entries stack in declaration order; an empty
/// list produces no output (and therefore no leading blank line).
///
/// The render is intentionally lossless. The LLM-reader of the
/// prose form needs to see *why* an annotation that looks
/// over-strict is correct on this def; eliding suppressions would
/// hide that contract metadata.
fn write_suppress_lines(out: &mut String, suppress: &[Suppress], level: usize) {
    for s in suppress {
        indent(out, level);
        out.push_str("// @suppress ");
        out.push_str(&s.code);
        out.push_str(": ");
        out.push_str(&s.because);
        out.push('\n');
    }
}

fn write_doc(out: &mut String, doc: &Option<String>, level: usize) {
    if let Some(d) = doc {
        // 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());
    }
    // Widow control: a 1-word orphan as the last line reads as a
    // typographic blemish (e.g. "...captures outer's param\ni."). If
    // the second-to-last line has ≥2 words and the merge fits in
    // budget, pull its tail word down so the last line has 2 words
    // and the penultimate line gives up one. Greedy fill never
    // produces a line that overflows budget when shortened from the
    // tail, so this never breaks the wrap invariant.
    if out.len() >= 2 {
        let last_word_count = out.last().unwrap().split_whitespace().count();
        if last_word_count == 1 {
            let prev_idx = out.len() - 2;
            let prev_words: Vec<&str> = out[prev_idx].split_whitespace().collect();
            if prev_words.len() >= 2 {
                let pulled = prev_words.last().unwrap();
                let last_line = out.last().unwrap();
                if pulled.len() + 1 + last_line.len() <= budget {
                    let pulled_owned = pulled.to_string();
                    let prev_new = prev_words[..prev_words.len() - 1].join(" ");
                    let last_line_owned = last_line.clone();
                    let combined = format!("{pulled_owned} {last_line_owned}");
                    out[prev_idx] = prev_new;
                    let last_idx = out.len() - 1;
                    out[last_idx] = combined;
                }
            }
        }
    }
    out
}

fn write_type_def(out: &mut String, td: &TypeDef, level: usize, owning_module: &str) {
    write_doc(out, &td.doc, level);
    indent(out, level);
    out.push_str("data ");
    out.push_str(&td.name);
    if !td.vars.is_empty() {
        out.push('<');
        for (i, v) in td.vars.iter().enumerate() {
            if i > 0 {
                out.push_str(", ");
            }
            out.push_str(v);
        }
        out.push('>');
    }
    out.push_str(" = ");
    for (i, c) in td.ctors.iter().enumerate() {
        if i > 0 {
            out.push_str(" | ");
        }
        write_ctor(out, c, owning_module);
    }
    if td.drop_iterative {
        out.push_str(" with drop-iterative");
    }
}

fn write_ctor(out: &mut String, c: &Ctor, owning_module: &str) {
    out.push_str(&c.name);
    if !c.fields.is_empty() {
        out.push('(');
        for (i, f) in c.fields.iter().enumerate() {
            if i > 0 {
                out.push_str(", ");
            }
            write_type(out, f, owning_module);
        }
        out.push(')');
    }
}

fn write_fn_def(out: &mut String, fd: &FnDef, level: usize, owning_module: &str) {
    // render `suppress` entries as `// @suppress <code>: <reason>`
    // comment lines **above** the doc string. They are contract metadata
    // that the LLM-reader needs to see to understand why an annotation
    // that looks over-strict is correct here. One line per entry, in
    // declaration order; never elided.
    write_suppress_lines(out, &fd.suppress, level);
    write_doc(out, &fd.doc, level);
    // The FnDef carries `params` (names) plus the type. The signature
    // surface combines them slot-for-slot. `fd.ty` is either a
    // `Type::Fn` or a `Type::Forall` wrapping one — in the latter case
    // we render the forall on the line above and then the inner fn
    // signature.
    let (forall_vars, forall_constraints, fn_ty) = match &fd.ty {
        Type::Forall { vars, constraints, body } => {
            (Some(vars.clone()), constraints.clone(), body.as_ref())
        }
        other => (None, Vec::new(), other),
    };

    if let Some(vars) = &forall_vars {
        indent(out, level);
        out.push_str("forall<");
        for (i, v) in vars.iter().enumerate() {
            if i > 0 {
                out.push_str(", ");
            }
            out.push_str(v);
        }
        out.push('>');
        if !forall_constraints.is_empty() {
            out.push_str(" where ");
            for (i, c) in forall_constraints.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(&c.class);
                out.push(' ');
                write_type(out, &c.type_, owning_module);
            }
        }
        out.push('\n');
    }

    indent(out, level);
    out.push_str("fn ");
    out.push_str(&fd.name);
    out.push('(');
    if let Type::Fn {
        params,
        param_modes,
        ret,
        ret_mode,
        effects,
    } = fn_ty
    {
        for (i, ty) in params.iter().enumerate() {
            if i > 0 {
                out.push_str(", ");
            }
            // Param name from FnDef.params, type+mode from Type::Fn.
            let pname = fd.params.get(i).map(String::as_str).unwrap_or("_");
            out.push_str(pname);
            out.push_str(": ");
            let mode = param_modes
                .get(i)
                .copied()
                .unwrap_or(ParamMode::Implicit);
            write_mode_type(out, ty, mode, owning_module);
        }
        out.push_str(") -> ");
        write_mode_type(out, ret, *ret_mode, owning_module);
        if !effects.is_empty() {
            out.push_str(" with ");
            // Stable order: as written in the AST. Effects are
            // semantically a set, but re-sorting would erase
            // author-asserted ordering; preserve the AST order.
            for (i, e) in effects.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(e);
            }
        }
    } else {
        // Defensive fallback: a non-Fn fn-type. Render the bare type so
        // nothing crashes; this path is unreachable for typechecked
        // input.
        out.push_str(") -> ");
        write_type(out, fn_ty, owning_module);
    }
    out.push_str(" {\n");
    indent(out, level + 1);
    write_term(out, &fd.body, level + 1, owning_module);
    out.push('\n');
    indent(out, level);
    out.push('}');
}

fn write_const_def(out: &mut String, cd: &ConstDef, level: usize, owning_module: &str) {
    write_doc(out, &cd.doc, level);
    indent(out, level);
    out.push_str("const ");
    out.push_str(&cd.name);
    out.push_str(": ");
    write_type(out, &cd.ty, owning_module);
    out.push_str(" = ");
    write_term(out, &cd.value, level, owning_module);
}

/// Render a class declaration in Rust-flavoured Form-B:
/// `class Name a [extends Super] { <methods> }`.
fn write_class_def(out: &mut String, c: &ClassDef, level: usize, owning_module: &str) {
    write_doc(out, &c.doc, level);
    indent(out, level);
    out.push_str("class ");
    out.push_str(&c.name);
    out.push(' ');
    out.push_str(&c.param);
    if let Some(sc) = &c.superclass {
        out.push_str(" extends ");
        out.push_str(&sc.class);
    }
    out.push_str(" {\n");
    for m in &c.methods {
        write_class_method(out, m, level + 1, owning_module);
    }
    indent(out, level);
    out.push('}');
}

/// Render one method line of a class: signature plus optional
/// `default { <body> }`. Class methods carry no parameter names
/// in the AST, so slots are named `x`, `x1`, ….
fn write_class_method(out: &mut String, m: &ClassMethod, level: usize, owning_module: &str) {
    indent(out, level);
    out.push_str("fn ");
    out.push_str(&m.name);
    out.push('(');
    if let Type::Fn { params, param_modes, ret, ret_mode, effects } = &m.ty {
        for (i, p) in params.iter().enumerate() {
            if i > 0 {
                out.push_str(", ");
            }
            // Class methods carry types but no parameter names — name slots
            // as `x`, `x1`, `x2`, … to keep the projection unambiguous
            // without inventing names that could collide with the body.
            if i == 0 {
                out.push('x');
            } else {
                out.push_str(&format!("x{i}"));
            }
            out.push_str(": ");
            let mode = param_modes.get(i).copied().unwrap_or(ParamMode::Implicit);
            write_mode_type(out, p, mode, owning_module);
        }
        out.push_str(") -> ");
        write_mode_type(out, ret, *ret_mode, owning_module);
        if !effects.is_empty() {
            out.push_str(" with ");
            for (i, e) in effects.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(e);
            }
        }
    } else {
        // Defensive fallback: a non-Fn class-method type. Render the
        // bare type so nothing crashes; this path is unreachable for
        // typechecked input.
        out.push_str(") -> ");
        write_type(out, &m.ty, owning_module);
    }
    if let Some(body) = &m.default {
        out.push_str(" default {\n");
        indent(out, level + 1);
        write_term(out, body, level + 1, owning_module);
        out.push('\n');
        indent(out, level);
        out.push_str("}\n");
    } else {
        out.push('\n');
    }
}

/// Render an instance declaration in Form-B:
/// `instance Class Type { <method bodies> }`.
fn write_instance_def(out: &mut String, i: &InstanceDef, level: usize, owning_module: &str) {
    write_doc(out, &i.doc, level);
    indent(out, level);
    out.push_str("instance ");
    out.push_str(&i.class);
    out.push(' ');
    write_type(out, &i.type_, owning_module);
    out.push_str(" {\n");
    for m in &i.methods {
        write_instance_method(out, m, level + 1, owning_module);
    }
    indent(out, level);
    out.push('}');
}

/// Render one method body of an instance: `fn name { <body> }`.
/// The signature is recoverable from the class declaration via
/// `InstanceDef.class` lookup, so it is intentionally elided.
fn write_instance_method(out: &mut String, m: &InstanceMethod, level: usize, owning_module: &str) {
    indent(out, level);
    out.push_str("fn ");
    out.push_str(&m.name);
    out.push_str(" {\n");
    indent(out, level + 1);
    write_term(out, &m.body, level + 1, owning_module);
    out.push('\n');
    indent(out, level);
    out.push_str("}\n");
}

// ---- types ----------------------------------------------------------------

fn write_mode_type(out: &mut String, t: &Type, mode: ParamMode, owning_module: &str) {
    match mode {
        ParamMode::Implicit => write_type(out, t, owning_module),
        ParamMode::Own => {
            out.push_str("own ");
            write_type(out, t, owning_module);
        }
        ParamMode::Borrow => {
            out.push_str("borrow ");
            write_type(out, t, owning_module);
        }
    }
}

fn write_type(out: &mut String, t: &Type, owning_module: &str) {
    match t {
        Type::Var { name } => out.push_str(name),
        Type::Con { name, args } => {
            // Trim a qualifier whose owner matches the current file's
            // module: `prelude.Ordering` printed from inside `prelude`
            // becomes bare `Ordering`. Cross-module qualifiers survive
            // verbatim. Mirrors the canonical-form rule "bare = local,
            // qualified = cross-module" on the prose surface.
            let display_name = match name.split_once('.') {
                Some((owner, suffix)) if owner == owning_module => suffix,
                _ => name.as_str(),
            };
            out.push_str(display_name);
            if !args.is_empty() {
                out.push('<');
                for (i, a) in args.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    write_type(out, a, owning_module);
                }
                out.push('>');
            }
        }
        Type::Fn {
            params,
            param_modes,
            ret,
            ret_mode,
            effects,
        } => {
            out.push('(');
            for (i, p) in params.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                let mode = param_modes
                    .get(i)
                    .copied()
                    .unwrap_or(ParamMode::Implicit);
                // In a bare `Type::Fn` outside a fn signature we have no
                // parameter names, so render `mode T` only (no `name:`).
                write_mode_type(out, p, mode, owning_module);
            }
            out.push_str(") -> ");
            write_mode_type(out, ret, *ret_mode, owning_module);
            if !effects.is_empty() {
                out.push_str(" with ");
                for (i, e) in effects.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    out.push_str(e);
                }
            }
        }
        Type::Forall { vars, constraints: _, body } => {
            out.push_str("forall<");
            for (i, v) in vars.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(v);
            }
            out.push_str("> ");
            write_type(out, body, owning_module);
        }
    }
}

// ---- terms ----------------------------------------------------------------

// Precedence ladder for paren elision. 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). After iter operator-routing-eq-ord.1 the only
// infix-rendered ops are the arithmetic builtins; comparison /
// equality go through the class-method `eq` / `compare` / `lt` /
// etc. and render as fn calls.
const PREC_NONE: u8 = 0;
const PREC_ADD: u8 = 1; // +  -           (left-assoc)
const PREC_MUL: u8 = 2; // *  /  %        (left-assoc)
const PREC_ATOMIC: u8 = 3;

/// Precedence + associativity of a canonical binary op name. Returns
/// `None` for any non-canonical name. Two-tuple: (level, left_assoc).
/// After iter operator-routing-eq-ord.1, only the five arithmetic
/// ops `+` / `-` / `*` / `/` / `%` are infix-rendered; the six
/// comparator names (`==` / `!=` / `<` / `<=` / `>` / `>=`) are no
/// longer surface identifiers, so their AST forms (only reachable
/// via error paths) fall through to the standard fn-call rendering.
fn binop_info(name: &str) -> Option<(u8, bool)> {
    Some(match name {
        "*" | "/" | "%" => (PREC_MUL, true),
        "+" | "-" => (PREC_ADD, true),
        _ => 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, owning_module: &str) {
    write_term_prec(out, t, level, PREC_NONE, owning_module);
}

fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8, owning_module: &str) {
    // 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, owning_module);
        out.push(' ');
        out.push_str(op);
        out.push(' ');
        write_term_prec(out, rhs, level, rhs_floor, owning_module);
        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, owning_module);
        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),
        Term::App { callee, args, tail } => {
            if *tail {
                out.push_str("tail ");
            }
            // 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, owning_module);
            out.push('(');
            for (i, a) in args.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                // 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, owning_module);
            }
            out.push(')');
        }
        Term::Let { name, value, body } => {
            // Inline `let x = rhs;` when (a) rhs is not a `Term::Do`
            // (keep effect sequencing visible), (b) `x` is used
            // exactly once in body (no duplication of work or shape),
            // and (c) the rhs renders on a single line (small enough
            // to read at the use-site). The result is a lossy
            // projection — the round-trip mediator (`ail merge-prose`)
            // sees the original .ail.json and can re-introduce a let
            // when the mode model demands it. For read-time, eliding
            // the trivial binding is a clear win.
            // RHS budget for inlining. Keeps the use-site readable: a
            // 50-char Cons tower inlined into `f(g(h(_)))` blows the
            // line out far past the surrounding lines. The threshold
            // is tuned so trivial bindings (`let p = build_pair(1)`)
            // collapse, while heavy literals (a 5-deep Cons) keep
            // their own line.
            const RHS_INLINE_BUDGET: usize = 40;
            let inlinable = !matches!(value.as_ref(), Term::Do { .. })
                && count_free_var(name, body) == 1
                && {
                    let mut buf = String::new();
                    write_term(&mut buf, value, level, owning_module);
                    !buf.contains('\n') && buf.len() <= RHS_INLINE_BUDGET
                };
            if inlinable {
                let inlined = subst_var_with_term(body, name, value);
                write_term_prec(out, &inlined, level, parent_prec, owning_module);
            } else {
                out.push_str("let ");
                out.push_str(name);
                out.push_str(" = ");
                write_term(out, value, level, owning_module);
                out.push_str(";\n");
                indent(out, level);
                write_term(out, body, level, owning_module);
            }
        }
        Term::LetRec {
            name,
            ty,
            params,
            body,
            in_term,
        } => {
            // Local recursive fn-binding. Render as a nested fn-shape
            // followed by the body.
            out.push_str("let-rec ");
            out.push_str(name);
            out.push('(');
            if let Type::Fn {
                params: ptys,
                param_modes,
                ret,
                ret_mode,
                effects,
            } = ty
            {
                for (i, pty) in ptys.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    let pname = params.get(i).map(String::as_str).unwrap_or("_");
                    out.push_str(pname);
                    out.push_str(": ");
                    let mode = param_modes
                        .get(i)
                        .copied()
                        .unwrap_or(ParamMode::Implicit);
                    write_mode_type(out, pty, mode, owning_module);
                }
                out.push_str(") -> ");
                write_mode_type(out, ret, *ret_mode, owning_module);
                if !effects.is_empty() {
                    out.push_str(" with ");
                    for (i, e) in effects.iter().enumerate() {
                        if i > 0 {
                            out.push_str(", ");
                        }
                        out.push_str(e);
                    }
                }
            } else {
                out.push_str(") -> ");
                write_type(out, ty, owning_module);
            }
            out.push_str(" {\n");
            indent(out, level + 1);
            write_term(out, body, level + 1, owning_module);
            out.push('\n');
            indent(out, level);
            out.push_str("};\n");
            indent(out, level);
            write_term(out, in_term, level, owning_module);
        }
        Term::If { cond, then, else_ } => {
            out.push_str("if ");
            write_term(out, cond, level, owning_module);
            out.push_str(" {\n");
            indent(out, level + 1);
            write_term(out, then, level + 1, owning_module);
            out.push('\n');
            indent(out, level);
            out.push_str("} else {\n");
            indent(out, level + 1);
            write_term(out, else_, level + 1, owning_module);
            out.push('\n');
            indent(out, level);
            out.push('}');
        }
        Term::Do { op, args, tail } => {
            if *tail {
                out.push_str("tail ");
            }
            out.push_str("do ");
            out.push_str(op);
            out.push('(');
            for (i, a) in args.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                write_term(out, a, level, owning_module);
            }
            out.push(')');
        }
        Term::Ctor {
            type_name: _,
            ctor,
            args,
        } => {
            // The Ctor `type_name` field is intentionally elided from
            // the prose surface — the type is recoverable from
            // typecheck context, and showing it on every Ctor would
            // clutter the read. The qualifier-trim that applies to
            // `Type::Con.name` therefore has no analogue here: there
            // is no `out.push_str(type_name)` site to trim.
            out.push_str(ctor);
            if !args.is_empty() {
                out.push('(');
                for (i, a) in args.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    write_term(out, a, level, owning_module);
                }
                out.push(')');
            }
        }
        Term::Match { scrutinee, arms } => {
            out.push_str("match ");
            write_term(out, scrutinee, level, owning_module);
            out.push_str(" {\n");
            for (i, arm) in arms.iter().enumerate() {
                indent(out, level + 1);
                write_pattern(out, &arm.pat);
                out.push_str(" => ");
                write_term(out, &arm.body, level + 1, owning_module);
                if i + 1 < arms.len() {
                    out.push(',');
                }
                out.push('\n');
            }
            indent(out, level);
            out.push('}');
        }
        Term::Lam {
            params,
            param_tys,
            ret_ty,
            effects,
            body,
        } => {
            // Rust-closure flavour: `|p1: T1, p2: T2| -> R with EFF { body }`
            out.push('|');
            for (i, (pname, pty)) in params.iter().zip(param_tys.iter()).enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(pname);
                out.push_str(": ");
                write_type(out, pty, owning_module);
            }
            out.push_str("| -> ");
            write_type(out, ret_ty, owning_module);
            if !effects.is_empty() {
                out.push_str(" with ");
                for (i, e) in effects.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    out.push_str(e);
                }
            }
            out.push_str(" {\n");
            indent(out, level + 1);
            write_term(out, body, level + 1, owning_module);
            out.push('\n');
            indent(out, level);
            out.push('}');
        }
        Term::Seq { lhs, rhs } => {
            // Semicolon-as-discard. `lhs;` on its own line, `rhs` on
            // the next at the same indent. The caller already indented us.
            write_term(out, lhs, level, owning_module);
            out.push_str(";\n");
            indent(out, level);
            write_term(out, rhs, level, owning_module);
        }
        Term::Clone { value } => {
            out.push_str("clone(");
            write_term(out, value, level, owning_module);
            out.push(')');
        }
        Term::ReuseAs { source, body } => {
            // Render as `reuse <source> as <body>`. The split keyword
            // reads as English subject-verb-object — the source is the
            // allocation being reclaimed, the body is what it becomes.
            // Braces only fire when the body's own rendering would span
            // multiple lines (Let, Seq, nested Match, multi-line If);
            // single-expression bodies (the 99% Ctor case) stay inline,
            // collapsing the whole match arm to one line.
            out.push_str("reuse ");
            write_term(out, source, level, owning_module);
            out.push_str(" as ");
            let mut body_buf = String::new();
            write_term(&mut body_buf, body, level + 1, owning_module);
            if body_buf.contains('\n') {
                out.push_str("{\n");
                indent(out, level + 1);
                out.push_str(&body_buf);
                out.push('\n');
                indent(out, level);
                out.push('}');
            } else {
                out.push_str(&body_buf);
            }
        }
        Term::Loop { binders, body } => {
            out.push_str("loop(");
            for (i, b) in binders.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                out.push_str(&b.name);
                out.push_str(" = ");
                write_term(out, &b.init, level, owning_module);
            }
            out.push_str(") {\n");
            indent(out, level + 1);
            write_term(out, body, level + 1, owning_module);
            out.push('\n');
            indent(out, level);
            out.push('}');
        }
        Term::Recur { args } => {
            out.push_str("recur(");
            for (i, a) in args.iter().enumerate() {
                if i > 0 {
                    out.push_str(", ");
                }
                write_term(out, a, level, owning_module);
            }
            out.push(')');
        }
    }
}

fn write_pattern(out: &mut String, p: &Pattern) {
    match p {
        Pattern::Wild => out.push('_'),
        Pattern::Var { name } => out.push_str(name),
        Pattern::Lit { lit } => write_lit(out, lit),
        Pattern::Ctor { ctor, fields } => {
            out.push_str(ctor);
            if !fields.is_empty() {
                out.push('(');
                for (i, f) in fields.iter().enumerate() {
                    if i > 0 {
                        out.push_str(", ");
                    }
                    write_pattern(out, f);
                }
                out.push(')');
            }
        }
    }
}

/// Floats milestone iter 5: render a Float literal's bit pattern
/// as surface-style decimal text. Finite values use Grisu3
/// (`f64::to_string`) with a `.0` suffix when neither `.` nor
/// `e`/`E` appears, parallel to
/// `crates/ailang-surface/src/print.rs::write_float_lit`. Non-finite
/// values render as `NaN` / `+Inf` / `-Inf` — these are valid in
/// Form-A (the canonical bytes carry the bit pattern) but cannot
/// be expressed in surface lex; prose is one-way render, so naming
/// them after the Mainstream-language spellings is more useful
/// than a panic or a `(float-bits hex)` placeholder.
fn write_float_lit(out: &mut String, bits: u64) {
    let f = f64::from_bits(bits);
    if f.is_nan() {
        out.push_str("NaN");
        return;
    }
    if f == f64::INFINITY {
        out.push_str("+Inf");
        return;
    }
    if f == f64::NEG_INFINITY {
        out.push_str("-Inf");
        return;
    }
    let s = f.to_string();
    out.push_str(&s);
    if !s.contains('.') && !s.contains('e') && !s.contains('E') {
        out.push_str(".0");
    }
}

fn write_lit(out: &mut String, lit: &Literal) {
    match lit {
        Literal::Int { value } => out.push_str(&value.to_string()),
        Literal::Bool { value } => out.push_str(if *value { "true" } else { "false" }),
        Literal::Str { value } => write_string_lit(out, value),
        Literal::Unit => out.push_str("()"),
        Literal::Float { bits } => write_float_lit(out, *bits),
    }
}

fn write_string_lit(out: &mut String, s: &str) {
    out.push('"');
    for c in s.chars() {
        match c {
            '"' => out.push_str("\\\""),
            '\\' => out.push_str("\\\\"),
            '\n' => out.push_str("\\n"),
            '\t' => out.push_str("\\t"),
            '\r' => out.push_str("\\r"),
            other => out.push(other),
        }
    }
    out.push('"');
}

// ---- helpers --------------------------------------------------------------

fn indent(out: &mut String, level: usize) {
    for _ in 0..level {
        out.push_str("  ");
    }
}

// ---- let-inlining helpers (Iter 20b, polish 1) ----------------------------
//
// These support the `Term::Let` arm's "inline single-use bindings" path.
// They are render-only; the AST passed to the renderer is never mutated.
// Substitution operates on a freshly cloned subtree.

/// Collect every name a pattern binds. Used to detect that a pattern arm
/// shadows the binder we are tracking, so its body must NOT be counted /
/// substituted.
fn pattern_binders(p: &Pattern, out: &mut std::collections::BTreeSet<String>) {
    match p {
        Pattern::Wild | Pattern::Lit { .. } => {}
        Pattern::Var { name } => {
            out.insert(name.clone());
        }
        Pattern::Ctor { fields, .. } => {
            for f in fields {
                pattern_binders(f, out);
            }
        }
    }
}

/// Count free occurrences of the variable `name` in `t`, respecting
/// inner shadowing introduced by `let`, `lam`, `match` arms, and
/// `let rec`.
fn count_free_var(name: &str, t: &Term) -> usize {
    match t {
        Term::Lit { .. } => 0,
        Term::Var { name: n } => {
            if n == name {
                1
            } else {
                0
            }
        }
        Term::App { callee, args, .. } => {
            count_free_var(name, callee) + args.iter().map(|a| count_free_var(name, a)).sum::<usize>()
        }
        Term::Let { name: n, value, body } => {
            let v = count_free_var(name, value);
            let b = if n == name { 0 } else { count_free_var(name, body) };
            v + b
        }
        Term::If { cond, then, else_ } => {
            count_free_var(name, cond) + count_free_var(name, then) + count_free_var(name, else_)
        }
        Term::Do { args, .. } => args.iter().map(|a| count_free_var(name, a)).sum(),
        Term::Ctor { args, .. } => args.iter().map(|a| count_free_var(name, a)).sum(),
        Term::Match { scrutinee, arms } => {
            let s = count_free_var(name, scrutinee);
            let a: usize = arms
                .iter()
                .map(|arm| {
                    let mut binds = std::collections::BTreeSet::new();
                    pattern_binders(&arm.pat, &mut binds);
                    if binds.contains(name) {
                        0
                    } else {
                        count_free_var(name, &arm.body)
                    }
                })
                .sum();
            s + a
        }
        Term::Lam { params, body, .. } => {
            if params.iter().any(|p| p == name) {
                0
            } else {
                count_free_var(name, body)
            }
        }
        Term::Seq { lhs, rhs } => count_free_var(name, lhs) + count_free_var(name, rhs),
        Term::LetRec { name: n, params, body, in_term, .. } => {
            // Body is in the recursive scope of `n` and the params.
            let body_shadowed = n == name || params.iter().any(|p| p == name);
            let in_shadowed = n == name;
            let bb = if body_shadowed { 0 } else { count_free_var(name, body) };
            let ib = if in_shadowed { 0 } else { count_free_var(name, in_term) };
            bb + ib
        }
        Term::Clone { value } => count_free_var(name, value),
        Term::ReuseAs { source, body } => count_free_var(name, source) + count_free_var(name, body),
        // loop-recur iter 1: a binder named `name` shadows the outer
        // binding for later binder inits and the body. Inits before
        // the shadowing binder still see the outer `name`.
        Term::Loop { binders, body } => {
            let mut total = 0usize;
            let mut shadowed = false;
            for b in binders {
                if !shadowed {
                    total += count_free_var(name, &b.init);
                }
                if b.name == name {
                    shadowed = true;
                }
            }
            if !shadowed {
                total += count_free_var(name, body);
            }
            total
        }
        Term::Recur { args } => {
            args.iter().map(|a| count_free_var(name, a)).sum()
        }
    }
}

/// Substitute every free `Var{name}` occurrence in `t` with a clone of
/// `replacement`. Respects inner shadowing the same way `count_free_var`
/// does. Used only inside the renderer; never reaches the AST consumer.
fn subst_var_with_term(t: &Term, name: &str, replacement: &Term) -> Term {
    match t {
        Term::Lit { .. } => t.clone(),
        Term::Var { name: n } => {
            if n == name {
                replacement.clone()
            } else {
                t.clone()
            }
        }
        Term::App { callee, args, tail } => Term::App {
            callee: Box::new(subst_var_with_term(callee, name, replacement)),
            args: args.iter().map(|a| subst_var_with_term(a, name, replacement)).collect(),
            tail: *tail,
        },
        Term::Let { name: n, value, body } => {
            let v = subst_var_with_term(value, name, replacement);
            let b = if n == name {
                (**body).clone()
            } else {
                subst_var_with_term(body, name, replacement)
            };
            Term::Let {
                name: n.clone(),
                value: Box::new(v),
                body: Box::new(b),
            }
        }
        Term::If { cond, then, else_ } => Term::If {
            cond: Box::new(subst_var_with_term(cond, name, replacement)),
            then: Box::new(subst_var_with_term(then, name, replacement)),
            else_: Box::new(subst_var_with_term(else_, name, replacement)),
        },
        Term::Do { op, args, tail } => Term::Do {
            op: op.clone(),
            args: args.iter().map(|a| subst_var_with_term(a, name, replacement)).collect(),
            tail: *tail,
        },
        Term::Ctor { type_name, ctor, args } => Term::Ctor {
            type_name: type_name.clone(),
            ctor: ctor.clone(),
            args: args.iter().map(|a| subst_var_with_term(a, name, replacement)).collect(),
        },
        Term::Match { scrutinee, arms } => Term::Match {
            scrutinee: Box::new(subst_var_with_term(scrutinee, name, replacement)),
            arms: arms
                .iter()
                .map(|arm| {
                    let mut binds = std::collections::BTreeSet::new();
                    pattern_binders(&arm.pat, &mut binds);
                    let body = if binds.contains(name) {
                        arm.body.clone()
                    } else {
                        subst_var_with_term(&arm.body, name, replacement)
                    };
                    ailang_core::ast::Arm { pat: arm.pat.clone(), body }
                })
                .collect(),
        },
        Term::Lam { params, param_tys, ret_ty, effects, body } => {
            let body = if params.iter().any(|p| p == name) {
                (**body).clone()
            } else {
                subst_var_with_term(body, name, replacement)
            };
            Term::Lam {
                params: params.clone(),
                param_tys: param_tys.clone(),
                ret_ty: ret_ty.clone(),
                effects: effects.clone(),
                body: Box::new(body),
            }
        }
        Term::Seq { lhs, rhs } => Term::Seq {
            lhs: Box::new(subst_var_with_term(lhs, name, replacement)),
            rhs: Box::new(subst_var_with_term(rhs, name, replacement)),
        },
        Term::LetRec { name: n, ty, params, body, in_term } => {
            let body_shadowed = n == name || params.iter().any(|p| p == name);
            let in_shadowed = n == name;
            let body_rw = if body_shadowed {
                (**body).clone()
            } else {
                subst_var_with_term(body, name, replacement)
            };
            let in_rw = if in_shadowed {
                (**in_term).clone()
            } else {
                subst_var_with_term(in_term, name, replacement)
            };
            Term::LetRec {
                name: n.clone(),
                ty: ty.clone(),
                params: params.clone(),
                body: Box::new(body_rw),
                in_term: Box::new(in_rw),
            }
        }
        Term::Clone { value } => Term::Clone {
            value: Box::new(subst_var_with_term(value, name, replacement)),
        },
        Term::ReuseAs { source, body } => Term::ReuseAs {
            source: Box::new(subst_var_with_term(source, name, replacement)),
            body: Box::new(subst_var_with_term(body, name, replacement)),
        },
        // loop-recur iter 1: lexical-shadow semantics — once a binder
        // named `name` is declared, later inits and the body are not
        // rewritten.
        Term::Loop { binders, body } => {
            let mut shadowed = false;
            let new_binders: Vec<ailang_core::ast::LoopBinder> = binders
                .iter()
                .map(|b| {
                    let init = if shadowed {
                        b.init.clone()
                    } else {
                        subst_var_with_term(&b.init, name, replacement)
                    };
                    if b.name == name {
                        shadowed = true;
                    }
                    ailang_core::ast::LoopBinder {
                        name: b.name.clone(),
                        ty: b.ty.clone(),
                        init,
                    }
                })
                .collect();
            let body_rw = if shadowed {
                (**body).clone()
            } else {
                subst_var_with_term(body, name, replacement)
            };
            Term::Loop {
                binders: new_binders,
                body: Box::new(body_rw),
            }
        }
        Term::Recur { args } => Term::Recur {
            args: args
                .iter()
                .map(|a| subst_var_with_term(a, name, replacement))
                .collect(),
        },
    }
}

// ---- unit tests -----------------------------------------------------------

#[cfg(test)]
mod tests {
    use super::*;
    use ailang_core::ast::{Arm, Ctor, FnDef, Literal, Pattern, Term, Type};

    fn render_term(t: &Term) -> String {
        let mut out = String::new();
        write_term(&mut out, t, 0, "");
        out
    }

    fn render_type(t: &Type) -> String {
        let mut out = String::new();
        write_type(&mut out, t, "");
        out
    }

    // ---- Lit / Var ----

    #[test]
    fn lit_int_renders_as_decimal() {
        assert_eq!(render_term(&Term::Lit { lit: Literal::Int { value: 42 } }), "42");
    }

    #[test]
    fn lit_bool_renders_as_keyword() {
        assert_eq!(
            render_term(&Term::Lit { lit: Literal::Bool { value: true } }),
            "true"
        );
        assert_eq!(
            render_term(&Term::Lit { lit: Literal::Bool { value: false } }),
            "false"
        );
    }

    #[test]
    fn lit_str_renders_with_escapes() {
        assert_eq!(
            render_term(&Term::Lit { lit: Literal::Str { value: "hi\n".into() } }),
            "\"hi\\n\""
        );
    }

    #[test]
    fn lit_unit_renders_as_unit_pair() {
        assert_eq!(render_term(&Term::Lit { lit: Literal::Unit }), "()");
    }

    /// Floats milestone iter 5.1: prose renders Float literals as
    /// surface-style decimal text. Finite values use shortest
    /// round-trippable decimal with `.0` suffix when neither `.` nor
    /// `e`/`E` is in the rendered string (parallel to surface print).
    /// Non-finite (NaN, ±Inf) render as the Mainstream-language
    /// spellings — `NaN`, `+Inf`, `-Inf` — because prose is a one-way
    /// render and the surface lex grammar's no-NaN/Inf restriction
    /// does not apply to it.
    #[test]
    fn renders_float_literal_finite() {
        use ailang_core::ast::*;
        let t = Term::Lit { lit: Literal::Float { bits: 0x3ff8_0000_0000_0000u64 } };
        let s = render_term(&t);
        assert_eq!(s, "1.5");

        let t = Term::Lit { lit: Literal::Float { bits: 0x4024_0000_0000_0000u64 } };
        let s = render_term(&t);
        assert_eq!(s, "10.0");
    }

    #[test]
    fn renders_float_literal_signed_zero() {
        use ailang_core::ast::*;
        let pos = Term::Lit { lit: Literal::Float { bits: 0x0u64 } };
        assert_eq!(render_term(&pos), "0.0");
        let neg = Term::Lit { lit: Literal::Float { bits: 0x8000_0000_0000_0000u64 } };
        assert_eq!(render_term(&neg), "-0.0");
    }

    #[test]
    fn renders_float_literal_non_finite() {
        use ailang_core::ast::*;
        let nan = Term::Lit { lit: Literal::Float { bits: 0x7ff8_0000_0000_0000u64 } };
        assert_eq!(render_term(&nan), "NaN");
        let pos_inf = Term::Lit { lit: Literal::Float { bits: 0x7ff0_0000_0000_0000u64 } };
        assert_eq!(render_term(&pos_inf), "+Inf");
        let neg_inf = Term::Lit { lit: Literal::Float { bits: 0xfff0_0000_0000_0000u64 } };
        assert_eq!(render_term(&neg_inf), "-Inf");
    }

    #[test]
    fn var_renders_as_name() {
        assert_eq!(render_term(&Term::Var { name: "x".into() }), "x");
    }

    // ---- App ----

    #[test]
    fn app_two_args_renders_as_call() {
        let t = Term::App {
            callee: Box::new(Term::Var { name: "f".into() }),
            args: vec![
                Term::Lit { lit: Literal::Int { value: 1 } },
                Term::Lit { lit: Literal::Int { value: 2 } },
            ],
            tail: false,
        };
        assert_eq!(render_term(&t), "f(1, 2)");
    }

    #[test]
    fn app_tail_renders_with_keyword() {
        let t = Term::App {
            callee: Box::new(Term::Var { name: "f".into() }),
            args: vec![],
            tail: true,
        };
        assert_eq!(render_term(&t), "tail f()");
    }

    // ---- Let / If ----

    #[test]
    fn let_with_single_use_inlines_rhs() {
        // `let x = 1; x` — single use of x, rhs is a literal, so the
        // binding is elided and the body renders the rhs at the
        // use-site.
        let t = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
            body: Box::new(Term::Var { name: "x".into() }),
        };
        assert_eq!(render_term(&t), "1");
    }

    #[test]
    fn let_with_two_uses_keeps_binding() {
        // `let x = 1; x + x` — two uses of x. Inlining would duplicate
        // work, so we keep the let.
        let t = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
            body: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "+".into() }),
                args: vec![
                    Term::Var { name: "x".into() },
                    Term::Var { name: "x".into() },
                ],
                tail: false,
            }),
        };
        assert_eq!(render_term(&t), "let x = 1;\nx + x");
    }

    #[test]
    fn let_with_zero_uses_keeps_binding() {
        // `let x = 1; 42` — x is unused. We keep the let; eliding it
        // would silently drop a binding the AST author chose to write.
        let t = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
            body: Box::new(Term::Lit { lit: Literal::Int { value: 42 } }),
        };
        assert_eq!(render_term(&t), "let x = 1;\n42");
    }

    #[test]
    fn let_with_do_rhs_keeps_binding() {
        // `let r = do io/get(); use(r)` — rhs is a Do, which carries
        // an effect. We keep effect sequencing visible; do not inline
        // even though r is used exactly once.
        let t = Term::Let {
            name: "r".into(),
            value: Box::new(Term::Do {
                op: "io/get".into(),
                args: vec![],
                tail: false,
            }),
            body: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "use".into() }),
                args: vec![Term::Var { name: "r".into() }],
                tail: false,
            }),
        };
        assert_eq!(render_term(&t), "let r = do io/get();\nuse(r)");
    }

    #[test]
    fn let_with_multiline_rhs_keeps_binding() {
        // `let x = (a; b); x` — single use, but the rhs renders as
        // two lines (a Seq), so inlining would smear a multiline
        // expression into the use-site. Keep the let.
        let t = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Seq {
                lhs: Box::new(Term::Var { name: "a".into() }),
                rhs: Box::new(Term::Var { name: "b".into() }),
            }),
            body: Box::new(Term::Var { name: "x".into() }),
        };
        // Outer rendering keeps the let. The rhs is a Seq, which
        // semicolon-separates a and b across lines.
        let rendered = render_term(&t);
        assert!(rendered.starts_with("let x ="), "got: {rendered}");
        assert!(rendered.ends_with("x"), "got: {rendered}");
    }

    #[test]
    fn let_with_long_rhs_keeps_binding_even_with_single_use() {
        // `let xs = <50-char Cons tower>; head(xs)` — single use,
        // single-line render, but the rhs exceeds the inline budget.
        // We keep the let: inlining a long literal smears the
        // surrounding line.
        // Build a 5-level Cons.
        let mk_cons = |h: i64, t: Term| -> Term {
            Term::Ctor {
                type_name: "L".into(),
                ctor: "Cons".into(),
                args: vec![Term::Lit { lit: Literal::Int { value: h } }, t],
            }
        };
        let nil = Term::Ctor {
            type_name: "L".into(),
            ctor: "Nil".into(),
            args: vec![],
        };
        let big = mk_cons(11, mk_cons(22, mk_cons(33, mk_cons(44, mk_cons(55, nil)))));
        let t = Term::Let {
            name: "xs".into(),
            value: Box::new(big),
            body: Box::new(Term::App {
                callee: Box::new(Term::Var { name: "head".into() }),
                args: vec![Term::Var { name: "xs".into() }],
                tail: false,
            }),
        };
        let rendered = render_term(&t);
        assert!(rendered.starts_with("let xs ="), "got: {rendered}");
        assert!(rendered.contains("head(xs)"), "got: {rendered}");
    }

    #[test]
    fn let_with_shadowing_inner_is_not_counted() {
        // `let x = 7; (let x = 99; x)` — outer x is never freely
        // referenced (the inner `let x` shadows it). Free-occurrence
        // count for the outer name is 0, so we keep the binding.
        let t = Term::Let {
            name: "x".into(),
            value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }),
            body: Box::new(Term::Let {
                name: "x".into(),
                value: Box::new(Term::Lit { lit: Literal::Int { value: 99 } }),
                body: Box::new(Term::Var { name: "x".into() }),
            }),
        };
        // Outer let is preserved (count == 0). Inner let is itself
        // inlinable (single use), so the body collapses to `99`.
        assert_eq!(render_term(&t), "let x = 7;\n99");
    }

    #[test]
    fn if_renders_with_braces_and_else() {
        let t = Term::If {
            cond: Box::new(Term::Lit { lit: Literal::Bool { value: true } }),
            then: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
            else_: Box::new(Term::Lit { lit: Literal::Int { value: 2 } }),
        };
        assert_eq!(
            render_term(&t),
            "if true {\n  1\n} else {\n  2\n}"
        );
    }

    // ---- Match ----

    #[test]
    fn match_two_arms_renders_with_arrows_and_commas() {
        let t = Term::Match {
            scrutinee: Box::new(Term::Var { name: "xs".into() }),
            arms: vec![
                Arm {
                    pat: Pattern::Ctor { ctor: "Nil".into(), fields: vec![] },
                    body: Term::Lit { lit: Literal::Int { value: 0 } },
                },
                Arm {
                    pat: Pattern::Ctor {
                        ctor: "Cons".into(),
                        fields: vec![
                            Pattern::Var { name: "h".into() },
                            Pattern::Var { name: "t".into() },
                        ],
                    },
                    body: Term::Var { name: "h".into() },
                },
            ],
        };
        assert_eq!(
            render_term(&t),
            "match xs {\n  Nil => 0,\n  Cons(h, t) => h\n}"
        );
    }

    // ---- Ctor ----

    #[test]
    fn ctor_nullary_renders_as_bare_name() {
        let t = Term::Ctor {
            type_name: "List".into(),
            ctor: "Nil".into(),
            args: vec![],
        };
        assert_eq!(render_term(&t), "Nil");
    }

    #[test]
    fn ctor_with_args_renders_as_call() {
        let t = Term::Ctor {
            type_name: "List".into(),
            ctor: "Cons".into(),
            args: vec![
                Term::Lit { lit: Literal::Int { value: 1 } },
                Term::Ctor {
                    type_name: "List".into(),
                    ctor: "Nil".into(),
                    args: vec![],
                },
            ],
        };
        assert_eq!(render_term(&t), "Cons(1, Nil)");
    }

    // ---- Lam ----

    #[test]
    fn lam_renders_as_rust_closure() {
        let t = Term::Lam {
            params: vec!["x".into()],
            param_tys: vec![Type::int()],
            ret_ty: Box::new(Type::int()),
            effects: vec![],
            body: Box::new(Term::Var { name: "x".into() }),
        };
        assert_eq!(render_term(&t), "|x: Int| -> Int {\n  x\n}");
    }

    // ---- Seq / Clone / ReuseAs / Do ----

    #[test]
    fn seq_renders_with_semicolon_and_newline() {
        let t = Term::Seq {
            lhs: Box::new(Term::Var { name: "a".into() }),
            rhs: Box::new(Term::Var { name: "b".into() }),
        };
        assert_eq!(render_term(&t), "a;\nb");
    }

    #[test]
    fn clone_renders_explicitly() {
        let t = Term::Clone {
            value: Box::new(Term::Var { name: "x".into() }),
        };
        assert_eq!(render_term(&t), "clone(x)");
    }

    #[test]
    fn reuse_as_inline_when_body_fits_on_one_line() {
        let t = Term::ReuseAs {
            source: Box::new(Term::Var { name: "xs".into() }),
            body: Box::new(Term::Ctor {
                type_name: "List".into(),
                ctor: "Nil".into(),
                args: vec![],
            }),
        };
        assert_eq!(render_term(&t), "reuse xs as Nil");
    }

    #[test]
    fn reuse_as_uses_braces_when_body_is_multiline() {
        // A Seq body forces a newline (`a;\nb`), so braces must fire.
        let t = Term::ReuseAs {
            source: Box::new(Term::Var { name: "xs".into() }),
            body: Box::new(Term::Seq {
                lhs: Box::new(Term::Var { name: "a".into() }),
                rhs: Box::new(Term::Var { name: "b".into() }),
            }),
        };
        assert_eq!(render_term(&t), "reuse xs as {\n  a;\n  b\n}");
    }

    #[test]
    fn do_renders_with_keyword_and_op() {
        let t = Term::Do {
            op: "io/print_str".into(),
            args: vec![Term::Lit {
                lit: Literal::Str {
                    value: "5".into(),
                },
            }],
            tail: false,
        };
        assert_eq!(render_term(&t), "do io/print_str(\"5\")");
    }

    // ---- Types ----

    #[test]
    fn type_con_no_args_drops_wrap() {
        assert_eq!(render_type(&Type::int()), "Int");
    }

    #[test]
    fn type_con_with_args_renders_as_generic() {
        let t = Type::Con {
            name: "List".into(),
            args: vec![Type::int()],
        };
        assert_eq!(render_type(&t), "List<Int>");
    }

    #[test]
    fn type_var_renders_as_name() {
        assert_eq!(render_type(&Type::Var { name: "a".into() }), "a");
    }

    #[test]
    fn type_fn_no_modes_no_effects() {
        let t = Type::fn_implicit(vec![Type::int()], Type::int(), vec![]);
        assert_eq!(render_type(&t), "(Int) -> Int");
    }

    #[test]
    fn type_fn_with_effects() {
        let t = Type::fn_implicit(vec![], Type::unit(), vec!["IO".into()]);
        assert_eq!(render_type(&t), "() -> Unit with IO");
    }

    #[test]
    fn type_fn_with_modes_renders_keywords_before_type() {
        let t = Type::Fn {
            params: vec![Type::int(), Type::bool_()],
            param_modes: vec![ParamMode::Own, ParamMode::Borrow],
            ret: Box::new(Type::int()),
            ret_mode: ParamMode::Own,
            effects: vec![],
        };
        assert_eq!(render_type(&t), "(own Int, borrow Bool) -> own Int");
    }

    #[test]
    fn type_forall_renders_with_angle_vars() {
        let t = Type::Forall {
            vars: vec!["a".into()],
            constraints: vec![],
            body: Box::new(Type::Var { name: "a".into() }),
        };
        assert_eq!(render_type(&t), "forall<a> a");
    }

    // ---- FnDef integration: modes BEFORE the type, in fn signature ----

    #[test]
    fn fn_def_signature_renders_modes_before_type() {
        let fd = FnDef {
            name: "head_or_zero".into(),
            ty: Type::Fn {
                params: vec![Type::Con {
                    name: "IntList".into(),
                    args: vec![],
                }],
                param_modes: vec![ParamMode::Own],
                ret: Box::new(Type::int()),
                ret_mode: ParamMode::Implicit,
                effects: vec![],
            },
            params: vec!["xs".into()],
            body: Term::Lit { lit: Literal::Int { value: 0 } },
            suppress: vec![],
            doc: None,
        export: None,
        };
        let mut out = String::new();
        write_fn_def(&mut out, &fd, 0, "");
        assert!(out.contains("xs: own IntList"), "got:\n{out}");
        assert!(out.contains(") -> Int "), "got:\n{out}");
    }

    #[test]
    fn fn_def_with_effects_appends_with_clause() {
        let fd = FnDef {
            name: "main".into(),
            ty: Type::fn_implicit(vec![], Type::unit(), vec!["IO".into()]),
            params: vec![],
            body: Term::Lit { lit: Literal::Unit },
            suppress: vec![],
            doc: None,
        export: None,
        };
        let mut out = String::new();
        write_fn_def(&mut out, &fd, 0, "");
        assert!(out.contains("() -> Unit with IO {"), "got:\n{out}");
    }

    /// a FnDef with a single `Suppress` entry renders the
    /// `// @suppress <code>: <reason>` line **above** the doc string,
    /// preserving both the suppression visibility and the doc content.
    /// The suppress line must appear before the `///`-prefixed doc
    /// lines, not after; the contract metadata leads.
    #[test]
    fn fn_def_renders_single_suppress_above_doc() {
        let fd = FnDef {
            name: "head_or_zero".into(),
            ty: Type::Fn {
                params: vec![Type::Con {
                    name: "IntList".into(),
                    args: vec![],
                }],
                param_modes: vec![ailang_core::ast::ParamMode::Own],
                ret: Box::new(Type::int()),
                ret_mode: ailang_core::ast::ParamMode::Implicit,
                effects: vec![],
            },
            params: vec!["xs".into()],
            body: Term::Lit { lit: Literal::Int { value: 0 } },
            suppress: vec![ailang_core::ast::Suppress {
                code: "over-strict-mode".into(),
                because: "RC codegen test fixture".into(),
            }],
            doc: Some("Take ownership.".into()),
        export: None,
        };
        let mut out = String::new();
        write_fn_def(&mut out, &fd, 0, "");
        // Suppress line is the FIRST line, before the doc.
        let first_line = out.lines().next().unwrap();
        assert_eq!(
            first_line, "// @suppress over-strict-mode: RC codegen test fixture",
            "first line must be the suppress comment; got:\n{out}"
        );
        // Doc string follows on the next line.
        let lines: Vec<&str> = out.lines().collect();
        assert_eq!(lines[1], "/// Take ownership.", "doc line should follow; got:\n{out}");
        // Fn signature follows the doc.
        assert!(
            out.contains("fn head_or_zero(xs: own IntList) -> Int"),
            "fn signature should follow; got:\n{out}"
        );
    }

    /// multiple `Suppress` entries render as one
    /// `// @suppress <code>: <reason>` line each, in declaration
    /// order, all above the doc string.
    #[test]
    fn fn_def_renders_multiple_suppress_in_order() {
        let fd = FnDef {
            name: "f".into(),
            ty: Type::fn_implicit(vec![], Type::int(), vec![]),
            params: vec![],
            body: Term::Lit { lit: Literal::Int { value: 0 } },
            suppress: vec![
                ailang_core::ast::Suppress {
                    code: "over-strict-mode".into(),
                    because: "first reason".into(),
                },
                ailang_core::ast::Suppress {
                    code: "some-other-code".into(),
                    because: "second reason".into(),
                },
            ],
            doc: None,
        export: None,
        };
        let mut out = String::new();
        write_fn_def(&mut out, &fd, 0, "");
        let lines: Vec<&str> = out.lines().collect();
        assert_eq!(lines[0], "// @suppress over-strict-mode: first reason");
        assert_eq!(lines[1], "// @suppress some-other-code: second reason");
        // Order: declaration order is preserved.
    }

    /// a FnDef with an empty `suppress` Vec emits no
    /// `// @suppress` line at all (and therefore no extra leading
    /// blank line). Pre-19b prose snapshots stay byte-identical when
    /// re-rendered through the 19b code.
    #[test]
    fn fn_def_with_empty_suppress_emits_no_suppress_lines() {
        let fd = FnDef {
            name: "f".into(),
            ty: Type::fn_implicit(vec![], Type::int(), vec![]),
            params: vec![],
            body: Term::Lit { lit: Literal::Int { value: 0 } },
            suppress: vec![],
            doc: Some("just a doc".into()),
        export: None,
        };
        let mut out = String::new();
        write_fn_def(&mut out, &fd, 0, "");
        assert!(
            !out.contains("// @suppress"),
            "no @suppress line for empty Vec; got:\n{out}"
        );
        // The doc still leads.
        let first_line = out.lines().next().unwrap();
        assert_eq!(first_line, "/// just a doc");
    }

    // ---- Doc string lines ----

    #[test]
    fn doc_string_renders_as_triple_slash_lines() {
        let td = TypeDef {
            name: "Foo".into(),
            vars: vec![],
            ctors: vec![Ctor {
                name: "MkFoo".into(),
                fields: vec![],
            }],
            doc: Some("line one\nline two".into()),
            drop_iterative: false,
        };
        let mut out = String::new();
        write_type_def(&mut out, &td, 0, "");
        assert!(out.starts_with("/// line one\n/// line two\n"), "got:\n{out}");
    }

    // ---- TypeDef ----

    #[test]
    fn type_def_renders_with_pipe_separated_ctors() {
        let td = TypeDef {
            name: "IntList".into(),
            vars: vec![],
            ctors: vec![
                Ctor { name: "Nil".into(), fields: vec![] },
                Ctor {
                    name: "Cons".into(),
                    fields: vec![Type::int(), Type::Con { name: "IntList".into(), args: vec![] }],
                },
            ],
            doc: None,
            drop_iterative: false,
        };
        let mut out = String::new();
        write_type_def(&mut out, &td, 0, "");
        assert_eq!(out, "data IntList = Nil | Cons(Int, IntList)");
    }

    // ======================================================================
    // 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() {
        // 2026-05-21 operator-routing-eq-ord: the six comparator
        // names are no longer surface identifiers; only the five
        // arithmetic ops infix-render.
        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)");
    }

    // 2026-05-21 operator-routing-eq-ord: removed
    // `non_assoc_same_level_keeps_parens_on_both_sides` —
    // `< < <` chains were the only sub-case where non-assoc
    // precedence mattered; with `<` no longer a surface op, the
    // remaining (arithmetic) infix ops are all left-assoc so the
    // non-assoc path is no longer reachable from any AST a user
    // could produce.

    #[test]
    fn atomic_subexpr_never_wraps() {
        // A var on either side of an arithmetic op never picks up
        // parens. (Pre-eq-ord this fixture used `==`; with `==` no
        // longer infix-rendered, the same property holds for `+`.)
        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 below the
        // unary floor `PREC_ATOMIC`, so the wrap stays. (Pre-eq-ord
        // this exercised `==`; with `==` no longer infix-rendered,
        // `+` is the parallel case for arithmetic.)
        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}");
    }

    #[test]
    fn doc_wrap_widow_control_pulls_one_word_back() {
        // A doc string whose greedy wrap leaves a 1-word orphan as
        // the last line should pull the previous line's tail word
        // down so the orphan has at least 2 words. This is exactly
        // the `nested_let_rec` case where "outer's param i." used
        // to wrap to "outer's param" / "i.".
        let doc = "Sum 1 + 2 + ... + n by nested LetRec helpers; inner captures \
                   outer's param i.";
        let td = TypeDef {
            name: "Foo".into(),
            vars: vec![],
            ctors: vec![Ctor { name: "MkFoo".into(), fields: vec![] }],
            doc: Some(doc.into()),
            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();
        // The last doc line MUST have ≥ 2 words.
        let last = doc_lines.last().unwrap();
        let last_word_count = last
            .trim_start_matches("///")
            .split_whitespace()
            .count();
        assert!(
            last_word_count >= 2,
            "expected widow control to leave ≥ 2 words on the last line; got {last:?}"
        );
        // No line over the 80-col budget.
        for line in &doc_lines {
            assert!(line.len() <= 80, "line over 80 cols: {line:?}");
        }
    }

    #[test]
    fn doc_wrap_widow_control_skips_when_combined_too_long() {
        // If the combined length of (pulled + " " + orphan) would
        // exceed budget, widow control must NOT fire — preserving
        // the wrap budget invariant takes priority over cosmetics.
        // Construct a case: prev-tail = a long word, orphan = a long
        // word — combined > 80.
        let pieces = "aaaaaaaaaaaaaaaaaaaaaaaaaaaaaaaa bbbbbbbbbbbbbbbbbbbbbbbbbbbbbbbb \
                      cccccccccccccccccccccccccccccccccccccccccc";
        let lines = wrap_words(pieces, 80);
        // Sanity: the wrap produced multiple lines.
        assert!(lines.len() >= 2);
        // No line exceeds budget.
        for l in &lines {
            assert!(l.len() <= 80, "line over budget: {l:?}");
        }
    }

    // ---- 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\
             }"
        );
    }

    /// When a `Type::Con.name` is qualified with the owning
    /// module's own name (e.g. `prelude.Ordering` inside
    /// `prelude`'s own file), the prose printer must trim the
    /// qualifier and emit bare `Ordering`. Cross-module qualified
    /// refs (`prelude.Ordering` inside any non-prelude file)
    /// round-trip verbatim.
    #[test]
    fn type_con_qualifier_trimmed_when_owner_matches_module() {
        use ailang_core::ast::{Module, Def, FnDef, Type, Term, ParamMode};

        let m = Module {
            schema: "ailang/v0".into(),
            name: "prelude".into(),
            imports: vec![],
            defs: vec![Def::Fn(FnDef {
                name: "noop".into(),
                ty: Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::Con {
                        name: "prelude.Ordering".into(),
                        args: vec![],
                    }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                params: vec![],
                body: Term::Ctor {
                    type_name: "prelude.Ordering".into(),
                    ctor: "EQ".into(),
                    args: vec![],
                },
                doc: None,
                suppress: vec![],
            export: None,
            })],
        };

        let prose = module_to_prose(&m);
        assert!(
            prose.contains("-> Ordering"),
            "expected bare `Ordering` in fn return type (owner == file's \
             module); got prose:\n{}",
            prose
        );
        assert!(
            !prose.contains("prelude.Ordering"),
            "expected NO `prelude.Ordering` after trim; got prose:\n{}",
            prose
        );
    }

    /// A cross-module Type::Con (owner != current file's module)
    /// must round-trip verbatim — no trim.
    #[test]
    fn type_con_qualifier_preserved_when_owner_differs() {
        use ailang_core::ast::{Module, Def, FnDef, Type, Term, ParamMode, Import};

        let m = Module {
            schema: "ailang/v0".into(),
            name: "user".into(),
            imports: vec![Import { module: "prelude".into(), alias: None }],
            defs: vec![Def::Fn(FnDef {
                name: "lt".into(),
                ty: Type::Fn {
                    params: vec![],
                    ret: Box::new(Type::Con {
                        name: "prelude.Ordering".into(),
                        args: vec![],
                    }),
                    effects: vec![],
                    param_modes: vec![],
                    ret_mode: ParamMode::Implicit,
                },
                params: vec![],
                body: Term::Ctor {
                    type_name: "prelude.Ordering".into(),
                    ctor: "LT".into(),
                    args: vec![],
                },
                doc: None,
                suppress: vec![],
            export: None,
            })],
        };

        let prose = module_to_prose(&m);
        assert!(
            prose.contains("prelude.Ordering"),
            "expected qualified `prelude.Ordering` preserved (owner != file's \
             module); got prose:\n{}",
            prose
        );
    }

    #[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}");
    }
}