Iter 16b.4: LetRec captures of match-arm pattern bindings
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<Int,Int>, 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) <noreply@anthropic.com>
This commit is contained in:
@@ -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.
|
||||
|
||||
@@ -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()]);
|
||||
}
|
||||
}
|
||||
|
||||
@@ -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<String, ScopeEntry>) -> 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::<Vec<_>>()
|
||||
);
|
||||
// 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
|
||||
|
||||
+118
@@ -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.
|
||||
|
||||
@@ -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"}
|
||||
@@ -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))))))))
|
||||
Reference in New Issue
Block a user