diff --git a/docs/README.md b/docs/README.md index dc5922f..4cb8e06 100644 --- a/docs/README.md +++ b/docs/README.md @@ -55,9 +55,11 @@ built the redefinition emitter, `handoffs/HANDOFF-x86-aggregates.md` took that a information, and `handoffs/HANDOFF-x86-cost.md` measured what the backend costs and set the survey running on its own so a refusal cannot sit unnoticed again. -The other four sessions are unrelated to each other. `handoffs/HANDOFF-arith.md` is why a divide by zero is a condition +The other six sessions are unrelated to each other. `handoffs/HANDOFF-arith.md` is why a divide by zero is a condition rather than a `SIGFPE`. `handoffs/HANDOFF-raylib-ports.md` is the running record of the last two raylib example -ports, whose lasting findings were folded into `PORTING.md`. `handoffs/HANDOFF-devtest-noise.md` is the linker +ports, whose lasting findings were folded into `PORTING.md`, and `handoffs/HANDOFF-cimport-ptr.md` is the arm +`cimport.ml`'s header check had been promising in a comment and not implementing — which is what those two ports +found, worked around and wrote up. `handoffs/HANDOFF-devtest-noise.md` is the linker error `dune test` used to print on every run. `handoffs/HANDOFF-emacs-flake.md` is the `test_emacs` flake that turned out to be `SIGPIPE` killing the daemon mid-reply, and it is worth reading for the two mechanisms it rules out as much as for the one it found. `handoffs/HANDOFF-tidy.md` is this reorganisation. diff --git a/docs/handoffs/HANDOFF-cimport-ptr.md b/docs/handoffs/HANDOFF-cimport-ptr.md index e082247..b88efd5 100644 --- a/docs/handoffs/HANDOFF-cimport-ptr.md +++ b/docs/handoffs/HANDOFF-cimport-ptr.md @@ -1,47 +1,132 @@ # Handoff — the pointer arm `agrees` already promised `lib/cimport.ml`'s `agrees` decides whether a hand-written `declare-c` and the C header -say the same thing. Its comment has always listed three differences that are "expected and -are not reported"; the code implements two of them. The missing one — *a `(Ptr T)` where +say the same thing. Its comment had always listed three differences that are "expected and +are not reported"; the code implemented two of them. The missing one — *a `(Ptr T)` where the header says `T *`* — is what `../PORTING.md` §A.1 and §A.2 ran into, and it is why -`GetCodepointPrevious` cannot be bound honestly and why `UpdateTexture` has to be handed +`GetCodepointPrevious` could not be bound honestly and why `UpdateTexture` had to be handed `(addr (.r (at (slice-from-ptr pixels n) 0)))`. -This file is the running record of building that arm. +The arm is built. This file is the record of what it accepts, what it still refuses, and +the one thing that turned out not to be its fault. -## The plan +## What the arm is -1. A `ptr_agrees` beside `agrees`, consulted only at the two `declare-c` sites in - `diff_bound`, where the C spelling is still in hand. `agrees` itself is left alone: - `check_structs` uses it for field *widths*, and loosening it there is the hazard the - check exists to catch. -2. Breadth, decided rather than fallen into — see "What it accepts" below. -3. Rewrite the comment at `lib/cimport.ml:1291` so it describes the code instead of - promising it, and take the rotting binding count out of it. -4. Use it: `get-codepoint-previous-raw` in `vendor/raylib/raylib.flan`, and the - `(Ptr Color)` binding for `UpdateTexture`. Delete both workarounds. -5. `docs/PORTING.md` §A.1 and §A.2 annotated closed in the file's existing style. +`ptr_agrees` and `agrees_c` beside `agrees` in `lib/cimport.ml`, consulted only from the +two `declare-c` sites in `diff_bound`. It takes the **C spelling** and not only the +rendered Flan type, because by the time a parameter has been rendered the header's word is +gone: `param_ty` turns `const char *` into `string` and `value_ty` turns `void *` into +`(Ptr u8)`, and neither of those is what the header said. A hand-written line that +disagrees with a rendering is not disagreeing with the header, and that distinction is the +whole of the arm. -## What it accepts (to be confirmed as it is built) +`agrees` itself is untouched. `check_structs` uses it for field **widths**, and a struct +field is about layout — every pointer in a struct is one word whatever it points at — so +widening it there would buy nothing and would cost the discipline the field check exists +to keep. + +## What it accepts - `(Ptr T)` against a C `T *` for the same `T`. -- `(Ptr u8)` against `char *` — a byte is a byte, and the two spellings of one are not a - width disagreement. Scoped to the pointee, never to `agrees` at large. -- `(Ptr T)` for any `T` against `void *`. `value_ty` already *invents* `(Ptr u8)` for a - `void *`, so the check as it stands enforces cimport's own guess as if the header had - said it. -- `const` does not enter into it, because a non-const `char *` parameter makes `param_ty` - refuse and `diff_bound` skips a parameter it cannot render at all. +- `(Ptr u8)` against `char *` and `const char *`. Inside a pointer, `char` and + `unsigned char` are two spellings of one byte and the package uses `(Ptr u8)` for both. + The `i8`/`u8` tolerance is the **pointee's** and not the world's; as a scalar or a field + the two are still a real disagreement, and there is a test for that. +- `(Ptr T)` for **any** `T` against `void *` and `const void *`. This is the judgement + call and the reason is sharper than "it is opaque": `value_ty` *invents* the `(Ptr u8)` + it renders a `void *` as, so the check without this arm was enforcing cimport's own guess + as if the header had said it. What is **not** given up is that it is a pointer at all — + the Flan side must still be a `(Ptr _)`, so an `i32` or a `string` declared against a + `void *` is still a finding. raylib spells thirty-odd parameters `void *` and none of + them is a scalar. +- `(Ptr Key)` against a header's `int *`, through the existing enum arm. The same four + bytes through a pointer as beside one. -## What it still refuses +## What it refuses -- `(Ptr A)` against `B *` for different named `A` and `B`. -- Anything that is not a pointer on the Flan side against a C pointer, and the reverse. +- `(Ptr A)` against `B *` for different named `A` and `B`. Two structs of the same size + are still two different structs. +- Anything that is not a pointer on the Flan side against a C pointer, `void *` included. +- Everything `agrees` already refused, unchanged. -## Status +## What `const` does here: nothing, and the reason is invisible -- [ ] the arm -- [ ] the comment -- [ ] tests, positive and negative -- [ ] the two raylib bindings -- [ ] PORTING.md +Worth writing down because reading the code does not show it. A non-const `char *` +parameter makes `param_ty` **refuse**, and `diff_bound`'s `| None -> None` means a +parameter the importer cannot render at all is *skipped rather than compared*. So a +hand-written `(Ptr u8)` over a `char *` has always passed — unexamined, not approved. Only +`const char *` ever reaches the comparison, and that is the case the arm exists for. The +rewritten comment at the head of `diff_bound` now says so. + +## The comment at `lib/cimport.ml:1291` + +Rewritten from a promise into a description. The count it carried — "176 `declare-c` +lines", against a real 196 — is gone rather than corrected, and the comment says why a +census written beside a growing file is not a thing to maintain. `vendor/raylib/headers` +carried the same rot ("425 declarations … 172 hand-written", really 463 and 196) and got +the same treatment. + +## Then it was used + +**§A.1 came out entirely, and it is the arm's own case.** +`vendor/raylib/raylib.flan` has `get-codepoint-previous-raw` — `(Ptr u8)` over a +`const char *`, which is precisely what the arm was missing — and a `get-codepoint-previous` +wrapper that takes the bytes and an offset and builds the interior pointer itself. +`generated.flan` no longer carries the `string`-faced version: a binding that is wrong for +the only direction it reads in is worse than no binding, and the hand-written declaration +suppresses the generated one by C symbol. `examples/text-codepoints-loading.flan`'s +`step-back` is one call to it; the continuation-byte walk and `continuation?` are deleted. +The answer is 12356 and 3, verified by running it. + +`test/programs/raylib-codepoints.flan` would have caught the old answer, verified by +perturbation rather than by argument: make `step-back` set `size` to 0 — which is exactly +what the broken string call produced — and both rows go red, because the backward walk +never reaches offset 0 and runs off the end of its array. + +**§A.2's call site came out; the cast moved rather than vanished.** The header check does +accept the `(Ptr Color)` binding now. What the header check was masking is that +`lib/shim.ml:651` refuses a second `declare-c` for a C symbol the package already binds, +and that rule is right: a shim emits one C prototype per declaration, and two prototypes +for `UpdateTexture` that disagree about a parameter type is a C file that does not compile. +Its message says what to write instead — "another Flan name for it is a defn" — so +`raylib.flan` has `update-texture-colors`, a one-line defn over the generated +`update-texture`: + +```flan +(defn update-texture-colors [texture Texture2D pixels (Ptr Color)] () + (update-texture texture (addr (.r pixels)))) +``` + +The `(Ptr u8)` face has to stay the declared one, because `(.data im-copy)` is already a +`(Ptr u8)` over the same bytes and `(Ptr u8)` → `(Ptr Color)` is the direction the language +cannot write. `(addr (.r pixels))` was checked against the bytes rather than reasoned +about: a `gen-image-color 2 1 red` through `load-image-colors`, read back through the `u8` +pointer, gives 230 41 55 255. So the honest statement is that §A.2 is half closed — the +example reads `(rl/update-texture-colors texture pixels)`, the cast exists once with a name +and a comment on it instead of once per call site, and the general gap the section is +actually about is a **pointer reinterpretation**, which is not a checker arm. + +## Verification + +- `dune build --root .` and `dune test --root .` clean; the dev suite is 232 checks, 0 + failures, unchanged — the new checks are in `test_flan.ml`, which reports pass/fail + rather than a count. +- Eleven new checks in `test/test_flan.ml` over three new functions in + `test/headers/sample.h` (`blit`, `scratch`, `pair_len_p`): six that must agree, five + that must still be reported, each asserting on the message and not on a count. All + eleven were confirmed live by breaking `ptr_agrees` in three different directions and + watching the right subset go red. +- The raylib acceptance cases ran rather than skipped (`ldconfig` finds + `libraylib.so.550`); the only "skipping" line in the whole run is the web one, which + wants a wasm build of raylib that is not in this tree. +- `flan generate-c vendor/raylib` completes, which is itself the check: it compares every + `defstruct`, every hand-written `declare-c` and every mapped constant against + `raylib-5.5.h` and refuses to write when they disagree. +- `bash web/examples/check.sh` green. +- `spike/x86/survey.sh` at 103 MATCH / 0 DIFFER / 0 REFUSED. + +## Still open + +- A pointer reinterpretation in the language. `(addr (.r p))` works when the first field + is the type you want and there is no general form of it. This is §A.2's real subject. +- Nothing else. The three differences the comment lists are now all three implemented.