Brummel/AILang
1
0
Fork 0
Code Issues 29 Pull Requests Actions Packages Projects Releases Wiki Activity

iter mut.2: typecheck for Term::Mut + Term::Assign

Browse Source 
Replaces the iter mut.1 dispatch stubs in synth with real typecheck
logic. Codegen stubs stay (deferred to mut.3); examples/mut.ail now
typechecks clean but still cannot run end-to-end.

Concretely:

- crates/ailang-check/src/lib.rs: three new CheckError variants
  (MutAssignOutOfScope, AssignTypeMismatch, UnsupportedMutVarType)
  with #[error('[code]: msg')] Display attrs matching the cli-diag-
  human bracketed-code convention; code() + ctx() arms emit
  kebab-case codes and structured JSON payloads.

- synth signature: new parameter mut_scope_stack: &mut Vec<IndexMap<
  String, Type>> after locals, threaded through every recursive call
  site (synth's 18 internal calls + mono.rs:712/1337 re-synth +
  lift.rs:723 + builtins.rs test helpers + the mq.3 in-test helper
  at lib.rs:6663). Stack is per-walk and lexically scoped — push on
  Term::Mut entry, pop on exit. Each frame is an IndexMap so
  declaration order is preserved for the diagnostic 'available' list.

- Term::Var resolution: prepended with innermost-first mut-scope
  lookup. Mut-vars are monomorphic — no Forall instantiation, no
  free_fn_owner recording. Innermost-wins shadowing falls out of
  the iteration order.

- Term::Mut arm: gate var types to Int/Float/Bool/Unit only via
  a small is_supported_mut_var_type helper; each var's init is
  synth'd in the in-progress scope (the var itself is not yet
  bound, so it does not self-shadow during init); push completed
  frame, synth body, pop. Block's type is body's type.

- Term::Assign arm: walk mut_scope_stack innermost-first looking for
  name. On miss: MutAssignOutOfScope with available flattened
  across all frames (innermost-first, deduplicated, preserving
  order). On hit: synth value, unify against declared type — on
  mismatch emit AssignTypeMismatch with rendered types; on success
  produce Type::unit().

- Five .ail.json fixtures under examples/ exercising each
  diagnostic plus a positive nested-shadow sanity case, driven by
  the new pin test crates/ailang-check/tests/mut_typecheck_pin.rs
  (load_workspace + check_workspace + assert exact codes).

- carve_out_inventory.rs EXPECTED extended 7 → 12 to cover the new
  negative-fixture set (consistent with the form-a-default-authoring
  spec §C4(b) precedent for type-rejection fixtures staying as
  .ail.json-only).

Plan deviations from recon: three additional synth() call sites
beyond the four enumerated (lift.rs:723, builtins.rs x2,
lib.rs:6663) surfaced via the build-red structural signal; each
threaded with a fresh empty stack. carve_out_inventory.rs extension
was required by the existing pin but not named in the recon — a
documentary concern for the next planner pass.

Tests: 579 → 592 green; examples/mut.ail typechecks clean
('ok (26 symbols across 2 modules)') via cargo run --bin ail --
check examples/mut.ail; cargo build green; full workspace test
green.

Journal: docs/journals/2026-05-15-iter-mut.2.md.

Refs: docs/specs/2026-05-15-mut-local.md, docs/plans/2026-05-15-iter-mut.2.md.
This commit is contained in:
Brummel
2026-05-15 01:37:25 +02:00
parent 3a5b1d3347
commit b24718a5ff
14 changed files with 1059 additions and 43 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/builtins.rs
+4
View File
@@ -342,6 +342,7 @@ mod tests {
let mut env = Env::default();
install(&mut env);
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
@@ -352,6 +353,7 @@ mod tests {
t,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"<test>",
&mut subst,
@@ -583,6 +585,7 @@ mod tests {
let mut env = Env::default();
install(&mut env);
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
@@ -593,6 +596,7 @@ mod tests {
&term,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"<test>",
&mut subst,
crates/ailang-check/src/lib.rs
+512 -38
View File
@@ -631,6 +631,43 @@ pub enum CheckError {
name: String,
},
/// 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, deduplicated, preserving order — so the diagnostic
/// surfaces "you might have meant one of: X / Y / Z" without
/// duplicates when the same name appears at multiple nesting
/// depths.
#[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>,
},
/// 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.
#[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,
},
/// 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".
#[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,
},
/// Iter 22b.3: an internal invariant in the typechecker / mono pass
/// was violated — surfaced as an error so callers can propagate
/// rather than abort, but in well-formed inputs (typecheck has
@@ -679,6 +716,9 @@ impl CheckError {
CheckError::NoInstance { .. } => "no-instance",
CheckError::AmbiguousMethodResolution { .. } => "ambiguous-method-resolution",
CheckError::UnknownClass { .. } => "unknown-class",
CheckError::MutAssignOutOfScope { .. } => "mut-assign-out-of-scope",
CheckError::AssignTypeMismatch { .. } => "assign-type-mismatch",
CheckError::UnsupportedMutVarType { .. } => "mut-var-unsupported-type",
CheckError::Internal(_) => "internal",
}
}
@@ -741,6 +781,15 @@ impl CheckError {
CheckError::UnknownClass { name } => {
serde_json::json!({ "name": name })
}
CheckError::MutAssignOutOfScope { name, available } => {
serde_json::json!({"name": name, "available": available})
}
CheckError::AssignTypeMismatch { name, declared, got } => {
serde_json::json!({"name": name, "expected": declared, "actual": got})
}
CheckError::UnsupportedMutVarType { name, ty } => {
serde_json::json!({"name": name, "type": ty})
}
_ => serde_json::Value::Object(serde_json::Map::new()),
}
}
@@ -1882,7 +1931,11 @@ fn check_fn(f: &FnDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> Result<
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
// Iter mut.2: fresh per-fn-body mut-scope stack. Empty at fn entry;
// pushed/popped by `Term::Mut` arms during the walk; discarded after
// the body type-checks.
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let body_ty = synth(&f.body, &env, &mut locals, &mut mut_scope_stack, &mut effects, &f.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
unify(&ret_ty, &body_ty, &mut subst)?;
// mq.3: surface synth-time warnings into the caller-supplied
// accumulator. The warnings already carry `def: Some(f.name)`
@@ -2631,7 +2684,11 @@ fn check_const(c: &ConstDef, env: &Env, out_warnings: &mut Vec<Diagnostic>) -> R
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let v = synth(&c.value, env, &mut locals, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
// Iter mut.2: fresh per-const-body mut-scope stack (always empty
// at this entry point — `Term::Mut` may appear inside a const body
// and push frames as the walk descends).
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let v = synth(&c.value, env, &mut locals, &mut mut_scope_stack, &mut effects, &c.name, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings)?;
out_warnings.extend(warnings);
unify(&c.ty, &v, &mut subst)?;
if !effects.is_empty() {
@@ -2648,6 +2705,14 @@ pub(crate) fn synth(
t: &Term,
env: &Env,
locals: &mut IndexMap<String, Type>,
// Iter mut.2: per-walk lexical mut-scope. Each frame is one
// `Term::Mut` block's `vars` (preserving declaration order via
// `IndexMap`). The stack is pushed on `Term::Mut` entry and
// popped on exit; `Term::Var` consults it innermost-first before
// the locals/globals chain; `Term::Assign` resolves its target
// name through it. Position: locals-adjacent because both are
// per-fn-body lexical scope state.
mut_scope_stack: &mut Vec<IndexMap<String, Type>>,
effects: &mut BTreeSet<String>,
in_def: &str,
subst: &mut Subst,
@@ -2669,6 +2734,18 @@ pub(crate) fn synth(
Literal::Float { .. } => Type::float(),
}),
Term::Var { name } => {
// Iter mut.2: mut-vars take precedence over every other
// resolution path (let-bound, param, top-level, builtin,
// class-method). Walk the stack innermost-first; the first
// frame containing `name` wins (lexical shadowing). Mut-vars
// are monomorphic per spec §"var element types" — no Forall
// instantiation, no `FreeFnCall` recording.
for frame in mut_scope_stack.iter().rev() {
if let Some(ty) = frame.get(name) {
return Ok(ty.clone());
}
}
// Lookup precedence: locals → local globals → class-method
// table → qualified cross-module ref. A `Forall` resolved at
// any of these levels is instantiated with fresh metavars at
@@ -3013,7 +3090,7 @@ pub(crate) fn synth(
Ok(maybe_instantiate(raw, counter))
}
Term::App { callee, args, .. } => {
let cty = synth(callee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let cty = synth(callee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let cty = subst.apply(&cty);
let (params, ret, fx) = match &cty {
Type::Fn { params, ret, effects: fx, .. } => {
@@ -3049,7 +3126,7 @@ pub(crate) fn synth(
});
}
for (a, exp) in args.iter().zip(params.iter()) {
let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(exp, &actual, subst)?;
}
for e in fx {
@@ -3058,9 +3135,9 @@ pub(crate) fn synth(
Ok(subst.apply(&ret))
}
Term::Let { name, value, body } => {
let v = synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let v = synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let prev = locals.insert(name.clone(), v);
let r = synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let r = synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
match prev {
Some(p) => {
locals.insert(name.clone(), p);
@@ -3072,10 +3149,10 @@ pub(crate) fn synth(
Ok(r)
}
Term::If { cond, then, else_ } => {
let c = synth(cond, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let c = synth(cond, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&Type::bool_(), &c, subst)?;
let t1 = synth(then, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let t2 = synth(else_, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let t1 = synth(then, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let t2 = synth(else_, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&t1, &t2, subst)?;
Ok(subst.apply(&t1))
}
@@ -3093,7 +3170,7 @@ pub(crate) fn synth(
});
}
for (a, exp) in args.iter().zip(sig.params.iter()) {
let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(exp, &actual, subst)?;
}
effects.insert(sig.effect.clone());
@@ -3188,7 +3265,7 @@ pub(crate) fn synth(
}
for (a, exp) in args.iter().zip(qualified_fields.iter()) {
let exp_inst = substitute_rigids(exp, &mapping);
let actual = synth(a, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let actual = synth(a, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&exp_inst, &actual, subst)?;
}
Ok(Type::Con {
@@ -3197,7 +3274,7 @@ pub(crate) fn synth(
})
}
Term::Match { scrutinee, arms } => {
let s_ty = synth(scrutinee, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let s_ty = synth(scrutinee, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
if arms.is_empty() {
return Err(CheckError::NonExhaustive {
ty: ailang_core::pretty::type_to_string(&s_ty),
@@ -3215,7 +3292,7 @@ pub(crate) fn synth(
let prev = locals.insert(n.clone(), t.clone());
pushed.push((n.clone(), prev));
}
let body_ty = synth(&arm.body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let body_ty = synth(&arm.body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
for (n, prev) in pushed.into_iter().rev() {
match prev {
Some(p) => {
@@ -3290,9 +3367,9 @@ pub(crate) fn synth(
Ok(subst.apply(&result_ty.expect("checked arms is non-empty")))
}
Term::Seq { lhs, rhs } => {
let lty = synth(lhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let lty = synth(lhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
unify(&Type::unit(), &lty, subst)?;
synth(rhs, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
synth(rhs, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
Term::Lam { params, param_tys, ret_ty, effects: lam_effects, body } => {
let mut pushed: Vec<(String, Option<Type>)> = Vec::new();
@@ -3301,7 +3378,7 @@ pub(crate) fn synth(
pushed.push((n.clone(), prev));
}
let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
for (n, prev) in pushed.into_iter().rev() {
match prev {
Some(p) => {
@@ -3389,7 +3466,7 @@ pub(crate) fn synth(
// subset rule against `declared_effs` — exactly like
// `Term::Lam`.
let mut body_effects: BTreeSet<String> = BTreeSet::new();
let body_ty = synth(body, env, locals, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
let body_ty = synth(body, env, locals, mut_scope_stack, &mut body_effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
// Restore body-scope locals (params + name).
for (n, prev) in pushed.into_iter().rev() {
@@ -3416,7 +3493,7 @@ pub(crate) fn synth(
// scope (params are not visible here; only the recursive
// binding is).
let prev_in = locals.insert(name.clone(), ty.clone());
let in_ty = synth(in_term, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
let in_ty = synth(in_term, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings);
match prev_in {
Some(p) => {
locals.insert(name.clone(), p);
@@ -3432,7 +3509,7 @@ pub(crate) fn synth(
// No constraint generated, no environment change. The
// wrapper records author intent for the future RC inc/dec
// emission pass (18c.3); typing is pure passthrough.
synth(value, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
synth(value, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
Term::ReuseAs { source, body } => {
// Iter 18d.1: `(reuse-as SRC NEW-CTOR)` requires `body` to
@@ -3446,7 +3523,7 @@ pub(crate) fn synth(
// shape-compatibility check (18d.2 will add a
// `reuse-as-shape-mismatch` diagnostic when codegen has
// the actual size info).
let _ = synth(source, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
let _ = synth(source, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)?;
match body.as_ref() {
Term::Ctor { .. } | Term::Lam { .. } => {}
other => {
@@ -3474,30 +3551,105 @@ pub(crate) fn synth(
}
// Body's type is the result type of the whole reuse-as
// expression.
synth(body, env, locals, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
synth(body, env, locals, mut_scope_stack, effects, in_def, subst, counter, residuals, free_fn_calls, warnings)
}
// Iter mut.1: typecheck recognition of `Term::Mut` and
// `Term::Assign` is deferred to iter mut.2 (see
// `docs/specs/2026-05-15-mut-local.md` §"Iteration mut.1"
// out-of-iteration boundary). The dispatch entry here stubs
// with `CheckError::Internal` so that a well-formed mut block
// reaching this point in mut.1 fails fast with a
// human-readable message — the Form-A surface parses these
// shapes and the AST round-trips them, but no fn body is
// expected to *use* them yet.
Term::Mut { .. } => {
Err(CheckError::Internal(
"Term::Mut not yet supported in typecheck (deferred to iter mut.2)".into(),
))
// Iter mut.2: a mut block opens a fresh lexical scope for its
// mut-vars. Each var's `init` is synthed in the outer scope
// plus already-declared vars of this same frame (vars are
// initialised in declaration order; later inits see earlier
// names). The body is synthed with the completed frame on the
// stack. The frame is popped on exit. The block's static type
// is the body's static type.
Term::Mut { vars, body } => {
let mut frame: IndexMap<String, Type> = IndexMap::new();
for v in vars {
if !is_supported_mut_var_type(&v.ty) {
return Err(CheckError::UnsupportedMutVarType {
name: v.name.clone(),
ty: ailang_core::pretty::type_to_string(&v.ty),
});
}
// Synth the init in the outer scope plus any vars
// already pushed into `frame`. The cleanest way to
// expose those bindings is to push a single in-flight
// frame (clone of the accumulator) onto the stack for
// the duration of the init walk, then pop. This keeps
// the `mut_scope_stack` truthful at all times.
mut_scope_stack.push(frame.clone());
let init_ty = synth(
&v.init, env, locals, mut_scope_stack, effects, in_def,
subst, counter, residuals, free_fn_calls, warnings,
)?;
mut_scope_stack.pop();
unify(&v.ty, &init_ty, subst)?;
frame.insert(v.name.clone(), v.ty.clone());
}
mut_scope_stack.push(frame);
let body_result = synth(
body, env, locals, mut_scope_stack, effects, in_def,
subst, counter, residuals, free_fn_calls, warnings,
);
mut_scope_stack.pop();
body_result
}
Term::Assign { .. } => {
Err(CheckError::Internal(
"Term::Assign not yet supported in typecheck (deferred to iter mut.2)".into(),
))
// Iter mut.2: `Term::Assign` resolves its target name through
// the mut-scope stack (innermost-first). On a hit, the value's
// synth type must match the var's declared type. The
// expression's static type is Unit.
Term::Assign { name, value } => {
let declared: Option<Type> = mut_scope_stack
.iter()
.rev()
.find_map(|frame| frame.get(name).cloned());
match declared {
None => {
// Flatten every mut-var name visible at this point,
// innermost-first, deduplicated 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) => {
let value_ty = synth(
value, env, locals, mut_scope_stack, effects, in_def,
subst, counter, residuals, free_fn_calls, warnings,
)?;
let applied_declared = subst.apply(&declared_ty);
let applied_value = subst.apply(&value_ty);
if applied_declared != applied_value {
return Err(CheckError::AssignTypeMismatch {
name: name.clone(),
declared: ailang_core::pretty::type_to_string(&applied_declared),
got: ailang_core::pretty::type_to_string(&applied_value),
});
}
Ok(Type::unit())
}
}
}
}
}
/// Iter mut.2: gate `MutVar.ty` to the four stack-resident scalar
/// primitives per spec `docs/specs/2026-05-15-mut-local.md` §"Out of
/// scope". Heap-RC-managed types (Str, ADTs, fn-values) and any
/// parameterised constructor are deferred to a follow-on milestone.
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")
)
}
/// If `t` is a `Forall`, instantiate it with fresh metavars; otherwise
/// pass through unchanged. Used at every var-resolution site.
fn maybe_instantiate(t: Type, counter: &mut u32) -> Type {
@@ -3851,6 +4003,326 @@ mod tests {
use super::*;
use ailang_core::SCHEMA;
/// Helper that synths a single Term against a default empty env +
/// fresh local / scope / effect state. Returns the substituted
/// final type. Used by the mut.2 pin tests below.
fn synth_standalone(term: &Term) -> Type {
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let ty = synth(
term,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"<test>",
&mut subst,
&mut counter,
&mut residuals,
&mut free_fn_calls,
&mut warnings,
)
.expect("synth must succeed");
subst.apply(&ty)
}
/// Iter mut.2 (Task 3): `Term::Var` consults the mut-scope stack
/// before locals/globals. With a non-empty stack carrying
/// `x → Float` and a local also binding `x → Int`, resolving
/// `Var x` returns Float — mut-scope wins lexically.
///
/// The frame is pre-populated directly on the stack (rather than
/// running a `Term::Mut` block that would push it) so this pin
/// isolates the Var-arm change from the Mut-arm work in Task 4.
#[test]
fn mut_var_resolution_shadows_outer_local() {
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
locals.insert("x".into(), Type::int()); // outer let-style binding
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut frame: IndexMap<String, Type> = IndexMap::new();
frame.insert("x".into(), Type::float()); // inner mut-var
mut_scope_stack.push(frame);
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let term = Term::Var { name: "x".into() };
let ty = synth(
&term,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"<test>",
&mut subst,
&mut counter,
&mut residuals,
&mut free_fn_calls,
&mut warnings,
)
.expect("synth must succeed");
assert_eq!(
ty,
Type::float(),
"mut-var `x : Float` on the scope stack must shadow local `x : Int` (got {ty:?})",
);
}
/// Iter mut.2 (Task 3): innermost-first walk on the mut-scope
/// stack. With two frames each binding `x` to a different type,
/// the innermost (last-pushed) wins.
#[test]
fn mut_var_resolution_picks_innermost_frame() {
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut outer: IndexMap<String, Type> = IndexMap::new();
outer.insert("x".into(), Type::int());
mut_scope_stack.push(outer);
let mut inner: IndexMap<String, Type> = IndexMap::new();
inner.insert("x".into(), Type::bool_());
mut_scope_stack.push(inner);
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let term = Term::Var { name: "x".into() };
let ty = synth(
&term,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"<test>",
&mut subst,
&mut counter,
&mut residuals,
&mut free_fn_calls,
&mut warnings,
)
.expect("synth must succeed");
assert_eq!(
ty,
Type::bool_(),
"innermost mut-var frame must win (expected Bool, got {ty:?})",
);
}
/// Iter mut.2 (Task 4): a well-formed mut block with one Int var,
/// an assign updating it, and a final read of the var synths to
/// Int. Property protected: `Term::Mut` arm pushes its `vars` as
/// a frame, synths the body in that extended scope, and returns
/// the body's type.
#[test]
fn mut_block_typechecks_with_int_var_and_returns_int() {
// (mut (var x (con Int) 0) (assign x (app + x 1)) x)
// Note: + is not in the empty Env, so use a simpler body that
// exercises Mut/Assign without depending on operator resolution.
// (mut (var x (con Int) 0) (assign x 1) x)
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::Lit { lit: Literal::Int { value: 1 } }),
}),
rhs: Box::new(Term::Var { name: "x".into() }),
}),
};
let ty = synth_standalone(&term);
assert_eq!(
ty,
Type::int(),
"mut block with Int var, assign, and final read must synth as Int (got {ty:?})",
);
}
/// Iter mut.2 (Task 5): inside a mut frame with `var x : Int = 0`,
/// `(assign x 1)` synths as Unit. Property protected: a successful
/// Term::Assign resolves through the mut-scope stack and yields
/// Unit (the Assign expression's static type).
#[test]
fn assign_to_in_scope_mut_var_synths_unit() {
// (mut (var x (con Int) 0) (assign x 1))
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_standalone(&term);
assert_eq!(
ty,
Type::unit(),
"mut block whose body is a lone assign must synth as Unit (got {ty:?})",
);
}
/// Iter mut.2 (Task 5): assigning to an out-of-scope name (no
/// enclosing mut frame contains it) fires
/// `MutAssignOutOfScope` with the available mut-var names listed.
#[test]
fn assign_to_out_of_scope_name_fires_diagnostic() {
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: "y".into(),
value: Box::new(Term::Lit { lit: Literal::Int { value: 1 } }),
}),
};
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let err = synth(
&term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
"<test>", &mut subst, &mut counter, &mut residuals,
&mut free_fn_calls, &mut warnings,
)
.expect_err("assign to unknown name must be rejected");
match err {
CheckError::MutAssignOutOfScope { name, available } => {
assert_eq!(name, "y");
assert_eq!(available, vec!["x".to_string()]);
}
other => panic!("expected MutAssignOutOfScope, got {other:?}"),
}
}
/// Iter mut.2 (Task 5): assigning a Float-typed value to an
/// Int-typed mut-var fires `AssignTypeMismatch` with rendered
/// declared / got type strings.
#[test]
fn assign_with_wrong_value_type_fires_diagnostic() {
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::Float { bits: 0x3ff8_0000_0000_0000 } }),
}),
};
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let err = synth(
&term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
"<test>", &mut subst, &mut counter, &mut residuals,
&mut free_fn_calls, &mut warnings,
)
.expect_err("Float assigned to Int mut-var must be rejected");
match err {
CheckError::AssignTypeMismatch { name, declared, got } => {
assert_eq!(name, "x");
assert_eq!(declared, "Int");
assert_eq!(got, "Float");
}
other => panic!("expected AssignTypeMismatch, got {other:?}"),
}
}
/// Iter mut.2 (Task 4): a mut block declaring a Str-typed mut-var
/// fires `CheckError::UnsupportedMutVarType` per spec §"Out of
/// scope" — heap-RC-managed types are deferred to a follow-on
/// milestone.
#[test]
fn mut_block_rejects_str_var_with_unsupported_type() {
let term = Term::Mut {
vars: vec![ailang_core::ast::MutVar {
name: "s".into(),
ty: Type::str_(),
init: Term::Lit { lit: Literal::Str { value: "hi".into() } },
}],
body: Box::new(Term::Var { name: "s".into() }),
};
let env = Env::default();
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
let mut residuals: Vec<ResidualConstraint> = Vec::new();
let mut free_fn_calls: Vec<FreeFnCall> = Vec::new();
let mut warnings: Vec<Diagnostic> = Vec::new();
let err = synth(
&term, &env, &mut locals, &mut mut_scope_stack, &mut effects,
"<test>", &mut subst, &mut counter, &mut residuals,
&mut free_fn_calls, &mut warnings,
)
.expect_err("Str-typed mut-var must be rejected");
assert!(
matches!(err, CheckError::UnsupportedMutVarType { ref name, .. } if name == "s"),
"expected UnsupportedMutVarType for `s`, got {err:?}",
);
}
/// Iter mut.2 (Task 1): every new CheckError variant has a stable
/// kebab-case code() arm and a non-panicking ctx() arm.
#[test]
fn mut_typecheck_diagnostics_have_kebab_codes() {
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");
// Smoke-test ctx() — must not panic, must produce a JSON object.
let _ = e1.ctx();
let _ = e2.ctx();
let _ = e3.ctx();
}
fn fn_def(name: &str, ty: Type, params: Vec<&str>, body: Term) -> Def {
Def::Fn(FnDef {
name: name.into(),
@@ -6571,6 +7043,7 @@ mod tests {
let term = Term::Var { name: "show".into() };
let mut locals: IndexMap<String, Type> = IndexMap::new();
let mut mut_scope_stack: Vec<IndexMap<String, Type>> = Vec::new();
let mut effects: BTreeSet<String> = BTreeSet::new();
let mut subst = Subst::default();
let mut counter: u32 = 0;
@@ -6581,6 +7054,7 @@ mod tests {
&term,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
"test_call_site",
&mut subst,
crates/ailang-check/src/lift.rs
+5 -1
View File
@@ -720,7 +720,11 @@ impl<'a> Lifter<'a> {
// (e.g. class-method-shadowed-by-fn) have already been
// surfaced upstream by `check_workspace`. Discard here.
let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
let ty = synth(t, &self.env, locals, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
// Iter mut.2: lift's letrec-capture synth re-entry walks one
// term at a time, beginning from a top-of-body position; fresh
// empty mut-scope stack is correct.
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
let ty = synth(t, &self.env, locals, &mut mut_scope_stack, &mut effects, in_def, &mut subst, &mut counter, &mut residuals, &mut free_fn_calls, &mut warnings_discarded)?;
Ok(subst.apply(&ty))
}
}
crates/ailang-check/src/mono.rs
+10
View File
@@ -709,10 +709,15 @@ pub fn collect_mono_targets(
// discards warnings — typecheck has already run and surfaced any
// shadow warnings; mono is a post-typecheck pass.
let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
// Iter mut.2: mono re-synth begins from top-of-body — empty
// mut-scope, since any `Term::Mut` will push its own frame as the
// walk descends.
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
crate::synth(
&f.body,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
&f.name,
&mut subst,
@@ -1334,10 +1339,15 @@ pub(crate) fn collect_residuals_ordered(
// discards warnings — typecheck has already run and surfaced any
// shadow warnings; mono is a post-typecheck pass.
let mut warnings_discarded: Vec<crate::diagnostic::Diagnostic> = Vec::new();
// Iter mut.2: mono re-synth begins from top-of-body — empty
// mut-scope, since any `Term::Mut` will push its own frame as the
// walk descends.
let mut mut_scope_stack: Vec<indexmap::IndexMap<String, crate::Type>> = Vec::new();
crate::synth(
&f.body,
&env,
&mut locals,
&mut mut_scope_stack,
&mut effects,
&f.name,
&mut subst,
crates/ailang-check/tests/mut_typecheck_pin.rs
+63
View File
@@ -0,0 +1,63 @@
//! Iter mut.2 (Task 6): 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" — names each fixture and the diagnostic
//! it must surface. The carve-out justification for landing these as
//! `.ail.json` rather than `.ail` mirrors the post-form-a precedent
//! (broken_unbound, test_22b2_*.ail.json) — negative typecheck
//! fixtures live as canonical JSON so the diagnostic code is the
//! load-bearing assertion, not the surface form.
use ailang_check::check_workspace;
use ailang_surface::load_workspace;
use std::path::PathBuf;
fn examples_dir() -> PathBuf {
let manifest = env!("CARGO_MANIFEST_DIR");
PathBuf::from(manifest)
.parent().expect("CARGO_MANIFEST_DIR has a parent (crates/ailang-check)")
.parent().expect("CARGO_MANIFEST_DIR has a grandparent (crates/)")
.join("examples")
}
/// Load the named fixture under `examples/`, run check_workspace, and
/// return the diagnostic code list (one entry per Diagnostic).
fn check_fixture(fixture_name: &str) -> Vec<String> {
let path = examples_dir().join(fixture_name);
let ws = load_workspace(&path)
.unwrap_or_else(|e| panic!("workspace `{fixture_name}` must load: {e:?}"));
let diags = check_workspace(&ws);
diags.iter().map(|d| d.code.clone()).collect()
}
#[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:?}");
}
crates/ailang-core/tests/carve_out_inventory.rs
+18 -4
View File
@@ -1,10 +1,18 @@
//! Carve-out inventory check — §T4 of the form-a-default-authoring
//! spec. Asserts that exactly the seven named carve-out files exist
//! spec. Asserts that exactly the named carve-out files exist
//! under `examples/*.ail.json` after milestone close. The list is
//! hardcoded; any change is a deliberate, brainstorm-level decision.
//!
//! Seven carve-outs post prelude-decouple (2026-05-14):
//! - §C4 (a) subject-matter: 7 fixtures (canonical-form rejection / unbound / class-def rejection).
//! Twelve carve-outs post iter mut.2 (2026-05-15):
//! - §C4 (a) subject-matter: 7 fixtures from form-a.1 milestone
//! close (canonical-form rejection / unbound / class-def rejection).
//! - Iter mut.2: 5 negative typecheck fixtures for the new mut /
//! var / assign forms. The diagnostic code is the load-bearing
//! assertion (mut-assign-out-of-scope, assign-type-mismatch,
//! mut-var-unsupported-type) — mirroring the §C4(a) negative-
//! fixture convention. The positive nested-shadow case is a
//! .ail.json carve-out for symmetry with its negative siblings
//! (the driver tests all five from one helper).
//! - §C4 (b) compile-time-embed: retired 2026-05-14 by milestone
//! prelude-decouple; the prelude is now embedded as `prelude.ail`
//! in `ailang-surface` and parsed at compile time via
@@ -13,7 +21,7 @@
use std::collections::BTreeSet;
const EXPECTED: &[&str] = &[
// §C4 (a) — subject-matter
// §C4 (a) — subject-matter (form-a.1 milestone close)
"broken_unbound.ail.json",
"test_22b2_invalid_superclass_param.ail.json",
"test_22b2_kind_mismatch.ail.json",
@@ -21,6 +29,12 @@ const EXPECTED: &[&str] = &[
"test_ct1_bad_qualifier.ail.json",
"test_ct1_bare_xmod_rejected.ail.json",
"test_ct1_qualified_class_rejected.ail.json",
// Iter mut.2 — negative typecheck fixtures + positive shadow-pin
"test_mut_assign_out_of_scope.ail.json",
"test_mut_assign_outside_mut.ail.json",
"test_mut_assign_type_mismatch.ail.json",
"test_mut_nested_shadow_legal.ail.json",
"test_mut_var_unsupported_type.ail.json",
];
fn examples_dir() -> std::path::PathBuf {