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

Iter 14e: explicit, verified tail calls

Browse Source 
Decision 8 ships. Term::App and Term::Do gain tail: bool with
serde-default false and skip-when-false serialisation. New
typecheck pass verify_tail_positions enforces tail-position rules
(Scheme-style propagation through match arms, seq.rhs, let body,
lam body). Codegen emits musttail call for marked App calls.

Hash invariance verified: only the two migrated print_list defs
(list_map_poly.print_list, sort.print_list) changed hashes; all
other defs across all 18 fixtures kept bit-identical hashes —
confirms the skip-when-false serialisation rule works.

Tests 76 -> 79: tail_call_in_non_tail_position_is_rejected,
tail_call_in_tail_position_is_accepted, plus an IR-grep e2e test
asserting that print_list's recursive call site emits musttail
in the lowered IR. Existing 25 e2e tests unchanged in behaviour
(map -> [2,3,4], sort -> sorted list).

IR evidence at the recursive site:
  %v7 = musttail call i8 @ail_list_map_poly_print_list(ptr %v6)
  ret i8 %v7

Two deviations called out in the implementer report and JOURNAL:
1. tail-do uses tail call, not musttail. Cross-type return
   (runtime helpers return i32, AILang Unit is i8) would have
   LLVM reject musttail. Path is implemented but not exercised
   by any current fixture; proper fix is runtime-helper signature
   change, punted.
2. block_terminated flag in codegen so tail-call emit
   (musttail call + ret) doesn't get a duplicate trailing ret
   from surrounding code (match-arm phi, fn-body, lambda thunk).
   Internal plumbing; required for IR well-formedness.

Form (A) productions now at ~30, exactly the constraint-1
budget. Future surface additions need to retire something or
explicit-budget-rebalance in DESIGN.md.

GC notes from implementer survey land in JOURNAL:
- Allocations cluster in lower_ctor; every term-ctor does
  malloc(8+8n).
- Tail recursion does not reduce alloc pressure, only stack.
  For map-style ctor-blocked recursions, allocation IS the
  bottleneck.
- Per-fn arena is sound only when fn return type contains no
  boxed ADT. Most current fixtures violate this.

Plan 14f: Boehm conservative GC (GC_malloc, -lgc) as a first
cut. Single-iter integration, no AST/schema change. Stress
test: build a 100k Cons list, observe RSS doesn't blow up.

After 14f the language is feature-complete enough for stdlib
work (15a).

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Brummel
2026-05-07 17:16:28 +02:00
parent 8d97a924de
commit d64031c234
16 changed files with 768 additions and 81 deletions
Download Patch File Download Diff File Expand all files Collapse all files
crates/ailang-check/src/diagnostic.rs
+1
View File
@@ -39,6 +39,7 @@
//! - `module-cycle` — workspace loader (Iter 5b, in the CLI path)
//! - `module-name-mismatch` — workspace loader (Iter 5b, in the CLI path)
//! - `module-hash-mismatch` — workspace loader (Iter 5b, in the CLI path)
//! - `tail-call-not-in-tail-position` (Iter 14e, see Decision 8)
use serde::Serialize;
crates/ailang-check/src/lib.rs
+222 -2
View File
@@ -395,6 +395,12 @@ pub enum CheckError {
/// for qualified cross-module references. Code: `invalid-def-name`.
#[error("invalid def name `{name}`: contains `.` (reserved for qualified refs)")]
InvalidDefName { name: String },
/// Iter 14e: a `Term::App { tail: true, .. }` or
/// `Term::Do { tail: true, .. }` was found in a non-tail position.
/// Code: `tail-call-not-in-tail-position`. See Decision 8.
#[error("call marked `tail` is not in tail position")]
TailCallNotInTailPosition,
}
type Result<T> = std::result::Result<T, CheckError>;
@@ -430,6 +436,7 @@ impl CheckError {
CheckError::UnknownModule { .. } => "unknown-module",
CheckError::UnknownImport { .. } => "unknown-import",
CheckError::InvalidDefName { .. } => "invalid-def-name",
CheckError::TailCallNotInTailPosition => "tail-call-not-in-tail-position",
}
}
@@ -894,6 +901,11 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
let body_ty = synth(&f.body, &env, &mut locals, &mut effects, &f.name, &mut subst, &mut counter)?;
unify(&ret_ty, &body_ty, &mut subst)?;
// Iter 14e: tail-position verification (Decision 8). Runs after
// the main type-check so that a tail-call marker on a malformed
// call doesn't drown out the underlying type error.
verify_tail_positions(&f.body, true)?;
let declared: BTreeSet<String> = declared_effs.into_iter().collect();
for e in &effects {
if !declared.contains(e) {
@@ -903,6 +915,77 @@ fn check_fn(f: &FnDef, env: &Env) -> Result<()> {
Ok(())
}
/// Iter 14e: verifies that every `Term::App { tail: true, .. }` and
/// `Term::Do { tail: true, .. }` actually sits in tail position, per
/// Decision 8.
///
/// `is_tail` is the tail-context flag for the term currently being
/// visited. The propagation rules (from DESIGN.md Decision 8):
///
/// - The body of a fn / Lam is visited with `is_tail = true`.
/// - `Match { scrutinee, arms }`: the scrutinee is **not** in tail
/// position; each arm body inherits the same `is_tail` as the match.
/// - `Seq { lhs, rhs }`: lhs is non-tail; rhs inherits.
/// - `Let { value, body, .. }`: value is non-tail; body inherits.
/// - `App { callee, args, tail }`: the callee and all args are
/// non-tail. If `tail == true`, the App itself must have arrived
/// with `is_tail == true`; otherwise diagnostic.
/// - `Do { args, tail }`: same rule as App; all args are non-tail.
/// - `Ctor { args }`: all args are non-tail.
/// - `Lam { body }`: the Lam value is at whatever `is_tail` was; the
/// recursion **into** the body opens a fresh tail scope (the body
/// is visited with `is_tail = true`).
/// - `Lit`, `Var`: leaves; no further descent.
pub fn verify_tail_positions(t: &Term, is_tail: bool) -> Result<()> {
match t {
Term::Lit { .. } | Term::Var { .. } => Ok(()),
Term::App { callee, args, tail } => {
if *tail && !is_tail {
return Err(CheckError::TailCallNotInTailPosition);
}
verify_tail_positions(callee, false)?;
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Do { args, tail, .. } => {
if *tail && !is_tail {
return Err(CheckError::TailCallNotInTailPosition);
}
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Let { value, body, .. } => {
verify_tail_positions(value, false)?;
verify_tail_positions(body, is_tail)
}
Term::Seq { lhs, rhs } => {
verify_tail_positions(lhs, false)?;
verify_tail_positions(rhs, is_tail)
}
Term::Match { scrutinee, arms } => {
verify_tail_positions(scrutinee, false)?;
for arm in arms {
verify_tail_positions(&arm.body, is_tail)?;
}
Ok(())
}
Term::Ctor { args, .. } => {
for a in args {
verify_tail_positions(a, false)?;
}
Ok(())
}
Term::Lam { body, .. } => {
// Entering a Lam body opens a fresh tail scope.
verify_tail_positions(body, true)
}
}
}
fn check_const(c: &ConstDef, env: &Env) -> Result<()> {
// Const types are never polymorphic — a Forall here is rejected
// outright. Any other type passes through to `synth` as before.
@@ -976,7 +1059,7 @@ fn synth(
};
Ok(maybe_instantiate(raw, counter))
}
Term::App { callee, args } => {
Term::App { callee, args, .. } => {
let cty = synth(callee, env, locals, effects, in_def, subst, counter)?;
let cty = subst.apply(&cty);
let (params, ret, fx) = match &cty {
@@ -1035,7 +1118,7 @@ fn synth(
}
Ok(r)
}
Term::Do { op, args } => {
Term::Do { op, args, .. } => {
let sig = env
.effect_ops
.get(op)
@@ -1425,6 +1508,7 @@ mod tests {
Term::Var { name: "a".into() },
Term::Var { name: "b".into() },
],
tail: false,
},
)],
};
@@ -1474,6 +1558,7 @@ mod tests {
args: vec![Term::Lit {
lit: Literal::Int { value: 1 },
}],
tail: false,
},
)],
};
@@ -1711,6 +1796,7 @@ mod tests {
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
tail: false,
},
);
// `use_bool` returns id(true) :: Bool.
@@ -1725,6 +1811,7 @@ mod tests {
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
tail: false,
},
);
let m = Module {
@@ -1766,6 +1853,7 @@ mod tests {
Term::App {
callee: Box::new(Term::Var { name: "id".into() }),
args: vec![Term::Lit { lit: Literal::Int { value: 42 } }],
tail: false,
},
);
let m = Module {
@@ -1805,6 +1893,7 @@ mod tests {
Term::App {
callee: Box::new(Term::Var { name: "f".into() }),
args: vec![Term::Var { name: "x".into() }],
tail: false,
},
);
// A monomorphic helper to be passed to apply.
@@ -1822,6 +1911,7 @@ mod tests {
Term::Var { name: "n".into() },
Term::Lit { lit: Literal::Int { value: 1 } },
],
tail: false,
},
);
let use_apply = fn_def(
@@ -1838,6 +1928,7 @@ mod tests {
Term::Var { name: "succ".into() },
Term::Lit { lit: Literal::Int { value: 41 } },
],
tail: false,
},
);
let m = Module {
@@ -1945,6 +2036,7 @@ mod tests {
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Int { value: 7 } }],
}],
tail: false,
},
);
let use_bool = fn_def(
@@ -1962,6 +2054,7 @@ mod tests {
ctor: "MkBox".into(),
args: vec![Term::Lit { lit: Literal::Bool { value: true } }],
}],
tail: false,
},
);
let m = Module {
@@ -2041,4 +2134,131 @@ mod tests {
let msg = format!("{err}");
assert!(msg.contains("type mismatch"), "got: {msg}");
}
/// Iter 14e: a `Term::App { tail: true, .. }` in non-tail position
/// must surface as `tail-call-not-in-tail-position`. Construction:
/// the recursive call sits as an argument to a Cons ctor (the
/// classic constructor-blocked recursion from the 14d survey).
#[test]
fn tail_call_in_non_tail_position_is_rejected() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "L".into(),
vars: vec![],
ctors: vec![
Ctor { name: "N".into(), fields: vec![] },
Ctor {
name: "C".into(),
fields: vec![
Type::int(),
Type::Con { name: "L".into(), args: vec![] },
],
},
],
doc: None,
}),
fn_def(
"loop",
Type::Fn {
params: vec![Type::Con { name: "L".into(), args: vec![] }],
ret: Box::new(Type::Con { name: "L".into(), args: vec![] }),
effects: vec![],
},
vec!["xs"],
// Body: C(0, tail-app loop xs) — the recursion is
// an arg to C, which is NOT a tail position.
Term::Ctor {
type_name: "L".into(),
ctor: "C".into(),
args: vec![
Term::Lit { lit: Literal::Int { value: 0 } },
Term::App {
callee: Box::new(Term::Var { name: "loop".into() }),
args: vec![Term::Var { name: "xs".into() }],
tail: true,
},
],
},
),
],
};
let err = check(&m).unwrap_err();
assert_eq!(err.code(), "tail-call-not-in-tail-position", "{err}");
}
/// Iter 14e: a `Term::App { tail: true, .. }` that genuinely sits
/// in tail position (as the rhs of a `Seq` that is the body of a
/// `Match` arm that is the body of the fn) must pass.
#[test]
fn tail_call_in_tail_position_is_accepted() {
let m = Module {
schema: SCHEMA.into(),
name: "t".into(),
imports: vec![],
defs: vec![
Def::Type(TypeDef {
name: "L".into(),
vars: vec![],
ctors: vec![
Ctor { name: "N".into(), fields: vec![] },
Ctor {
name: "C".into(),
fields: vec![
Type::int(),
Type::Con { name: "L".into(), args: vec![] },
],
},
],
doc: None,
}),
fn_def(
"drain",
Type::Fn {
params: vec![Type::Con { name: "L".into(), args: vec![] }],
ret: Box::new(Type::unit()),
effects: vec!["IO".into()],
},
vec!["xs"],
Term::Match {
scrutinee: Box::new(Term::Var { name: "xs".into() }),
arms: vec![
Arm {
pat: Pattern::Ctor {
ctor: "N".into(),
fields: vec![],
},
body: Term::Lit { lit: Literal::Unit },
},
Arm {
pat: Pattern::Ctor {
ctor: "C".into(),
fields: vec![
Pattern::Var { name: "h".into() },
Pattern::Var { name: "t".into() },
],
},
body: Term::Seq {
lhs: Box::new(Term::Do {
op: "io/print_int".into(),
args: vec![Term::Var { name: "h".into() }],
tail: false,
}),
rhs: Box::new(Term::App {
callee: Box::new(Term::Var { name: "drain".into() }),
args: vec![Term::Var { name: "t".into() }],
tail: true,
}),
},
},
],
},
),
],
};
check(&m).expect("tail-call in tail position should typecheck");
}
}