From d5f63bc3e550237eb58a29080849075b060dd9da Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 7 May 2026 21:00:49 +0200 Subject: [PATCH] =?UTF-8?q?Iter=2016b.2=20=E2=80=94=20LetRec=20captures=20?= =?UTF-8?q?of=20fn-params=20(path-1=20safe=20subset)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Lift 16b.1's no-capture restriction. The desugar pass's `scope` becomes a `BTreeMap` carrying `KnownType` for fn/Lam-params, sentinels for Let-/Match-bindings. LetRec captures of `KnownType` names are lifted: the synthetic top-level fn's signature gets the capture types appended, and every call site of the LetRec name is rewritten via `subst_call_with_extras` to pass the captures positionally. Captures from let-bindings, match-arm patterns, polymorphic enclosing fns, and name-as-value uses are rejected at desugar with panics pointing at 16b.3-16b.7. Demo: `sum_below(n)` recurses via `(let-rec loop (params i) ... (body ... uses n ...) (in (app loop 1)))`. Lifts to `loop$lr_0(i: Int, n: Int) -> Int` with `(app loop X)` rewritten to `(app loop$lr_0 X n)`. Outputs 0, 10, 45. Tests: 103 -> 106 (+1 e2e local_rec_capture_demo, +2 desugar unit; the 16b.1 capture-panic test was repurposed into the positive fn-param-capture test). Co-Authored-By: Claude Opus 4.7 (1M context) --- crates/ail/tests/e2e.rs | 17 + crates/ailang-core/src/desugar.rs | 620 +++++++++++++++++++++++++--- docs/JOURNAL.md | 157 +++++++ examples/local_rec_capture.ail.json | 1 + examples/local_rec_capture.ailx | 35 ++ 5 files changed, 776 insertions(+), 54 deletions(-) create mode 100644 examples/local_rec_capture.ail.json create mode 100644 examples/local_rec_capture.ailx diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index 47f59cd..98f21cb 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -450,6 +450,23 @@ fn local_rec_factorial_demo() { assert_eq!(lines, vec!["1", "6", "120"]); } +/// Iter 16b.2: LetRec capture of a fn-param (path-1 safe subset). +/// Property protected: the desugar pass lifts a LetRec whose body +/// captures one or more enclosing-scope names (here: `n` from +/// `sum_below`'s params) into a synthetic top-level fn whose +/// signature has the capture types appended, and rewrites every +/// call site of the LetRec name in body and in_term to pass the +/// captures positionally as extra args. Without 16b.2, the +/// 16b.1-era panic ("would capture") would fire and the build +/// would fail. Three call sites: sum_below(1)=0, sum_below(5)=10, +/// sum_below(10)=45. +#[test] +fn local_rec_capture_demo() { + let stdout = build_and_run("local_rec_capture.ail.json"); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines, vec!["0", "10", "45"]); +} + /// Guards `ail diff`: a modified body changes the hash of `sum`, while /// `main` stays unchanged. Expects exit code 1, `changed` contains exactly /// `sum`, `unchanged` contains `main`, `added`/`removed` empty. diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 7ee6794..79a52e3 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -102,7 +102,36 @@ //! bodies that capture from the enclosing scope (queued as 16b.2). use crate::ast::*; -use std::collections::BTreeSet; +use std::collections::{BTreeMap, BTreeSet}; + +/// Iter 16b.2: per-name scope information used by the LetRec lifter. +/// `KnownType(t)` is set for fn-params and Lam-params, where the +/// type is statically declared. Other binder kinds use the +/// placeholder variants and the LetRec lifter rejects captures of +/// those names with a clear error pointing at the follow-up iter +/// that will lift the restriction. +#[derive(Debug, Clone)] +enum ScopeEntry { + /// Fn-param or Lam-param, type known at this point. + KnownType(Type), + /// Bound by `Term::Let` — value's type is inferred at + /// typecheck, unknown at desugar. Captures error → 16b.3. + /// Also used for fn-params of a `Type::Forall`-typed enclosing + /// fn, where the param types may mention outer type vars and + /// the lifted signature would need a synthesized `Forall` — + /// out of scope for 16b.2 (queued for 16b.6). + LetBound, + /// Bound by a `Term::Match` arm pattern — type would require + /// constructor-field substitution from the scrutinee. Not + /// computed in this iter. Captures error → 16b.4. + MatchArm, + /// Bound by a `Term::LetRec` (its own name) — fn-typed, but + /// the value flows through a recursive position; supported + /// for fn/Lam-param transitivity but not for nested-LetRec + /// mutual capture. The LetRec lifter rejects captures of a + /// name with this entry → 16b.7. + EnclosingLetRec, +} /// Rewrite `m` so that every [`Pattern::Ctor`] sub-pattern is a /// [`Pattern::Var`] or [`Pattern::Wild`] (i.e. flat) and every @@ -151,11 +180,41 @@ pub fn desugar_module(m: &Module) -> Module { for def in &mut out.defs { match def { Def::Fn(f) => { - let scope: BTreeSet = f.params.iter().cloned().collect(); + // Iter 16b.2: build initial scope from fn-params with + // their declared types (peeled out of `f.ty`). For a + // `Type::Forall`-quantified fn, the param types may + // mention outer type vars; constructing a lifted + // `Forall` signature is out of scope for 16b.2, so + // every param of a polymorphic enclosing fn enters + // the scope as `LetBound` — captures of those names + // by an inner LetRec are rejected at the same site + // as let-binding captures. + let mut scope: BTreeMap = BTreeMap::new(); + match &f.ty { + Type::Fn { params: ptys, .. } if ptys.len() == f.params.len() => { + for (p, pty) in f.params.iter().zip(ptys.iter()) { + scope.insert(p.clone(), ScopeEntry::KnownType(pty.clone())); + } + } + Type::Forall { .. } => { + for p in &f.params { + scope.insert(p.clone(), ScopeEntry::LetBound); + } + } + _ => { + // Defensive: if the fn type is malformed (e.g. + // arity mismatch, non-Fn). Fall back to LetBound + // for every param so captures are rejected + // cleanly rather than silently mistyped. + for p in &f.params { + scope.insert(p.clone(), ScopeEntry::LetBound); + } + } + } f.body = d.desugar_term(&f.body, &scope); } Def::Const(c) => { - let scope: BTreeSet = BTreeSet::new(); + let scope: BTreeMap = BTreeMap::new(); c.value = d.desugar_term(&c.value, &scope); } Def::Type(_) => {} @@ -309,15 +368,20 @@ impl Desugarer { /// Recursively rewrites `t`: descends into every child first /// (bottom-up), then dispatches a [`Term::Match`] to /// [`desugar_match`](Self::desugar_match) and a [`Term::LetRec`] - /// to the 16b.1 lifter. + /// to the 16b.1 / 16b.2 lifter. /// - /// `scope` is the set of names lexically bound at this point — - /// initialised at the def boundary (fn params for [`Def::Fn`], - /// empty for [`Def::Const`]) and extended locally by every - /// binder ([`Term::Let`], [`Term::Lam`], [`Term::Match`] arms, - /// [`Term::LetRec`]). Used by the LetRec lifter to detect - /// captures. - fn desugar_term(&mut self, t: &Term, scope: &BTreeSet) -> Term { + /// `scope` maps every name lexically bound at this point to its + /// [`ScopeEntry`] — initialised at the def boundary (fn-params + /// with `KnownType` for monomorphic enclosing fns; `LetBound` + /// for `Type::Forall`-quantified ones; empty for [`Def::Const`]) + /// and extended locally by every binder ([`Term::Let`] → + /// `LetBound`; [`Term::Lam`] → `KnownType`; [`Term::Match`] arm + /// pattern bindings → `MatchArm`; [`Term::LetRec`] → its own + /// name as `EnclosingLetRec`, params as `KnownType`). Used by + /// the LetRec lifter (16b.2) to classify each capture and + /// either accept it (KnownType) or reject with a clear error + /// pointing at the follow-up iter. + fn desugar_term(&mut self, t: &Term, scope: &BTreeMap) -> Term { match t { Term::Lit { .. } | Term::Var { .. } => t.clone(), Term::App { callee, args, tail } => Term::App { @@ -328,7 +392,7 @@ impl Desugarer { Term::Let { name, value, body } => { let v = self.desugar_term(value, scope); let mut inner = scope.clone(); - inner.insert(name.clone()); + inner.insert(name.clone(), ScopeEntry::LetBound); let b = self.desugar_term(body, &inner); Term::Let { name: name.clone(), @@ -358,7 +422,11 @@ impl Desugarer { .iter() .map(|a| { let mut inner = scope.clone(); - pattern_binds(&a.pat, &mut inner); + let mut pat_binds: BTreeSet = BTreeSet::new(); + pattern_binds(&a.pat, &mut pat_binds); + for n in pat_binds { + inner.insert(n, ScopeEntry::MatchArm); + } Arm { pat: a.pat.clone(), body: self.desugar_term(&a.body, &inner), @@ -375,8 +443,8 @@ impl Desugarer { body, } => { let mut inner = scope.clone(); - for p in params { - inner.insert(p.clone()); + for (p, pty) in params.iter().zip(param_tys.iter()) { + inner.insert(p.clone(), ScopeEntry::KnownType(pty.clone())); } Term::Lam { params: params.clone(), @@ -391,26 +459,49 @@ impl Desugarer { rhs: Box::new(self.desugar_term(rhs, scope)), }, Term::LetRec { name, ty, params, body, in_term } => { - // Iter 16b.1: lift to a synthetic top-level fn. - // - // Body's scope: outer ∪ {name} ∪ params (recursive - // self-reference is legal; params shadow outer names). + // Iter 16b.1: lift to a synthetic top-level fn (no-capture). + // Iter 16b.2: extend the lift to the path-1 safe subset — + // captures of fn-params / Lam-params (whose types are + // known statically). Captures of Let / MatchArm / + // EnclosingLetRec names, captures from a polymorphic + // enclosing fn, and any non-callee use of `name` are + // still rejected at desugar time, with a follow-up + // iter pointer in the panic message. + + // Peel `ty` to its inner Fn so we know the LetRec's + // own param types (for body-scope) and so we can + // detect a Forall LetRec early. + let inner_params_tys: Vec = match peel_forall_to_fn(ty) { + Some(Type::Fn { params: ps, .. }) => ps.clone(), + _ => panic!( + "Iter 16b.2: LetRec `{}` must have a Fn type (or Forall); got {:?}", + name, ty + ), + }; + if inner_params_tys.len() != params.len() { + panic!( + "Iter 16b.2: LetRec `{}` param count {} != type's param count {}", + name, params.len(), inner_params_tys.len() + ); + } + + // Body's scope: outer ∪ {name → EnclosingLetRec} ∪ + // params with their declared types as KnownType. let mut body_scope = scope.clone(); - body_scope.insert(name.clone()); - for p in params { - body_scope.insert(p.clone()); + body_scope.insert(name.clone(), ScopeEntry::EnclosingLetRec); + for (p, pty) in params.iter().zip(inner_params_tys.iter()) { + body_scope.insert(p.clone(), ScopeEntry::KnownType(pty.clone())); } let desugared_body = self.desugar_term(body, &body_scope); - // in_term's scope: outer ∪ {name} (params are lambda- - // local to the LetRec's body, not visible in `in`). + // 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(name.clone()); + in_scope.insert(name.clone(), ScopeEntry::EnclosingLetRec); let desugared_in = self.desugar_term(in_term, &in_scope); - // Capture detection: free vars of the desugared body - // wrt {name} ∪ params, intersected with the outer - // `scope`. Anything in that intersection is a capture - // (16b.2 territory). + // Capture detection (against the *outer* scope, before + // the body-scope extension). let mut local_bound: BTreeSet = BTreeSet::new(); local_bound.insert(name.clone()); for p in params { @@ -418,30 +509,125 @@ impl Desugarer { } let mut frees: BTreeSet = BTreeSet::new(); free_vars_in_term(&desugared_body, &local_bound, &mut frees); - let captures: Vec = frees.intersection(scope).cloned().collect(); - if !captures.is_empty() { + let captures: Vec = frees + .iter() + .filter(|f| scope.contains_key(*f)) + .cloned() + .collect(); + + // 16b.2: classify each capture's ScopeEntry. KnownType + // is supported; everything else errors with a follow-up + // iter pointer. + let mut capture_types: Vec<(String, Type)> = Vec::new(); + for c in &captures { + match scope.get(c).expect("capture-in-scope-by-construction") { + ScopeEntry::KnownType(t) => { + capture_types.push((c.clone(), t.clone())); + } + ScopeEntry::LetBound => panic!( + "Iter 16b.2: LetRec `{}` captures `{}` from a let-binding \ + (or polymorphic enclosing fn); not supported. Queued for \ + 16b.3 (let-binding captures with type info from typecheck).", + name, c + ), + ScopeEntry::MatchArm => panic!( + "Iter 16b.2: LetRec `{}` captures `{}` from a match-arm \ + pattern binding; not supported. Queued for 16b.4 (match-arm \ + captures with constructor-field substitution).", + name, c + ), + ScopeEntry::EnclosingLetRec => panic!( + "Iter 16b.2: LetRec `{}` captures `{}` from an enclosing \ + LetRec; nested mutual-capture is not supported. Queued for \ + 16b.7.", + name, c + ), + } + } + + // 16b.2: validate that `name` is only ever used as the + // callee of a Term::App in body and in_term — never as + // a Term::Var in any value position. This guards + // against `(let g f ...)` bindings and `(app some_hof + // f)` value-passing, which would need closure + // conversion. + if let Some(violation) = find_non_callee_use(&desugared_body, name) { panic!( - "Iter 16b.1: local recursive `let` `{}` would capture {:?} \ - from enclosing scope; capture is queued for 16b.2. Lift \ - the helper to top-level for now.", - name, captures + "Iter 16b.2: LetRec `{}` is used as a value in its own body \ + (not as the callee of `app`); not supported. Queued for 16b.5 \ + (closure conversion). Offending term: {:?}", + name, violation + ); + } + if let Some(violation) = find_non_callee_use(&desugared_in, name) { + panic!( + "Iter 16b.2: LetRec `{}` is used as a value in the in-clause \ + (not as the callee of `app`); not supported. Queued for 16b.5. \ + Offending term: {:?}", + name, violation ); } - // Lift: synthesise a fresh top-level def name and - // substitute every reference to the local `name` - // (in body and in_term) to the lifted name. + // Build augmented type: original Fn with capture types + // appended to `params`. A Forall LetRec is rejected + // (would need synthesised Forall — out of scope). + let augmented_ty = match ty { + Type::Fn { params: ps, ret, effects } => { + let mut new_ps = ps.clone(); + for (_, t) in &capture_types { + new_ps.push(t.clone()); + } + Type::Fn { + params: new_ps, + ret: ret.clone(), + effects: effects.clone(), + } + } + Type::Forall { .. } => panic!( + "Iter 16b.2: LetRec `{}` has a Forall type; captures from a \ + polymorphic context are not supported. Queued for 16b.6.", + name + ), + other => panic!( + "Iter 16b.2: LetRec `{}` has non-Fn/Forall type {:?}", + name, other + ), + }; + // Augmented param-name list: original params + capture + // names (using the captured variable names directly so + // the lifted body's references already resolve + // correctly). + let mut augmented_params = params.clone(); + for (cn, _) in &capture_types { + augmented_params.push(cn.clone()); + } + + // Lift. let lifted_name = self.fresh_lifted(name); - let body_lifted = subst_var(&desugared_body, name, &lifted_name); - let in_lifted = subst_var(&desugared_in, name, &lifted_name); + + // Rewrite (app name args) to (app lifted_name args... cap0 + // cap1 ...) FIRST, then substitute name -> lifted_name + // everywhere (handles non-call references, but in 16b.2 + // those are now ruled out by `find_non_callee_use` — + // the second pass remains for symmetry with 16b.1 and + // for the case where there are zero captures). + let extras: Vec = + capture_types.iter().map(|(n, _)| n.clone()).collect(); + let body_call_rw = + subst_call_with_extras(&desugared_body, name, &lifted_name, &extras); + let body_full = subst_var(&body_call_rw, name, &lifted_name); + let in_call_rw = + subst_call_with_extras(&desugared_in, name, &lifted_name, &extras); + let in_full = subst_var(&in_call_rw, name, &lifted_name); + self.lifted.push(Def::Fn(FnDef { name: lifted_name, - ty: ty.clone(), - params: params.clone(), - body: body_lifted, + ty: augmented_ty, + params: augmented_params, + body: body_full, doc: None, })); - in_lifted + in_full } } } @@ -844,6 +1030,158 @@ fn subst_var(t: &Term, from: &str, to: &str) -> Term { } } +/// Iter 16b.2: peel a `Type::Forall { body: Type::Fn { ... } }` to +/// expose the inner `Type::Fn`. Returns `Some(&Type::Fn)` if the +/// type is `Fn` or `Forall`; `None` otherwise. +fn peel_forall_to_fn(t: &Type) -> Option<&Type> { + match t { + Type::Fn { .. } => Some(t), + Type::Forall { body, .. } => peel_forall_to_fn(body), + _ => None, + } +} + +/// Iter 16b.2: walk `t` and rewrite every `Term::App { callee = +/// Var{name}, args }` to `Term::App { callee = Var{lifted}, args = +/// args ++ extras_as_vars }`. Recurses into all sub-terms. Does +/// not touch `Term::Var { name }` in non-callee positions — that's +/// flagged separately by [`find_non_callee_use`]. +fn subst_call_with_extras(t: &Term, name: &str, lifted: &str, extras: &[String]) -> Term { + match t { + Term::Lit { .. } => t.clone(), + Term::Var { .. } => t.clone(), + Term::App { callee, args, tail } => { + let mut new_args: Vec = args + .iter() + .map(|a| subst_call_with_extras(a, name, lifted, extras)) + .collect(); + let new_callee = match callee.as_ref() { + Term::Var { name: n } if n == name => { + // Append extras as Var references — at this site, + // the captured variable names are still in scope + // because the lifted fn appends them as extra + // params with the same names. + for ex in extras { + new_args.push(Term::Var { name: ex.clone() }); + } + Box::new(Term::Var { name: lifted.to_string() }) + } + _ => Box::new(subst_call_with_extras(callee, name, lifted, extras)), + }; + Term::App { + callee: new_callee, + args: new_args, + tail: *tail, + } + } + Term::Let { name: n, value, body } => Term::Let { + name: n.clone(), + value: Box::new(subst_call_with_extras(value, name, lifted, extras)), + body: Box::new(subst_call_with_extras(body, name, lifted, extras)), + }, + Term::If { cond, then, else_ } => Term::If { + cond: Box::new(subst_call_with_extras(cond, name, lifted, extras)), + then: Box::new(subst_call_with_extras(then, name, lifted, extras)), + else_: Box::new(subst_call_with_extras(else_, name, lifted, extras)), + }, + Term::Do { op, args, tail } => Term::Do { + op: op.clone(), + args: args + .iter() + .map(|a| subst_call_with_extras(a, name, lifted, extras)) + .collect(), + tail: *tail, + }, + Term::Ctor { type_name, ctor, args } => Term::Ctor { + type_name: type_name.clone(), + ctor: ctor.clone(), + args: args + .iter() + .map(|a| subst_call_with_extras(a, name, lifted, extras)) + .collect(), + }, + Term::Match { scrutinee, arms } => Term::Match { + scrutinee: Box::new(subst_call_with_extras(scrutinee, name, lifted, extras)), + arms: arms + .iter() + .map(|a| Arm { + pat: a.pat.clone(), + body: subst_call_with_extras(&a.body, name, lifted, extras), + }) + .collect(), + }, + Term::Lam { + params, + param_tys, + ret_ty, + effects, + body, + } => Term::Lam { + params: params.clone(), + param_tys: param_tys.clone(), + ret_ty: ret_ty.clone(), + effects: effects.clone(), + body: Box::new(subst_call_with_extras(body, name, lifted, extras)), + }, + Term::Seq { lhs, rhs } => Term::Seq { + lhs: Box::new(subst_call_with_extras(lhs, name, lifted, extras)), + rhs: Box::new(subst_call_with_extras(rhs, name, lifted, extras)), + }, + Term::LetRec { name: n, ty, params, body, in_term } => Term::LetRec { + name: n.clone(), + ty: ty.clone(), + params: params.clone(), + body: Box::new(subst_call_with_extras(body, name, lifted, extras)), + in_term: Box::new(subst_call_with_extras(in_term, name, lifted, extras)), + }, + } +} + +/// Iter 16b.2: returns `Some(t)` if `t` contains a `Term::Var { +/// name }` reference in a position that is **not** the callee of a +/// `Term::App`. Returns `None` if every reference is in callee +/// position. Used by the LetRec lifter to enforce the "direct-call +/// only" restriction in 16b.2. +fn find_non_callee_use(t: &Term, name: &str) -> Option { + match t { + Term::Lit { .. } => None, + Term::Var { name: n } if n == name => Some(t.clone()), + Term::Var { .. } => None, + Term::App { callee, args, .. } => { + // Allowed: callee = Var{name}. Args are checked normally. + // Disallowed: callee != Var{name} but recursing into the + // callee surfaces the name as a non-callee position. + if !matches!(callee.as_ref(), Term::Var { name: n } if n == name) { + if let Some(v) = find_non_callee_use(callee, name) { + return Some(v); + } + } + for a in args { + if let Some(v) = find_non_callee_use(a, name) { + return Some(v); + } + } + None + } + Term::Let { value, body, .. } => { + find_non_callee_use(value, name).or_else(|| find_non_callee_use(body, name)) + } + Term::If { cond, then, else_ } => find_non_callee_use(cond, name) + .or_else(|| find_non_callee_use(then, name)) + .or_else(|| find_non_callee_use(else_, name)), + Term::Do { args, .. } => args.iter().find_map(|a| find_non_callee_use(a, name)), + Term::Ctor { args, .. } => args.iter().find_map(|a| find_non_callee_use(a, name)), + Term::Match { scrutinee, arms } => find_non_callee_use(scrutinee, name) + .or_else(|| arms.iter().find_map(|a| find_non_callee_use(&a.body, name))), + Term::Lam { body, .. } => find_non_callee_use(body, name), + Term::Seq { lhs, rhs } => { + find_non_callee_use(lhs, name).or_else(|| find_non_callee_use(rhs, name)) + } + Term::LetRec { body, in_term, .. } => find_non_callee_use(body, name) + .or_else(|| find_non_callee_use(in_term, name)), + } +} + #[cfg(test)] mod tests { use super::*; @@ -1103,25 +1441,30 @@ mod tests { } } - /// Iter 16b.1: a LetRec whose body references a var bound in the - /// enclosing scope (here, `outer` is a parameter of the - /// surrounding fn) panics at desugar time. 16b.2 will lift this. + /// Iter 16b.2: a LetRec whose body captures a fn-param of the + /// enclosing scope (here, `outer` is a parameter of `main`) is + /// **lifted** with the capture appended to the lifted fn's + /// signature. The original 16b.1 panic ("would capture") is + /// gone for fn-param captures; this test was renamed and + /// repurposed to assert the lift succeeds and produces the + /// expected augmented signature + call-site rewrite. #[test] - #[should_panic(expected = "would capture")] - fn let_rec_with_capture_panics() { + fn let_rec_capture_fn_param_lifts_with_extra_arg() { let m = Module { schema: crate::SCHEMA.to_string(), name: "t".into(), imports: vec![], defs: vec![Def::Fn(FnDef { - name: "main".into(), + name: "outer".into(), ty: Type::Fn { params: vec![Type::int()], ret: Box::new(Type::int()), effects: vec![], }, - params: vec!["outer".into()], - // (let-rec helper (params x) ... (body (app + x outer)) ...) + params: vec!["n".into()], + // (let-rec helper (params x) (type Int -> Int) + // (body (app + x n)) -- captures `n` + // (in (app helper 5))) body: Term::LetRec { name: "helper".into(), ty: Type::Fn { @@ -1134,19 +1477,188 @@ mod tests { callee: Box::new(Term::Var { name: "+".into() }), args: vec![ Term::Var { name: "x".into() }, - Term::Var { name: "outer".into() }, + Term::Var { name: "n".into() }, ], tail: false, }), in_term: Box::new(Term::App { callee: Box::new(Term::Var { name: "helper".into() }), - args: vec![Term::Lit { lit: Literal::Int { value: 1 } }], + args: vec![Term::Lit { lit: Literal::Int { value: 5 } }], tail: false, }), }, doc: None, })], }; + let out = desugar_module(&m); + // (a) two defs: original outer + lifted helper. + assert_eq!(out.defs.len(), 2, "expected one lifted fn appended"); + let lifted = match &out.defs[1] { + Def::Fn(f) => f, + _ => panic!("expected lifted FnDef"), + }; + // (b) lifted ty has the capture type appended. + assert_eq!( + lifted.ty, + Type::Fn { + params: vec![Type::int(), Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + "lifted fn type should have capture appended; got {:?}", + lifted.ty + ); + // (b') param-name list has the capture name appended. + assert_eq!(lifted.params, vec!["x".to_string(), "n".to_string()]); + // (c) the lifted body is `(app + x n)` — `n` is now a + // fn-param of the lifted def, so the body is unchanged. + match &lifted.body { + Term::App { callee, args, .. } => { + match callee.as_ref() { + Term::Var { name } => assert_eq!(name, "+"), + other => panic!("expected `+` callee, got {other:?}"), + } + assert_eq!(args.len(), 2); + match &args[0] { + Term::Var { name } => assert_eq!(name, "x"), + other => panic!("expected x, got {other:?}"), + } + match &args[1] { + Term::Var { name } => assert_eq!(name, "n"), + other => panic!("expected n, got {other:?}"), + } + } + other => panic!("expected lifted body to be App, got {other:?}"), + } + // (d) `outer`'s body is now `(app helper$lr_0 5 n)` — + // call-site got the capture appended. + let outer_body = match &out.defs[0] { + Def::Fn(f) => &f.body, + _ => unreachable!(), + }; + match outer_body { + Term::App { callee, args, .. } => { + match callee.as_ref() { + Term::Var { name } => assert_eq!(name, &lifted.name), + other => panic!("expected lifted callee, got {other:?}"), + } + assert_eq!(args.len(), 2, "expected 2 args (1 original + 1 capture)"); + match &args[0] { + Term::Lit { lit: Literal::Int { value: 5 } } => {} + other => panic!("expected 5, got {other:?}"), + } + match &args[1] { + Term::Var { name } => assert_eq!(name, "n"), + other => panic!("expected n, got {other:?}"), + } + } + other => panic!("expected outer body to be App, got {other:?}"), + } + } + + /// Iter 16b.2: a LetRec whose body captures a `Term::Let`-bound + /// name has no statically-known type at desugar time; the + /// lifter rejects with a `16b.3` pointer. + #[test] + #[should_panic(expected = "16b.3")] + fn let_rec_capture_let_binding_panics() { + // (let y 7 in (let-rec helper (params x) ... (body (app + x y)) + // (in (app helper 1)))) + let letrec = Term::LetRec { + name: "helper".into(), + ty: Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec!["x".into()], + body: Box::new(Term::App { + callee: Box::new(Term::Var { name: "+".into() }), + args: vec![ + Term::Var { name: "x".into() }, + Term::Var { name: "y".into() }, + ], + tail: false, + }), + in_term: Box::new(Term::App { + callee: Box::new(Term::Var { name: "helper".into() }), + args: vec![Term::Lit { lit: Literal::Int { value: 1 } }], + tail: false, + }), + }; + let m = Module { + schema: crate::SCHEMA.to_string(), + name: "t".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: "main".into(), + ty: Type::Fn { + params: vec![], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec![], + body: Term::Let { + name: "y".into(), + value: Box::new(Term::Lit { lit: Literal::Int { value: 7 } }), + body: Box::new(letrec), + }, + doc: None, + })], + }; + let _ = desugar_module(&m); + } + + /// Iter 16b.2: if the LetRec name is used as a value (not as + /// the callee of an `app`), the lifter rejects with a `16b.5` + /// pointer (closure conversion). Here `(let g f ...)` binds the + /// LetRec name `f` to a let-bound name `g`, which is a value + /// position — not a callee. + #[test] + #[should_panic(expected = "16b.5")] + fn let_rec_name_as_value_panics() { + // (let-rec f (params x) (type Int->Int) + // (body (let g f (app g x))) -- f used as a value + // (in (app f 1))) + let letrec = Term::LetRec { + name: "f".into(), + ty: Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec!["x".into()], + body: Box::new(Term::Let { + name: "g".into(), + value: Box::new(Term::Var { name: "f".into() }), + body: Box::new(Term::App { + callee: Box::new(Term::Var { name: "g".into() }), + args: vec![Term::Var { name: "x".into() }], + tail: false, + }), + }), + in_term: Box::new(Term::App { + callee: Box::new(Term::Var { name: "f".into() }), + args: vec![Term::Lit { lit: Literal::Int { value: 1 } }], + tail: false, + }), + }; + let m = Module { + schema: crate::SCHEMA.to_string(), + name: "t".into(), + imports: vec![], + defs: vec![Def::Fn(FnDef { + name: "main".into(), + ty: Type::Fn { + params: vec![], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec![], + body: letrec, + doc: None, + })], + }; let _ = desugar_module(&m); } diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 1b80b66..d724e10 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -3540,3 +3540,160 @@ planning only, awaiting user input on path 1 vs path 2), 16d (planning needed — pick path a vs b), 16e (`==` extension), 17a (gated). All implementation work in this session-arc is suspended at this planning checkpoint. + +## Iter 16b.2 — LetRec captures of fn-params (path-1 safe subset) + +**Goal.** Lift 16b.1's no-capture restriction for the **path-1 safe +subset** described in the 16b.2 planning entry: support a +`(let-rec ...)` whose body captures one or more names from the +enclosing scope, **provided every capture comes from a fn-param or +Lam-param** (whose types are statically declared at desugar time). +The lifted top-level fn's signature gets the capture types appended +to `params`; every call site of the LetRec name is rewritten to +pass the captures positionally as extra args. Anything outside the +safe subset is rejected at desugar time with a panic that names the +violation and points at the follow-up iter that will handle it +(16b.3 / 16b.4 / 16b.5 / 16b.6 / 16b.7). + +**Path-1 restrictions in force (rejected at desugar with a +follow-up-iter pointer).** + +- **Let-binding capture** (`Term::Let`-bound name, type unknown at + desugar). Queued for **16b.3**. +- **Match-arm pattern-binding capture** (constructor-field + substitution from the scrutinee's ADT not done at desugar). + Queued for **16b.4**. +- **Name-as-value use** (the LetRec name `f` appears anywhere + except as the callee of a `Term::App` — e.g. `(let g f ...)` or + `(app some_hof f)`). Needs closure conversion. Queued for + **16b.5**. +- **Polymorphic enclosing fn** (`Type::Forall`). Captured fn-param + types may mention outer type vars; constructing the lifted + signature's `Forall` is error-prone. Encoded as + `ScopeEntry::LetBound` for every fn-param of a `Forall`-typed + enclosing fn — caught at the same site as let-binding captures. + Queued for **16b.6**. +- **Nested LetRec mutual capture** (an inner LetRec captures the + outer LetRec's name or params). Queued for **16b.7**. + +**What shipped.** + +- `crates/ailang-core/src/desugar.rs` (1341 → 1853 LOC, +512). The + hot changes: + - New `enum ScopeEntry { KnownType(Type), LetBound, MatchArm, + EnclosingLetRec }`. The `scope` parameter threaded through + `desugar_term` and helpers became + `&BTreeMap` (was `&BTreeSet`). + Every binder ([`Term::Let`], [`Term::Lam`], [`Term::Match`] + arm, [`Term::LetRec`]) inserts the appropriate variant; + `desugar_module` seeds fn-param entries from `f.ty` (peeled + `Forall`). + - `Term::LetRec` arm rewritten end-to-end: peel `ty` to its + inner `Type::Fn` to learn the LetRec's own param types, + extend body-scope with `EnclosingLetRec` for `name` + + `KnownType(_)` for params, recurse on body and in_term, run + `free_vars_in_term` against `{name} ∪ params`, intersect + with the outer scope's keys, classify each capture's + `ScopeEntry` (KnownType → accept; everything else → panic + with the follow-up iter pointer), validate via + `find_non_callee_use` that `name` only appears as a callee, + build the augmented `Type::Fn` with capture types appended, + rewrite call sites via `subst_call_with_extras`, then + `subst_var` for any non-call references (defensive — none + survive the validator), append the lifted `FnDef`. + - Two new free helpers (~150 LOC together): + `subst_call_with_extras(t, name, lifted, extras)` rewrites + every `Term::App { callee = Var{name} }` to + `Term::App { callee = Var{lifted}, args ++ extras_as_vars }`, + walking through every variant; `find_non_callee_use(t, name)` + walks `t` and returns `Some(t)` at the first `Term::Var { + name == name }` reference in a non-callee position, `None` + otherwise. Plus `peel_forall_to_fn` (one-liner). + - The 16b.1 panic is gone for fn-param captures (replaced by + the lifter); it persists for every other capture kind, with + a sharper message. +- `crates/ail/tests/e2e.rs` (+18): `local_rec_capture_demo` — + e2e count 38 → 39. Asserts that the `local_rec_capture` fixture + prints `0\n10\n45\n`. +- `examples/local_rec_capture.ailx` + `.ail.json` (35 LOC source): + `sum_below(n)` returns the sum of integers `1 + ... + (n-1)`. + Body uses an inner `(let-rec loop (params i) ... (body ... (app + >= i n) ... (app loop (app + i 1))) (in (app loop 1)))`. The + helper captures `n` from `sum_below`'s param list; the desugar + pass lifts it to `loop$lr_0(i: Int, n: Int) -> Int` and rewrites + every `(app loop X)` to `(app loop$lr_0 X n)`. `main` drives + `sum_below` at 1, 5, 10 → outputs `0`, `10`, `45`. +- `crates/ailang-core/src/desugar.rs::tests` (3 new): + `let_rec_capture_fn_param_lifts_with_extra_arg` (positive), + `let_rec_capture_let_binding_panics` + (`#[should_panic(expected = "16b.3")]`), + `let_rec_name_as_value_panics` + (`#[should_panic(expected = "16b.5")]`). The 16b.1 + `let_rec_with_capture_panics` test was repurposed into the + positive `let_rec_capture_fn_param_lifts_with_extra_arg`: its + fixture (a fn-param capture) is now legal and produces the + expected augmented signature. + +**The augmented-signature mechanism.** Given +`(let-rec f (params p1..pk) (type Fn(t1..tk) -> tr) (body B) (in I))` +inside a fn whose scope contains +`{c1: T1, ..., cm: Tm}` (KnownType entries) used as free vars in +`B`: + +- Lifted signature: `f$lr_N : Fn(t1..tk, T1..Tm) -> tr` with the + same `effects` set as the original. +- Lifted param-name list: `p1..pk, c1..cm` (capture names appended + unchanged so the lifted body's references resolve directly). +- Body rewrite: every `(app f a1..an)` in `B` → `(app f$lr_N + a1..an c1..cm)`. The `c1..cm` are `Term::Var` references that + resolve, in the lifted body, to the appended params with the + same names. Free uses of `f` in non-callee position are + pre-rejected by `find_non_callee_use`. +- In-term rewrite: every `(app f a1..an)` in `I` → `(app f$lr_N + a1..an c1..cm)`. The `c1..cm` are `Term::Var` references that + resolve, in the in-term's enclosing fn, to the captured names + themselves (still in scope). + +The rewrite is order-sensitive: `subst_call_with_extras` runs +**before** `subst_var`, so a recursive self-call inside `B` first +becomes `(app f$lr_N ... c1..cm)`, then any leftover bare `Var{f}` +(none in 16b.2 — pre-rejected) gets renamed to `Var{f$lr_N}`. The +second pass is defensive. + +**Tests: 102 → 106 (+4).** + +- e2e: 38 → 39 (`local_rec_capture_demo`). +- `ailang-core::desugar::tests`: 6 → 9. Net +3 because the + 16b.1-era `let_rec_with_capture_panics` test was repurposed + rather than removed (its fn-param-capture fixture is now a + positive lift), and two pure-negative tests were added. +- All other crates unchanged. + +**Cumulative state, post-16b.2.** + +- Stdlib unchanged (5 modules, 29 combinators). +- `Term` enum: 11 variants (unchanged; LetRec is still + desugar-eliminated, no schema impact). All pre-16b.2 fixtures + hash bit-identically. +- 16a desugar pass now does three jobs: nested-ctor-pattern + flattening (16a), literal-pattern lowering (16c), and LetRec + lift (16b.1 → 16b.2 path-1). Single AST→AST hop between + `load_module` and typecheck. +- The `unreachable!("Term::LetRec eliminated by desugar")` arms + in `ailang-check` × 2 and `ailang-codegen` × 4 remain correct + — every LetRec is still gone before either stage runs. + +**Queue update post-16b.2 path-1.** 16b.2 path-1 done. Open: +**16b.3** (LetRec captures of `Term::Let`-bound names — would +need a post-typecheck re-run of the lift, or a small inference +on the let-value's type), **16b.4** (LetRec captures of match-arm +pattern bindings — needs ADT-def lookup + constructor-field +substitution), **16b.5** (closure conversion — lifts the +"name-as-value-only" restriction for both LetRec and Lam), +**16b.6** (LetRec inside a `Type::Forall`-quantified fn — needs +synthesised `Forall` for the lifted signature), **16b.7** +(nested LetRec mutual capture — generalised lifting that +accumulates captures across nesting). 16d (chain-machinery +exhaustiveness or `__unreachable__` — planning needed), 16e +(`==` extension to Bool/Str/Unit), 17a (per-fn arena, gated) +unchanged. diff --git a/examples/local_rec_capture.ail.json b/examples/local_rec_capture.ail.json new file mode 100644 index 0000000..0fdb095 --- /dev/null +++ b/examples/local_rec_capture.ail.json @@ -0,0 +1 @@ +{"defs":[{"body":{"body":{"cond":{"args":[{"name":"i","t":"var"},{"name":"n","t":"var"}],"fn":{"name":">=","t":"var"},"t":"app"},"else":{"args":[{"name":"i","t":"var"},{"args":[{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"fn":{"name":"loop","t":"var"},"t":"app"}],"fn":{"name":"+","t":"var"},"t":"app"},"t":"if","then":{"lit":{"kind":"int","value":0},"t":"lit"}},"in":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"loop","t":"var"},"t":"app"},"name":"loop","params":["i"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},"doc":"Sum 1 + 2 + ... + (n-1). Helper captures n from the enclosing scope.","kind":"fn","name":"sum_below","params":["n"],"type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"}],"fn":{"name":"sum_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"doc":"Drive sum_below at 1, 5, 10. Expected (per line): 0, 10, 45.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"local_rec_capture","schema":"ailang/v0"} diff --git a/examples/local_rec_capture.ailx b/examples/local_rec_capture.ailx new file mode 100644 index 0000000..e4c17d6 --- /dev/null +++ b/examples/local_rec_capture.ailx @@ -0,0 +1,35 @@ +; Iter 16b.2 — LetRec captures of fn-params (path-1 safe subset). +; `sum_below(n)` returns the sum of integers from 1 up to but not +; including n. The recursive helper `loop` captures the upper +; bound `n` from `sum_below`'s param list and recurses on its own +; counter `i`. The 16b.2 desugar pass lifts `loop` to a synthetic +; top-level fn `loop$lr_0(i: Int, n: Int) -> Int` (capture appended) +; and rewrites every `(app loop ARGS)` to `(app loop$lr_0 ARGS n)`. +; +; Expected stdout (one per line): 0 (sum below 1), 10 (1+2+3+4), +; 45 (1+2+...+9). + +(module local_rec_capture + + (fn sum_below + (doc "Sum 1 + 2 + ... + (n-1). Helper captures n from the enclosing scope.") + (type (fn-type (params (con Int)) (ret (con Int)))) + (params n) + (body + (let-rec loop + (params i) + (type (fn-type (params (con Int)) (ret (con Int)))) + (body + (if (app >= i n) + 0 + (app + i (app loop (app + i 1))))) + (in (app loop 1))))) + + (fn main + (doc "Drive sum_below at 1, 5, 10. Expected (per line): 0, 10, 45.") + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (do io/print_int (app sum_below 1)) + (seq (do io/print_int (app sum_below 5)) + (do io/print_int (app sum_below 10)))))))