prose: split reuse-as keyword + inline single-use lets (iter 20b polish)

reuse-as: render `(reuse-as src body)` as `reuse src as body` with
adaptive braces — inline for single-line bodies (the 99% Ctor case),
braced for multi-line (Let, Seq, nested Match). Reads as English
subject-verb-object instead of compound keyword + always-block.

let-inlining: `let x = rhs; <body using x once>` collapses to
`<body[x := rhs]>` when (a) rhs is not a `Term::Do` (keep effect
sequencing visible), (b) x is used exactly once (no work duplication),
(c) rhs renders single-line AND ≤ 40 chars (no line smearing). Lossy
projection — round-trip mediator sees the original .ail.json and can
re-introduce a let when the mode model demands it.

Helpers `count_free_var` and `subst_var_with_term` are render-local;
both respect inner shadowing (let, lam, match arm pattern binders,
let rec). Pre-render value at current level + check for newline + len
budget; on inline, write_term_prec gets passed parent_prec so the
substituted term still wraps correctly inside binops.

Snapshot drift: rc_app_let_partial_drop_leak.prose.txt — boilerplate
`let p = build_pair(1)` collapsed into the match scrutinee. Improves
readability. Cons-tower in rc_own_param_drop kept its let thanks to
the length budget (52 chars > 40).

Tests: 59 unit (+ 9 new) + 4 snapshot, all green. Coverage:
inline-single-use, two-uses-keeps, zero-uses-keeps, Do-rhs-keeps,
multiline-rhs-keeps, length-budget-keeps, shadowing-not-counted,
reuse-as inline + braces.
This commit is contained in:
2026-05-08 23:03:10 +02:00
parent bfe49084de
commit 8375eb81ed
2 changed files with 399 additions and 24 deletions
+398 -22
View File
@@ -531,17 +531,41 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
out.push(')');
}
Term::Let { name, value, body } => {
// `let x = value;` then body on the next line at the same
// level. Both lines are emitted by the *enclosing* context's
// indentation; the caller indented us once already, so for
// the body we re-indent.
out.push_str("let ");
out.push_str(name);
out.push_str(" = ");
write_term(out, value, level);
out.push_str(";\n");
indent(out, level);
write_term(out, body, level);
// 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);
!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);
} else {
out.push_str("let ");
out.push_str(name);
out.push_str(" = ");
write_term(out, value, level);
out.push_str(";\n");
indent(out, level);
write_term(out, body, level);
}
}
Term::LetRec {
name,
@@ -713,14 +737,28 @@ fn write_term_prec(out: &mut String, t: &Term, level: usize, parent_prec: u8) {
out.push(')');
}
Term::ReuseAs { source, body } => {
out.push_str("reuse-as ");
// 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);
out.push_str(" {\n");
indent(out, level + 1);
write_term(out, body, level + 1);
out.push('\n');
indent(out, level);
out.push('}');
out.push_str(" as ");
let mut body_buf = String::new();
write_term(&mut body_buf, body, level + 1);
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);
}
}
}
}
@@ -778,6 +816,203 @@ fn indent(out: &mut String, level: usize) {
}
}
// ---- 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),
}
}
/// 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)),
},
}
}
// ---- unit tests -----------------------------------------------------------
#[cfg(test)]
@@ -862,13 +1097,141 @@ mod tests {
// ---- Let / If ----
#[test]
fn let_renders_as_binding_and_body() {
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), "let x = 1;\nx");
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]
@@ -976,7 +1339,7 @@ mod tests {
}
#[test]
fn reuse_as_renders_with_keyword_and_braces() {
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 {
@@ -985,7 +1348,20 @@ mod tests {
args: vec![],
}),
};
assert_eq!(render_term(&t), "reuse-as xs {\n Nil\n}");
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]
@@ -18,8 +18,7 @@ fn use_cell(c: own Cell) -> Int {
}
fn main() -> Unit with IO {
let p = build_pair(1);
do io/print_int(match p {
do io/print_int(match build_pair(1) {
MkPair(a, _) => use_cell(a)
})
}