From b4abf356dd92b22ba959135ae5ede5b49d30e58d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20L=C3=BCning?= Date: Tue, 20 Oct 2026 10:54:48 +0200 Subject: [PATCH] defk-rt2.11: the rest of the typing stays twice (ADR-0008 extended); drop Elixir mode's dead ctx write The spike found the seam (a node id stamped after desugar keys 99.2% of Elixir mode's typings to the compiler's, C unchanged) but not the case for it: the u64 accumulator inference decides results, so sharing it retires the oracle's check, and the rest gains about 20 lines. ADR-0008 records this and how to revisit it. ElixirMode.definitions/3 set the compiler ctx's file, which nothing on its path reads: it is definitions/2 now. --- docs/adr/0006-public-api-surface.md | 2 +- ...8-builtin-typing-shared-semantics-twice.md | 42 ++++++++++++++++++- docs/agents/compiler-map.md | 2 +- lib/defk.ex | 2 +- lib/defk/elixir_mode.ex | 24 +++++------ test/compiler_ctx_test.exs | 6 +-- 6 files changed, 57 insertions(+), 21 deletions(-) diff --git a/docs/adr/0006-public-api-surface.md b/docs/adr/0006-public-api-surface.md index 8d718b0d..b3457de3 100644 --- a/docs/adr/0006-public-api-surface.md +++ b/docs/adr/0006-public-api-surface.md @@ -65,7 +65,7 @@ above. | `Defk.Test.reason/1` | `@doc` in hidden module | tests 9 | **public** | what "same reason" means in agreement; users need it to assert a raise. Rename candidate | | `Defk.Case.in_both_modes/1` (macro) | hidden module | tests 2 | **hidden** | see open question 4 | | `Defk.ElixirMode.with_mode/2` | `@doc` | tests 6, 1 example, README, `language.md` | **public** | the documented per-process switch | -| `Defk.ElixirMode.setup!/4`, `native_name/1`, `process_mode_key/0`, `definitions/3`, `fun_name/1` | `@doc false` | `Defk` at compile time | **hidden** | | +| `Defk.ElixirMode.setup!/4`, `native_name/1`, `process_mode_key/0`, `definitions/2`, `fun_name/1` | `@doc false` | `Defk` at compile time | **hidden** | | | `Defk.Bits.wrap64/1`, `mulhi/2`, `clz/1`, `ctz/1`, `popcount/1`, `rotl64/2`, `rotr64/2`, `clz/2`, `ctz/2`, `rotl/3`, `rotr/3`, `f64_to_u64/1` (12) | `@doc`, `@spec`, doctests | Elixir mode, tests, `language.md` | **public** | each is a kernel builtin's meaning; renaming one is a language change | | `Defk.Report.print/1` | `@doc`, `@spec` | 1 test, 1 example, README, `performance.md`, `fast-path-report.md` | **public** | the way to read the report | | `Defk.Report.format/1` | `@doc`, `@spec` | `print/1` | **public** | the same text as a string (for tests and tools) | diff --git a/docs/adr/0008-builtin-typing-shared-semantics-twice.md b/docs/adr/0008-builtin-typing-shared-semantics-twice.md index 62410cbb..1dff597f 100644 --- a/docs/adr/0008-builtin-typing-shared-semantics-twice.md +++ b/docs/adr/0008-builtin-typing-shared-semantics-twice.md @@ -1,7 +1,8 @@ # ADR-0008: Builtin typing is shared data; builtin semantics are written twice on purpose - Date: 2026-10-12 -- Status: accepted (2026-10-12, maintainer, architecture review grilling) +- Status: accepted (2026-10-12, maintainer, architecture review grilling); + extended 2026-10-20 (the rest of the typing, below) - Source: /improve-codebase-architecture session 2026-10-12; evidence in the review of `Defk.Compiler.builtin/4` and `Defk.ElixirMode.builtin/4` @@ -45,3 +46,42 @@ remains defined as same exception module for the same reason.) exist and agree. - Anyone proposing to generate the Elixir emissions (or `Ops` bodies) from the table should be pointed here: it would silently retire the oracle. + +## Extension (2026-10-20): the rest of the typing also stays twice + +- Status: accepted (2026-10-20, maintainer) +- Source: the spike `defk-rt2.11` (its ticket comment has the numbers) + +Beyond the builtins, Elixir mode types every node again: `expr/2` +returns `{quoted, type}`, and the u64 accumulator inference +(`settle_accs/3`, `note_u64_mix/3`) is a hand copy of the compiler's +`u64_accs/2`. The spike asked whether the compiler could hand Elixir mode +its node types, so that Elixir mode only emits. + +The seam exists. The compiler runs first, on the same desugared kernels, +and a unique id stamped into each node's meta keys a node (a line and a +column do not: a kernel built by a macro has no columns). The stamp left +the C of every test and example module byte-identical, and 99.2% of +Elixir mode's 58,361 keyed node typings equalled the compiler's own. The +rest are four special cases: `bitstring` and `[u8]` naming, nodes the +compiler types twice (u64 retries, `in` guards), float trees that do not +pass `lower_expr`, and helpers that are only inlined. + +Decision: Elixir mode keeps its own typing. Two reasons: + +- The u64 accumulator inference is semantics, not typing: it decides the + result. `3 - 5` on a u64 accumulator raises, on an i64 one it is `-2`. + Shared, an inference error in the compiler would pass every agreement + test, which is what the decision above forbids. +- Without that part the gain is about 20 lines (`body_type/3`, the + `leaf_types` look ahead). `expr/2`'s types and `trial/1` stay in any + case, as the emission and the write discovery use them. The cost is a + stamping step, type records in several lowering paths, the four special + cases, and an Elixir mode that depends on the compiler's lowering + instead of the AST. + +## How to revisit + +A proposal to share node types with Elixir mode answers both reasons: an +independent check of the u64 accumulator inference, and a gain larger than +the four special cases and the coupling. diff --git a/docs/agents/compiler-map.md b/docs/agents/compiler-map.md index 5e6379c0..6969dbb1 100644 --- a/docs/agents/compiler-map.md +++ b/docs/agents/compiler-map.md @@ -120,7 +120,7 @@ of rows the lowering declares as it emits; defk-ch4), not from the C text. Its translation state (binding counter, writes log, look-ahead leaf types, u64 candidates and hits) is one process-dictionary key, `:defk_em`, holding one `Defk.ElixirMode.State`, fresh per kernel and deleted when - `definitions/3` returns; the `env` map (vars, sigs) is threaded + `definitions/2` returns; the `env` map (vars, sigs) is threaded explicitly. `lib/defk/elixir_mode/guard.ex` evaluates a case guard that can fail. - `lib/defk/inline_size.ex`: the code-size warning (defk-6ag). diff --git a/lib/defk.ex b/lib/defk.ex index 7362cfff..ca69d1ec 100644 --- a/lib/defk.ex +++ b/lib/defk.ex @@ -458,7 +458,7 @@ defmodule Defk do sigs = Enum.reject(all_sigs, &Defk.Bitstring.helper?/1) elixir_mode = - if elixir?, do: Defk.ElixirMode.definitions(kernels, all_sigs, env.file), else: [] + if elixir?, do: Defk.ElixirMode.definitions(kernels, all_sigs), else: [] Defk.Generated.defs( placement: placement, diff --git a/lib/defk/elixir_mode.ex b/lib/defk/elixir_mode.ex index 198b847f..c8d8f5f7 100644 --- a/lib/defk/elixir_mode.ex +++ b/lib/defk/elixir_mode.ex @@ -146,20 +146,16 @@ defmodule Defk.ElixirMode do @doc false # Quoted definitions: `__defk_elixir__/2` and one private function per kernel. - def definitions(raw_kernels, sigs, file) do - # the compiler's ctx keeps the file for the rejections this translation - # raises (err! reads it); the translation's own state is `@state`, gone - # when this returns - Defk.Compiler.Ctx.set(:file, file) + # The translation's state is `@state`, gone when this returns; it never + # reads the compiler's ctx (a rejection reaching it raises plainly, + # raise_form!/4). + def definitions(raw_kernels, sigs) do + by_key = Map.new(sigs, &{{&1.name, &1.arity}, &1}) - try do - by_key = Map.new(sigs, &{{&1.name, &1.arity}, &1}) - - Enum.zip_with(raw_kernels, sigs, fn raw, sig -> kernel(raw.body, sig, by_key) end) - |> definitions_of(sigs) - after - Process.delete(@state) - end + Enum.zip_with(raw_kernels, sigs, fn raw, sig -> kernel(raw.body, sig, by_key) end) + |> definitions_of(sigs) + after + Process.delete(@state) end defp definitions_of(kernels, sigs) do @@ -204,7 +200,7 @@ defmodule Defk.ElixirMode do # holding one struct (as the compiler's :defk_ctx): the binding counter, # the writes log (write tracking), the leaf types a reduce_while look # ahead collects, and the u64 candidates and hits of settle_accs/3. Fresh - # per kernel, deleted when definitions/3 returns. The `env` map (vars, + # per kernel, deleted when definitions/2 returns. The `env` map (vars, # sigs) is threaded explicitly; this is the rest. defmodule State do diff --git a/test/compiler_ctx_test.exs b/test/compiler_ctx_test.exs index 78c0e6bf..b99fa73a 100644 --- a/test/compiler_ctx_test.exs +++ b/test/compiler_ctx_test.exs @@ -34,8 +34,8 @@ defmodule Defk.CompilerCtxTest do # Elixir mode's translation keeps its own state the same way, in one key # (:defk_em) holding one struct, fresh per kernel and gone when - # definitions/3 returns: no translation state outlives a compile either. - test "after ElixirMode.definitions/3, the ctx is still the only defk-prefixed key" do + # definitions/2 returns: no translation state outlives a compile either. + test "after ElixirMode.definitions/2, the ctx is still the only defk-prefixed key" do for k <- defk_keys(), do: Process.delete(k) kernel = %{ @@ -55,7 +55,7 @@ defmodule Defk.CompilerCtxTest do } {_c, sigs, _report} = Defk.Compiler.compile(Defk.CompilerCtxTest.E, [kernel], nil) - defs = Defk.ElixirMode.definitions([kernel], sigs, "ctx_test.ex") + defs = Defk.ElixirMode.definitions([kernel], sigs) assert match?([_ | _], defs) assert defk_keys() == [:defk_ctx]