From c0668178bbe80c99975f914635914bce0927ad03 Mon Sep 17 00:00:00 2001 From: Brummel Date: Thu, 7 May 2026 22:16:12 +0200 Subject: [PATCH] Iter 16b.4: LetRec captures of match-arm pattern bindings MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Flips the desugar's MatchArm-capture rejection from panic to defer. The 16b.3 lift_letrecs pass already handled match-arm bindings via type_check_pattern_for_lift (Pattern::Var, Pattern::Ctor with sub- patterns, ctor-field substitution against scrutinee args), so this iter is a single-line classification change in desugar plus the fixture and tests that exercise it. - desugar.rs: MatchArm classification now defers (same arm as LetBound); EnclosingLetRec panic remains for 16b.7. - examples/local_rec_match_capture.{ailx,ail.json}: enclosing fn pattern-matches on Pair, inner LetRec captures both match-arm bindings simultaneously. Lifts to loop$lr_0(i: Int, threshold: Int, n: Int) -> Int. - e2e + check + desugar tests: 110 → 113 (+3). First fixture lifting more than one capture; subst_call_with_extras already handled it generically. Co-Authored-By: Claude Opus 4.7 (1M context) --- crates/ail/tests/e2e.rs | 20 +++ crates/ailang-check/src/lib.rs | 116 +++++++++++++ crates/ailang-core/src/desugar.rs | 197 ++++++++++++++++++---- docs/JOURNAL.md | 118 +++++++++++++ examples/local_rec_match_capture.ail.json | 1 + examples/local_rec_match_capture.ailx | 59 +++++++ 6 files changed, 478 insertions(+), 33 deletions(-) create mode 100644 examples/local_rec_match_capture.ail.json create mode 100644 examples/local_rec_match_capture.ailx diff --git a/crates/ail/tests/e2e.rs b/crates/ail/tests/e2e.rs index d70755e..e99b3ea 100644 --- a/crates/ail/tests/e2e.rs +++ b/crates/ail/tests/e2e.rs @@ -485,6 +485,26 @@ fn local_rec_let_capture_demo() { assert_eq!(lines, vec!["0", "5", "9"]); } +/// Iter 16b.4: LetRec capture of a Match-arm pattern binding. +/// Property protected: the desugar pass leaves a LetRec whose +/// captures are `Pattern::Ctor`-Var-bound (here `threshold` and +/// `n`, both fields of `MkPair` in `Pair Int Int`) in place; the +/// post-typecheck `lift_letrecs` pass walks the enclosing +/// `Term::Match` arm, calls `type_check_pattern_for_lift` to +/// substitute the matched ADT's type args (`[Int, Int]`) into +/// `MkPair`'s declared field types, and lifts to a synthetic +/// top-level fn `loop$lr_0(i: Int, threshold: Int, n: Int) -> +/// Int`, rewriting every call site. Without 16b.4, the 16b.3-era +/// panic ("16b.4 — match-arm captures") would fire. +/// count_below(MkPair 10 0)=0, count_below(MkPair 10 5)=5, +/// count_below(MkPair 10 15)=9. +#[test] +fn local_rec_match_capture_demo() { + let stdout = build_and_run("local_rec_match_capture.ail.json"); + let lines: Vec<&str> = stdout.lines().collect(); + assert_eq!(lines, vec!["0", "5", "9"]); +} + /// 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-check/src/lib.rs b/crates/ailang-check/src/lib.rs index 609d623..f805399 100644 --- a/crates/ailang-check/src/lib.rs +++ b/crates/ailang-check/src/lib.rs @@ -3278,4 +3278,120 @@ mod tests { other => panic!("expected App after Let, got {other:?}"), } } + + /// Iter 16b.4: a LetRec whose body captures a `Pattern::Ctor`-Var + /// match-arm binding is lifted by `lift_letrecs` to a synthetic + /// top-level fn whose signature has the binding's type appended. + /// Property protected: `type_check_pattern_for_lift` substitutes + /// the matched ADT's type args (`[Int, Int]`) into the ctor's + /// declared field types (`[a, b]`) and returns `[(x, Int), + /// (y, Int)]`; the lifted fn picks up `x: Int` as the capture + /// type. Without 16b.4, the desugar pass would have panicked + /// before reaching `lift_letrecs`. + #[test] + fn lift_letrecs_on_match_arm_capture_produces_synthetic_fn() { + // (data Pair (vars a b) (ctor MkPair a b)) + // (fn outer : (Pair Int Int) -> Int = \p. + // match p + // case (pat-ctor MkPair x y) -> + // let-rec helper : (Int) -> Int = \z. + z x + // in (app helper 0)) + let pair_td = TypeDef { + name: "Pair".into(), + vars: vec!["a".into(), "b".into()], + ctors: vec![Ctor { + name: "MkPair".into(), + fields: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "b".into() }, + ], + }], + doc: None, + }; + let letrec = Term::LetRec { + name: "helper".into(), + ty: Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec!["z".into()], + body: Box::new(Term::App { + callee: Box::new(Term::Var { name: "+".into() }), + args: vec![ + Term::Var { name: "z".into() }, + Term::Var { name: "x".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: 0 } }], + tail: false, + }), + }; + let outer_body = Term::Match { + scrutinee: Box::new(Term::Var { name: "p".into() }), + arms: vec![Arm { + pat: Pattern::Ctor { + ctor: "MkPair".into(), + fields: vec![ + Pattern::Var { name: "x".into() }, + Pattern::Var { name: "y".into() }, + ], + }, + body: letrec, + }], + }; + let m = Module { + schema: SCHEMA.into(), + name: "t".into(), + imports: vec![], + defs: vec![ + Def::Type(pair_td), + fn_def( + "outer", + Type::Fn { + params: vec![Type::Con { + name: "Pair".into(), + args: vec![Type::int(), Type::int()], + }], + ret: Box::new(Type::int()), + effects: vec![], + }, + vec!["p"], + outer_body, + ), + ], + }; + // Typecheck must succeed. + check(&m).expect("typecheck before lift"); + let desugared = ailang_core::desugar::desugar_module(&m); + // Match-arm capture: desugar leaves the LetRec in place. + let lifted = lift_letrecs(&desugared).expect("lift_letrecs"); + // Pair (Type) + outer (Fn) + helper$lr_0 (Fn) = 3. + assert_eq!(lifted.defs.len(), 3, "expected one synthetic fn appended"); + let synth = match &lifted.defs[2] { + Def::Fn(f) => f, + _ => panic!("expected synthetic FnDef at index 2"), + }; + assert!( + synth.name.starts_with("helper$lr_"), + "lifted name `{}` should start with `helper$lr_`", + synth.name + ); + // Lifted ty: original (Int) -> Int with capture type Int + // appended → (Int, Int) -> Int. + assert_eq!( + synth.ty, + Type::Fn { + params: vec![Type::int(), Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + "lifted ty should have the match-arm-capture type Int appended; got {:?}", + synth.ty + ); + assert_eq!(synth.params, vec!["z".to_string(), "x".to_string()]); + } } diff --git a/crates/ailang-core/src/desugar.rs b/crates/ailang-core/src/desugar.rs index 6728ba8..a8ed234 100644 --- a/crates/ailang-core/src/desugar.rs +++ b/crates/ailang-core/src/desugar.rs @@ -121,9 +121,14 @@ enum ScopeEntry { /// 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. + /// Bound by a `Term::Match` arm pattern — type requires + /// constructor-field substitution from the scrutinee. The + /// desugar pass cannot resolve it (the scrutinee's type may + /// only be known after inference); captures of this kind are + /// deferred to `ailang-check::lift_letrecs` (Iter 16b.4), + /// which uses `type_check_pattern_for_lift` to substitute the + /// scrutinee's type args into the matched ctor's declared + /// field types and extend the locals scope accordingly. MatchArm, /// Bound by a `Term::LetRec` (its own name) — fn-typed, but /// the value flows through a recursive position; supported @@ -378,9 +383,11 @@ impl Desugarer { /// `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. + /// the LetRec lifter to decide between (a) the 16b.2 fast path + /// (all KnownType captures → lift here), (b) the 16b.3/16b.4 + /// defer path (any LetBound or MatchArm capture → leave the + /// LetRec in place for `ailang-check::lift_letrecs`), and (c) + /// the 16b.7 panic path (EnclosingLetRec capture). fn desugar_term(&mut self, t: &Term, scope: &BTreeMap) -> Term { match t { Term::Lit { .. } | Term::Var { .. } => t.clone(), @@ -470,14 +477,21 @@ impl Desugarer { // desugared. A post-typecheck pass (`lift_letrecs` in // `ailang-check`) walks every surviving LetRec and lifts // it using the typechecker's resolved types. + // Iter 16b.4: extends the defer path to `MatchArm` + // captures. The post-typecheck pass already walks + // `Term::Match` arms and (since 16b.3) calls + // `type_check_pattern_for_lift` to extend locals with + // pattern bindings — that machinery resolves Match-arm + // capture types via constructor-field substitution + // against the matched ctor's declared field types. // // 16b.2's fast path (KnownType-only captures → lift here) - // STILL fires when applicable. Only when at least one - // capture is `LetBound` does the desugar defer. + // STILL fires when applicable. Any `LetBound` or + // `MatchArm` capture forces the all-or-nothing defer + // path. // - // `MatchArm` and `EnclosingLetRec` captures STILL panic - // (16b.4 / 16b.7 — separate iters needing extra - // machinery beyond what `lift_letrecs` does). + // `EnclosingLetRec` captures STILL panic (16b.7 — + // nested mutual recursion needs separate machinery). // // The non-callee-use check (16b.5 violation) runs FIRST // so the diagnostic fires consistently regardless of @@ -553,30 +567,36 @@ impl Desugarer { .cloned() .collect(); - // 16b.3: classify each capture's ScopeEntry. - // - All KnownType → lift here (16b.2 fast path). - // - Any LetBound → defer to `lift_letrecs` (16b.3). - // - Any MatchArm → panic (16b.4). + // 16b.4: classify each capture's ScopeEntry. + // - All KnownType → lift here (16b.2 fast path). + // - Any LetBound → defer to `lift_letrecs` (16b.3). + // - Any MatchArm → defer to `lift_letrecs` (16b.4). + // The post-typecheck pass resolves the binding's type + // from the enclosing match's scrutinee type, with + // constructor-field substitution against the matched + // ctor's declared field types. // - Any EnclosingLetRec → panic (16b.7). - // Mixed KnownType+LetBound get deferred (decision is - // all-or-nothing for a single LetRec; the - // post-typecheck pass handles every capture kind it - // supports uniformly). - let mut has_let_bound = false; + // Mixed KnownType + (LetBound | MatchArm) get deferred: + // any non-KnownType capture forces the all-or-nothing + // defer path. The post-typecheck pass handles every + // supported capture kind uniformly. + let mut needs_defer = false; for c in &captures { match scope.get(c).expect("capture-in-scope-by-construction") { ScopeEntry::KnownType(_) => {} ScopeEntry::LetBound => { - has_let_bound = true; + needs_defer = true; + } + ScopeEntry::MatchArm => { + // 16b.4: defer instead of panic. `lift_letrecs` + // resolves the type via `type_check_pattern_for_lift` + // (added in 16b.3) which already substitutes the + // matched ADT's type args into the ctor's + // declared field types. + needs_defer = true; } - ScopeEntry::MatchArm => panic!( - "Iter 16b.3: 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.3: LetRec `{}` captures `{}` from an enclosing \ + "Iter 16b.4: LetRec `{}` captures `{}` from an enclosing \ LetRec; nested mutual-capture is not supported. Queued for \ 16b.7.", name, c @@ -584,11 +604,12 @@ impl Desugarer { } } - // 16b.3: defer-arm. At least one capture is LetBound, so - // we can't resolve the lifted signature here. Reconstruct - // the LetRec with desugared sub-terms and let - // `ailang-check::lift_letrecs` handle it after typecheck. - if has_let_bound { + // 16b.3/16b.4: defer-arm. At least one capture is LetBound + // or MatchArm-bound, so we can't resolve the lifted + // signature here. Reconstruct the LetRec with desugared + // sub-terms and let `ailang-check::lift_letrecs` handle + // it after typecheck. + if needs_defer { return Term::LetRec { name: name.clone(), ty: ty.clone(), @@ -1687,6 +1708,116 @@ mod tests { ); } + /// Iter 16b.4: a LetRec whose body captures a name bound by a + /// `Pattern::Ctor` Var sub-pattern (a `ScopeEntry::MatchArm` + /// binding) is no longer rejected at desugar time. The desugar + /// pass leaves the LetRec in place (with body and in_term + /// recursively desugared) so the post-typecheck pass in + /// `ailang-check` can lift it using the typechecker's resolved + /// types — including constructor-field substitution against + /// the matched ADT's type args. The 16b.3-era panic for this + /// shape is gone. + #[test] + fn let_rec_capture_match_arm_is_deferred_to_post_typecheck() { + // Module-level scope: + // (data Pair (vars a b) (ctor MkPair a b)) + // (fn outer : (Pair Int Int) -> Int = \p. + // match p + // case (pat-ctor MkPair x y) -> + // let-rec helper : (Int) -> Int = \z. (+ z x) + // in (app helper 0) + // ) + let pair_td = TypeDef { + name: "Pair".into(), + vars: vec!["a".into(), "b".into()], + ctors: vec![Ctor { + name: "MkPair".into(), + fields: vec![ + Type::Var { name: "a".into() }, + Type::Var { name: "b".into() }, + ], + }], + doc: None, + }; + let letrec = Term::LetRec { + name: "helper".into(), + ty: Type::Fn { + params: vec![Type::int()], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec!["z".into()], + body: Box::new(Term::App { + callee: Box::new(Term::Var { name: "+".into() }), + args: vec![ + Term::Var { name: "z".into() }, + Term::Var { name: "x".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: 0 } }], + tail: false, + }), + }; + let outer_body = Term::Match { + scrutinee: Box::new(Term::Var { name: "p".into() }), + arms: vec![Arm { + pat: Pattern::Ctor { + ctor: "MkPair".into(), + fields: vec![ + Pattern::Var { name: "x".into() }, + Pattern::Var { name: "y".into() }, + ], + }, + body: letrec, + }], + }; + let m = Module { + schema: crate::SCHEMA.to_string(), + name: "t".into(), + imports: vec![], + defs: vec![ + Def::Type(pair_td), + Def::Fn(FnDef { + name: "outer".into(), + ty: Type::Fn { + params: vec![Type::Con { + name: "Pair".into(), + args: vec![Type::int(), Type::int()], + }], + ret: Box::new(Type::int()), + effects: vec![], + }, + params: vec!["p".into()], + body: outer_body, + doc: None, + }), + ], + }; + let out = desugar_module(&m); + // No fn was lifted (the LetRec is deferred) — the module's + // defs count is unchanged at 2 (Pair + outer). + assert_eq!( + out.defs.len(), + 2, + "expected no lifted fn (LetRec deferred); got {:?}", + out.defs.iter().map(|d| d.name()).collect::>() + ); + // The original LetRec must STILL be present somewhere in + // outer's body (after match desugar — the match arm has only + // `Var` sub-patterns so it stays flat and the body is reachable). + let outer_body_out = match &out.defs[1] { + Def::Fn(f) => &f.body, + _ => unreachable!(), + }; + assert!( + any_let_rec(outer_body_out), + "expected Term::LetRec to still be present in body; got {outer_body_out:#?}" + ); + } + /// 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 diff --git a/docs/JOURNAL.md b/docs/JOURNAL.md index 6330b4f..5a6e523 100644 --- a/docs/JOURNAL.md +++ b/docs/JOURNAL.md @@ -3887,3 +3887,121 @@ the post-order traversal in `lift_letrecs` but the mutual case is genuinely harder). 16d (chain-machinery exhaustiveness or `__unreachable__`), 16e (`==` extension to Bool/Str/Unit), 17a (per-fn arena, gated) unchanged. + +## Iter 16b.4 — LetRec captures of match-arm pattern bindings + +**Goal.** Lift the 16b.3-era "match-arm capture rejected" panic. A +`(let-rec ...)` whose body captures a name bound by a `Term::Match` +arm pattern (a `Pattern::Var`, or a `Pattern::Var` sub-pattern of +a `Pattern::Ctor`) is now legal. Same architectural path as 16b.3: +desugar defers it; `lift_letrecs` resolves the capture's type from +the enclosing match's scrutinee type, applying constructor-field +substitution against the matched ctor's declared field types. + +**What changed in desugar.** Exactly one classification arm. The +LetRec capture loop used to treat `ScopeEntry::MatchArm` as a hard +panic (queued for 16b.4); it now sets `needs_defer = true` and +falls through to the same defer-arm 16b.3 wrote for `LetBound`. +The `has_let_bound` boolean was renamed to `needs_defer` so it +covers both LetBound and MatchArm captures uniformly. Mixed scopes +(some KnownType + some MatchArm, or some MatchArm + some LetBound) +defer just like the 16b.3 mixed case — the all-or-nothing decision +is preserved. `EnclosingLetRec` still panics (queued for 16b.7). +Total desugar diff: ~25 LOC of comment/classification changes; no +new helpers, no new traversals. + +**What `lift_letrecs` already supported.** The post-typecheck pass +needed **zero** code changes. 16b.3's `type_check_pattern_for_lift` +was already written to handle the full pattern grammar: + +- `Pattern::Wild` / `Pattern::Lit`: bind nothing (no-op). +- `Pattern::Var`: binds the entire scrutinee's type. +- `Pattern::Ctor`: looks up the ADT in `env.types` (or + `env.module_types` for a qualified `module.Type`), validates ctor + arity, builds the type-var → arg substitution from + `td.vars` zip `s_ty.args`, applies it to each `cdef.fields[i]`, + and recurses on each sub-pattern with the substituted field + type. The recursion handles arbitrarily-nested Ctor patterns + for free (though desugar's 16a flattening means lift_letrecs + rarely sees deeply-nested ctor patterns in practice). + +The only reason 16b.3 left the MatchArm path under a `panic!` was +to keep 16b.3's scope tight — the machinery for resolving the +type was already in place and exercised by 16b.3's own test +suite, just gated behind the desugar panic. + +**The fixture: `examples/local_rec_match_capture.ailx` (+ `.ail.json`).** +Defines `data Pair (vars a b) (ctor MkPair a b)`. `count_below(p)` +takes a `Pair Int Int` (threshold, n), pattern-matches with +`(pat-ctor MkPair threshold n)` (so `threshold` and `n` are both +match-arm bindings of type `Int` — the ADT's `[a, b]` ctor fields +substituted against the scrutinee's `[Int, Int]` type args), and +inside that arm runs a recursive `loop` that captures BOTH +match-arm bindings to count integers in `1..=n` strictly less than +`threshold`. The lift produces a synthetic top-level fn +`loop$lr_0(i: Int, threshold: Int, n: Int) -> Int` and rewrites +every `(app loop ARGS)` in the arm body to +`(app loop$lr_0 ARGS threshold n)`. Drives at `MkPair 10 0`, +`MkPair 10 5`, `MkPair 10 15` → output `0\n5\n9\n` (the same +numbers as the 16b.3 fixture so the comparison is direct). + +The fixture exercises the full 16b.4 chain: parameterised ADT +construction, match on the ctor, two simultaneous match-arm +captures (not just one), and `lift_letrecs` resolving both via +constructor-field substitution. + +**What this iter exercises that 16b.3 did not.** + +- The MatchArm branch of `type_check_pattern_for_lift` (was + unreachable in real programs because desugar always panicked + before the lift saw such captures; covered by the 16b.3 test + suite synthetically but never end-to-end). +- Multi-capture LetRec (16b.2 used a single fn-param capture; + 16b.3 used a single Let-capture; this is the first fixture with + two captures appended in the lifted signature, in a fixed + order driven by the BTreeSet's deterministic iteration). +- Constructor-field substitution at the lift site (the type args + of the scrutinee type `Pair Int Int` flow into the synthetic + fn's signature via the substitution map). + +**Tests: 113 → 116 (+3).** + +- e2e: 40 → 41 (`local_rec_match_capture_demo`, asserts the + `0/5/9` stdout from the new fixture). +- `ailang-check::tests`: 27 → 28 + (`lift_letrecs_on_match_arm_capture_produces_synthetic_fn`: + builds a Pair-using module, asserts the lifted FnDef's name + starts with `helper$lr_`, params are `[z, x]`, and the type is + `(Int, Int) -> Int`). +- `ailang-core::desugar::tests`: 9 → 10 + (`let_rec_capture_match_arm_is_deferred_to_post_typecheck`: + asserts no fn was lifted at desugar time and a Term::LetRec + still survives in the outer body for the post-typecheck pass). + +**Cumulative state, post-16b.4.** + +- Stdlib unchanged (5 modules, 29 combinators). +- `Term` enum: 11 variants (unchanged). All pre-16b.4 fixture + hashes bit-identical (verified via `ail manifest` on the four + prior LetRec/lit_pat fixtures: hashes match pre-16b.4 values). +- Compiler stages: load → desugar → typecheck → lift_letrecs → + codegen (unchanged from 16b.3). +- The `unreachable!` arms in `ailang-codegen` and the typing rule + in `ailang-check` are unchanged. +- Compiler bugs surfaced and fixed in dogfood since 14a: 5/5 + (unchanged). + +**Queue update post-16b.4.** 16b.4 done. Open: **16b.5** (closure +conversion — lifts the "name-as-value-only" restriction for both +LetRec and Lam; needs ABI-level work, out of scope for the 16b.x +sweep that's been about scope-of-capture restrictions only), +**16b.6** (LetRec inside a `Type::Forall`-quantified fn — needs a +synthesised `Forall` for the lifted signature plus rigid-var +threading; the `lift_letrecs` panic at the Forall-LetRec arm is +the entry point), **16b.7** (nested LetRec mutual capture — +generalised lifting that accumulates captures across nesting; +the post-order traversal in `lift_letrecs` already handles the +strictly-nested non-mutual case but the mutual case needs joint +lifting). 16d (chain-machinery exhaustiveness or +`__unreachable__`), 16e (`==` extension to Bool/Str/Unit), +17a (per-fn arena, gated) unchanged. diff --git a/examples/local_rec_match_capture.ail.json b/examples/local_rec_match_capture.ail.json new file mode 100644 index 0000000..fceab04 --- /dev/null +++ b/examples/local_rec_match_capture.ail.json @@ -0,0 +1 @@ +{"defs":[{"ctors":[{"fields":[{"k":"var","name":"a"},{"k":"var","name":"b"}],"name":"MkPair"}],"kind":"type","name":"Pair","vars":["a","b"]},{"body":{"arms":[{"body":{"body":{"cond":{"args":[{"name":"i","t":"var"},{"name":"n","t":"var"}],"fn":{"name":">","t":"var"},"t":"app"},"else":{"cond":{"args":[{"name":"i","t":"var"},{"name":"threshold","t":"var"}],"fn":{"name":"<","t":"var"},"t":"app"},"else":{"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"},"t":"if","then":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"},{"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"}}},"pat":{"ctor":"MkPair","fields":[{"name":"threshold","p":"var"},{"name":"n","p":"var"}],"p":"ctor"}}],"scrutinee":{"name":"p","t":"var"},"t":"match"},"doc":"Match-arm captures `threshold` and `n`; inner LetRec captures both.","kind":"fn","name":"count_below","params":["p"],"type":{"effects":[],"k":"fn","params":[{"args":[{"k":"con","name":"Int"},{"k":"con","name":"Int"}],"k":"con","name":"Pair"}],"ret":{"k":"con","name":"Int"}}},{"body":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"},{"lit":{"kind":"int","value":0},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"Pair"}],"fn":{"name":"count_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"},{"lit":{"kind":"int","value":5},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"Pair"}],"fn":{"name":"count_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"args":[{"lit":{"kind":"int","value":10},"t":"lit"},{"lit":{"kind":"int","value":15},"t":"lit"}],"ctor":"MkPair","t":"ctor","type":"Pair"}],"fn":{"name":"count_below","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"doc":"Drive count_below at MkPair 10 {0,5,15}. Expected: 0, 5, 9.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"local_rec_match_capture","schema":"ailang/v0"} \ No newline at end of file diff --git a/examples/local_rec_match_capture.ailx b/examples/local_rec_match_capture.ailx new file mode 100644 index 0000000..cec3593 --- /dev/null +++ b/examples/local_rec_match_capture.ailx @@ -0,0 +1,59 @@ +; Iter 16b.4 — LetRec captures of match-arm pattern bindings. +; `count_below(p)` takes a `Pair Int Int` (threshold, n), pattern- +; matches on `(MkPair threshold n)`, and inside that match arm runs +; a recursive helper `loop` that captures BOTH match-arm bindings +; (`threshold` and `n`) and counts how many integers in 1..=n are +; strictly less than `threshold`. +; +; The 16b.2/16b.3 desugar passes cannot lift this LetRec — both +; `threshold` and `n` are bound by a `Pattern::Ctor` Var sub- +; pattern (`ScopeEntry::MatchArm`). Before 16b.4 this panicked at +; desugar time. Now the desugar pass leaves the LetRec in place; +; the post-typecheck `lift_letrecs` pass walks the enclosing match, +; resolves each pattern binding's type via constructor-field +; substitution against the matched ctor's declared field types +; (here: `Pair Int Int`'s ctor `MkPair` has fields `[Int, Int]`, +; and the scrutinee's `Type::Con.args` are also `[Int, Int]`, so +; substitution is a no-op and both bindings get type `Int`), and +; lifts to `loop$lr_0(i: Int, threshold: Int, n: Int) -> Int`. +; +; The match has a single ctor and no catch-all; the chain machinery +; treats the only arm as default-dominating since there's no `_` +; arm needed for an exhaustive single-ctor ADT (Pair has one ctor). +; +; Expected stdout (one per line): +; count_below(MkPair 10 0) = 0 +; count_below(MkPair 10 5) = 5 (1..=5 all below 10) +; count_below(MkPair 10 15) = 9 (1..=9 below 10, 10..=15 not) + +(module local_rec_match_capture + + (data Pair (vars a b) + (ctor MkPair a b)) + + (fn count_below + (doc "Match-arm captures `threshold` and `n`; inner LetRec captures both.") + (type (fn-type (params (con Pair (con Int) (con Int))) (ret (con Int)))) + (params p) + (body + (match p + (case (pat-ctor MkPair threshold n) + (let-rec loop + (params i) + (type (fn-type (params (con Int)) (ret (con Int)))) + (body + (if (app > i n) + 0 + (if (app < i threshold) + (app + 1 (app loop (app + i 1))) + (app loop (app + i 1))))) + (in (app loop 1))))))) + + (fn main + (doc "Drive count_below at MkPair 10 {0,5,15}. Expected: 0, 5, 9.") + (type (fn-type (params) (ret (con Unit)) (effects IO))) + (params) + (body + (seq (do io/print_int (app count_below (term-ctor Pair MkPair 10 0))) + (seq (do io/print_int (app count_below (term-ctor Pair MkPair 10 5))) + (do io/print_int (app count_below (term-ctor Pair MkPair 10 15))))))))