From 5b66de77ac8ea58674b4841b48a21fc623ef5fbd Mon Sep 17 00:00:00 2001 From: Brummel Date: Fri, 29 May 2026 16:45:47 +0200 Subject: [PATCH] =?UTF-8?q?spec:=20intrinsic-bodies=20=E2=80=94=20revise?= =?UTF-8?q?=20AST=20repr=20to=20Term::Intrinsic=20leaf=20(refs=20#9)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Forward-fix on c42034b. plan-recon for intrinsic-bodies.1 surfaced that the original AST representation — FnDef.body / Term::Lam.body made Option plus an `intrinsic: bool` flag — has a ~150-site blast radius across six crates: every body read/construct site breaks when a mandatory public field goes optional. That blast radius is the signal (CLAUDE.md design-rationale rule) that the representation was wrong, not merely expensive. The Form-A surface (user's chosen Approach 1) and the Local-Reasoning semantics (Design X marker placement) are UNCHANGED. Only the internal AST representation changes, which is orchestrator authority over AST design. New representation: a single new leaf Term variant, Term::Intrinsic ({ "t": "intrinsic" }), is the body of a compiler-supplied definition. FnDef.body (Term) and Term::Lam.body (Box) keep their existing types. A def is intrinsic iff matches!(body, Term::Intrinsic). Three structural reasons (not effort): 1. Established pattern. The project adds new constructs as additive Term variants — Term::New, Term::Loop, Term::Recur, Term::Clone, Term::ReuseAs all landed this way, documented "strictly additive, pre-existing fixtures hash bit-identically" in design/contracts/0002-data-model.md. Term::Intrinsic follows it. Option A introduced a brand-new pattern (mandatory field → optional) absent from the schema. 2. Meaning at the right locus. "This body is compiler-supplied" is a property of the body, not the container. Term::Intrinsic sits at the body position — fn body, or instance-method lambda body (Design X local-signature placement preserved exactly). 3. Illegal state unrepresentable. Option A admitted intrinsic:true with body:Some(...), forcing an intrinsic-with-body reject. Under the variant a body is either Term::Intrinsic or a real term, never both — the reject is deleted, the state cannot occur. This is the same make-illegal-states-unrepresentable discipline as the honesty theme the milestone exists to serve. Blast radius collapses from ~150 body-read/construct sites to the exhaustive match-on-Term arms (canonical/hash/visit + schema_coverage), which the no-wildcard Term match turns into compile errors until each gains a Term::Intrinsic case — the project's normal new-variant discipline. Sections revised: § Architecture points 1/3/4, § Concrete code shapes (Implementation shape now shows the leaf variant, not the Option+flag), § Components, § Data flow, § Error handling (the intrinsic-with-body row removed), § Testing strategy (the both-body-and-intrinsic reject test removed; schema_coverage Term::Intrinsic observation added). The scheme/ail surface examples are byte-unchanged. Re-ran the brainstorm gates on the revision: Step-7 parse gate green (both ail blocks exit 0, unchanged); Step-7.5 grounding-check PASS on the four new load-bearing claims (additive-variant precedent + contract wording, exhaustive-Term-match mechanism, mono.rs synthesise_mono_fn destructure unchanged under preserved body type, Term::Recur as non-reducing-leaf precedent). --- docs/specs/0055-intrinsic-bodies.md | 178 +++++++++++++++++----------- 1 file changed, 106 insertions(+), 72 deletions(-) diff --git a/docs/specs/0055-intrinsic-bodies.md b/docs/specs/0055-intrinsic-bodies.md index 5a1ef26..e20aa96 100644 --- a/docs/specs/0055-intrinsic-bodies.md +++ b/docs/specs/0055-intrinsic-bodies.md @@ -54,25 +54,50 @@ Three landing points, two iterations. **Iteration `intrinsic-bodies.1` — the mechanism.** -1. **AST.** `FnDef.body` and `Term::Lam.body` become *optional*; a - new `intrinsic: bool` flag rides each. `intrinsic: true` ⟺ - `body` absent. The flag is additive and `skip_serializing_if`-gated, - so every existing fixture's canonical-JSON hash stays bit-identical - (the standard additive-schema pattern, `design/contracts/0002-data-model.md`). -2. **Form-A surface.** Parser accepts `(intrinsic)` as a sibling - attribute to `(body ...)` inside both `fn-def` and `lam`; the - printer emits it. Round-trip (`parse ∘ print = id`) holds by the - standard fixture gate. -3. **Checker.** An `(intrinsic)` definition type-checks against its - *signature only* — there is no body to check. Two new rejects: - (a) a definition carrying **both** a body and `intrinsic` is - malformed; (b) an `(intrinsic)` definition outside a `(kernel)`-tier - module or the prelude is rejected with `intrinsic-outside-kernel-tier`. -4. **Codegen.** An `(intrinsic)` definition routes through - `intercepts::lookup`; if no intercept is registered for its - mangled name, codegen emits the existing deferral diagnostic. - The current "lower the body" path is simply not taken for these - definitions. +1. **AST.** A new leaf term variant `Term::Intrinsic` is the body of + a compiler-supplied definition. `FnDef.body` and `Term::Lam.body` + keep their existing types (`Term` / `Box`) — they are not made + optional. A definition is intrinsic iff its body *is* + `Term::Intrinsic`. The variant is strictly additive: a fixture that + does not use it serialises bit-identically (the established + additive-term-variant pattern — `Term::New`, `Term::Loop`, + `Term::Recur`, `Term::Clone`, `Term::ReuseAs` all landed this way, + `design/contracts/0002-data-model.md`). This is the load-bearing + representation choice: it puts "this body is compiler-supplied" at + the body position where it semantically belongs, keeps the + ~150-site `body`-read/construct surface across six crates untouched + (only exhaustive `match`-on-`Term` arms gain a case), and makes the + illegal "body AND intrinsic" state *unrepresentable* rather than + rejected — a body is either `Term::Intrinsic` or a real term, never + both. (The rejected alternative, `body: Option` + an + `intrinsic: bool` flag, splits one fact across two fields, admits + that illegal state, and breaks every `body` consumer in the + workspace.) +2. **Form-A surface.** For a top-level fn, the parser accepts + `(intrinsic)` as a sibling clause where `(body ...)` would go and + maps it to `body = Term::Intrinsic`; the printer emits `(intrinsic)` + in that slot when the body is `Term::Intrinsic`. For a lambda, + `(intrinsic)` sits at the positional body slot (where the body term + goes today) and parses to `Term::Intrinsic`; the printer emits it + there. Round-trip (`parse ∘ print = id`) holds by the standard + fixture gate. The fn-vs-lam surface asymmetry mirrors the existing + one (a fn carries a named `(body X)` clause; a lambda carries its + body positionally) — `(intrinsic)` follows each form's existing body + placement. +3. **Checker.** A definition whose body is `Term::Intrinsic` + type-checks against its *signature only* — there is no body term to + infer. One new reject: an intrinsic definition outside a + `(kernel)`-tier module or the prelude is rejected with + `intrinsic-outside-kernel-tier`. (There is no `intrinsic-with-body` + reject — the representation makes that state impossible, see point 1.) +4. **Codegen.** A definition whose body is `Term::Intrinsic` routes + through `intercepts::lookup`; if no intercept is registered for its + mangled name, codegen emits the existing deferral diagnostic. The + current "lower the body" path is not taken for these definitions — + `lower_term` is never called on a `Term::Intrinsic` body (and a + `Term::Intrinsic` reaching `lower_term` through any other path is a + codegen-internal error, since an intrinsic body must be consumed by + the intercept route). 5. **Ratifier.** One throwaway intrinsic in the `kernel_stub` fixture — a nullary `answer : () -> Int` whose intercept emits `ret i64 42` — drives the mechanism end-to-end (parse → check → @@ -178,30 +203,32 @@ error: [surface-parse-error] parse error in fn-def: unknown fn attribute ### Implementation shape (secondary — the AST delta) -Before → after on the two load-bearing structs. Exact bytes are the +The change is one new leaf `Term` variant. Exact bytes are the planner's job; this fixes the shape only. -`FnDef` (`crates/ailang-core/src/ast.rs`): +`Term::Intrinsic` (`crates/ailang-core/src/ast.rs`): ```jsonc -// before -{ "kind": "fn", "name": "...", "type": Type, "params": [...], "body": Term, ... } - -// after — body optional, intrinsic flag additive -{ "kind": "fn", "name": "...", "type": Type, "params": [...], - "body": Term, // present ⟺ intrinsic absent/false - "intrinsic": true, // optional; omitted when false (hash-stable when omitted). - // When true: body MUST be absent; the def is legal only in a - // (kernel)-tier module or the prelude; codegen routes through - // intercepts::lookup on the mangled name. - ... } +// new leaf term — the body of a compiler-supplied definition. +// Strictly additive (no skip_serializing_if needed; a fixture that +// does not carry it hashes bit-identically — the same additive-variant +// pattern as Term::New / Term::Loop / Term::Recur / Term::Clone). +// Never reduces to a value: codegen consumes it via intercepts::lookup, +// the typechecker treats a def with this body as signature-only. +{ "t": "intrinsic" } ``` -`Term::Lam` (same crate) takes the symmetric pair: `body` becomes -optional, `intrinsic: bool` is added. An instance method whose body -is a lambda (every `eq`/`compare` instance) carries the marker on the -*lambda body*, **not** on the method as a whole — and this placement -is load-bearing, not incidental. +`FnDef.body` (currently `Term`) and `Term::Lam.body` (currently +`Box`) are **unchanged in type** — they simply may now hold +`Term::Intrinsic`. A top-level intrinsic fn is +`FnDef { body: Term::Intrinsic, .. }`; an intrinsic instance-method +lambda is `Term::Lam { body: Box::new(Term::Intrinsic), .. }`. "Is +this definition intrinsic?" is `matches!(body, Term::Intrinsic)`. + +The marker sits at the body position — for a top-level fn that is the +fn body; for an instance method that is the *lambda body*, **not** the +method as a whole — and this placement is load-bearing, not +incidental. The reason is local reasoning (`design/INDEX.md` § Goal: "every definition carries its full type and effect set, so a signature can @@ -217,64 +244,71 @@ are the parameter types and return type, readable at the definition site. Hoisting the marker to the method (`(method eq (intrinsic))`) would erase that local signature — a reader would have to climb to the `Eq` class declaration and substitute `a := Int` mentally to -recover it. So the marker replaces the lambda's *body*, leaving the -lambda's typed shell — the local signature — in place. The mono pass -(`crates/ailang-check/src/mono.rs::synthesise_mono_fn`) already reads -the method's parameter names and inner body out of this lambda; the -intrinsic marker rides where the dummy body sits today, so that path -is unchanged. +recover it. So the marker is the lambda's *body* (`Term::Intrinsic`), +leaving the lambda's typed shell — the local signature — in place. The +mono pass (`crates/ailang-check/src/mono.rs::synthesise_mono_fn`) +already reads the method's parameter names and inner body out of this +lambda (`Term::Lam { params, body, .. } => (params, *body)`); with the +inner body being `Term::Intrinsic`, the synthesised `FnDef` carries +`body: Term::Intrinsic` and is itself intrinsic. The destructure +itself is unchanged — only what the inner body *is* differs. -Serde note: `Option` serialises `Some(t)` as `t` (not as a -tagged wrapper), so a non-intrinsic def's `"body": {...}` is -byte-identical before and after. `None` is `skip_serializing_if`-omitted. -This is what keeps every existing fixture's hash stable; the -`design_schema_drift.rs` schema mirror and the `0002-data-model.md` -contract move in the same iteration as the struct change. +Hash-stability note: `Term::Intrinsic` is a new enum variant, not a +new field, so a fixture that does not use it serialises exactly as +before — the same mechanism that kept hashes stable when `Term::New`, +`Term::Loop`, and `Term::Recur` were added. The `design_schema_drift.rs` +schema mirror, the `schema_coverage.rs` variant corpus (a fixture must +now exercise `Term::Intrinsic`), and the `0002-data-model.md` contract +all move in the same iteration as the variant. ## Components | Component | Iteration | Change | |---|---|---| -| `crates/ailang-core/src/ast.rs` | .1 | `FnDef.body` / `Lam.body` → optional; `intrinsic: bool` added to both. | -| `crates/ailang-core` canonical/hash/visit | .1 | Visitors gain an explicit intrinsic arm (no body to walk). Schema-coverage corpus extended. | -| `crates/ailang-surface` (lex/parse/print) | .1 | `(intrinsic)` attribute parsed + printed in `fn-def` and `lam`; round-trip gated. | -| `crates/ailang-check/src/lib.rs` | .1 | Intrinsic def checks signature-only; rejects body+intrinsic; rejects intrinsic outside kernel-tier/prelude (`intrinsic-outside-kernel-tier`). | -| `crates/ailang-codegen/src/lib.rs` | .1 | Intrinsic def routes through `intercepts::lookup`; body-lowering path not taken for it. | +| `crates/ailang-core/src/ast.rs` | .1 | New leaf variant `Term::Intrinsic`. `FnDef.body` / `Lam.body` types unchanged. | +| `crates/ailang-core` canonical/hash/visit | .1 | Exhaustive `match`-on-`Term` arms gain a `Term::Intrinsic` case (leaf, no sub-terms to walk). Schema-coverage corpus extended to exercise it. | +| `crates/ailang-surface` (lex/parse/print) | .1 | `(intrinsic)` parsed + printed: as a body-slot clause in `fn-def`, at the positional body slot in `lam`; maps to/from `Term::Intrinsic`; round-trip gated. | +| `crates/ailang-check/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` checks signature-only; rejects intrinsic outside kernel-tier/prelude (`intrinsic-outside-kernel-tier`). No `intrinsic-with-body` reject — the representation forbids that state. | +| `crates/ailang-check/src/mono.rs` | .1 | `synthesise_mono_fn` lambda-destructure unchanged; an inner `Term::Intrinsic` body flows through to an intrinsic synthesised `FnDef`. | +| `crates/ailang-codegen/src/lib.rs` | .1 | A def whose body is `Term::Intrinsic` routes through `intercepts::lookup`; `lower_term` is never called on it. | | `crates/ailang-kernel-stub` + `ailang-surface` parse hop | .1 | `answer` smoke intrinsic added to the stub fixture; its intercept registered. | | `examples/prelude.ail` | .2 | 18 dummy bodies → `(intrinsic)`. | | `crates/ailang-codegen/src/intercepts.rs` (pin) | .2 | `registry_contains_all_legacy_arms` upgraded to a source↔registry bijection pin. | | codegen dummy-body path | .2 | Removed. | -| `design/contracts/0002-data-model.md` | .1 | `fn` + `lam` schema gain `intrinsic`; `body` documented optional. | +| `design/contracts/0002-data-model.md` | .1 | New `{ "t": "intrinsic" }` Term entry; note in `fn`/`lam` that the body may be `Term::Intrinsic`. | | `design/contracts/0007-honesty-rule.md` | .2 | The prelude-dummy infraction is closed; note its resolution if the contract references it. | ## Data flow Authoring → parse → AST → check → codegen, unchanged in topology; -the intrinsic flag is read at three of those stations: +`Term::Intrinsic` is recognised at three of those stations: -1. **Parse.** `(intrinsic)` sets `intrinsic = true`, leaves `body = None`. - A `fn-def`/`lam` carrying both `(body ...)` and `(intrinsic)` is a - parse-level malformation (or a check-level one — planner picks the - station; the reject must exist). -2. **Check.** Intrinsic def: validate the signature, skip body - inference. Enforce the kernel-tier/prelude scope. The module's - `kernel: true` flag (or prelude identity) is already available to - the checker via the loaded workspace. -3. **Codegen.** Intrinsic def: `intercepts::lookup(mangled_name)`. - Hit → emit the intercept. Miss → the existing deferral diagnostic - (same one raw-buf.2 reuses for unregistered `RawBuf` ops). +1. **Parse.** `(intrinsic)` in a fn body slot or a lambda body slot + produces a `Term::Intrinsic` body. There is no "both body and + intrinsic" surface form to reject — the grammar offers one body + slot, and `(intrinsic)` either fills it or it does not. +2. **Check.** A def whose body is `Term::Intrinsic`: validate the + signature, skip body inference. Enforce the kernel-tier/prelude + scope. The module's `kernel: true` flag (or prelude identity) is + already available to the checker via the loaded workspace. +3. **Codegen.** A def whose body is `Term::Intrinsic`: + `intercepts::lookup(mangled_name)`. Hit → emit the intercept. + Miss → the existing deferral diagnostic (same one raw-buf.2 reuses + for unregistered `RawBuf` ops). ## Error handling | Condition | Diagnostic | Station | |---|---|---| -| `(intrinsic)` and `(body ...)` on the same def | `intrinsic-with-body` (malformed) | parse or check | | `(intrinsic)` in a non-kernel, non-prelude module | `intrinsic-outside-kernel-tier` | check | | Intrinsic def with no registered intercept | existing codegen deferral | codegen | -The middle row is the honesty-rule guard at the workspace boundary: +The first row is the honesty-rule guard at the workspace boundary: user code cannot mark a body as compiler-supplied, so the lie cannot -re-enter through user modules. +re-enter through user modules. (There is deliberately no +"body-and-intrinsic" row — `Term::Intrinsic` is a body, so a def +either has it or has a real body, never both. The illegal state is +unrepresentable, not diagnosed.) ## Testing strategy @@ -286,11 +320,11 @@ re-enter through user modules. - Check accept: the `kernel_stub` `answer` intrinsic checks clean. - Check reject (scope): a user module with an `(intrinsic)` fn is rejected with `intrinsic-outside-kernel-tier`. -- Check reject (malformed): a def with both body and intrinsic is rejected. - E2E: `answer` builds and runs, exit/print observing `42` — the mechanism works from source to native. - Schema drift: `design_schema_drift.rs` green against the new - `0002-data-model.md`. + `0002-data-model.md`; `schema_coverage.rs` observes `Term::Intrinsic` + in the fixture corpus. **intrinsic-bodies.2:**