Closes family 20: prose-edit cycle is end-to-end. ail merge-prose
<original.ail.json> <edited.prose.txt> composes a shaped LLM prompt
to stdout. User pipes to their LLM (Claude/etc.), gets new .ail.json,
runs ail check, saves.
No built-in API client — AILang stays a compiler + tooling, the LLM
mediator is supplied externally. PROSE_ROUNDTRIP.md documents the
6-step cycle, the prompt contract (preserve modes/effects/tail
flags from original), failure modes, and the design choice to omit
an API client.
Family 20 now closes: 20a renderer + 20b polish + 20d mediator
shipped; 20c rolled into 20a. Three deferred polishes (let-inlining,
print sugar, doc-wrap widow control) wait for corpus signal.
Eleven binary builtins (+ - * / % == != < <= > >=) render as
lhs op rhs when called with two args (tail-flagged keeps prefix).
Standard Rust-aligned 4-level precedence table elides parens.
not(x) renders as !x. Long /// doc strings wrap at 80 cols on
word boundaries.
bench_list_sum: 'if ==(n, 0)' becomes 'if n == 0', '+(acc, h)'
becomes 'acc + h', tail keyword still visible on tail calls.
19 new unit tests (47 total). 4 snapshots (3 re-rendered + 1 new
bench fixture). Public API unchanged.
When a fn-param is annotated (own T) but the body never consumes
it (consume_count == 0) and never destructures it via match, the
linearity pass now emits a Severity::Warning diagnostic with a
form-A-rendered (borrow T) rewrite as suggested_rewrite. Pure
advisory, Decision 10 unchanged.
First Warning-severity diagnostic the typechecker emits; three
CLI exit paths gated on Error-only.
JOURNAL: design entry + iter 19a shipping entry.
Three sibling sites previously fell back to shallow `ailang_rc_dec`
when a binder had non-empty `moved_slots` and a dynamic runtime ctor
tag: Iter B Own-param dec at fn-return (lib.rs), Iter A arm-close
pattern-binder dec (match_lower.rs), and emit_inlined_partial_drop's
non-Ctor branch (drop.rs). Shallow freed the outer cell but did not
walk the unmoved ptr fields — silent leak.
Adds `emit_partial_drop_fn_for_type`: a per-ADT helper structurally
parallel to `emit_drop_fn_for_type` but taking an i64 moved-slots
bitmask. Each ptr-field's dec is gated on the corresponding mask
bit; the outer box is dec'd at join. Emitted alongside the per-type
drop fn for every ADT under --alloc=rc.
Three call sites rewritten to resolve the partial_drop symbol from
the binder's static type and build the mask from `moved_slots`.
Three RED-then-GREEN fixtures (rc_own_param_/rc_match_arm_/
rc_app_let_partial_drop_leak) pin the carve-outs in regression
coverage; live cell counts go from 3/1/3 (pre-fix) to 0/0/0.
e2e count: 66 → 69.
The pre-existing `alloc_rc_own_param_dec_at_fn_return` IR-shape
assertion is widened to accept `partial_drop_<m>_<T>(%arg_xs,
i64 mask)` as a third valid drop shape (the canonical fu2 case).
Closes the JOURNAL queue's only remaining iter; the "wait for
organic fixture" stance from the 18g tidy is retracted — known
leaks are bugs, CLAUDE.md's TDD rule covers them autonomously.
Records the four-phase reorganisation that moved 2470 lines
out of lib.rs into purpose-named sibling submodules. Captures
the visibility model (descendant-module privacy + selective
pub(crate)), the deliberate non-extractions (lower_term, the
app/call cluster), and the framing as a navigability tidy
rather than a feature-driven change.
Closes two of the three queued debts from the 18g tidy in the
same session. Tag-conditional partial-drop helper stays queued
— substantial, no observable fixture, all current fallback paths
cleanly use shallow ailang_rc_dec.
The 18-arc + 18g sub-arc + 18g tidy + post-tidy follow-ups are
all closed. Decision 9 has been re-framed to match the
orchestrator's dual-allocator stance (commit f10a77e). Next iter
is queue-driven; nothing load-bearing is open.
The 18-arc validated the RC pipeline end-to-end; the orchestrator's
call (JOURNAL 2026-05-08) was to keep Boehm as default and RC as
the ready alternative rather than retire Boehm. Decision 9's
'transitional Boehm' framing was wrong shape for that policy —
this edit re-casts it as 'dual allocator: Boehm GC for general
workloads, RC for real-time-sensitive workloads', preserving the
rest of the section.
Decision 10 holds as the specification of the RC alternative; this
edit only changes the framing of how the two allocators relate.
User's stance on the retirement question raised in 18f / 18g.2:
keep the dual-allocator setup. Boehm = default, RC = validated
alternative ready to flip. Re-opening trigger is operational
(maintenance cost), not performance.
Concrete consequences recorded: no default flip, -lgc stays, and
Decision 9's 'transitional' framing should be re-cast as 'dual
allocator' in a follow-up DESIGN.md edit (queued). Decision 10
holds as the canonical real-time path. The three RC-side debts
from the 18g tidy remain queued and don't block the dual stance.
Resolves the architect's drift report on the 18g sub-arc:
- DESIGN.md: ratify mode-metadata's codegen role. param_modes /
ret_mode were already on Type::Fn since 18a; with 18d.4 / 18g
they became load-bearing for drop-emission decisions in
codegen. The new 'Mode metadata is load-bearing for codegen'
subsection records the four seams (Iter A + Iter B + 18g.1 +
18g.2) and names the let-alias-of-borrow carve-out the gates
do not propagate through.
- bench/run.sh: post-throughput, invoke bench/latency_harness.py
on the three canonical arms (Implicit @ gc, explicit @ rc,
Implicit @ rc control). The Boehm-retirement bench numbers
are now reproducible by anyone running the harness, not just
by hand on a specific host.
- Negative coverage: examples/rc_let_implicit_returning_app
+ alloc_rc_let_binder_for_implicit_returning_app_does_not_drop
pin the asymmetry to the (own)-ret-mode test (live=0 there,
live=1 here). The Borrow-ret-mode case is covered by the
language design itself — typechecker rejects 'borrow-
passthrough' shapes with consume-while-borrowed.
JOURNAL entry records four items as deferred known debt:
emit_inlined_partial_drop dynamic-tag fallback, carve-out
diagnostics surface, bench-number stat-of-N, and the
cross-family ordering observation about CLAUDE.md's tidy-iter
rule.
The 18-arc is formally closed with this tidy. Next iter is
the orchestrator's Boehm-retirement decision (Path A vs Path B
from JOURNAL 2026-05-08 18f entry, joined by the post-18g.2
re-bench numbers).
Re-runs the latency bench post-18g.2 and records the result:
RC p99 = 311.6 µs (1.37× median), max = 348.2 µs (1.53× median);
Boehm p99 = 7249 µs (69.65× median), max = 7923 µs. RC is 23×
better on p99 and 23× better on max. RSS: RC 42 MB vs Boehm
66 MB — RC is now LOWER RSS, not higher. Median throughput: RC
is 2.18× slower (alloc-path tax).
Decision 10's real-time commitment has its evidence base. Boehm
retirement is now an orchestrator call between (A) 'retire,
accept the throughput tax until a slab allocator is built' and
(B) 'build the slab allocator first, retire after'. No commit
yet flips defaults.
Documents the 18-arc as complete on the correctness property:
explicit-mode RC reports live=0 on the canonical bench fixture
(allocs=11068575 frees=11068575). Remaining open work is
orchestrator-territory or queued (tag-conditional partial-drop,
let-alias-aware mode propagation, tidy-iter).
Records the diagnosis (18f.2 bencher finding -> tail-call drop
elision in match arms whose body consumes pattern-binders into
the tail-call), the new pre-tail-call seam in lower_match, the
opt-in rc-stats counter test infrastructure (18g.0), the TDD
record, and the end-to-end verification on bench_latency_explicit
(11M -> 1M live cells; the 1M residue is the persistent Tree
cache and queues as 18g.2).
Bencher ran the tail-latency bench post-RC-fix. Boehm's p99=7131µs
is 74× its median (96µs); explicit-mode RC's p99=453µs is 1.62× its
median (280µs). Decision 10's real-time claim has a first piece of
evidence on the correct axis (tail latency) — 18f's throughput
bench measured the wrong thing.
Surprise finding: explicit-mode RC leaks at the same RSS rate as
implicit-mode RC (511MB peak on both). The (own ...) +
(reuse-as) + (drop-iterative) annotations don't drive deallocation
in tail-recursive arms because pattern-binder t is consumed into
the tail-call (consume_count > 0, Iter A skips); the outer LCons
husk has all its ptr fields moved out but no drop site shallow-decs
it. Genuine 18d.4 implementation gap, queued as Iter 18g (#82).
Retirement decision (Path A vs Path B from 18f) still open; now
joined by the outer-cell-shallow-dec finding. Both feed the
eventual decision.
Iter B (Own-param dec at fn return) gates on param_modes[i] ==
ParamMode::Own and skips Implicit/Borrow because those modes carry
no caller-handed-off-ownership signal. Iter A (arm-close pattern-
binder dec) is the same shape — pattern-binders loaded out of a
scrutinee owe their drop-validity to the scrutinee's ownership —
but Iter A had no such gate and fired on every ptr-typed binder
with consume_count == 0.
Concrete failure (regression test): pin (params t) is Implicit,
caller loop holds t and re-passes it to itself. pin's (TNode v l r)
arm dec'd l and r, fragmenting the tree the caller still references.
Next recursion tripped ailang_rc_dec underflow.
Fix: thread current_param_modes onto the emitter, set it in
emit_fn from the fn type's param_modes (and reset/save it across
lambda thunk emission). In lower_match, derive scrutinee_is_owned
from the scrutinee's mode (Own only; let-binders and temps are
treated as owned) and skip Iter A when not owned.
Carve-out: a let-alias of a non-Own param is not yet detected;
the regression doesn't trigger it and a propagation pass belongs
in its own iter. Recorded in JOURNAL.
Red: alloc_rc_pattern_bind_in_implicit_fn_does_not_dec_borrowed_children.
Pre-fix the rc binary aborted with refcount underflow; post-fix
matches alloc=gc ("0").
Records the bench numbers (rc/bump 2.5–2.9x on the Implicit-mode
fixtures, missing Decision 10's 1.3x retirement target) and the
two paths forward — lower the threshold (Path A, pragmatic; rc
and gc are within 5% of each other so retirement under "RC ≤
Boehm ± 5%" qualifies) vs build a slab/pool allocator first
(Path B, larger iter, closes most of the gap to bump).
The 1.3x criterion was orchestrator-level commitment in
Decision 10 and not meeting it is a prompt for an orchestrator-
level discussion, not for the implementer to autonomously flip
the default. 18f deliberately stops without flipping default,
without dropping -lgc, without marking Decision 9 historical.
Records the schema additions (TypeDef.drop_iterative, serde-skip
when false), why heap-stretchy-buffer worklist was chosen over
slot-repurposing (not every box has a free ptr-slot to thread
through), the mono-typed worklist trade-off (simpler loop body,
small cross-type cascade penalty), the four new ABI symbols in
runtime/rc.c, and the validation against Decision 10's brief.
Validation note: hand-run confirmed the 1M-cell fixture with the
annotation exits 0; same fixture without the annotation SIGSEGVs
(exit 139). The annotation is load-bearing, not cosmetic.
Closes with the dispatch line for 18f (RC validation bench +
Boehm retirement decision) and reaffirms the post-18f tidy-iter
will be ailang-architect-driven drift cleanup over the whole
18-arc surface.
Records the two emission seams (pattern-binder at arm close,
Own-param at fn return), why they fit one iter (uniform
emission shape), the explicit dynamic-tag partial-drop fallback
to shallow ailang_rc_dec when moved_slots is non-empty for a
dynamic-runtime-ctor binder, the side effect on reuse_as_demo's
sum_list (correctness improvement, stdout unchanged, existing
assertions still hold), and the closing of 18d.3's regression.
Notes that 18d.3 + 18d.4 together close the move-aware-pattern
story for the static case; dynamic-tag partial-drop is the
remaining hygiene gap and is structurally orthogonal (would
exist even without moves). 18e (worklist) may be the natural
place to also close the dynamic-tag fallback.
Records strategy (b) (codegen-side bookkeeping, no source
mutation), why strategy (a) was retired (borrow contracts +
desugar re-scrutinise), the moved_slots side table and its
consumers (Term::Let close + reuse arm), and the narrow
memory-hygiene regression on borrow_only_recursive_list_drop
that 18d.4 will close. Also flags 18d.3 as the first iter to
ship with an undetected (no valgrind in CI) memory-hygiene
regression — accepted with explicit follow-up iter, not
papered over.
Records the runtime refcount-1 dispatch design (Lean 4 / Roc
lineage), why the dispatch lives at codegen rather than in
runtime/rc.c (per-site decision, no new ABI), the new
reuse_shape pre-codegen pass with its five reason sub-codes,
and — crucially — the explicit field-cleanup scope cut. The
reuse arm does not dec old pointer-typed fields because the
canonical fixture's pattern-bound subterms alias the new field
values (`(reuse-as xs (Cons _ (map_inc t)))` returns t's
in-place-rewritten box as the new tail). The root cause is
upstream: pattern-matching does not null out source slots. 18d.2
ships the perf-only half (alloc + outer cascade elided);
18d.3 / 18e closes the leak with move-aware patterns.
Records the schema floor (Term::ReuseAs wrapper, identity
codegen), the three diagnostics that close the
schema-permits-meaningless-forms gap (reuse-as-non-allocating-
body, reuse-as-source-not-bare-var, use-after-consume), and the
"source-not-bare-var rule lives in linearity, not typecheck"
design point — that constraint is a use-rule about reuse
semantics, not a type-rule, so it sits in the linearity pass
where it's gated on the all-explicit-mode activation. Closes
with the dispatch note for 18d.2 (in-place rewrite under
--alloc=rc, plus reuse-as-shape-mismatch diagnostic).
The schema sketch in Decision 10 already committed to
Term::ReuseAs { source, body } as a wrapper, but did not record
WHY the wrapper form was chosen over a reuse_from: Option<String>
modifier on Term::Ctor. Adds the two substantive reasons:
- Compositional flexibility: wrapper generalises to record
literals, opaque box wrappers, capability cells — anything
future iters might add as an allocating construct. Modifier
would replicate per Term variant.
- Source-locality: (reuse-as SRC NEW-CTOR) reads as a sentence
with the source-binder at the head. Modifier scatters intent.
The trade-off accepted: schema permits Term::ReuseAs around a
non-allocating body. Caught at typecheck via
reuse-as-non-allocating-body diagnostic. Same shape as
Decision 7's Term::If composability accepts.
Recording before 18d.1 ships — per CLAUDE.md "design rationale
ne implementation effort", a schema choice has to name its
substantive reasons before code is written, not retroactively.
Records the drop-symbol scheme (uniform @drop_<m>_<T> for every
ADT, even no-boxed-children ones; pair+env drop fns for escaping
closures), field_drop_call's per-type dispatch and the three
fall-back cases (Str / Fn / Type::Var), the unchanged Term::Let
emission gates, and the explicit deferral of stack-recursion to
18e's worklist allocator. Also lists the four known-debt items
(stack-recursive drop, closure-typed ADT fields, Type::Var
fields, fn parameters) so 18d's design surface is clear.
Records the inference's max-over-paths semantics, the codegen
gates (consume_count == 0, body-tail-not-binder,
block-not-terminated, non-escape membership), the @-prefix elide
on closure-pair globals, the rc_box_drop fixture's choice of a
no-boxed-children ADT (shallow free sufficient), and the explicit
scope cut for per-type drop fn (18c.4). Closes with the dispatch
note for 18c.4 and the reminder that the new CLAUDE.md tidy-iter
rule fires after 18f when the 18-arc closes.
Records what shipped in 18c.2 (activation gate, two diagnostic
codes, position model, the new parse_term / term_to_form_a
round-trip in ailang-surface, gate on clean-typecheck), the
three known false negatives that are deliberate scope cuts
(missing-consume-of-Own, lam captures conservative, pattern
bindings start fresh), and the dispatch for 18c.3 (uniqueness
inference + codegen inc/dec — the iter where RC actually starts
collecting memory).
User correction during the post-RC-overnight check-in: the 18a
"Type::Fn metadata vs. new Type variant" call was justified
across DESIGN.md, JOURNAL, and the commit message primarily by
"avoids ~250 match-arm sites". That is an observation about the
current state of the code, not a design rationale.
CLAUDE.md gains two binding rules:
- Design rationale ≠ implementation effort. Effort is at most a
tiebreaker; a choice whose only stated reason is effort is
suspect. The rule names the 18a misstep as the canonical
anti-example so future sessions catch it earlier.
- Direction freedom + bounce-back conditions inlined (was
previously a cross-reference to a private auto-memory file
outside the repo, which the user couldn't see).
DESIGN.md Decision 10's Schema-additions block now leads with
the substantive reasons for per-position metadata: semantic
locality (modes belong to fn-parameter positions, not to types
in general — Decision 1 line); compositional clarity (type
identity vs. calling convention factor apart); future-proofing
(per-position metadata generalises; Type-variant approach
combinatoric blows up). The match-arm count remains parenthetical,
explicitly named a tiebreaker.
JOURNAL records the correction itself — the mistake stays as a
data point because how design discipline corrupts is informative.
Records that 18c.1 ran zero-surprise (mechanical recursion at
~10 sites across 6 files), the future-work seam in codegen for
18c.3 is a single line (emit one rc_inc call before returning
the inner SSA reg), and 18c.2's linearity check should start
as 'green for borrow_own_demo' since that fixture's shape is
exactly what the check needs to accept.
Records that the codegen change was a one-line extension because
the 18a bump path had centralised the allocator-symbol decision
on fn_name(). Documents the runtime ABI (8-byte refcount header,
ailang_rc_alloc/inc/dec) and the deliberate no-inc/dec posture:
programs leak intentionally under --alloc=rc; 18c lights up the
actual reference counting.
Next-step plan for 18c is split into three sub-iters
(clone schema / linearity check / inference + codegen) since
each wants its own verification cycle.
Records the schema-choice rationale (per-position metadata on
Type::Fn vs new Type variants — the latter would be a 250-site
mechanical migration, the former is one iter), the
padding-on-read trick that kept construction sites unchanged,
and the forward-compat note on the new fixture's borrow+own
sharing pattern.
Adds form-A surface (borrow T) / (own T) wrappers in fn-type
params and ret slots. Internally these are not new Type variants
but per-position metadata on Type::Fn:
Type::Fn { params, param_modes, ret, ret_mode, effects }
enum ParamMode { Implicit, Own, Borrow }
This keeps Type itself unchanged, so unification, occurs, apply,
and ~190 other Type match-arms in the typechecker need no new
branch. Fields use serde skip-if-default predicates so canonical
JSON hashes for every pre-18a fixture stay bit-identical (sum,
list, hof, closure, list_map, etc.: zero diff under git).
Iter 18a is purely additive: typechecker treats modes as
transparent (mode-compat check deferred to 18c), no codegen
change (--alloc=gc / Boehm path unchanged), no linearity
enforcement. The annotation info flows into the JSON side-table
that 18c will consume.
Equality of mode slices is length-tolerant: a vec![] (the form
written by mechanically-updated construction sites that elide
modes) compares equal to vec![Implicit; n]. This kept the patch
from being a 100-site mechanical migration through the
typechecker. 18c will choose: keep the slack, or normalise to
full-length on construction.
New fixture examples/borrow_own_demo.{ailx,ail.json} exercises
both modes. list_length declares (borrow (con List)); sum_list
declares (own (con List)). Stdout: 3 then 6.
Documentation: DESIGN.md schema-additions block clarified that
modes are Type::Fn metadata (not Type variants); migration plan
flag rename --memory=rc → --alloc=rc to match the existing CLI
flag.
Verification:
- cargo build --workspace green
- cargo test --workspace green (154 tests, +1 vs baseline 153)
- git diff examples/{sum,list,hof,closure,list_map,...}.ail.json: empty
- borrow_own_demo runtime stdout: "3\n6\n"
- canonical JSON contains "param_modes":["borrow"] and ["own"]
Avoids the ~190 Type match-arms in the typechecker that a new
Type variant would require. ParamMode enum (Implicit | Own |
Borrow) attaches per-param to Type::Fn, with serde defaults so
existing fixture hashes stay bit-identical.
Replaces the earlier "RC + inference, no annotations" position
with a two-layer architecture: inference (intra-fn) + mandatory
LLM-author mode annotations on fn signatures (inter-fn). Adds
structured rationale for rejecting region inference (regions
assume stack-shaped lifetimes; real programs need
non-stack-shaped lifetimes for caches / memo tables) and linear
types as primary mechanism.
Schema additions enumerated for the 18-series:
Type::Borrow / Type::Own (Iter 18a)
Term::Clone (Iter 18c)
Term::ReuseAs (Iter 18d)
TypeDef.drop_iterative (Iter 18e)
Migration plan extended from 18a-d (4 iters) to 18a-f (6 iters).
JOURNAL records the regions excursion, the scope-shape reduction,
and the LLM-author lever as the structural advantage Decision 10
cashes in on.
Adds --alloc=<gc|bump> to ail build/run. Bump path links a 256MB
no-free arena C stub instead of libgc; IR is byte-identical except
for the @GC_malloc → @bump_malloc symbol swap. Bench harness times
two allocation-heavy workloads (list cons/sum and balanced tree
build/walk) under both modes.
Numbers (RUNS=5, median of 4):
bench_list_sum gc 0.141s bump 0.048s +194%
bench_tree_walk gc 0.103s bump 0.041s +151%
Bucket: large. ~60% of runtime is Boehm on these workloads —
upper bound for any realistic program. Both fixtures hold the
heap fully live, so the cost we're seeing is Boehm's allocate
path itself, not collection work; that fact narrows the design
space for the GC discussion.
- crates/ailang-codegen: AllocStrategy enum, three callsites and
the IR header parameterised.
- crates/ail/src/main.rs: --alloc flag plumbed; bump runtime
located + compiled on demand.
- runtime/bump.c: 256MB static arena, abort-on-overflow.
- examples/bench_list_sum, bench_tree_walk: accumulator-form
fixtures (textbook recursive sum was constructor-blocked).
- bench/run.sh: harness with Python timing helper (Arch's
/usr/bin/time isn't part of the base install).
No language-level changes; default --alloc=gc, all 141 workspace
tests green, all 5 IR snapshots unchanged, 11 prior fixtures
produce identical stdout.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds a conservative escape analysis that flags Term::Ctor and
Term::Lam allocations as non-escaping when they are bound by a
let, never flow to a fn arg / ctor field / tail-return / lambda
capture, and remain inside the allocating fn's frame. Codegen
lowers flagged sites to LLVM `alloca` instead of `@GC_malloc`;
escaping sites continue to use Boehm.
- escape.rs (new): name-based taint propagation; let-only
candidates; tail-position / app-arg / ctor-field / lam-capture
all taint.
- codegen: three sites switched (lower_ctor, lam env, closure
pair). Save/restore non_escape across lambda thunk emit.
- examples/escape_local_demo.{ailx,ail.json}: focused fixture
exercising both branches (peek and recursive count).
- e2e + escape unit tests: 133 → 141 (+8).
Stop-gate: 17a closes the queue. Memory-management discussion
(GC scope) is the next user-driven step. Per-fn arena observations
appended to JOURNAL — including the headline finding that 0/270
shipped allocations are flagged non-escaping under this rule
(real AILang threads ctors directly between fns; build-locally /
consume-locally is not idiomatic).
All existing fixture stdouts and content hashes bit-identical;
IR snapshots unchanged.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lifts the Int-only restriction on `==`. Declared type becomes
forall a. Fn(a, a) -> Bool; codegen monomorphises and dispatches:
Int → icmp eq i64
Bool → icmp eq i1
Str → call @strcmp + icmp eq i32 0
Unit → constant true (operands still emitted for side effects)
ADT / Fn / other → CodegenError::Internal
This unblocks 16c's build_eq for non-Int lit patterns. == joins
__unreachable__ as the second polymorphic builtin (same Forall
machinery).
- check/builtins.rs: == registered as Forall(a, Fn(a, a) -> Bool).
- codegen: lower_eq dispatch table; @strcmp declared in IR header
alongside @printf/@GC_malloc/@puts.
- examples/eq_demo.{ailx,ail.json}: covers all four supported
scalars including a Str-lit-pattern match.
- IR snapshots refreshed: only +declare i32 @strcmp(ptr, ptr) in
the header; every define body bit-identical.
- e2e + check + codegen tests: 124 → 133 (+9, of which +1 is the
e2e fixture and the rest exercise the new dispatch / typecheck
surface).
Other comparison ops (<, <=, >, >=, !=) remain Int-only — out of
scope for this iter.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Eliminates the Unit-typed chain default that 16c left in place.
Adds __unreachable__ : forall a. a — codegen lowers to LLVM
unreachable. The 16a/16c chain machinery now uses it as the
deepest fall-through, so exhaustive matches with non-Unit arms
no longer need a (case _ ...) workaround.
- check/builtins.rs: register __unreachable__ as Forall(a, a).
- codegen: Term::Var "__unreachable__" emits LLVM unreachable
and sets block_terminated; If/Match/fn-body gate downstream
work on that flag.
- desugar: chain default switched from Lit{Unit} to Var.
- examples/lit_pat: categorize_first's trailing _ arm removed.
Hash changes from c4faec3abc2ed388 to 644de0c0ec15fc17.
- examples/unreachable_demo: positive fixture using safe_div
with __unreachable__ in the impossible branch.
- e2e + desugar tests: 122 → 124 (+2).
Path-a from 16b.2 planning: real primitive over a desugar-time
exhaustiveness pre-check (which would need cross-module type
registry access from desugar).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
Lifts the monomorphic-only restriction. Lifted top-level fn now
becomes Forall(α..., Fn(t..., T...) -> tr) when the enclosing fn
is polymorphic; capture types may mention outer type vars and
the existing mono pipeline (Iter 12b/14a) specializes them
correctly at call sites.
- desugar.rs / lift.rs: scope-building unified — Forall fn-params
are now KnownType, not LetBound. Lift wraps augmented_ty in
Forall mirroring the enclosing fn.
- Name-as-value-in-in-term in a polymorphic enclosing fn is
rejected (eta-Lam wrap from 16b.5 has no Forall). Queued
separately as closure-conversion-with-polymorphism.
- examples/poly_rec_capture.{ailx,ail.json}: apply_n_times :
Forall(a). drives at Int and Bool to exercise two mono
instantiations.
- e2e + check + desugar tests: 116 → 120 (+4).
Codegen pipeline untouched — apply_subst_to_type substitutes
through Fn.params uniformly (original params + appended captures).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Drops the direct-call-only restriction on the LetRec name when it
appears in `in_term`. No new ABI: the lift wraps the in-term in
`(let f (lam P (app f$lr_N P CAPTURES)) in_term')` so codegen's
existing Iter-8b closure-pair machinery handles it. Body-position
name-as-value still rejected (deferred — eta-of-self is harder).
- desugar.rs / lift.rs: split find_non_callee_use into body
(panic) and in_term (wrap).
- examples/local_rec_as_value.{ailx,ail.json}: no-capture path
(factorial passed to apply5 → 120).
- examples/local_rec_as_value_capture.{ailx,ail.json}: capture
path; lifted fn has captures, eta-Lam picks them up via 8b.
- e2e + desugar tests: 113 → 116 (+3).
Codegen Lam machinery handled the wrapped form on the first try.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
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>
Adds path-2 from the 16b.2 planning entry. Desugar now defers
LetRecs whose captures include Term::Let-bound names; a new
ailang-check::lift_letrecs pass runs after typecheck and uses the
elaborated env to resolve capture types. ailang-check learns a real
Term::LetRec typing rule in synth and verify_tail_positions.
- desugar: Term::LetRec arm gains a defer-arm; helpers promoted to
pub for reuse by the lift pass; find_non_callee_use moved before
classification.
- ailang-check::synth/verify_tail_positions: real LetRec rules
(effect-subset, locals install, recursive name in body+in_term).
- ailang-check::lift.rs (new, 720 LOC): post-typecheck lift with
post-order traversal, env-walk for capture-type resolution,
fast-path skip when no LetRec is present.
- ail::main.rs: build path now does load → check → desugar →
lift_letrecs → codegen.
- examples/local_rec_let_capture.{ailx,ail.json}: new fixture
capturing a let-bound `threshold` in a recursive helper.
- e2e + check unit tests: 106 → 110 (+4).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Lift 16b.1's no-capture restriction. The desugar pass's `scope`
becomes a `BTreeMap<String, ScopeEntry>` 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) <noreply@anthropic.com>
Orchestrator-level planning artifact, not an iteration log.
Captures the design space for 16b.2 so the user can review
trade-offs before implementation. Three architectural paths
considered (desugar-only with restrictions, post-typecheck pass,
mini-inference inside desugar); recommends the first as the
incremental path. Lists restrictions for the safe subset
(fn/Lam-param captures only, direct-call only, monomorphic
enclosing fn, single-level LetRec) and queues the lifted
restrictions as 16b.3-16b.7. Adjacent open items (16d chain
terminator, 16e == extension) likewise scoped.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Desugar `Pattern::Lit` (top-level and nested in Ctor) to
`Term::If { cond = (== sv lit), then = body, else_ = fall_k }`.
After 16c, no Pattern::Lit survives the desugar pass; codegen
and typechecker never see one. `is_flat` reclassifies Lit as
non-flat to force the chain machinery; new `build_eq` helper
constructs the equality test per literal kind.
Tests: 99 → 103 (+1 e2e lit_pat_demo, +3 desugar unit). Demo
fixture exercises top-level lit arms (classify) and nested
lit-in-Ctor (categorize_first) with a local IntList; output
100/200/999/-1/0/7.
Known limitations documented in DESIGN.md and JOURNAL: (a)
chain machinery's Unit terminator means non-Wild-terminated
exhaustive matches with lit arms still need a trailing `_`
catch-all to type-check; (b) `==` is currently Int-only, so
Bool/Str/Unit lit patterns desugar correctly but error at
typecheck.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Add `(let-rec NAME (params ...) (type ...) (body ...) (in ...))`
as a form-A surface and a `Term::LetRec` AST variant. The 16a
desugar pass lifts each LetRec whose body has no captures from
the enclosing scope to a synthetic top-level fn `<hint>$lr_N`
and substitutes the original name; typecheck and codegen never
see LetRec. Capture detection panics at desugar time, queued
for 16b.2.
Tests: 95 → 99 (+1 e2e local_rec_factorial_demo, +2 desugar
unit, +1 parse unit). The new fixture `examples/local_rec_demo`
runs `fact` at n=1, 3, 5 → prints 1, 6, 120.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Adds the two canonical prefix-slicing combinators to std_list.
First fns in std_list to combine `if` + Int arithmetic + recursive
ADT pattern in one body.
take : forall a. (Int, List<a>) -> List<a>
— first n elements (or all of xs if shorter than n).
drop : forall a. (Int, List<a>) -> List<a>
— list with first n elements removed (Nil if n >= length).
Both use `(if (<= n 0) ...)` as the base-case guard since
literal sub-patterns inside Ctor patterns aren't yet supported
(queued as 16c — would let take/drop collapse the if into the
match).
examples/std_list_more_demo: builds [1, 2, 3, 4, 5] once and
exercises take/drop at n=0, n=mid, n=overflow on each. Expected
output 0, 3, 5, 5, 3, 0 (one per line).
Tests: 95/95 (e2e went from 35 to 36). std_list grew from 10 to
12 combinators; total stdlib 5 modules / 29 combinators. No new
compiler bug surfaced.
Pre-existing std_list defs are byte-identical (verified via diff
on .ailx and round-trip on .ail.json), so the five downstream
importers (std_list_demo, std_list_stress, std_either_list,
std_either_list_demo, list_map_poly) need no regeneration.
Fix the codegen asymmetry that 15g surfaced. unify_for_subst had an
arg-side-only early-return for $u-prefixed synth wildcards. The
function's prev-binding recursion can swap a $u from arg into param
position when re-unifying a previously-bound type against a fresh
arg. Reduced repro: `length [Left 1, Right 10]` — `a` first binds
to `Either<Int, $u>`, then the recursive unification against
`Either<$u, Int>` lands $u in param-pos[1] and falls through to
the catch-all error.
Fix is three lines: add a symmetric $u early-return for param side.
$u is a synth-only wildcard regardless of which side it ends up on
after the prev-binding swap. Doc comment expanded to record the
origin and justification.
std_either_list_demo refactored: mkleft/mkright workaround helpers
removed; the list is now constructed inline by mixing
(term-ctor std_either.Either Left 1) and (... Right 10) directly.
Same expected output (2, 3, 2, 3); the demo doubles as the 15g-aux
regression fixture.
Tests: 94/94, unchanged. The fix expanded what compiles without
changing observable behaviour for any prior fixture.
First stdlib fn that imports three other stdlib modules (std_list,
std_either, std_pair) and returns a compound polymorphic ADT tree
(Pair<List<e>, List<a>>). Stresses monomorphisation across nested
parameterised ADTs.
What shipped:
- examples/std_either_list.{ailx,ail.json}: 3 combinators —
- lefts : forall e a. (List<Either<e, a>>) -> List<e>
- rights : forall e a. (List<Either<e, a>>) -> List<a>
- partition_eithers : forall e a. (List<Either<e, a>>)
-> Pair<List<e>, List<a>>
lefts/rights use depth-2 nested Ctor patterns (Cons (Left l) t)
— exercises 16a's desugar pass at a depth not reached by any
prior fixture.
- examples/std_either_list_demo.{ailx,ail.json}: drives all three
combinators on a five-element List<Either<Int, Int>>; expected
output one per line: 2, 3, 2, 3.
- crates/ail/tests/e2e.rs::std_either_list_demo: e2e count 34 → 35.
- docs/JOURNAL.md: Iter 15g entry.
Compiler bug surfaced (queued as 15g-aux, not fixed):
unify_for_subst in ailang-codegen/src/lib.rs accepts $u wildcards
only on the arg side. Mixing inline (Either Left n) and (Either
Right n) in a list literal lands $u on the param side via the
outer List<a>'s binding and errors. Reduced repro: `length [Left
1, Right 10]`. Demo works around with monomorphic mkleft/mkright
helpers; workaround documented inline. Fix is a one-line symmetric
extension of the early-return.
Tests: 94/94. Stdlib: 5 modules, 27 combinators.
After six feature iters since the last docs sweep, DESIGN.md had
visible drift. Patched in place rather than queueing the next
codegen-heavy iter against a stale spec.
DESIGN.md changes (+72 LOC):
- Decision 6: form (A) marked shipped (Iter 14c, sole projection
since 15e); body kept as audit trail.
- Pipeline: desugar pass added between resolve+hash and typecheck;
invariant noted that CheckedModule.symbols hashes from the
original module, not the desugared one (so ail diff/manifest
preserve on-disk identity).
- CLI: added deps, diff, workspace, builtins (shipped earlier but
never doc'd).
- "What is not (yet) supported": re-anchored from "end of Iter 13"
to "as of Iter 16a"; removed lifted gates (cross-module ADTs,
no-GC, flat-pattern-only); added tighter follow-up gates
(literal sub-patterns, local recursive let).
- "What IS supported": promoted nested Ctor patterns (16a),
cross-module ADTs (14h), form-(A) text surface (14b/14c/15e),
Boehm GC (Decision 9 / 14f) into the smoke-test list.
- Smoke tests: added std_list_demo, std_maybe_demo, std_either_demo,
std_pair_demo, nested_pat fixtures.
JOURNAL: 16a-aux entry recording the drift sites and what was
explicitly *not* changed (Goal, Decisions 1-5, 7-9, Mangling,
Convention, Data model, Verification — spot-checked, all current).
Tests: 93/93 unchanged (doc-only). Build clean.
Fourth stdlib module. Pair<a, b> is the canonical product with two
type vars and a single constructor MkPair. Five combinators: fst,
snd, swap, map_first (Pair<a, b> -> Pair<c, b>), map_second
(Pair<a, b> -> Pair<a, c>).
Smallest dogfood for the parameterised-ADT path so far: no
recursion in the data def or any combinator, single-arm matches
throughout. Demo prints 7, 9, 9, 7, 8, 18 deterministically.
No compiler bug surfaced (fourth stdlib iter in a row to land
clean). The only fixable issue was a paren-balance typo in the
demo's seq chain.
Cumulative: 4 stdlib modules, 24 combinators. Type-system surface
exercised end-to-end now spans 1/2/3-type-var data, 1/2/3-type-var
fns, recursive ADTs, cross-module imports of all of the above,
flat and nested patterns, TCO via monomorphised musttail, GC.
Tests: 93/93 (e2e 33 → 34).
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
Brummel