From 19901474675d3c1887775589d4d6ba0a6e1cf8e0 Mon Sep 17 00:00:00 2001 From: Brummel Date: Sat, 30 May 2026 12:35:07 +0200 Subject: [PATCH] =?UTF-8?q?plan:=20unique-binder-names=20=E2=80=94=20desug?= =?UTF-8?q?ar=20alpha-rename=20for=20#43=20A2b=20(refs=20#43)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Executable plan for spec 0056. Three tasks: - Task 1 (atomic compile unit): introduce a `Scope` struct threading two maps — `entries` keyed by each binder's effective (post-rename) name, `rename` mapping authored→effective for shadow detection and Term::Var resolution; add `fresh_binder` ($) and `rename_pattern_binders`; rewrite every binder site (Let, flat-Match pattern, Lam params, Loop binders) with rename-on-shadow, plus the LetRec arm and both def-boundary constructions, to the new API. - Task 2: correct the UniquenessTable doc-comment; verify the four RED tests go GREEN; full-suite regression gate. - Task 3: regression guard — a desugar unit test pinning that a shadowing let is alpha-renamed and that a letrec capturing the shadow-renamed binder still resolves (the entries-keyed-by-effective choice is what keeps capture detection correct under rename). Recon surfaced two facts the spec's sketch did not: the scope is a bare BTreeMap (so resolved_name/bind live on a new Scope type, not the map), and the LetRec capture-detection reads effective names from the desugared body — hence entries are keyed by effective name. Both stay internal to desugar.rs, preserving acceptance criterion 5 (no change to uniqueness.rs logic / codegen gates / linearity.rs). Both no-change consumers verified: match_lower.rs:795 keys by the emitted (renamed) pattern binder; linearity builds table and lookups from the same desugared tree. --- docs/plans/0111-unique-binder-names.md | 559 +++++++++++++++++++++++++ 1 file changed, 559 insertions(+) create mode 100644 docs/plans/0111-unique-binder-names.md diff --git a/docs/plans/0111-unique-binder-names.md b/docs/plans/0111-unique-binder-names.md new file mode 100644 index 0000000..f985905 --- /dev/null +++ b/docs/plans/0111-unique-binder-names.md @@ -0,0 +1,559 @@ +# Unique Binder Names per Fn — Implementation Plan + +> **Parent spec:** `docs/specs/0056-unique-binder-names.md` +> +> **For agentic workers:** REQUIRED SUB-SKILL: use the +> `implement` skill to run this plan. Steps use `- [ ]` +> checkboxes for tracking. + +**Goal:** Make every binder name unique within its fn by alpha-renaming +shadowing binders during desugaring, so the uniqueness side-table key +`(def_name, binder_name)` is injective again — closing the A2b leg of +RawBuf drop-leak #43. + +**Architecture:** The lexical scope threaded through `desugar_term` +becomes a small `Scope` struct carrying two maps: `entries` keyed by +each binder's **effective** (post-rename) name (feeding the existing +type/capture lookups unchanged), and `rename` mapping every in-scope +**authored** name to its current effective name (the shadow-detector +and the `Term::Var` resolver). At each binder-introduction site (`Let`, +flat-`Match` pattern-binders, `Lam` params, `Loop` binders) a binder +whose authored name is already bound gets a fresh `$` name; its +references resolve through `rename`. Never-renamed binders (fn-params, +`LetRec` name/params) record an identity rename so an inner renamable +binder that shadows them is still detected. No consumer of the +uniqueness table changes — they all key by name, and the name is now a +per-fn injective identity. + +**Tech Stack:** `crates/ailang-core/src/desugar.rs` (the entire fix), +`crates/ailang-check/src/uniqueness.rs` (doc-comment correction only). +The four RED tests and their fixtures already exist in the tree +(`crates/ail/tests/e2e.rs`, `examples/{raw_buf_*,flat_pat_shadow_*}.ail`). + +--- + +## Files this plan creates or modifies + +- Modify: `crates/ailang-core/src/desugar.rs` — add `Scope` struct + + impl after `ScopeEntry` (line 144); add `Desugarer::fresh_binder` + (after line 455); add free fn `rename_pattern_binders`; change + `desugar_term`'s `scope` parameter type and rewrite every binder + site + `Term::Var` + the two def-boundary scope constructions. +- Modify: `crates/ailang-check/src/uniqueness.rs:90-98` — correct the + `UniquenessTable` doc-comment (pop-order + "every fixture unique" + claims are both wrong). +- Test (pre-existing, RED today): `crates/ail/tests/e2e.rs` — + `raw_buf_{int,float,bool}_shadow_rebind_drop_balances_rc_stats`, + `flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed`. +- Test (new, regression guard): `crates/ailang-core/src/desugar.rs` + in-source `#[cfg(test)] mod tests` — a shadowing-let desugar unit + test and a letrec-captures-shadowed-binder robustness test. + +--- + +## Task 1: Scope-with-renames + rename-on-shadow across all binder sites + +This task is one atomic compilation unit: changing `desugar_term`'s +`scope` parameter type forces every scope-construction and +scope-mutation site to update in the same task. It ends with a clean +`cargo build -p ailang-core` and the existing in-source desugar tests +still green (non-shadowing output is byte-identical). + +**Files:** +- Modify: `crates/ailang-core/src/desugar.rs` + +- [ ] **Step 1: Add the `Scope` struct and impl** + +Insert immediately after the `ScopeEntry` enum's closing brace (after +line 144, before the `/// Rewrite `m` …` doc-comment on line 146): + +```rust +/// Lexical scope threaded through desugaring. +/// +/// `entries` is keyed by each binder's **effective** (post-shadow- +/// rename) name and feeds the existing type-/capture-lookups +/// unchanged. `rename` maps every in-scope **authored** name to its +/// current effective name; it is the shadow-detector ([`is_bound`]) +/// and the [`Term::Var`] resolver ([`resolved_name`]). +/// +/// For a program with no shadowing, every effective name equals its +/// authored name and `rename` is all-identity, so the desugared +/// output is byte-identical to the pre-rename pass. +/// +/// [`is_bound`]: Scope::is_bound +/// [`resolved_name`]: Scope::resolved_name +#[derive(Clone, Default)] +struct Scope { + entries: BTreeMap, + rename: BTreeMap, +} + +impl Scope { + /// Is the **effective** name `eff` an entry here? (capture / + /// type lookups, which operate on the desugared tree's names). + fn contains_key(&self, eff: &str) -> bool { + self.entries.contains_key(eff) + } + + /// The [`ScopeEntry`] for an **effective** name. + fn get(&self, eff: &str) -> Option<&ScopeEntry> { + self.entries.get(eff) + } + + /// Is the **authored** name already lexically bound here? — the + /// shadow test. True for any binder kind, including identity- + /// renamed fixed binders (fn-params, LetRec name/params). + fn is_bound(&self, authored: &str) -> bool { + self.rename.contains_key(authored) + } + + /// Resolve an **authored** name to its current effective name. + /// Verbatim for free names (module-level fns, builtins, ctors), + /// which were never bound at a binder site in this fn. + fn resolved_name(&self, authored: &str) -> String { + self.rename + .get(authored) + .cloned() + .unwrap_or_else(|| authored.to_string()) + } + + /// Install a possibly-renamed binder: record `entries[effective]` + /// and `rename[authored → effective]`. + fn insert_effective(&mut self, authored: &str, effective: String, entry: ScopeEntry) { + self.entries.insert(effective.clone(), entry); + self.rename.insert(authored.to_string(), effective); + } + + /// Install a never-renamed binder (fn-params, LetRec name/params). + /// The identity rename keeps the name visible to [`is_bound`] so an + /// inner *renamable* binder that shadows it is still detected. + fn insert_fixed(&mut self, name: &str, entry: ScopeEntry) { + self.entries.insert(name.to_string(), entry); + self.rename.insert(name.to_string(), name.to_string()); + } +} +``` + +- [ ] **Step 2: Add the `fresh_binder` generator** + +Insert into the `impl Desugarer` block immediately after `fresh_lifted` +(after line 455, before the `/// Recursively rewrites …` doc on 457): + +```rust + /// A binder name unique within the current fn: `$` with + /// the lowest `n ≥ 1` free in both `scope` (in-scope effective + /// names) and `used` (the `$mp_` / `$lr_` synthetic space). + /// Records the minted name in `used` so a later mint is distinct. + /// Authored names cannot contain `$` (the lexer reserves it for + /// synthetic names), so `$` never collides with an + /// authored binder. + fn fresh_binder(&mut self, base: &str, scope: &Scope) -> String { + let mut n = 1u64; + loop { + let candidate = format!("{base}${n}"); + n += 1; + if !self.used.contains(&candidate) && !scope.contains_key(&candidate) { + self.used.insert(candidate.clone()); + return candidate; + } + } + } +``` + +- [ ] **Step 3: Add the `rename_pattern_binders` free fn** + +Insert near the other pattern free fns (immediately before the +`pattern_binds` fn at line 1281 — locate it by `fn pattern_binds`): + +```rust +/// Rewrites the `Pattern::Var` binder names in `pat` per `renamed` +/// (authored → effective); leaves `Wild` / `Lit` and any binder not in +/// the map untouched. Threads shadow-renamed flat-pattern binders into +/// the emitted pattern so codegen's arm-close drop gate keys by the +/// same renamed name the arm body references. +fn rename_pattern_binders(pat: &Pattern, renamed: &BTreeMap) -> Pattern { + match pat { + Pattern::Wild => Pattern::Wild, + Pattern::Lit { lit } => Pattern::Lit { lit: lit.clone() }, + Pattern::Var { name } => Pattern::Var { + name: renamed.get(name).cloned().unwrap_or_else(|| name.clone()), + }, + Pattern::Ctor { ctor, fields } => Pattern::Ctor { + ctor: ctor.clone(), + fields: fields + .iter() + .map(|f| rename_pattern_binders(f, renamed)) + .collect(), + }, + } +} +``` + +- [ ] **Step 4: Change `desugar_term`'s signature and split the `Var` arm** + +At line 475, change the parameter type: + +```rust + fn desugar_term(&mut self, t: &Term, scope: &Scope) -> Term { +``` + +At line 477, replace the shared `Lit | Var` arm: + +```rust + Term::Lit { .. } => t.clone(), + Term::Var { name } => Term::Var { + name: scope.resolved_name(name), + }, +``` + +- [ ] **Step 5: Rewrite the `Term::Let` binder site** + +Replace lines 483-493 (the `Term::Let` arm): + +```rust + Term::Let { name, value, body } => { + let v = self.desugar_term(value, scope); + let mut inner = scope.clone(); + let effective = if inner.is_bound(name) { + self.fresh_binder(name, &inner) + } else { + name.clone() + }; + inner.insert_effective(name, effective.clone(), ScopeEntry::LetBound); + let b = self.desugar_term(body, &inner); + Term::Let { + name: effective, + value: Box::new(v), + body: Box::new(b), + } + } +``` + +- [ ] **Step 6: Rewrite the `Term::Match` arm loop (rename pattern binders)** + +Replace lines 509-528 (the `Term::Match` arm): + +```rust + Term::Match { scrutinee, arms } => { + // Recurse into children first (bottom-up). + let scrutinee = self.desugar_term(scrutinee, scope); + let arms: Vec = arms + .iter() + .map(|a| { + let mut inner = scope.clone(); + let mut pat_binds: BTreeSet = BTreeSet::new(); + pattern_binds(&a.pat, &mut pat_binds); + let mut renamed: BTreeMap = BTreeMap::new(); + for n in &pat_binds { + let effective = if inner.is_bound(n) { + self.fresh_binder(n, &inner) + } else { + n.clone() + }; + if effective != *n { + renamed.insert(n.clone(), effective.clone()); + } + inner.insert_effective(n, effective, ScopeEntry::MatchArm); + } + let pat = if renamed.is_empty() { + a.pat.clone() + } else { + rename_pattern_binders(&a.pat, &renamed) + }; + Arm { + pat, + body: self.desugar_term(&a.body, &inner), + } + }) + .collect(); + self.desugar_match(scrutinee, arms) + } +``` + +- [ ] **Step 7: Rewrite the `Term::Lam` param loop** + +Replace lines 529-547 (the `Term::Lam` arm): + +```rust + Term::Lam { + params, + param_tys, + ret_ty, + effects, + body, + } => { + let mut inner = scope.clone(); + let mut new_params: Vec = Vec::with_capacity(params.len()); + for (p, pty) in params.iter().zip(param_tys.iter()) { + let effective = if inner.is_bound(p) { + self.fresh_binder(p, &inner) + } else { + p.clone() + }; + inner.insert_effective(p, effective.clone(), ScopeEntry::KnownType(pty.clone())); + new_params.push(effective); + } + Term::Lam { + params: new_params, + param_tys: param_tys.clone(), + ret_ty: ret_ty.clone(), + effects: effects.clone(), + body: Box::new(self.desugar_term(body, &inner)), + } + } +``` + +- [ ] **Step 8: Rewrite the `Term::Loop` binder loop** + +Replace lines 563-586 (the `Term::Loop` arm): + +```rust + Term::Loop { binders, body } => { + // loop-recur iter 1: structural recursion. Each + // binder's init is desugared in scope of the outer env + // plus already-declared binders; the body sees all + // binders. A binder whose name shadows an enclosing + // binding is alpha-renamed (uniqueness-table injectivity). + let mut inner = scope.clone(); + let new_binders: Vec = binders + .iter() + .map(|b| { + let init = self.desugar_term(&b.init, &inner); + let effective = if inner.is_bound(&b.name) { + self.fresh_binder(&b.name, &inner) + } else { + b.name.clone() + }; + inner.insert_effective(&b.name, effective.clone(), ScopeEntry::LetBound); + LoopBinder { + name: effective, + ty: b.ty.clone(), + init, + } + }) + .collect(); + Term::Loop { + binders: new_binders, + body: Box::new(self.desugar_term(body, &inner)), + } + } +``` + +- [ ] **Step 9: Update the `Term::LetRec` arm to the new scope API** + +The LetRec name and its params are **not** renamed (out of the spec's +renamable set; a lifted LetRec gets its own def namespace, so its +binders cannot collide in the `(def, name)` key). They use +`insert_fixed` so an inner renamable binder that shadows them is still +detected, and so capture detection — which reads the **effective** names +of the desugared body — keeps working when an enclosing binder was +renamed (the effective name is in `entries`). + +In lines 644-655, replace the four scope mutations: + +```rust + // Body's scope: outer ∪ {name → EnclosingLetRec} ∪ + // params with their declared types as KnownType. + let mut body_scope = scope.clone(); + body_scope.insert_fixed(name, ScopeEntry::EnclosingLetRec); + for (p, pty) in params.iter().zip(inner_params_tys.iter()) { + body_scope.insert_fixed(p, ScopeEntry::KnownType(pty.clone())); + } + let desugared_body = self.desugar_term(body, &body_scope); + // in_term's scope: outer ∪ {name → EnclosingLetRec} + // (params are lambda-local to the LetRec's body, + // not visible in `in`). + let mut in_scope = scope.clone(); + in_scope.insert_fixed(name, ScopeEntry::EnclosingLetRec); + let desugared_in = self.desugar_term(in_term, &in_scope); +``` + +No other change in the LetRec arm: the capture-detection +`scope.contains_key(*f)` (line 714) and `scope.get(c)` (lines 733, 776) +now resolve through the delegating methods and read effective names — +exactly the names present in the desugared body. The defer-path +`Term::LetRec { name: name.clone(), … }` (line 765) is unchanged (the +LetRec name is never renamed). + +- [ ] **Step 10: Convert the two def-boundary scope constructions** + +`Def::Fn` (lines 219-247): change the construction and both param +inserts. Replace line 219: + +```rust + let mut scope = Scope::default(); +``` + +Replace line 235 (inside the `KnownType` arm): + +```rust + scope.insert_fixed(p, ScopeEntry::KnownType(pty.clone())); +``` + +Replace line 244 (inside the defensive `LetBound` fallback): + +```rust + scope.insert_fixed(p, ScopeEntry::LetBound); +``` + +`Def::Const` (line 259): replace: + +```rust + let scope = Scope::default(); +``` + +- [ ] **Step 11: Build gate — `ailang-core` compiles clean** + +Run: `cargo build -p ailang-core 2>&1 | tail -5` +Expected: finishes with no `error[` lines (warnings tolerated). + +- [ ] **Step 12: Non-shadow regression — existing desugar tests green** + +Run: `cargo test -p ailang-core 2>&1 | tail -15` +Expected: `test result: ok.` — every existing in-source desugar test +passes. (These feed no shadowing input, so their desugared output is +byte-identical; this is the evidence the rename is on-shadow-only.) + +--- + +## Task 2: Turn the four RED tests GREEN + correct the doc-comment + +**Files:** +- Modify: `crates/ailang-check/src/uniqueness.rs:90-98` +- Test (pre-existing): `crates/ail/tests/e2e.rs` + +- [ ] **Step 1: Correct the `UniquenessTable` doc-comment** + +Replace the doc-comment at `crates/ailang-check/src/uniqueness.rs:90-98` +(the block directly above `pub type UniquenessTable = …` on line 99): + +```rust +/// Side table indexed by `(def_name, binder_name)`. Built fresh for +/// each codegen invocation; the side table is not cached. +/// +/// The key is injective per fn: desugaring alpha-renames any binder +/// whose name shadows an enclosing binding to a fresh `$` +/// (see `ailang-core::desugar`), so within one `def_name` every +/// `binder_name` denotes exactly one binding. Codegen consumers look +/// up by current-scope binder name and always resolve the binding +/// they mean — there is no shadow collapse. +``` + +- [ ] **Step 2: Let-shadow leak tests pass** + +Run: `cargo test -p ail --test e2e shadow_rebind 2>&1 | tail -8` +Expected: PASS for `raw_buf_int_shadow_rebind_drop_balances_rc_stats`, +`raw_buf_float_shadow_rebind_drop_balances_rc_stats`, +`raw_buf_bool_shadow_rebind_drop_balances_rc_stats` (`live == 0`; they +asserted `live == 1` RED before this fix). + +- [ ] **Step 3: Flat-pattern differential test passes** + +Run: `cargo test -p ail --test e2e flat_pat_shadow 2>&1 | tail -8` +Expected: PASS for +`flat_pat_shadow_binder_does_not_leak_more_than_alpha_renamed` (shadow +`live` now equals the alpha-renamed control's `live`; it was `5` vs `3` +RED before). + +- [ ] **Step 4: Full workspace suite — no regressions** + +Run: `cargo test 2>&1 | tail -20` +Expected: every crate reports `test result: ok.`; no failures, no +fixture whose output drifted. + +--- + +## Task 3: Regression guard — letrec capture of a shadow-renamed binder + +The LetRec-capture interaction (Task 1 Step 9) is load-bearing but has +no fixture today. This unit test pins it: a let that shadows an outer +let, with a `Term::LetRec` in the inner scope whose body captures the +shadowed binder. The captured `Term::Var` in the desugared output must +carry the **renamed** name and remain a recognised capture (no +`UnknownVar`-class free var leaks into the lifted/deferred fn). + +**Files:** +- Test (new): `crates/ailang-core/src/desugar.rs` in-source + `#[cfg(test)] mod tests`. + +- [ ] **Step 1: Add a shadowing-let desugar unit test** + +Add to the in-source `#[cfg(test)] mod tests` (locate it by +`mod tests`; place the test beside the existing `flat_match_is_unchanged_shape` +test): + +```rust + /// A `let` that shadows an enclosing same-named `let` is + /// alpha-renamed to a fresh `$`, and references in its + /// body resolve to the renamed binder — the uniqueness-table + /// `(def, name)` key is injective per fn (refs #43). + #[test] + fn shadowing_let_is_alpha_renamed() { + let mut d = Desugarer { + counter: 0, + used: BTreeSet::new(), + lifted: Vec::new(), + module_top_names: BTreeSet::new(), + current_def_forall_vars: Vec::new(), + }; + // (let x 1 (let x (+ x 1) x)) + let inner = Term::Let { + name: "x".into(), + value: Box::new(Term::App { + callee: Box::new(Term::Var { name: "+".into() }), + args: vec![ + Term::Var { name: "x".into() }, + Term::Lit { lit: Literal::Int { value: 1 } }, + ], + tail: false, + }), + body: Box::new(Term::Var { name: "x".into() }), + }; + let outer = Term::Let { + name: "x".into(), + value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }), + body: Box::new(inner), + }; + let out = d.desugar_term(&outer, &Scope::default()); + // Outer binder keeps `x`; inner binder becomes `x$1`; the + // inner value's `x` ref resolves to the outer `x`; the inner + // body's `x` ref resolves to `x$1`. + let Term::Let { name: o_name, body: o_body, .. } = &out else { + panic!("expected outer Let, got {out:?}"); + }; + assert_eq!(o_name, "x"); + let Term::Let { name: i_name, value: i_val, body: i_body } = o_body.as_ref() else { + panic!("expected inner Let, got {o_body:?}"); + }; + assert_eq!(i_name, "x$1", "shadowing inner binder must be renamed"); + // inner value `(+ x 1)` still refers to the outer `x` + let Term::App { args, .. } = i_val.as_ref() else { + panic!("expected App in inner value, got {i_val:?}"); + }; + assert!( + matches!(&args[0], Term::Var { name } if name == "x"), + "inner value's ref must resolve to outer `x`, got {:?}", + args[0] + ); + // inner body `x` resolves to the renamed `x$1` + assert!( + matches!(i_body.as_ref(), Term::Var { name } if name == "x$1"), + "inner body's ref must resolve to renamed `x$1`, got {i_body:?}", + ); + } +``` + +`Term`, `Literal`, `Scope`, `Desugarer`, and `BTreeSet` resolve via the +test module's `use super::*;` (the same path the neighbouring +`flat_match_is_unchanged_shape` test uses); confirm that import is +present and add the missing names to it if not. + +- [ ] **Step 2: Run the new unit test** + +Run: `cargo test -p ailang-core shadowing_let_is_alpha_renamed 2>&1 | tail -8` +Expected: PASS. + +- [ ] **Step 3: Re-confirm the full `ailang-core` suite** + +Run: `cargo test -p ailang-core 2>&1 | tail -8` +Expected: `test result: ok.`