Iter 16b.7: nested LetRec mutual capture (params, not name)
Inner LetRec capturing outer LetRec's params now lifts cleanly via
the existing post-order traversal — outer's params are KnownType
in inner's outer-scope, so 16b.2's fast-path handles them. Inner
LetRec capturing outer's NAME remains rejected (closure-of-self
in body, deferred separately).
Plus hardening: lift.rs's deferred path tracks the outer LetRec
name in a parallel `enclosing_letrec_names` set so the symmetric
inner-captures-outer-name rejection fires there too — without it
a silent lift produced a runtime arity mismatch.
- examples/nested_let_rec.{ailx,ail.json}: outer counts down via
inner that captures the outer's threshold param.
- desugar.rs: clarified panic message for outer-name capture.
- lift.rs: enclosing_letrec_names tracking.
- e2e + desugar tests: 120 → 122 (+2).
End-of-16b series: feature-complete except for closure-of-self
in body and closure-with-polymorphism, both queued separately.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
@@ -565,6 +565,31 @@ fn poly_rec_capture_demo() {
|
||||
assert_eq!(lines, vec!["5", "false"]);
|
||||
}
|
||||
|
||||
/// Iter 16b.7: nested LetRec where the inner one captures the OUTER
|
||||
/// LetRec's PARAMS (not its name).
|
||||
///
|
||||
/// Property protected: when an inner LetRec lifts inside an outer
|
||||
/// LetRec's body, the outer's params are `ScopeEntry::KnownType` in
|
||||
/// the inner's outer-scope (set up by the desugar pass at the same
|
||||
/// site that marks the outer's NAME as `EnclosingLetRec`). The inner
|
||||
/// lift therefore takes the 16b.2 fast path with the outer's params
|
||||
/// appended to the inner's signature; once the outer is then lifted,
|
||||
/// the call sites of `inner$lr_M(args, outer_param)` continue to
|
||||
/// resolve `outer_param` as outer's still-in-scope param (later
|
||||
/// renamed by the outer's own lift to its lifted-fn param of the
|
||||
/// same name). Inner capturing the OUTER's NAME remains rejected —
|
||||
/// see the desugar/lift `EnclosingLetRec` panic with the
|
||||
/// closure-of-self message.
|
||||
///
|
||||
/// `nested_sum(n)` = sum of 1..=n by counting i ones for each i in
|
||||
/// 1..=n. Expected stdout: 1, 6, 15 for n in {1, 3, 5}.
|
||||
#[test]
|
||||
fn nested_let_rec_demo() {
|
||||
let stdout = build_and_run("nested_let_rec.ail.json");
|
||||
let lines: Vec<&str> = stdout.lines().collect();
|
||||
assert_eq!(lines, vec!["1", "6", "15"]);
|
||||
}
|
||||
|
||||
/// 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.
|
||||
|
||||
@@ -131,6 +131,7 @@ pub fn lift_letrecs(m: &Module) -> Result<Module> {
|
||||
module_names: &mut module_names,
|
||||
lifted: Vec::new(),
|
||||
current_def_forall_vars: Vec::new(),
|
||||
enclosing_letrec_names: BTreeSet::new(),
|
||||
};
|
||||
let _ = &mut counter; // counter lives in lifter from here on
|
||||
|
||||
@@ -211,6 +212,13 @@ struct Lifter<'a> {
|
||||
/// Iter 16b.6: enclosing fn's Forall.vars (or empty if mono).
|
||||
/// Reset on entry to each `Def::Fn`.
|
||||
current_def_forall_vars: Vec<String>,
|
||||
/// Iter 16b.7: names of LetRecs whose bodies are currently being
|
||||
/// lifted (i.e. enclosing `Term::LetRec` names visible at this
|
||||
/// point in the walk). Mirrors the desugar pass's
|
||||
/// `ScopeEntry::EnclosingLetRec` marker. An inner LetRec capturing
|
||||
/// any of these names is rejected — same chicken-and-egg as
|
||||
/// 16b.5-body / closure-of-self.
|
||||
enclosing_letrec_names: BTreeSet<String>,
|
||||
}
|
||||
|
||||
impl<'a> Lifter<'a> {
|
||||
@@ -377,7 +385,17 @@ impl<'a> Lifter<'a> {
|
||||
let prev = locals.insert(n.clone(), t.clone());
|
||||
body_pushed.push((n.clone(), prev));
|
||||
}
|
||||
// Iter 16b.7: mark `name` as an enclosing LetRec while
|
||||
// lifting its body, so any inner LetRec that captures
|
||||
// `name` panics with the closure-of-self message rather
|
||||
// than silently lifting with `name` as a fn-typed extra
|
||||
// param (which would mis-compile when `name` itself has
|
||||
// its own captures).
|
||||
let name_was_marked = self.enclosing_letrec_names.insert(name.clone());
|
||||
let lifted_body = self.lift_in_term(body, locals, in_def)?;
|
||||
if name_was_marked {
|
||||
self.enclosing_letrec_names.remove(name);
|
||||
}
|
||||
for (n, prev) in body_pushed.into_iter().rev() {
|
||||
match prev {
|
||||
Some(p) => {
|
||||
@@ -446,6 +464,28 @@ impl<'a> Lifter<'a> {
|
||||
.cloned()
|
||||
.collect();
|
||||
|
||||
// Iter 16b.7: if any capture refers to an enclosing
|
||||
// LetRec's NAME (rather than its params or a regular
|
||||
// local), reject. Lifting `name$lr_N` with `outer` as a
|
||||
// fn-typed extra param would mis-compile: the outer
|
||||
// LetRec has not been lifted yet, and once it is, its
|
||||
// own captures must be threaded through every value-
|
||||
// position use — exactly the closure-of-self problem.
|
||||
// Outer-LetRec PARAMS (KnownType in the desugar marker)
|
||||
// are fine and reach here as ordinary locals.
|
||||
for c in &captures {
|
||||
if self.enclosing_letrec_names.contains(c) {
|
||||
panic!(
|
||||
"Iter 16b.7: nested LetRec `{name}` captures outer LetRec name \
|
||||
`{c}` — closure conversion of a LetRec inside its own body \
|
||||
would be required (the capture's value is the outer LetRec's \
|
||||
pre-lift fn-value, which has no callable form before the \
|
||||
outer lift completes). Queued as `closure-of-self` (informally \
|
||||
16b.5-body / closure-poly)."
|
||||
);
|
||||
}
|
||||
}
|
||||
|
||||
// Resolve each capture's type via the locals table
|
||||
// (populated as we walked).
|
||||
let mut capture_types: Vec<(String, Type)> = Vec::new();
|
||||
|
||||
@@ -651,9 +651,12 @@ impl Desugarer {
|
||||
needs_defer = true;
|
||||
}
|
||||
ScopeEntry::EnclosingLetRec => panic!(
|
||||
"Iter 16b.4: LetRec `{}` captures `{}` from an enclosing \
|
||||
LetRec; nested mutual-capture is not supported. Queued for \
|
||||
16b.7.",
|
||||
"Iter 16b.7: nested LetRec `{}` captures outer LetRec name \
|
||||
`{}` — closure conversion of a LetRec inside its own body \
|
||||
would be required (the capture's value is the outer LetRec's \
|
||||
pre-lift fn-value, which has no callable form before the \
|
||||
outer lift completes). Queued as `closure-of-self` (informally \
|
||||
16b.5-body / closure-poly).",
|
||||
name, c
|
||||
),
|
||||
}
|
||||
@@ -2289,6 +2292,178 @@ mod tests {
|
||||
let _ = desugar_module(&m);
|
||||
}
|
||||
|
||||
/// Iter 16b.7: a nested LetRec whose inner LetRec captures the
|
||||
/// OUTER LetRec's NAME (not its params or any other local) is
|
||||
/// rejected at desugar time with the closure-of-self message.
|
||||
/// Capturing the outer's PARAMS is supported (covered by the
|
||||
/// `nested_let_rec` fixture / e2e); capturing the NAME is the
|
||||
/// chicken-and-egg case where the outer's value form does not
|
||||
/// exist before the outer's lift completes.
|
||||
#[test]
|
||||
#[should_panic(expected = "16b.7")]
|
||||
fn nested_let_rec_inner_captures_outer_name_panics() {
|
||||
// Outer LetRec body contains an inner LetRec that references
|
||||
// `outer` (the outer LetRec's own name) inside its body — as
|
||||
// a callee, even, but the panic fires on the capture
|
||||
// classification, not on a non-callee check.
|
||||
//
|
||||
// Shape inside main:
|
||||
// (let-rec outer (params i) (type Int->Int)
|
||||
// (body (let-rec inner (params j) (type Int->Int)
|
||||
// (body (app outer j)) ;; inner captures outer-NAME
|
||||
// (in (app inner 0))))
|
||||
// (in (app outer 1)))
|
||||
let inner = Term::LetRec {
|
||||
name: "inner".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["j".into()],
|
||||
body: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "outer".into() }),
|
||||
args: vec![Term::Var { name: "j".into() }],
|
||||
tail: false,
|
||||
}),
|
||||
in_term: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "inner".into() }),
|
||||
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
|
||||
tail: false,
|
||||
}),
|
||||
};
|
||||
let outer = Term::LetRec {
|
||||
name: "outer".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["i".into()],
|
||||
body: Box::new(inner),
|
||||
in_term: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "outer".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: outer,
|
||||
doc: None,
|
||||
})],
|
||||
};
|
||||
let _ = desugar_module(&m);
|
||||
}
|
||||
|
||||
/// Iter 16b.7 (positive companion): a nested LetRec whose inner
|
||||
/// LetRec captures the OUTER LetRec's PARAM (not its name) lifts
|
||||
/// cleanly through the existing 16b.2 fast path. The outer's
|
||||
/// params live in the inner's outer-scope as `KnownType`, so the
|
||||
/// inner classifies them like any other fn-param capture and
|
||||
/// appends them to its lifted signature. The post-order traversal
|
||||
/// then lifts the outer next; references to the outer's params
|
||||
/// inside the inner-call rewrites stay in scope (the outer hasn't
|
||||
/// renamed its params yet).
|
||||
#[test]
|
||||
fn nested_let_rec_inner_captures_outer_param_lifts() {
|
||||
// Shape inside main:
|
||||
// (let-rec outer (params i) (type Int->Int)
|
||||
// (body (let-rec inner (params j) (type Int->Int)
|
||||
// (body (app + i j)) ;; inner captures outer-PARAM i
|
||||
// (in (app inner 0))))
|
||||
// (in (app outer 1)))
|
||||
let inner = Term::LetRec {
|
||||
name: "inner".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["j".into()],
|
||||
body: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "+".into() }),
|
||||
args: vec![
|
||||
Term::Var { name: "i".into() },
|
||||
Term::Var { name: "j".into() },
|
||||
],
|
||||
tail: false,
|
||||
}),
|
||||
in_term: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "inner".into() }),
|
||||
args: vec![Term::Lit { lit: Literal::Int { value: 0 } }],
|
||||
tail: false,
|
||||
}),
|
||||
};
|
||||
let outer = Term::LetRec {
|
||||
name: "outer".into(),
|
||||
ty: Type::Fn {
|
||||
params: vec![Type::int()],
|
||||
ret: Box::new(Type::int()),
|
||||
effects: vec![],
|
||||
},
|
||||
params: vec!["i".into()],
|
||||
body: Box::new(inner),
|
||||
in_term: Box::new(Term::App {
|
||||
callee: Box::new(Term::Var { name: "outer".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: outer,
|
||||
doc: None,
|
||||
})],
|
||||
};
|
||||
let out = desugar_module(&m);
|
||||
// Three defs: original `main` + lifted `inner$lr_0` + lifted
|
||||
// `outer$lr_1`. Inner is lifted first (post-order), with outer's
|
||||
// param `i` appended; outer is lifted next, with no captures.
|
||||
let names: Vec<String> = out.defs.iter().map(|d| d.name().to_string()).collect();
|
||||
assert_eq!(
|
||||
names.len(),
|
||||
3,
|
||||
"expected main + two lifted fns; got {names:?}"
|
||||
);
|
||||
assert_eq!(names[0], "main");
|
||||
assert!(
|
||||
names[1].starts_with("inner$lr_") && names[2].starts_with("outer$lr_"),
|
||||
"expected inner then outer lifted-fn names; got {names:?}"
|
||||
);
|
||||
// The lifted inner must have two params: its own (`j`) plus the
|
||||
// captured outer-param (`i`).
|
||||
if let Def::Fn(inner_lifted) = &out.defs[1] {
|
||||
assert_eq!(
|
||||
inner_lifted.params,
|
||||
vec!["j".to_string(), "i".to_string()],
|
||||
"inner lifted params should be [j, i] (own + captured outer param)"
|
||||
);
|
||||
} else {
|
||||
panic!("expected Def::Fn at defs[1]");
|
||||
}
|
||||
}
|
||||
|
||||
/// Iter 16c: walks a term, returns true iff any [`Pattern::Lit`] is
|
||||
/// reachable in any [`Term::Match`] arm. After 16c desugaring, the
|
||||
/// invariant is `false` for every desugared output — `Pattern::Lit`
|
||||
|
||||
+153
@@ -4342,3 +4342,156 @@ pair generic over the enclosing fn's type vars).
|
||||
(chain-machinery exhaustiveness or `__unreachable__`), 16e
|
||||
(`==` extension to Bool/Str/Unit), 17a (per-fn arena, gated)
|
||||
unchanged.
|
||||
|
||||
## Iter 16b.7 — nested LetRec mutual capture (params, not name)
|
||||
|
||||
**Goal.** Lift the "nested LetRec mutual capture" rejection,
|
||||
but only for the case where the inner LetRec captures the
|
||||
OUTER LetRec's PARAMS. Capturing the OUTER's NAME from an
|
||||
inner LetRec body remains rejected — it is the same
|
||||
chicken-and-egg as 16b.5-body / closure-of-self (the value
|
||||
form of the outer LetRec doesn't exist before its own lift
|
||||
completes), and a clearer error is now emitted in its place.
|
||||
|
||||
**Architectural confirmation (the empirical result).** The
|
||||
params-only case worked **out of the box**. The desugar pass
|
||||
already enters outer's params into the inner's outer-scope as
|
||||
`ScopeEntry::KnownType` while marking only the outer's NAME
|
||||
as `EnclosingLetRec` (`desugar.rs:552-555`); the same shape
|
||||
holds in the post-typecheck lifter via the `locals` map
|
||||
(`lift.rs:373-378`). Post-order traversal then lifts the
|
||||
inner LetRec first under the existing 16b.2 fast path, with
|
||||
the outer's param appended to the inner's signature; once
|
||||
the outer is then lifted, every call site inside outer's
|
||||
body of the form `inner$lr_M(args, outer_param_x)` continues
|
||||
to refer to `outer_param_x` because outer hasn't yet renamed
|
||||
its params (outer's lift only renames its OWN name → lifted-
|
||||
name, not its params). After outer's own lift, those param
|
||||
references resolve to outer's lifted-fn's params (same name).
|
||||
|
||||
So: no implementation change was needed for the supported
|
||||
case. The work in 16b.7 is the test/fixture/JOURNAL surface
|
||||
plus tightening the rejection of the still-unsupported
|
||||
sub-case (inner-captures-outer-NAME) to point at the right
|
||||
follow-up.
|
||||
|
||||
**What shipped.**
|
||||
|
||||
- `examples/nested_let_rec.ailx` + `.ail.json` (50 LOC
|
||||
source). `nested_sum(n)` returns the sum of `1..=n` by
|
||||
combining two recursive helpers: outer LetRec `outer`
|
||||
iterates `i` over `1..=n`; for each `i` it calls inner
|
||||
LetRec `inner(j)` to count one for each `j` in `1..=i`.
|
||||
Inner captures `i` (outer's PARAM) and produces the count
|
||||
`i`; outer captures `n` (the enclosing fn's param) and
|
||||
sums those counts. Total = `n*(n+1)/2`. Drives at
|
||||
`n ∈ {1, 3, 5}` → output `1\n6\n15\n`. The fixture
|
||||
exercises the post-order lift, with inner lifted first as
|
||||
`inner$lr_0(j: Int, i: Int) -> Int` and outer lifted next
|
||||
as `outer$lr_1(i: Int, n: Int) -> Int`.
|
||||
- `crates/ail/tests/e2e.rs::nested_let_rec_demo` (+18 LOC):
|
||||
e2e count 44 → 45.
|
||||
- `crates/ailang-core/src/desugar.rs`: tightened the
|
||||
`ScopeEntry::EnclosingLetRec` panic (lines 653-660) from
|
||||
the 16b.4-era "nested mutual-capture is not supported,
|
||||
queued for 16b.7" message to a 16b.7 message that names
|
||||
the precise constraint ("captures outer LetRec name `<n>`
|
||||
— closure conversion of a LetRec inside its own body
|
||||
would be required") and points at the right follow-up
|
||||
(`closure-of-self` / 16b.5-body / closure-poly).
|
||||
- `crates/ailang-check/src/lift.rs`: added
|
||||
`Lifter.enclosing_letrec_names: BTreeSet<String>`,
|
||||
populated on entry to each LetRec arm via
|
||||
`BTreeSet::insert(name)` and removed on exit, mirroring
|
||||
the desugar pass's `EnclosingLetRec` marker. The capture
|
||||
classification step now panics with the same 16b.7
|
||||
message if any capture is in `enclosing_letrec_names`.
|
||||
This closes a defensive hole the post-typecheck path
|
||||
would otherwise leave open: without the marker, a
|
||||
deferred outer LetRec (one with Let/Match captures) whose
|
||||
inner LetRec captured the outer's name would silently
|
||||
lift the inner with the outer's pre-lift fn-type as an
|
||||
extra param, producing a type-correct AST that calls a
|
||||
fn-value with the wrong arity at runtime once the outer
|
||||
was itself lifted with captures. The new check rejects
|
||||
that path symmetrically with the desugar path.
|
||||
- `crates/ailang-core/src/desugar.rs::tests` (+2 net):
|
||||
`nested_let_rec_inner_captures_outer_name_panics`
|
||||
(`#[should_panic(expected = "16b.7")]`) and
|
||||
`nested_let_rec_inner_captures_outer_param_lifts`
|
||||
(positive — asserts two synthetic fns appended in
|
||||
inner-first/outer-second order, and that the inner
|
||||
lifted fn has params `[j, i]`).
|
||||
|
||||
**What stays rejected.** Inner LetRec capturing the OUTER
|
||||
LetRec's NAME (`EnclosingLetRec` in the desugar marker;
|
||||
`enclosing_letrec_names` set in the lifter). The proper fix
|
||||
is closure conversion of a LetRec inside its own body — the
|
||||
same shape as 16b.5-body, queued there. Both desugar and
|
||||
lift now panic with the same clarified message.
|
||||
|
||||
**Tests: 120 → 122 (+2).**
|
||||
|
||||
- e2e: 44 → 45 (`nested_let_rec_demo`).
|
||||
- `ailang-core::desugar::tests`: 23 → 25 (+2: one negative
|
||||
panic test + one positive lift test).
|
||||
- All other crates unchanged.
|
||||
|
||||
**Cross-iter regression check.** All eight prior LetRec
|
||||
fixtures (`local_rec_demo`, `lit_pat`,
|
||||
`local_rec_capture`, `local_rec_let_capture`,
|
||||
`local_rec_match_capture`, `local_rec_as_value`,
|
||||
`local_rec_as_value_capture`, `poly_rec_capture`) build,
|
||||
run, and produce identical stdout. Their on-disk hashes
|
||||
(verified via `ail manifest` on `local_rec_capture`) are
|
||||
bit-identical: the desugar/lift edits change runtime
|
||||
behaviour for previously-rejected cases only and never
|
||||
touch canonical-bytes input.
|
||||
|
||||
**Cumulative state, post-16b.7.**
|
||||
|
||||
- Stdlib unchanged (5 modules, 29 combinators).
|
||||
- `Term` enum: 11 variants (unchanged). All pre-16b.7
|
||||
fixture hashes bit-identical.
|
||||
- Compiler stages: load → desugar → typecheck →
|
||||
lift_letrecs → codegen (unchanged).
|
||||
- The four `unreachable!("Term::LetRec eliminated by
|
||||
desugar")` arms in `ailang-codegen` remain correct.
|
||||
- Compiler bugs surfaced and fixed in dogfood since 14a:
|
||||
5/5 (unchanged).
|
||||
|
||||
**End-of-16b series note.** With 16b.7, the LetRec-capture
|
||||
work is feature-complete except for the two deferred
|
||||
closure-of-self sub-cases:
|
||||
|
||||
- **`closure-of-self` (informally 16b.5-body)**: name-as-
|
||||
value of a LetRec INSIDE its own body, OR an inner
|
||||
LetRec capturing an outer LetRec's NAME. Both reduce to
|
||||
the same problem: the LetRec's value-form does not exist
|
||||
before its own lift completes, so any non-callee use
|
||||
inside its body needs either eta-conversion-of-self
|
||||
(constructing the value form before the lift, with the
|
||||
unlifted name in scope) or a true closure conversion
|
||||
that doesn't lift the LetRec to a top-level fn at all.
|
||||
- **`closure-poly` (informally 16b.5b)**: name-as-value of
|
||||
a LetRec inside a polymorphic enclosing fn. Needs a
|
||||
closure pair generic over the enclosing fn's type vars
|
||||
— a meaningful ABI extension. Independent of
|
||||
`closure-of-self` but closely related.
|
||||
|
||||
Every supported case is exercised by a fixture +
|
||||
e2e + (where applicable) a desugar/lift unit test. The
|
||||
16b.x sweep can be considered closed pending those two
|
||||
deferrals; both are tracked separately in the queue and
|
||||
neither blocks day-to-day authoring of recursive helpers.
|
||||
|
||||
**Queue update post-16b.7.** 16b.7 done. Open:
|
||||
**`closure-of-self`** (informally 16b.5-body — name-as-
|
||||
value of a LetRec inside its own body, including nested-
|
||||
LetRec inner-captures-outer-name; needs eta-conversion-of-
|
||||
self or true closure conversion). **`closure-poly`**
|
||||
(informally 16b.5b — name-as-value of a LetRec inside a
|
||||
polymorphic enclosing fn; needs polymorphic closure
|
||||
pairs). 16d (chain-machinery exhaustiveness or
|
||||
`__unreachable__`), 16e (`==` extension to
|
||||
Bool/Str/Unit), 17a (per-fn arena, gated) unchanged.
|
||||
|
||||
@@ -0,0 +1 @@
|
||||
{"defs":[{"body":{"body":{"cond":{"args":[{"name":"i","t":"var"},{"name":"n","t":"var"}],"fn":{"name":">","t":"var"},"t":"app"},"else":{"args":[{"body":{"cond":{"args":[{"name":"j","t":"var"},{"name":"i","t":"var"}],"fn":{"name":">","t":"var"},"t":"app"},"else":{"args":[{"lit":{"kind":"int","value":1},"t":"lit"},{"args":[{"args":[{"name":"j","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"fn":{"name":"inner","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":"inner","t":"var"},"t":"app"},"name":"inner","params":["j"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},{"args":[{"args":[{"name":"i","t":"var"},{"lit":{"kind":"int","value":1},"t":"lit"}],"fn":{"name":"+","t":"var"},"t":"app"}],"fn":{"name":"outer","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":"outer","t":"var"},"t":"app"},"name":"outer","params":["i"],"t":"letrec","type":{"effects":[],"k":"fn","params":[{"k":"con","name":"Int"}],"ret":{"k":"con","name":"Int"}}},"doc":"Sum 1 + 2 + ... + n by nested LetRec helpers; inner captures outer's param i.","kind":"fn","name":"nested_sum","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":"nested_sum","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"lhs":{"args":[{"args":[{"lit":{"kind":"int","value":3},"t":"lit"}],"fn":{"name":"nested_sum","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"rhs":{"args":[{"args":[{"lit":{"kind":"int","value":5},"t":"lit"}],"fn":{"name":"nested_sum","t":"var"},"t":"app"}],"op":"io/print_int","t":"do"},"t":"seq"},"t":"seq"},"doc":"Drive nested_sum at 1, 3, 5. Expected (per line): 1, 6, 15.","kind":"fn","name":"main","params":[],"type":{"effects":["IO"],"k":"fn","params":[],"ret":{"k":"con","name":"Unit"}}}],"imports":[],"name":"nested_let_rec","schema":"ailang/v0"}
|
||||
@@ -0,0 +1,53 @@
|
||||
; Iter 16b.7 — nested LetRec mutual capture (params, not name).
|
||||
;
|
||||
; `nested_sum(n)` returns the sum 1 + 2 + ... + n by combining two
|
||||
; recursive helpers. The OUTER let-rec `outer(i)` iterates i over
|
||||
; 1..=n; for each i it calls the INNER let-rec `inner(j)` to count
|
||||
; how many integers are in 1..=i (= i). The total is then
|
||||
; 1 + 2 + ... + n = n*(n+1)/2.
|
||||
;
|
||||
; The shape exercises:
|
||||
; - outer captures `n` from `nested_sum`'s fn-params (16b.2 case).
|
||||
; - inner captures `i` from outer LetRec's PARAMS (16b.7 case
|
||||
; under iter — outer LetRec's params are KnownType in body
|
||||
; scope, so the inner lift sees a resolvable capture type).
|
||||
; - inner does NOT capture outer's NAME (still rejected in 16b.7).
|
||||
;
|
||||
; Expected stdout (one per line):
|
||||
; nested_sum(1) = 1
|
||||
; nested_sum(3) = 6
|
||||
; nested_sum(5) = 15
|
||||
|
||||
(module nested_let_rec
|
||||
|
||||
(fn nested_sum
|
||||
(doc "Sum 1 + 2 + ... + n by nested LetRec helpers; inner captures outer's param i.")
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(params n)
|
||||
(body
|
||||
(let-rec outer
|
||||
(params i)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > i n)
|
||||
0
|
||||
(app +
|
||||
(let-rec inner
|
||||
(params j)
|
||||
(type (fn-type (params (con Int)) (ret (con Int))))
|
||||
(body
|
||||
(if (app > j i)
|
||||
0
|
||||
(app + 1 (app inner (app + j 1)))))
|
||||
(in (app inner 1)))
|
||||
(app outer (app + i 1)))))
|
||||
(in (app outer 1)))))
|
||||
|
||||
(fn main
|
||||
(doc "Drive nested_sum at 1, 3, 5. Expected (per line): 1, 6, 15.")
|
||||
(type (fn-type (params) (ret (con Unit)) (effects IO)))
|
||||
(params)
|
||||
(body
|
||||
(seq (do io/print_int (app nested_sum 1))
|
||||
(seq (do io/print_int (app nested_sum 3))
|
||||
(do io/print_int (app nested_sum 5)))))))
|
||||
Reference in New Issue
Block a user