The pointer arm agrees promised, and the comment stops promising it

lib/cimport.ml

@@ -856,6 +856,78 @@ let agrees env (a : Ast.texpr) (b : Ast.texpr) =
   || (enum_like env a && int32_like nb)
   || (enum_like env b && int32_like na)
 
+(* ── A hand-written pointer, against the pointer the header spells ──
+
+   The second tolerance, and the one [agrees] cannot express on its own. By the
+   time a C parameter has become a Flan type, what the header actually said
+   about it is gone: [param_ty] renders [const char *] as [string] and
+   [value_ty] renders [void *] as [(Ptr u8)], and both of those are the
+   importer's own choice rather than the header's word. A hand-written line
+   that says [(Ptr u8)] over a [const char *] is not disagreeing with the
+   header — it is disagreeing with a rendering — so the comparison has to be
+   made against the C spelling, which is why this takes the string and [agrees]
+   does not.
+
+   It is consulted only from the [declare-c] check below, never from
+   [check_structs]. A struct field is about *layout*, and every pointer in a
+   struct is one word whatever it points at, so the element type is not the
+   thing that check is for; widening it there would buy nothing and would cost
+   the width discipline the field check exists to keep.
+
+   The [i8]/[u8] tolerance likewise lives here and not in [agrees]. Inside a
+   pointer, [char] and [unsigned char] are two spellings of one byte and the
+   package uses [(Ptr u8)] for both — [Image.data] is [void *] in the header.
+   As a *field* or a *scalar* they are still a real disagreement and [agrees]
+   goes on saying so. *)
+
+let byte s = String.equal s "i8" || String.equal s "u8"
+
+(* [const int *] → [Some "const int"]. Anything that is not a pointer, [None].
+   Only the outermost [*] comes off, so [void **] arrives here as a pointer to
+   [void *], which is a pointer to something and not a [void *]. *)
+let c_pointee (s : string) : string option =
+  let s = String.trim s in
+  if String.length s > 0 && s.[String.length s - 1] = '*' then
+    Some (String.trim (String.sub s 0 (String.length s - 1)))
+  else None
+
+let ptr_agrees env ~(c : string) (t : Ast.texpr) =
+  match (c_pointee c, t.Ast.t) with
+  | Some inner, Ast.Tapp ("Ptr", [ elem ]) ->
+    (* [void *] agrees with a pointer to anything, and this is the judgement
+       call of the arm. C's [void *] is opaque about *what it points at* — that
+       is the whole of what the spelling means — so there is no element type in
+       the header to disagree with, and a check that reported one would be
+       reporting [value_ty]'s guess of [u8] back at the author as if the header
+       had said it. What is *not* given up is that it is a pointer at all: the
+       match above requires [(Ptr _)] on the Flan side, so an [i32] or a
+       [string] declared against a [void *] is still a finding. That
+       asymmetry is the point — raylib spells thirty-odd parameters [void *]
+       and none of them is a scalar. *)
+    let b = bare inner in
+    if String.equal b "void" then true
+    else (
+      match (try Some (value_ty env inner) with Refused _ -> None) with
+      | None ->
+        (* A pointee this cannot render says nothing, exactly as an
+           unrenderable field type says nothing in [check_structs]. *)
+        false
+      | Some want ->
+        let a = ty_source want and b = ty_source elem in
+        (* [agrees] and not [String.equal], so a [(Ptr Key)] against the
+           header's [(Ptr int)] lands on the enum arm. The four bytes are the
+           same four bytes through a pointer as they are beside one. *)
+        agrees env want elem || (byte a && byte b))
+  | _ -> false
+
+(* The two together, for the one caller that still has the C spelling. A
+   [(Ptr A)] against a [B *] for unrelated named [A] and [B] falls through
+   both and stays a finding: two structs of the same size are still two
+   different structs, and a binding that says the wrong one reads a
+   plausible picture out of the wrong offsets. *)
+let agrees_c env ~(c : string) (want : Ast.texpr) (got : Ast.texpr) =
+  agrees env want got || ptr_agrees env ~c got
+
 let check_structs ~env ~(structs : (string * Ast.field list) list) (d : dump) =
   let record n =
     match List.find_opt (fun r -> r.rname = n) d.records with
@@ -1291,22 +1363,38 @@ let decl_source (d : Ast.decl) =
 (* ── A hand-written binding, against the header's own signature ────── *)
 
 (* The other half of closing the trusted gap, and the one that pays off
-   immediately: [vendor/raylib] carries 176 [declare-c] lines that were
+   immediately: every [declare-c] line in [vendor/raylib] was transcribed by
-   transcribed by hand from raylib's documentation, and until now nothing could
+   hand from raylib's documentation, and until this nothing could say whether
-   say whether any of them was right. This says so, one at a time.
+   any of them was right. This says so, one at a time. (There is no count here
+   on purpose. The last one written down said 176 when there were 196, which is
+   the only thing a hand-maintained census of a growing file ever does.)
 
-   Compared as *rendered Flan types*, not as C spellings, because the two sides
+   Compared as *rendered Flan types* wherever the rendering is the whole story,
-   are not written in the same language and only the Flan rendering is
+   and against the C spelling where it is not. Three differences are expected
-   commensurable. Three differences are expected and are not reported:
+   and are not reported, and all three are now implemented rather than
+   promised:
 
    - the Flan name. [IsKeyPressed] is [key-pressed?] by hand and
      [is-key-pressed] by rule, and the hand-written one is better. The C symbol
      is what identifies the function here, not the name.
    - an enum parameter. The header says [KeyboardKey] and the importer has no
      way to know the package calls that [Key], so it says [i32]; the
-     hand-written [Key] is the same int with a better face.
+     hand-written [Key] is the same int with a better face. That is [agrees].
    - a [(Ptr T)] where the header says [T *] and the hand-written line chose
-     something more specific for a reason it recorded.
+     something more specific for a reason it recorded. That is [ptr_agrees],
+     and it needs the C spelling because the rendering has already thrown the
+     answer away: [param_ty] turns [const char *] into [string] and [value_ty]
+     turns [void *] into [(Ptr u8)], neither of which is what the header said.
+     [(Ptr u8)] over a [char *], and [(Ptr] anything[)] over a [void *], now
+     agree; [(Ptr A)] over a [B *] does not.
+
+   What [const] does here, since the arm above says nothing about it: nothing,
+   and the reason is worth knowing because it is invisible. A non-const
+   [char *] parameter makes [param_ty] *refuse*, and the [| None -> None] below
+   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 pointer arm exists for.
 
    What is left after those is a real disagreement about a width, an arity or a
    direction — which is exactly the class of bug docs/BUILT.md warns about, where
@@ -1331,7 +1419,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) =
             integer is the expected difference and not a finding, and an enum
             against anything else still is one. *)
          let norm (t : Ast.texpr) = ty_source t in
-         let same a b = agrees env a b in
+         let same ~c a b = agrees_c env ~c a b in
          if c.cvariadic then None
          else if List.length fn.Ast.params <> List.length c.cparams then
            say
@@ -1345,7 +1433,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) =
                   match (try Some (param_ty env ct) with Refused _ -> None) with
                   | None -> None
                   | Some want ->
-                    if same want p.Ast.fty then None
+                    if same ~c:ct want p.Ast.fty then None
                     else
                       Some
                         (Printf.sprintf "parameter %s is %s and the header says %s (%s)"
@@ -1361,7 +1449,7 @@ let diff_bound ~env ~(bound : (Ast.fn * string) list) (d : dump) =
                 let agrees =
                   match (want, fn.Ast.ret) with
                   | None, None -> true
-                  | Some a, Some b -> same a b
+                  | Some a, Some b -> same ~c:c.cret a b
                   | _ -> false
                 in
                 if agrees then None

test/headers/sample.h

@@ -59,6 +59,16 @@ Pair point_of(Point p);                      /* the second typedef name */
 int mood_value(Mood m);                      /* a C enum is an int */
 void take_nothing(void);
 
+/* The pointer arm of the declare-c check, which compares against the C
+ * spelling because the rendering has thrown the answer away. blit's two
+ * parameters are void *, which is opaque about what it points at and so
+ * agrees with a pointer to anything; scratch is the same question in return
+ * position. pair_len_p is a pointer to a *named* type, which is what has to go
+ * on being refused when a hand-written line names a different one. */
+void blit(void *dst, const void *src, int n);
+void *scratch(int n);
+float pair_len_p(const Pair *p);
+
 /* --- refused, one per reason --- */
 const char *name_of(int which);              /* returns char * */
 void fill_buffer(char *out, int cap);        /* non-const char *: C writes it */

test/test_flan.ml

@@ -1910,6 +1910,57 @@ let () =
        ~bound:(bound_of "(declare-c mv [m Mood] i32 \"mood_value\")") dump
      = []);
 
+  (* The pointer arm. The importer renders a C pointer into whichever Flan type
+     it thinks is the nicest face — [const char *] becomes [string], [void *]
+     becomes [(Ptr u8)] — and a hand-written line that wants the raw address
+     instead is disagreeing with that choice rather than with the header. These
+     say which of those disagreements are real. *)
+  let agreed name src =
+    check ("declare-c against the header: " ^ name)
+      (Cimport.diff_bound ~env ~bound:(bound_of src) dump = [])
+  in
+  (* The case docs/PORTING.md §A.1 could not write: GetCodepointPrevious reads
+     backwards from its pointer, so a Flan string — which crosses as a
+     NUL-terminated copy — is the one thing it must not be handed. *)
+  agreed "a (Ptr u8) where the header says const char *"
+    "(declare-c name-length [text (Ptr u8)] i32 \"name_length\")";
+  (* And the string face goes on being right, because this is an addition. *)
+  agreed "a string where the header says const char *"
+    "(declare-c name-length [text string] i32 \"name_length\")";
+  agreed "a pointer that matches the header exactly"
+    "(declare-c count-at [values (Ptr i32)  n i32] i32 \"count_at\")";
+  (* void * is opaque about what it points at, so there is no element type in
+     the header to disagree with — §A.2's LoadImageColors → UpdateTexture. *)
+  agreed "any pointer where the header says void *"
+    "(declare-c blit [dst (Ptr Pair)  src (Ptr Shade)  n i32] \"blit\")";
+  agreed "any pointer where the header returns void *"
+    "(declare-c scratch [n i32] (Ptr Pair) \"scratch\")";
+  (* An enum through a pointer is the same four bytes an enum is beside one. *)
+  agreed "a (Ptr enum) where the header says a pointer to int"
+    "(declare-c count-at [values (Ptr Mood)  n i32] i32 \"count_at\")";
+
+  (* And the refusals, which are the whole value of the arm: a binding that
+     lies about the header still has to be caught, and the message still has to
+     name the disagreement. *)
+  differs "a pointer to the wrong named type"
+    "(declare-c pair-len-p [p (Ptr Shade)] f32 \"pair_len_p\")"
+    "parameter p is (Ptr Shade) and the header says (Ptr Pair)";
+  differs "a pointer to the wrong width"
+    "(declare-c count-at [values (Ptr f64)  n i32] i32 \"count_at\")"
+    "parameter values is (Ptr f64)";
+  (* void * gives up the element type and nothing else. It is still a pointer,
+     and a scalar declared against one is still a finding. *)
+  differs "a scalar where the header says void *"
+    "(declare-c blit [dst i64  src (Ptr u8)  n i32] \"blit\")"
+    "parameter dst is i64";
+  differs "a scalar where the header says a pointer"
+    "(declare-c count-at [values i32  n i32] i32 \"count_at\")"
+    "parameter values is i32";
+  (* The byte tolerance is the pointee's and not the world's: inside a pointer
+     i8 and u8 are two spellings of one byte, and as a scalar they are not. *)
+  differs "a byte where the header says a wider integer"
+    "(declare-c add [a u8  b i32] i32 \"add_ints\")" "parameter a is u8";
+
   (* The name rule. Reversibility is by storage — the C symbol is kept verbatim
      in the declaration — so what the rule has to be is injective over one
      header, which the collision case above asserts. These pin its shape. *)