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` (<name>$<n>) 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.
This commit is contained in:
@@ -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>$<n>` 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<String, ScopeEntry>,
|
||||
rename: BTreeMap<String, String>,
|
||||
}
|
||||
|
||||
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: `<base>$<n>` 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 `<base>$<n>` 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<String, String>) -> 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<Arm> = arms
|
||||
.iter()
|
||||
.map(|a| {
|
||||
let mut inner = scope.clone();
|
||||
let mut pat_binds: BTreeSet<String> = BTreeSet::new();
|
||||
pattern_binds(&a.pat, &mut pat_binds);
|
||||
let mut renamed: BTreeMap<String, String> = 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<String> = 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<LoopBinder> = 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 `<name>$<n>`
|
||||
/// (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 `<name>$<n>`, 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.`
|
||||
Reference in New Issue
Block a user