plan: mut.2 — typecheck for Term::Mut / Term::Assign
Seven tasks: three new CheckError variants + code() + ctx() arms (Task 1); synth signature extended with mut_scope_stack threaded through ~19 recursive call sites in lib.rs plus the two re-synth sites in mono.rs:712/1337 (Task 2); Term::Var resolution prepended with innermost-first mut-scope lookup (Task 3); Term::Mut arm (Task 4) and Term::Assign arm (Task 5) replacing the iter mut.1 Internal stubs with real logic; five negative fixtures + driver (Task 6); positive verification of examples/mut.ail typechecking clean (Task 7). Four Boss decisions encoded: fixtures under examples/ with driver at crates/ailang-check/tests/ (convention wins over spec wording); mut_scope_stack as a synth parameter not an Env field (matches the locals/effects/subst threading convention); MutAssignOutOfScope's available list flattens all frames innermost-first; mono.rs:712/1337 the two re-synth sites that need the threading.
This commit is contained in:
@@ -0,0 +1,820 @@
|
||||
# mut.2 — typecheck — Implementation Plan
|
||||
|
||||
> **Parent spec:** `docs/specs/2026-05-15-mut-local.md`
|
||||
>
|
||||
> **For agentic workers:** REQUIRED SUB-SKILL: use `skills/implement`
|
||||
> to run this plan. Steps use `- [ ]` checkboxes for tracking.
|
||||
|
||||
**Goal:** Replace the iter mut.1 dispatch stubs for `Term::Mut` and
|
||||
`Term::Assign` in `synth` with real typecheck logic. Add three new
|
||||
`CheckError` variants (`MutAssignOutOfScope`, `AssignTypeMismatch`,
|
||||
`UnsupportedMutVarType`) and their `code()` + `ctx()` arms. Introduce
|
||||
a `mut_scope_stack: &mut Vec<IndexMap<String, Type>>` parameter on
|
||||
`synth`, thread it through all call sites (recursive inside `lib.rs`
|
||||
plus the two re-synth sites in `mono.rs`), prepend it to the
|
||||
`Term::Var` resolution chain. Ship five fixtures under `examples/`
|
||||
plus one Rust driver under `crates/ailang-check/tests/` to gate the
|
||||
behaviour. Codegen stays untouched — `examples/mut.ail` still does
|
||||
not run, but it now typechecks cleanly.
|
||||
|
||||
**Architecture:** The natural locality for mut-scope state is a
|
||||
`synth`-parameter slot (matching the existing `locals` / `effects` /
|
||||
`subst` / `counter` / `residuals` / `free_fn_calls` / `warnings`
|
||||
threading pattern), NOT an `Env` field. The stack is per-walk
|
||||
(reset on every fn body) and lexically scoped (push on
|
||||
`Term::Mut`-entry, pop on `Term::Mut`-exit); both properties argue
|
||||
against an `Env` field. Each frame is an `IndexMap<String, Type>` so
|
||||
declaration order is preserved (relevant for the `available` list in
|
||||
`MutAssignOutOfScope`). The `Term::Var` resolution order becomes:
|
||||
mut-scope (innermost-first) → existing chain (locals → params →
|
||||
top-level defs → builtins → class-methods). Innermost-wins on
|
||||
shadowing falls out for free.
|
||||
|
||||
**Tech Stack:** `ailang-check` only. No `ailang-core`, `ailang-surface`,
|
||||
`ailang-codegen`, `ailang-prose`, or `ail` changes.
|
||||
|
||||
---
|
||||
|
||||
**Files this plan creates or modifies:**
|
||||
|
||||
- Create: `examples/test_mut_assign_out_of_scope.ail.json` — `assign` to a name not declared as a mut-var of any enclosing `Term::Mut`.
|
||||
- Create: `examples/test_mut_assign_type_mismatch.ail.json` — `(assign x 1.0)` against `(var x (con Int) 0)`.
|
||||
- Create: `examples/test_mut_var_unsupported_type.ail.json` — `(var s (con Str) "...")` — the deferred-type case.
|
||||
- Create: `examples/test_mut_assign_outside_mut.ail.json` — `Term::Assign` directly in a fn body with no `Term::Mut` ancestor.
|
||||
- Create: `examples/test_mut_nested_shadow_legal.ail.json` — positive: outer `var x : Int` shadowed by inner `var x : Float` in nested mut.
|
||||
- Create: `crates/ailang-check/tests/mut_typecheck_pin.rs` — driver test loading each fixture and asserting expected diagnostic code (or empty for the positive case).
|
||||
- Modify: `crates/ailang-check/src/lib.rs:384-746` — add three `CheckError` variants + `code()` arms + `ctx()` arms.
|
||||
- Modify: `crates/ailang-check/src/lib.rs:2647-2662` — `synth` signature: add `mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>`.
|
||||
- Modify: `crates/ailang-check/src/lib.rs:1885, 2634` — top-of-walk synth entry points (`check_fn` and `check_const` — find exact names by looking for synth-callers in lib.rs that do NOT recurse from synth itself).
|
||||
- Modify: `crates/ailang-check/src/lib.rs:2671-2941` — prepend mut-scope resolution to `Term::Var` arm.
|
||||
- Modify: `crates/ailang-check/src/lib.rs:3488-3497` — replace `Term::Mut` and `Term::Assign` `Internal` stubs with real logic.
|
||||
- Modify: `crates/ailang-check/src/lib.rs:~19 internal synth() calls` — thread new param through every recursive site.
|
||||
- Modify: `crates/ailang-check/src/mono.rs:712, 1337` — thread new param through both `crate::synth(...)` call sites.
|
||||
|
||||
---
|
||||
|
||||
## Task 1 — `CheckError` variants + `code()` + `ctx()`
|
||||
|
||||
**Files:**
|
||||
- Modify: `crates/ailang-check/src/lib.rs:384-746`
|
||||
|
||||
- [ ] **Step 1: Write the failing pin test**
|
||||
|
||||
Add to `crates/ailang-check/src/lib.rs` `#[cfg(test)] mod tests` block:
|
||||
|
||||
```rust
|
||||
#[test]
|
||||
fn mut_typecheck_diagnostics_have_kebab_codes() {
|
||||
use indexmap::IndexMap;
|
||||
let e1 = CheckError::MutAssignOutOfScope {
|
||||
name: "foo".into(),
|
||||
available: vec!["bar".into(), "baz".into()],
|
||||
};
|
||||
let e2 = CheckError::AssignTypeMismatch {
|
||||
name: "count".into(),
|
||||
declared: "Int".into(),
|
||||
got: "Float".into(),
|
||||
};
|
||||
let e3 = CheckError::UnsupportedMutVarType {
|
||||
name: "s".into(),
|
||||
ty: "Str".into(),
|
||||
};
|
||||
assert_eq!(e1.code(), "mut-assign-out-of-scope");
|
||||
assert_eq!(e2.code(), "assign-type-mismatch");
|
||||
assert_eq!(e3.code(), "mut-var-unsupported-type");
|
||||
let _ = (e1.ctx(), e2.ctx(), e3.ctx()); // smoke-test ctx() doesn't panic
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Run to verify red**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_typecheck_diagnostics_have_kebab_codes`
|
||||
Expected: FAIL — `CheckError` has no `MutAssignOutOfScope` / `AssignTypeMismatch` / `UnsupportedMutVarType` variants.
|
||||
|
||||
- [ ] **Step 3: Add the three variants**
|
||||
|
||||
In the `CheckError` enum body (around `crates/ailang-check/src/lib.rs:384-639`),
|
||||
immediately before the `Internal` variant at line 638, insert:
|
||||
|
||||
```rust
|
||||
/// Iter mut.2: `Term::Assign { name, .. }` reached typecheck but
|
||||
/// `name` is not a mut-var of any enclosing `Term::Mut` on the
|
||||
/// lexical scope stack.
|
||||
///
|
||||
/// `available` lists every mut-var name visible at the assign
|
||||
/// site, flattened across all enclosing mut-frames (innermost
|
||||
/// first), so the diagnostic can surface "you might have meant
|
||||
/// one of: X / Y / Z".
|
||||
MutAssignOutOfScope {
|
||||
name: String,
|
||||
available: Vec<String>,
|
||||
},
|
||||
|
||||
/// Iter mut.2: `Term::Assign { name, value }` reached typecheck
|
||||
/// inside a valid mut-scope, but `value`'s synth type differs
|
||||
/// from the var's declared type.
|
||||
AssignTypeMismatch {
|
||||
name: String,
|
||||
declared: String,
|
||||
got: String,
|
||||
},
|
||||
|
||||
/// Iter mut.2: `Term::Mut { vars, .. }` declared a `MutVar`
|
||||
/// whose declared `ty` is not one of the four supported scalar
|
||||
/// primitives (Int, Float, Bool, Unit). The temporary
|
||||
/// restriction is named explicitly in spec
|
||||
/// `docs/specs/2026-05-15-mut-local.md` §"Out of scope".
|
||||
UnsupportedMutVarType {
|
||||
name: String,
|
||||
ty: String,
|
||||
},
|
||||
```
|
||||
|
||||
- [ ] **Step 4: Add `code()` arms**
|
||||
|
||||
In the `impl CheckError { pub fn code(&self) -> &'static str { match self { ... } } }`
|
||||
block (around line 648), add three new arms before the `Internal` arm:
|
||||
|
||||
```rust
|
||||
CheckError::MutAssignOutOfScope { .. } => "mut-assign-out-of-scope",
|
||||
CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
|
||||
CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
|
||||
```
|
||||
|
||||
- [ ] **Step 5: Add `ctx()` arms**
|
||||
|
||||
In the `impl CheckError { pub fn ctx(&self) -> serde_json::Value { match self { ... } } }`
|
||||
block (around line 688), add three new arms before the `Internal` arm.
|
||||
Each emits a structured JSON payload consistent with sibling
|
||||
diagnostics:
|
||||
|
||||
```rust
|
||||
CheckError::MutAssignOutOfScope { name, available } => json!({
|
||||
"name": name,
|
||||
"available": available,
|
||||
}),
|
||||
CheckError::AssignTypeMismatch { name, declared, got } => json!({
|
||||
"name": name,
|
||||
"expected": declared,
|
||||
"actual": got,
|
||||
}),
|
||||
CheckError::UnsupportedMutVarType { name, ty } => json!({
|
||||
"name": name,
|
||||
"type": ty,
|
||||
}),
|
||||
```
|
||||
|
||||
- [ ] **Step 6: Add `Display`-style message for each variant**
|
||||
|
||||
The existing `CheckError` derives `thiserror::Error` and the variants
|
||||
carry `#[error("...")]` attributes — verify by reading 1-2 existing
|
||||
variants for the exact attribute shape, then add:
|
||||
|
||||
```rust
|
||||
#[error("[mut-assign-out-of-scope] cannot assign to `{name}` here — not declared as a mut-var in the enclosing (mut ...) block. Available mut-vars in scope: [{}]", available.join(", "))]
|
||||
MutAssignOutOfScope { name: String, available: Vec<String> },
|
||||
|
||||
#[error("[assign-type-mismatch] cannot assign `{got}` to mut-var `{name} : {declared}` — the assigned value's type must match the var's declared type")]
|
||||
AssignTypeMismatch { name: String, declared: String, got: String },
|
||||
|
||||
#[error("[mut-var-unsupported-type] mut-var `{name} : {ty}` is not supported in this milestone — only stack-resident primitive types (Int, Float, Bool, Unit) may be declared as mut-vars. Heap-RC-managed types (Str, ADTs, fn-values) are deferred to a follow-on milestone.")]
|
||||
UnsupportedMutVarType { name: String, ty: String },
|
||||
```
|
||||
|
||||
The bracketed-`[code]:` prefix is consistent with the cli-diag-human
|
||||
iter convention (2026-05-14).
|
||||
|
||||
- [ ] **Step 7: Run to verify green**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_typecheck_diagnostics_have_kebab_codes`
|
||||
Expected: PASS.
|
||||
|
||||
Run: `cargo build --workspace 2>&1 | tail -10`
|
||||
Expected: green (no other consumers of `CheckError` are broken because
|
||||
adding variants is additive and we have not introduced consumers yet).
|
||||
|
||||
---
|
||||
|
||||
## Task 2 — `synth` signature: thread `mut_scope_stack`
|
||||
|
||||
**Files:**
|
||||
- Modify: `crates/ailang-check/src/lib.rs:2647-2662` — signature.
|
||||
- Modify: `crates/ailang-check/src/lib.rs` — ~19 internal recursive call sites.
|
||||
- Modify: `crates/ailang-check/src/lib.rs:1885, 2634` — entry-point callers.
|
||||
- Modify: `crates/ailang-check/src/mono.rs:712, 1337` — re-synth call sites.
|
||||
|
||||
The new parameter is `mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>`.
|
||||
Position: immediately after `locals` (canonical mid-position; matches
|
||||
the existing convention of locals-adjacent scope state).
|
||||
|
||||
- [ ] **Step 1: Extend `synth` signature**
|
||||
|
||||
In `crates/ailang-check/src/lib.rs:2647`, change:
|
||||
|
||||
```rust
|
||||
pub(crate) fn synth(
|
||||
term: &Term,
|
||||
locals: &IndexMap<String, Type>,
|
||||
// ... existing params ...
|
||||
) -> Result<(Type, ...), CheckError> {
|
||||
```
|
||||
|
||||
to:
|
||||
|
||||
```rust
|
||||
pub(crate) fn synth(
|
||||
term: &Term,
|
||||
locals: &IndexMap<String, Type>,
|
||||
mut_scope_stack: &mut Vec<indexmap::IndexMap<String, Type>>,
|
||||
// ... existing params ...
|
||||
) -> Result<(Type, ...), CheckError> {
|
||||
```
|
||||
|
||||
(The exact return shape and the other params are whatever the
|
||||
function already has — preserve them verbatim and only add the new
|
||||
slot.)
|
||||
|
||||
- [ ] **Step 2: Run to verify the parameter is exposed**
|
||||
|
||||
Run: `cargo build --workspace -p ailang-check 2>&1 | head -10`
|
||||
Expected: many `error[E0061]: this function takes N arguments but ...`
|
||||
errors at every `synth(...)` call site. This is the structural red
|
||||
signal.
|
||||
|
||||
- [ ] **Step 3: Update entry-point callers in `lib.rs`**
|
||||
|
||||
Locate the two top-of-walk entry points around lines 1885 and 2634
|
||||
(grep for `synth(` calls that are NOT inside `pub(crate) fn synth`
|
||||
itself). Each entry-point caller passes a fresh empty stack:
|
||||
|
||||
```rust
|
||||
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, Type>> = Vec::new();
|
||||
let result = synth(term, &locals, &mut mut_scope_stack, /* existing args */)?;
|
||||
```
|
||||
|
||||
The stack is dropped at the end of the entry point; it is per-fn-body.
|
||||
|
||||
- [ ] **Step 4: Update all recursive `synth(...)` call sites in `lib.rs`**
|
||||
|
||||
Per the recon, the recursive call sites are at lines 3016, 3052,
|
||||
3061, 3063, 3075, 3077, 3078, 3096, 3191, 3200, 3218, 3293, 3295,
|
||||
3304, 3392, 3419, 3435, 3477 (and possibly some lift / mono call
|
||||
sites; the build errors enumerate them). Each becomes:
|
||||
|
||||
```rust
|
||||
synth(<term>, locals, mut_scope_stack, /* existing args */)
|
||||
```
|
||||
|
||||
The implementer should grep for `synth(` in `lib.rs` after Step 3 and
|
||||
update every remaining call site.
|
||||
|
||||
- [ ] **Step 5: Update `mono.rs` re-synth call sites**
|
||||
|
||||
Two sites: `crates/ailang-check/src/mono.rs:712` and `:1337`. Both
|
||||
invoke `crate::synth(...)`. Both need:
|
||||
|
||||
```rust
|
||||
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, Type>> = Vec::new();
|
||||
crate::synth(<term>, locals, &mut mut_scope_stack, /* existing args */)
|
||||
```
|
||||
|
||||
(Each call site gets its own fresh stack — these are re-synth sites
|
||||
that begin from a top-of-body position, so an empty stack is correct.)
|
||||
|
||||
- [ ] **Step 6: Verify build green**
|
||||
|
||||
Run: `cargo build --workspace 2>&1 | tail -10`
|
||||
Expected: green.
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
|
||||
Expected: all existing tests still pass (the new parameter is
|
||||
unconsumed at the existing call sites; behaviour is identical).
|
||||
|
||||
---
|
||||
|
||||
## Task 3 — `Term::Var` resolution: prepend mut-scope
|
||||
|
||||
**Files:**
|
||||
- Modify: `crates/ailang-check/src/lib.rs:2671-2941` — `Term::Var` arm in `synth`.
|
||||
|
||||
- [ ] **Step 1: Locate the `Term::Var` resolution arm**
|
||||
|
||||
In `synth`, find the `Term::Var { name } => { ... }` arm. The
|
||||
existing resolution chain consults `locals` first, then params, then
|
||||
the top-level def map, then builtins, then class-method dispatch.
|
||||
|
||||
- [ ] **Step 2: Prepend mut-scope lookup**
|
||||
|
||||
Immediately before the existing `locals.get(name)` lookup, insert:
|
||||
|
||||
```rust
|
||||
// Iter mut.2: mut-vars take precedence over let-bound / param /
|
||||
// top-level / builtin / class-method resolutions. Innermost-first.
|
||||
for frame in mut_scope_stack.iter().rev() {
|
||||
if let Some(ty) = frame.get(name) {
|
||||
// Mut-vars are monomorphic by spec §"var element types" —
|
||||
// no Forall instantiation, no free_fn_owner recording.
|
||||
return Ok((ty.clone(), /* whatever return-tuple shape is */));
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
The exact return-tuple shape must match the existing `Term::Var`
|
||||
arm's return shape (the function returns more than just `Type`; see
|
||||
the locals-hit branch for the canonical form, then mirror it).
|
||||
|
||||
- [ ] **Step 3: Pin test — mut-var shadows outer let**
|
||||
|
||||
Add to `#[cfg(test)] mod tests`:
|
||||
|
||||
```rust
|
||||
#[test]
|
||||
fn mut_var_resolution_shadows_outer_let() {
|
||||
// (let x 1 (mut (var x (con Float) 2.0) x))
|
||||
// -> the inner x is Float, the outer x is Int;
|
||||
// the body's x resolves to the mut-var (Float).
|
||||
let term = Term::Let {
|
||||
name: "x".into(),
|
||||
value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
|
||||
body: Box::new(Term::Mut {
|
||||
vars: vec![ailang_core::ast::MutVar {
|
||||
name: "x".into(),
|
||||
ty: Type::float(),
|
||||
init: Term::Lit { lit: Literal::Float { bits: "4000000000000000".into() } },
|
||||
}],
|
||||
body: Box::new(Term::Var { name: "x".into() }),
|
||||
}),
|
||||
};
|
||||
let (ty, _) = synth_in_builtins_env(&term);
|
||||
assert_eq!(ty, Type::float(), "inner mut-var x : Float must shadow outer let x : Int");
|
||||
}
|
||||
```
|
||||
|
||||
(`synth_in_builtins_env` is the existing test helper; use whichever
|
||||
helper the existing builtins-related tests in lib.rs use to drive
|
||||
`synth`.)
|
||||
|
||||
- [ ] **Step 4: Run to verify pass**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_var_resolution_shadows_outer_let`
|
||||
Expected: PASS.
|
||||
|
||||
---
|
||||
|
||||
## Task 4 — `Term::Mut` typecheck arm
|
||||
|
||||
**Files:**
|
||||
- Modify: `crates/ailang-check/src/lib.rs:3488-3492` — replace `Term::Mut` `Internal` stub.
|
||||
|
||||
- [ ] **Step 1: Write the failing positive pin**
|
||||
|
||||
Add to `#[cfg(test)] mod tests`:
|
||||
|
||||
```rust
|
||||
#[test]
|
||||
fn mut_block_typechecks_with_int_var_and_returns_int() {
|
||||
// (mut (var x (con Int) 0) (assign x (app + x 1)) x)
|
||||
// -> Int.
|
||||
let term = Term::Mut {
|
||||
vars: vec![ailang_core::ast::MutVar {
|
||||
name: "x".into(),
|
||||
ty: Type::int(),
|
||||
init: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
}],
|
||||
body: Box::new(Term::Seq {
|
||||
lhs: Box::new(Term::Assign {
|
||||
name: "x".into(),
|
||||
value: Box::new(Term::App {
|
||||
func: Box::new(Term::Var { name: "+".into() }),
|
||||
args: vec![
|
||||
Term::Var { name: "x".into() },
|
||||
Term::Lit { lit: Literal::Int { value: 1 } },
|
||||
],
|
||||
// ... whatever tail-call flag default the existing tests use
|
||||
}),
|
||||
}),
|
||||
rhs: Box::new(Term::Var { name: "x".into() }),
|
||||
}),
|
||||
};
|
||||
let (ty, _) = synth_in_builtins_env(&term);
|
||||
assert_eq!(ty, Type::int(), "mut block returning a mut-var of type Int must synth as Int");
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Run to verify red**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_block_typechecks_with_int_var_and_returns_int`
|
||||
Expected: FAIL with `CheckError::Internal` from the mut.1 stub.
|
||||
|
||||
- [ ] **Step 3: Replace the `Term::Mut` stub with real logic**
|
||||
|
||||
At `crates/ailang-check/src/lib.rs:3488-3492` (the `Term::Mut` arm
|
||||
in `synth`), replace:
|
||||
|
||||
```rust
|
||||
Term::Mut { .. } => {
|
||||
Err(CheckError::Internal(
|
||||
"Term::Mut not yet supported in typecheck (deferred to iter mut.2)".into(),
|
||||
))
|
||||
}
|
||||
```
|
||||
|
||||
with:
|
||||
|
||||
```rust
|
||||
Term::Mut { vars, body } => {
|
||||
// Gate var types: only Int / Float / Bool / Unit allowed in
|
||||
// mut.2 per spec §"Out of scope".
|
||||
fn is_supported_mut_var_type(ty: &Type) -> bool {
|
||||
matches!(ty, Type::Con { name, args }
|
||||
if args.is_empty()
|
||||
&& matches!(name.as_str(), "Int" | "Float" | "Bool" | "Unit"))
|
||||
}
|
||||
|
||||
// Build a fresh frame.
|
||||
let mut frame: indexmap::IndexMap<String, Type> = indexmap::IndexMap::new();
|
||||
for v in vars {
|
||||
if !is_supported_mut_var_type(&v.ty) {
|
||||
return Err(CheckError::UnsupportedMutVarType {
|
||||
name: v.name.clone(),
|
||||
ty: render_type(&v.ty), // existing helper; or use std::fmt path
|
||||
});
|
||||
}
|
||||
// Synth init in the outer scope (current mut_scope_stack contents
|
||||
// are already on the stack; this frame is not yet pushed, so the
|
||||
// var's own name does not shadow itself during init).
|
||||
let (init_ty, /* ...other return components... */) = synth(
|
||||
&v.init,
|
||||
locals,
|
||||
mut_scope_stack,
|
||||
/* existing args */
|
||||
)?;
|
||||
// Unify init type with declared type.
|
||||
unify(&init_ty, &v.ty, /* existing unify args */)?;
|
||||
// Bind name → declared type in the current frame.
|
||||
frame.insert(v.name.clone(), v.ty.clone());
|
||||
}
|
||||
|
||||
// Push the completed frame.
|
||||
mut_scope_stack.push(frame);
|
||||
|
||||
// Synth body in the extended scope.
|
||||
let body_result = synth(body, locals, mut_scope_stack, /* existing args */);
|
||||
|
||||
// Pop the frame regardless of body outcome.
|
||||
mut_scope_stack.pop();
|
||||
|
||||
// Return the body's type (or propagate the error).
|
||||
body_result
|
||||
}
|
||||
```
|
||||
|
||||
The exact return-tuple shape and the names of helpers (`unify`,
|
||||
`render_type` for the type→String renderer) must match the existing
|
||||
code conventions; the implementer reads the canonical form from
|
||||
adjacent arms (e.g. the `Term::Let` arm for the unify pattern and
|
||||
the type-renderer call shape).
|
||||
|
||||
The function `is_supported_mut_var_type` lives as a small helper at
|
||||
file scope (top of `lib.rs` near the other `is_*` helpers) or inline.
|
||||
Either is acceptable; pick whichever matches the existing convention.
|
||||
|
||||
- [ ] **Step 4: Run to verify pass**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_block_typechecks_with_int_var_and_returns_int`
|
||||
Expected: PASS.
|
||||
|
||||
---
|
||||
|
||||
## Task 5 — `Term::Assign` typecheck arm
|
||||
|
||||
**Files:**
|
||||
- Modify: `crates/ailang-check/src/lib.rs:3493-3497` — replace `Term::Assign` `Internal` stub.
|
||||
|
||||
- [ ] **Step 1: Write the failing positive pin**
|
||||
|
||||
Add to `#[cfg(test)] mod tests`:
|
||||
|
||||
```rust
|
||||
#[test]
|
||||
fn assign_to_in_scope_mut_var_synths_unit() {
|
||||
// Inside a mut frame with (var x Int 0), (assign x 1) :: Unit.
|
||||
let term = Term::Mut {
|
||||
vars: vec![ailang_core::ast::MutVar {
|
||||
name: "x".into(),
|
||||
ty: Type::int(),
|
||||
init: Term::Lit { lit: Literal::Int { value: 0 } },
|
||||
}],
|
||||
body: Box::new(Term::Assign {
|
||||
name: "x".into(),
|
||||
value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
|
||||
}),
|
||||
};
|
||||
let (ty, _) = synth_in_builtins_env(&term);
|
||||
assert_eq!(ty, Type::unit(), "mut block whose body is a lone assign must synth as Unit");
|
||||
}
|
||||
```
|
||||
|
||||
- [ ] **Step 2: Run to verify red**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check assign_to_in_scope_mut_var_synths_unit`
|
||||
Expected: FAIL with the `Term::Assign` `Internal` stub.
|
||||
|
||||
- [ ] **Step 3: Replace the `Term::Assign` stub with real logic**
|
||||
|
||||
At `crates/ailang-check/src/lib.rs:3493-3497`, replace:
|
||||
|
||||
```rust
|
||||
Term::Assign { .. } => {
|
||||
Err(CheckError::Internal(
|
||||
"Term::Assign not yet supported in typecheck (deferred to iter mut.2)".into(),
|
||||
))
|
||||
}
|
||||
```
|
||||
|
||||
with:
|
||||
|
||||
```rust
|
||||
Term::Assign { name, value } => {
|
||||
// Walk mut_scope_stack innermost-first looking for `name`.
|
||||
let declared: Option<Type> = mut_scope_stack
|
||||
.iter()
|
||||
.rev()
|
||||
.find_map(|frame| frame.get(name).cloned());
|
||||
|
||||
match declared {
|
||||
None => {
|
||||
// Flatten every mut-var name in every frame, innermost-
|
||||
// first, dedup-preserving-order.
|
||||
let mut available: Vec<String> = Vec::new();
|
||||
for frame in mut_scope_stack.iter().rev() {
|
||||
for k in frame.keys() {
|
||||
if !available.contains(k) {
|
||||
available.push(k.clone());
|
||||
}
|
||||
}
|
||||
}
|
||||
Err(CheckError::MutAssignOutOfScope {
|
||||
name: name.clone(),
|
||||
available,
|
||||
})
|
||||
}
|
||||
Some(declared_ty) => {
|
||||
// Synth the value.
|
||||
let (value_ty, /* ... */) = synth(
|
||||
value,
|
||||
locals,
|
||||
mut_scope_stack,
|
||||
/* existing args */
|
||||
)?;
|
||||
// Compare to declared.
|
||||
if /* unifies, see existing convention */ != declared {
|
||||
return Err(CheckError::AssignTypeMismatch {
|
||||
name: name.clone(),
|
||||
declared: render_type(&declared_ty),
|
||||
got: render_type(&value_ty),
|
||||
});
|
||||
}
|
||||
// Produce Unit.
|
||||
Ok((Type::unit(), /* whatever return-tuple shape */))
|
||||
}
|
||||
}
|
||||
}
|
||||
```
|
||||
|
||||
The unification step uses the same machinery as `Term::Let`'s init
|
||||
check — read the adjacent arm to copy the canonical shape (likely
|
||||
`unify(&value_ty, &declared_ty, &mut subst)?` or similar; the
|
||||
implementer matches the existing convention).
|
||||
|
||||
- [ ] **Step 4: Run to verify pass**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check assign_to_in_scope_mut_var_synths_unit`
|
||||
Expected: PASS.
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
|
||||
Expected: all check-side tests pass; build is green.
|
||||
|
||||
---
|
||||
|
||||
## Task 6 — Five fixtures + driver test
|
||||
|
||||
**Files:**
|
||||
- Create: `examples/test_mut_assign_out_of_scope.ail.json`
|
||||
- Create: `examples/test_mut_assign_type_mismatch.ail.json`
|
||||
- Create: `examples/test_mut_var_unsupported_type.ail.json`
|
||||
- Create: `examples/test_mut_assign_outside_mut.ail.json`
|
||||
- Create: `examples/test_mut_nested_shadow_legal.ail.json`
|
||||
- Create: `crates/ailang-check/tests/mut_typecheck_pin.rs`
|
||||
|
||||
These fixtures are `.ail.json` (canonical-form-rejection style)
|
||||
because they exercise typecheck failures specifically; the form-A
|
||||
parser would not necessarily reject them, but typecheck must. The
|
||||
seven-file form-A carve-out list (per pd.3, journal 2026-05-14)
|
||||
explicitly admits negative typecheck fixtures as `.ail.json`-only.
|
||||
Note the existing convention precedent: `examples/broken_unbound.ail.json`
|
||||
and `examples/test_22b2_*.ail.json`.
|
||||
|
||||
- [ ] **Step 1: Create `test_mut_assign_out_of_scope.ail.json`**
|
||||
|
||||
```json
|
||||
{
|
||||
"name": "test_mut_assign_out_of_scope",
|
||||
"imports": [],
|
||||
"defs": [
|
||||
{
|
||||
"kind": "fn",
|
||||
"name": "main",
|
||||
"ty": { "k": "fn", "params": [], "ret": { "k": "con", "name": "Unit" }, "effects": ["IO"] },
|
||||
"params": [],
|
||||
"body": {
|
||||
"t": "mut",
|
||||
"vars": [
|
||||
{ "name": "x", "type": { "k": "con", "name": "Int" }, "init": { "t": "lit", "lit": { "kind": "int", "value": 0 } } }
|
||||
],
|
||||
"body": {
|
||||
"t": "assign",
|
||||
"name": "y",
|
||||
"value": { "t": "lit", "lit": { "kind": "int", "value": 1 } }
|
||||
}
|
||||
}
|
||||
}
|
||||
]
|
||||
}
|
||||
```
|
||||
|
||||
The exact module-level shape (root keys, FnDef field names) must
|
||||
match the canonical schema; the implementer cross-checks against
|
||||
`examples/broken_unbound.ail.json` as the closest precedent.
|
||||
|
||||
- [ ] **Step 2: Create the four remaining fixtures**
|
||||
|
||||
Each follows the same shape, varying:
|
||||
- `test_mut_assign_type_mismatch.ail.json` — `var x : Int = 0`; `assign x 1.5` (Float).
|
||||
- `test_mut_var_unsupported_type.ail.json` — `var s : Str = "hello"`.
|
||||
- `test_mut_assign_outside_mut.ail.json` — fn body is `Term::Assign { name: "x", value: ... }` directly (no enclosing `Term::Mut`).
|
||||
- `test_mut_nested_shadow_legal.ail.json` — outer mut has `var x : Int = 1`; inner mut has `var x : Float = 2.0` plus body that returns `x` (Float). The outer body returns whatever the inner mut returns.
|
||||
|
||||
The positive fixture's main fn returns Float and must typecheck
|
||||
clean.
|
||||
|
||||
- [ ] **Step 3: Create the driver test**
|
||||
|
||||
`crates/ailang-check/tests/mut_typecheck_pin.rs`:
|
||||
|
||||
```rust
|
||||
//! Iter mut.2: pin tests that the five typecheck fixtures produce
|
||||
//! the expected diagnostic codes (or zero diagnostics for the
|
||||
//! positive nested-shadow case).
|
||||
//!
|
||||
//! Spec: docs/specs/2026-05-15-mut-local.md §"Testing strategy /
|
||||
//! Typecheck negative tests".
|
||||
|
||||
use std::path::PathBuf;
|
||||
|
||||
fn examples_dir() -> PathBuf {
|
||||
PathBuf::from(env!("CARGO_MANIFEST_DIR"))
|
||||
.parent().unwrap()
|
||||
.parent().unwrap()
|
||||
.join("examples")
|
||||
}
|
||||
|
||||
fn check_fixture(fixture_name: &str) -> Vec<String> {
|
||||
// Whatever the existing canonical helper is for the
|
||||
// load-then-check-then-collect-codes pattern. Inspect
|
||||
// crates/ailang-check/tests/show_dispatch_pin.rs (or whichever
|
||||
// pin test is closest) for the convention.
|
||||
todo!("convention from sibling pin tests");
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn assign_out_of_scope_emits_mut_assign_out_of_scope() {
|
||||
let codes = check_fixture("test_mut_assign_out_of_scope.ail.json");
|
||||
assert_eq!(codes, vec!["mut-assign-out-of-scope".to_string()]);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn assign_type_mismatch_emits_assign_type_mismatch() {
|
||||
let codes = check_fixture("test_mut_assign_type_mismatch.ail.json");
|
||||
assert_eq!(codes, vec!["assign-type-mismatch".to_string()]);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn mut_var_str_type_emits_mut_var_unsupported_type() {
|
||||
let codes = check_fixture("test_mut_var_unsupported_type.ail.json");
|
||||
assert_eq!(codes, vec!["mut-var-unsupported-type".to_string()]);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn assign_outside_mut_emits_mut_assign_out_of_scope() {
|
||||
let codes = check_fixture("test_mut_assign_outside_mut.ail.json");
|
||||
assert_eq!(codes, vec!["mut-assign-out-of-scope".to_string()]);
|
||||
}
|
||||
|
||||
#[test]
|
||||
fn nested_shadow_typechecks_clean() {
|
||||
let codes = check_fixture("test_mut_nested_shadow_legal.ail.json");
|
||||
assert!(codes.is_empty(), "expected zero diagnostics, got {:?}", codes);
|
||||
}
|
||||
```
|
||||
|
||||
The `check_fixture` helper body must match the existing
|
||||
sibling-pin-test convention. The implementer reads
|
||||
`crates/ailang-check/tests/show_dispatch_pin.rs` (or whichever is
|
||||
closest) and copies the canonical shape. **Do NOT leave a `todo!()`
|
||||
in the final file** — that is a placeholder forbidden by the plan
|
||||
discipline. Resolve to the canonical helper before declaring done.
|
||||
|
||||
- [ ] **Step 4: Run the driver**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check mut_typecheck_pin`
|
||||
Expected: all five tests PASS.
|
||||
|
||||
- [ ] **Step 5: Run full check-crate tests**
|
||||
|
||||
Run: `cargo test --workspace -p ailang-check 2>&1 | tail -5`
|
||||
Expected: every test green, including all the new ones + the
|
||||
existing baseline.
|
||||
|
||||
---
|
||||
|
||||
## Task 7 — Verify `examples/mut.ail` typechecks clean
|
||||
|
||||
**Files:**
|
||||
- (no edits; verification only)
|
||||
|
||||
- [ ] **Step 1: Hand-check via `cargo run ail check`**
|
||||
|
||||
Run: `cargo run --quiet --bin ail -- check examples/mut.ail 2>&1`
|
||||
Expected: zero diagnostics (all six fns in the fixture typecheck
|
||||
clean — they were authored to do so).
|
||||
|
||||
If any of the six fns emit a diagnostic, that is a real bug in
|
||||
either the spec semantics or the implementation. Stop, diagnose,
|
||||
and either fix the typecheck logic or amend the fixture (the latter
|
||||
needs Boss sign-off because the fixture is the spec's load-bearing
|
||||
positive sample).
|
||||
|
||||
- [ ] **Step 2: Verify the workspace tests pass**
|
||||
|
||||
Run: `cargo test --workspace 2>&1 | tail -5`
|
||||
Expected: every test green.
|
||||
|
||||
---
|
||||
|
||||
## Self-review checklist
|
||||
|
||||
- [ ] **Spec coverage:** every section of spec §"Iteration mut.2 —
|
||||
Typecheck" has a matching task. Cross-check: typecheck arm for
|
||||
`Term::Mut` (Task 4), typecheck arm for `Term::Assign` (Task 5),
|
||||
`Term::Var` resolution prepending (Task 3), three diagnostics
|
||||
(Task 1), five fixtures (Task 6). All covered.
|
||||
|
||||
- [ ] **Placeholder scan:** grep for "TBD" / "TODO" / "implement
|
||||
later" / "similar to Task" / "appropriate error handling" / "fill
|
||||
in later". The Task 6 Step 3 driver contains a `todo!()` in the
|
||||
*plan text* (intentional, as the helper convention is read off
|
||||
sibling tests at execution time) — but a literal `todo!()` MUST
|
||||
NOT survive into the committed file. The Step 3 instruction names
|
||||
this explicitly.
|
||||
|
||||
- [ ] **Type-name consistency:** `CheckError::MutAssignOutOfScope`,
|
||||
`CheckError::AssignTypeMismatch`, `CheckError::UnsupportedMutVarType`,
|
||||
`mut_scope_stack`, `IndexMap<String, Type>`, `Type::int()`,
|
||||
`Type::float()`, `Type::unit()`, the kebab codes (`mut-assign-out-of-scope`,
|
||||
`assign-type-mismatch`, `mut-var-unsupported-type`). Each appears
|
||||
identically across tasks.
|
||||
|
||||
- [ ] **Step granularity:** each step is 2-5 minutes (a single match
|
||||
arm; a single signature change; a single fixture).
|
||||
|
||||
- [ ] **No commit steps:** verified — the plan contains no `git commit`
|
||||
instructions.
|
||||
|
||||
- [ ] **Boss decisions named:** the four recon open questions are
|
||||
resolved in this plan: (1) fixtures go to `examples/` with the
|
||||
driver under `crates/ailang-check/tests/` (Task 6 lead paragraph);
|
||||
(2) `mut_scope_stack` is a `synth` parameter, not an `Env` field
|
||||
(Task 2 Step 1); (3) `MutAssignOutOfScope.available` is flattened
|
||||
across all enclosing frames innermost-first (Task 5 Step 3); (4)
|
||||
`mono.rs` re-synth sites verified at lines 712 + 1337 (Task 2
|
||||
Step 5).
|
||||
|
||||
---
|
||||
|
||||
## Acceptance gate for iteration mut.2
|
||||
|
||||
- `cargo build --workspace` green.
|
||||
- `cargo test --workspace` green.
|
||||
- All five new tests under `crates/ailang-check/tests/mut_typecheck_pin.rs`
|
||||
green.
|
||||
- The three `CheckError` variants have `code()` arms returning the
|
||||
three kebab codes.
|
||||
- `examples/mut.ail` (the six-fn round-trip fixture from mut.1)
|
||||
typechecks clean via `cargo run --bin ail -- check examples/mut.ail`.
|
||||
- `Term::Mut` and `Term::Assign` reaching codegen still produce
|
||||
`CodegenError::Internal` (codegen recognition is deferred to mut.3
|
||||
and is NOT in scope for this iteration).
|
||||
|
||||
The iteration does NOT include any `examples/mut_counter.ail` or
|
||||
`examples/mut_sum_floats.ail` end-to-end run; those land with mut.3.
|
||||
Reference in New Issue
Block a user