JOURNAL: Iter 18d.1 — Term::ReuseAs schema + linearity check
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).
This commit is contained in:
+127
@@ -6639,3 +6639,130 @@ a tag-overwrite + field-rewrite, eliding both the `@drop_` and
|
||||
the `@ailang_rc_alloc` calls. Inference identifies the cases
|
||||
where the rewrite is safe (the freed binder's last use is
|
||||
exactly here, the new ctor has the same shape, no aliasing).
|
||||
|
||||
## Iter 18d.1 — `Term::ReuseAs` schema + linearity check
|
||||
|
||||
Schema floor for explicit reuse hints. Adds `Term::ReuseAs
|
||||
{ source: Box<Term>, body: Box<Term> }` with serde tag
|
||||
`"reuse-as"` and form-A `(reuse-as <source> <body>)`. Schema
|
||||
shape (wrapper around a body, NOT a `reuse_from: Option<String>`
|
||||
modifier on `Term::Ctor`) and the substantive rationale were
|
||||
ratified in DESIGN.md before this iter shipped — see the
|
||||
"compositional flexibility" + "source-locality at the head"
|
||||
paragraph in Decision 10's schema-additions block.
|
||||
|
||||
Codegen is **identity** under every `--alloc` strategy — lower
|
||||
`body`, drop `source` on the floor. The same staging the 18c.1
|
||||
→ 18c.3 split used: schema floor first so authors can write the
|
||||
form, behaviour layered on later. Iter 18d.2 will replace the
|
||||
identity codegen with the in-place rewrite under `--alloc=rc`.
|
||||
|
||||
### User-visible diagnostics
|
||||
|
||||
The wrapper schema permits `Term::ReuseAs` around a body that
|
||||
isn't a constructor, which would be meaningless. Three
|
||||
diagnostics close that gap:
|
||||
|
||||
- **`reuse-as-non-allocating-body`** (typecheck) — `body` must
|
||||
be `Term::Ctor` or `Term::Lam` (the two AST shapes that
|
||||
allocate under `--alloc=rc`). A non-allocating body emits this
|
||||
diagnostic with `ctx = {"got": "<term-tag>"}` and a
|
||||
`suggested_rewrite` that drops the wrapper.
|
||||
|
||||
- **`reuse-as-source-not-bare-var`** (linearity) — `source`
|
||||
must be `Term::Var { name }` referring to an in-scope binder.
|
||||
Anything else (literal, nested expression, out-of-scope var)
|
||||
emits this with the same drop-the-wrapper suggested rewrite.
|
||||
This rule is enforced by the linearity check rather than by
|
||||
the typechecker because the constraint is about reuse
|
||||
semantics, not type well-formedness; placing it in the
|
||||
linearity pass also gates it on the all-explicit-mode
|
||||
activation rule, so back-compat fixtures are unaffected.
|
||||
|
||||
- **`use-after-consume`** (existing 18c.2 code, fired at a
|
||||
reuse-as site) — `source`'s named binder must not have been
|
||||
consumed earlier in the body. The fix is the same: drop the
|
||||
wrapper.
|
||||
|
||||
Visiting `Term::ReuseAs { source: Var { name }, body }` marks
|
||||
`name` as consumed for the rest of the body's walk, so a
|
||||
subsequent use of the same binder flags `use-after-consume`
|
||||
against it. The linearity check thereby enforces "reuse-as
|
||||
consumes the source exactly once".
|
||||
|
||||
### Why the "source not bare var" rule is in linearity, not typecheck
|
||||
|
||||
The schema permits `(reuse-as (some-expression) <body>)`
|
||||
syntactically. But reuse-as semantics says "free `source`'s
|
||||
slot, write `body` into it" — that only makes sense if
|
||||
`source` denotes a unique heap allocation we can name. A
|
||||
binder name is the AILang way to name a unique heap
|
||||
allocation; an arbitrary expression doesn't have that
|
||||
property. Forcing `source` to be `Term::Var` is a *use-rule*,
|
||||
not a *type-rule* — it's about the discipline of how reuse-as
|
||||
is composed, not about whether the wrapping expression
|
||||
typechecks. Linearity is where use-rules live.
|
||||
|
||||
This pattern matches Decision 1's "schema permits exactly what
|
||||
is meaningful" trade-off: the schema doesn't try to forbid
|
||||
non-var sources structurally; the linearity pass does, with a
|
||||
diagnostic the LLM author can act on.
|
||||
|
||||
### Uniqueness awareness
|
||||
|
||||
The 18c.3 uniqueness inference also walks `Term::ReuseAs` —
|
||||
`source` is treated as Consume (counts toward `consume_count`),
|
||||
`body` walks normally. The codegen consumer in 18d.2 will use
|
||||
this to know when the source is in fact unique at the reuse-as
|
||||
site (a precondition for the in-place rewrite to be safe).
|
||||
|
||||
### Test additions
|
||||
|
||||
- 4 surface parse-tests (round-trip, no-args rejection, one-arg
|
||||
rejection, full `parse_term` / `term_to_form_a` round-trip).
|
||||
- 1 typecheck unit test (`reuse_as_with_non_allocating_body_is_reported`).
|
||||
- 2 linearity unit tests (`reuse_as_with_non_var_source_is_reported`,
|
||||
`reuse_as_after_consume_is_use_after_consume`).
|
||||
- 1 integration test (`reuse_as_happy_path_in_map_inc_is_linearity_clean`)
|
||||
— exercises the canonical case: `(fn (own (con List)) → (own
|
||||
(con List)))` whose body is `(match xs (Nil → Nil) (Cons h t →
|
||||
(reuse-as xs (Cons (+ h 1) (map_inc t)))))`. Asserts no
|
||||
diagnostics.
|
||||
- 1 E2E test (`reuse_as_demo_is_identity_in_18d1`) — runs
|
||||
`examples/reuse_as_demo.ail.json` under `--alloc=gc` and
|
||||
asserts `9` (the sum of `[2, 3, 4]`).
|
||||
- New fixture `examples/reuse_as_demo.{ailx,ail.json}` — the
|
||||
canonical `map_inc`-via-reuse-as program. Identity codegen
|
||||
produces the same output as the non-reuse-as version, so the
|
||||
fixture's role in 18d.1 is to exercise the schema + linearity
|
||||
+ parser surface; 18d.2 will repurpose it as the in-place-
|
||||
rewrite IR-shape lock-in.
|
||||
|
||||
### Test deltas
|
||||
|
||||
- E2E: 55 → 56.
|
||||
- ailang-check unit: 43 → 46 (+3).
|
||||
- ailang-check workspace: 8 → 9 (+1).
|
||||
- surface: 14 → 18 (+4).
|
||||
- All other buckets unchanged.
|
||||
- `cargo test --workspace` green.
|
||||
- No existing fixture's canonical JSON changed —
|
||||
`Term::ReuseAs` is new, so no 18c-or-prior fixture serialises
|
||||
to a different byte-string.
|
||||
|
||||
### Next
|
||||
|
||||
Iter 18d.2: codegen lowers `Term::ReuseAs { source, body=Ctor }`
|
||||
under `--alloc=rc` to in-place tag-overwrite + field-rewrite,
|
||||
eliding the `ailang_rc_alloc` call AND the per-field-drop
|
||||
cascade for the source's old fields (the dec is replaced by
|
||||
unconditional store of the new field values; ownership of the
|
||||
old-field references must transfer to a per-field dec before
|
||||
the store, since the old slot's pointer-typed values would
|
||||
otherwise leak). Other allocators ignore the wrapper (same
|
||||
identity behaviour as 18d.1 ships universally).
|
||||
|
||||
Adds the `reuse-as-shape-mismatch` diagnostic when codegen
|
||||
discovers the source's ctor and the body's ctor have
|
||||
different sizes / layouts (only checkable once codegen has
|
||||
resolved both ctors' field counts).
|
||||
|
||||
Reference in New Issue
Block a user