diff --git a/crates/ailang-prose/src/lib.rs b/crates/ailang-prose/src/lib.rs index 40b1657..9a0c338 100644 --- a/crates/ailang-prose/src/lib.rs +++ b/crates/ailang-prose/src/lib.rs @@ -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 as `. 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) { + 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::() + } + 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] diff --git a/examples/rc_app_let_partial_drop_leak.prose.txt b/examples/rc_app_let_partial_drop_leak.prose.txt index cb95cdc..68a243b 100644 --- a/examples/rc_app_let_partial_drop_leak.prose.txt +++ b/examples/rc_app_let_partial_drop_leak.prose.txt @@ -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) }) }