Collision bindings, and what a headless FFI test cannot pin

Finishing the 2D lane's unfinished work: the collision family was written and
had no tests when the session ended. It is the best material a headless table
gets, since every one of these is pure and needs no GL context.

Two plausible tests in a row turned out to check nothing, and that is the part
worth keeping. A struct round trip is symmetric and passes for any field order -
the texture lane found that one. The second is subtler: no axis-aligned geometry
can pin Vector2's fields, because exchanging x and y is a reflection that is
applied on the way in and undone on the way out. Swapping the shim's own typedef
leaves every collision case passing. Distances never even see it.

What does pin Vector2 is the rotated camera, because a rotation is not
axis-aligned and does not commute with the reflection. That case is load-bearing
and the comment now says so, because the collision cases look like they cover
the same ground and do not.

What the new cases do pin is Rectangle, completely: swapping width and height
turns three of the four predicates the wrong way. Verified by doing it.

collision-lines answers (Option Vector2) rather than a bool and an
out-parameter, because raylib leaves the out-parameter untouched when the
segments do not meet and a caller who forgets reads whatever was there.
This commit is contained in:
Joseph Ferano 2026-09-11 19:01:32 +07:00
parent f5d4cd5188
commit 27172d260f
6 changed files with 270 additions and 1 deletions

26
NEXT.md
View File

@ -273,6 +273,32 @@ build depends on the shared library being linkable and not on `raylib-devel`.
`vendor/raylib/link` carries `-l:libraylib.so.550` because Fedora ships the
runtime library without the `.so` symlink.
### What a headless FFI test can and cannot pin
Worth knowing before writing another one, because two plausible tests in a row
turned out to check nothing.
- **A struct round trip is worthless.** Hand raylib a struct, read it back,
compare: store-and-return is symmetric, so C writes and reads the same wrong
slots and the test passes for *any* field order. Found by permuting two
fields and getting identical output.
- **Axis-aligned geometry cannot pin `Vector2`.** Exchanging `x` and `y` is a
reflection, applied to the inputs on the way in and undone on the way out, so
the printed answer is unchanged. Every collision predicate, and every
distance, passes with the fields swapped — verified by swapping the shim's
own typedef. Distances are worse: the reflection does not even reach them.
- **What does pin `Vector2` is the rotated camera**, because a 90-degree
rotation is not axis-aligned and therefore does not commute with the
reflection. That case is load-bearing and must not be deleted on the grounds
that the collision cases look like they cover it.
- **What pins `Rectangle` is arithmetic on its fields**`GetCollisionRec`
computes four numbers from four different field pairs, and the point/rect
predicates turn the wrong way when width and height are exchanged.
The rule that falls out: make raylib **compute** something whose answer differs
per axis, then verify the test can fail by permuting the fields and watching it
go red. A case not verified that way is decoration.
## Packages
`lib/load.ml` resolves `(import rl "vendor:raylib")` before the checker runs.

View File

@ -221,6 +221,10 @@ let source = {flan|
;; [lo, hi). An empty or reversed range answers lo a defined value rather
;; than a remainder by zero, which is immediate undefined behaviour and not a
;; wrong number. The span must fit in i32, since hi - lo is computed there.
;; One draw, and therefore modulo bias: the low (2^32 % span) values of the
;; range come up very slightly more often. Rejection sampling would remove it
;; and would consume an unpredictable number of draws, which is the one thing
;; this generator exists not to do.
(defn rand-i32-range [lo i32 hi i32] i32
(if (<= hi lo)
lo

View File

@ -46,6 +46,10 @@
;; ((140-100)/2)+8 = 28 and ((90-50)/2)+4 = 24. Swap offset and target in the
;; defstruct and this reads (143,-16); swap rotation and zoom and the zoom
;; becomes 0, the transform is singular, and both come back NaN.
(defn show-bool [name string b bool]
(print-str name) (print-str " ")
(print-line (if b "yes" "no")))
(defn show-v [v rl/Vector2]
(print-f64 (f64 (.x v))) (newline)
(print-f64 (f64 (.y v))) (newline))
@ -136,4 +140,61 @@
(rl/get-world-to-screen-2d (rl/Vector2 {:x 28.0 :y 24.0}) spun)
60.0 90.0))
;; ── Collision, which is the best material a headless test gets ──────
;;
;; Every one of these is pure: raylib computes an answer out of the fields,
;; so a wrong field order gives a wrong answer rather than the same struct
;; back. Each case below is paired with one that must come out the other
;; way, because a predicate that always said yes would pass a single case.
(let [r (rl/Rectangle {:x 0.0 :y 0.0 :width 10.0 :height 4.0})]
;; Inside on both axes, then outside on y only. Swap width and height and
;; both of these flip, which is what makes the pair worth more than either.
(show-bool "point in rect" (rl/collision-point-rec? (rl/Vector2 {:x 5.0 :y 3.0}) r))
(show-bool "point below rect" (rl/collision-point-rec? (rl/Vector2 {:x 5.0 :y 5.0}) r))
;; Overlapping by one unit, then clear of it. Pins x against width.
(show-bool "rects overlap"
(rl/collision-recs? r (rl/Rectangle {:x 9.0 :y 1.0 :width 10.0 :height 10.0})))
(show-bool "rects apart"
(rl/collision-recs? r (rl/Rectangle {:x 11.0 :y 1.0 :width 10.0 :height 10.0}))))
;; Centres five apart with radii summing to six, then seven apart. The radius
;; is a scalar beside two Vector2s, so this pins it against their fields.
(show-bool "circles touch"
(rl/collision-circles? (rl/Vector2 {:x 0.0 :y 0.0}) 3.0
(rl/Vector2 {:x 5.0 :y 0.0}) 3.0))
(show-bool "circles clear"
(rl/collision-circles? (rl/Vector2 {:x 0.0 :y 0.0}) 3.0
(rl/Vector2 {:x 7.0 :y 0.0}) 3.0))
;; The one that answers with a number rather than a yes: a horizontal segment
;; at y = 7 crossed by a vertical one at x = 3, so the answer is (3 7).
;;
;; Asymmetric rather than the two diagonals of a square meeting at (5 5),
;; which would give the same answer however the fields were ordered — but be
;; clear about what that buys, because it is less than it looks.
;;
;; **Nothing in this section pins Vector2's own two fields, and nothing
;; axis-aligned can.** Exchanging x and y is a reflection: it is applied to
;; the inputs on the way in and undone on the way out, so the printed answer
;; is identical. Verified by actually swapping the shim's typedef — every
;; collision case here still passes. Distances are worse still, being
;; unchanged by the reflection in the first place.
;;
;; The rotated camera above is what pins them, and it works precisely because
;; a 90-degree rotation is not axis-aligned, so the reflection does not
;; commute with it. That case is load-bearing; do not delete it because the
;; collision ones look like they cover the same ground.
;;
;; What this section *does* pin is Rectangle, completely — swapping width and
;; height turns three of the four predicates below the wrong way.
(match (rl/collision-lines (rl/Vector2 {:x 0.0 :y 7.0}) (rl/Vector2 {:x 10.0 :y 7.0})
(rl/Vector2 {:x 3.0 :y 0.0}) (rl/Vector2 {:x 3.0 :y 10.0}))
(Some p) (show-v p)
None (print-line "no crossing"))
;; Parallel, so they never meet: None rather than a point nobody wrote.
(match (rl/collision-lines (rl/Vector2 {:x 0.0 :y 0.0}) (rl/Vector2 {:x 1.0 :y 2.0})
(rl/Vector2 {:x 5.0 :y 0.0}) (rl/Vector2 {:x 6.0 :y 2.0}))
(Some p) (show-v p)
None (print-line "no crossing"))
0)

View File

@ -212,7 +212,11 @@ let () =
7\n0\n17\n2\n4\n\
28\n24\n140\n90\n\
rotated screen-to-world ok\n\
rotated world-to-screen ok\n"
rotated world-to-screen ok\n\
point in rect yes\npoint below rect no\n\
rects overlap yes\nrects apart no\n\
circles touch yes\ncircles clear no\n\
3\n7\nno crossing\n"
in
if Sys.command "ldconfig -p 2>/dev/null | grep -q libraylib" = 0 then begin
outputs "raylib ffi, headless" "programs/raylib-ffi.flan" raylib_out;

View File

@ -214,6 +214,112 @@
(get-collision-rec-raw (addr x) (addr y) (addr out))
out))
;; ── Collision ───────────────────────────────────────────────────────
;;
;; All of these are pure geometry: no window, no GL context, no state. That
;; makes them the other half of what the acceptance table can assert, and the
;; only part of the 2D surface that is tested as thoroughly as it is bound.
;;
;; Each takes its aggregates through pointers for the usual reason, and each
;; wrapper copies its parameters into locals first — a parameter is not an
;; assignable place (spec-memory.md), so there is no address to take.
(declare collision-recs?-raw [a (Ptr Rectangle) b (Ptr Rectangle)] bool
"flan_rl_check_collision_recs")
(defn collision-recs? [a Rectangle b Rectangle] bool
(let [x a y b]
(collision-recs?-raw (addr x) (addr y))))
(declare collision-circles?-raw
[c1 (Ptr Vector2) r1 f32 c2 (Ptr Vector2) r2 f32] bool
"flan_rl_check_collision_circles")
(defn collision-circles? [c1 Vector2 r1 f32 c2 Vector2 r2 f32] bool
(let [a c1 b c2]
(collision-circles?-raw (addr a) r1 (addr b) r2)))
(declare collision-circle-rec?-raw
[center (Ptr Vector2) radius f32 rec (Ptr Rectangle)] bool
"flan_rl_check_collision_circle_rec")
(defn collision-circle-rec? [center Vector2 radius f32 rec Rectangle] bool
(let [c center r rec]
(collision-circle-rec?-raw (addr c) radius (addr r))))
(declare collision-circle-line?-raw
[center (Ptr Vector2) radius f32 p1 (Ptr Vector2) p2 (Ptr Vector2)] bool
"flan_rl_check_collision_circle_line")
(defn collision-circle-line? [center Vector2 radius f32
p1 Vector2 p2 Vector2] bool
(let [c center a p1 b p2]
(collision-circle-line?-raw (addr c) radius (addr a) (addr b))))
(declare collision-point-rec?-raw [point (Ptr Vector2) rec (Ptr Rectangle)] bool
"flan_rl_check_collision_point_rec")
(defn collision-point-rec? [point Vector2 rec Rectangle] bool
(let [p point r rec]
(collision-point-rec?-raw (addr p) (addr r))))
(declare collision-point-circle?-raw
[point (Ptr Vector2) center (Ptr Vector2) radius f32] bool
"flan_rl_check_collision_point_circle")
(defn collision-point-circle? [point Vector2 center Vector2 radius f32] bool
(let [p point c center]
(collision-point-circle?-raw (addr p) (addr c) radius)))
(declare collision-point-triangle?-raw
[point (Ptr Vector2) a (Ptr Vector2) b (Ptr Vector2) c (Ptr Vector2)] bool
"flan_rl_check_collision_point_triangle")
(defn collision-point-triangle? [point Vector2 a Vector2 b Vector2
c Vector2] bool
(let [p point x a y b z c]
(collision-point-triangle?-raw (addr p) (addr x) (addr y) (addr z))))
;; `threshold` is in pixels, and it is not optional in practice: raylib's test
;; is a distance comparison in floats, so a point exactly on the line fails at
;; a threshold of 0. 1 is the useful smallest value.
(declare collision-point-line?-raw
[point (Ptr Vector2) p1 (Ptr Vector2) p2 (Ptr Vector2) threshold i32] bool
"flan_rl_check_collision_point_line")
(defn collision-point-line? [point Vector2 p1 Vector2 p2 Vector2
threshold i32] bool
(let [p point a p1 b p2]
(collision-point-line?-raw (addr p) (addr a) (addr b) threshold)))
;; A slice crosses as ptr+len, which is exactly what raylib wants here, so
;; this is the one collision call that needs no per-element copying. The
;; polygon is not closed explicitly — raylib joins the last point to the
;; first.
(declare collision-point-poly?-raw [point (Ptr Vector2) points [Vector2]] bool
"flan_rl_check_collision_point_poly")
(defn collision-point-poly? [point Vector2 points [Vector2]] bool
(let [p point]
(collision-point-poly?-raw (addr p) points)))
;; The one that answers with more than yes or no: where the two segments meet.
;; None is "they do not", so the point cannot be read when there isn't one —
;; raylib's own signature leaves the out-parameter untouched in that case and
;; a caller that forgets reads whatever was there.
(declare collision-lines-raw
[a1 (Ptr Vector2) a2 (Ptr Vector2) b1 (Ptr Vector2) b2 (Ptr Vector2)
out (Ptr Vector2)] bool
"flan_rl_check_collision_lines")
(defn collision-lines [a1 Vector2 a2 Vector2 b1 Vector2 b2 Vector2]
(Option Vector2)
(let [p a1 q a2 r b1 s b2
out (Vector2 {})]
(if (collision-lines-raw (addr p) (addr q) (addr r) (addr s) (addr out))
(Some out)
None)))
;; ── Textures ────────────────────────────────────────────────────────
;;
;; Everything here needs a GL context, so a window has to be open first —

68
vendor/raylib/shim.c vendored
View File

@ -59,6 +59,21 @@ extern void BeginMode2D(Camera2D camera);
extern void EndMode2D(void);
extern Vector2 GetScreenToWorld2D(Vector2 position, Camera2D camera);
extern Vector2 GetWorldToScreen2D(Vector2 position, Camera2D camera);
extern bool CheckCollisionRecs(Rectangle rec1, Rectangle rec2);
extern bool CheckCollisionCircles(Vector2 c1, float r1, Vector2 c2, float r2);
extern bool CheckCollisionCircleRec(Vector2 center, float radius, Rectangle rec);
extern bool CheckCollisionCircleLine(Vector2 center, float radius,
Vector2 p1, Vector2 p2);
extern bool CheckCollisionPointRec(Vector2 point, Rectangle rec);
extern bool CheckCollisionPointCircle(Vector2 point, Vector2 center, float radius);
extern bool CheckCollisionPointTriangle(Vector2 point, Vector2 p1, Vector2 p2,
Vector2 p3);
extern bool CheckCollisionPointLine(Vector2 point, Vector2 p1, Vector2 p2,
int threshold);
extern bool CheckCollisionPointPoly(Vector2 point, const Vector2 *points,
int pointCount);
extern bool CheckCollisionLines(Vector2 a1, Vector2 a2, Vector2 b1, Vector2 b2,
Vector2 *collisionPoint);
/* A Flan string arrives as ptr+len and is not NUL-terminated, so a C API that
* wants a C string needs a copy. Two callers want one: the window title and a
@ -164,3 +179,56 @@ void flan_rl_get_world_to_screen_2d(const Vector2 *position,
const Camera2D *camera, Vector2 *out) {
*out = GetWorldToScreen2D(*position, *camera);
}
bool flan_rl_check_collision_recs(const Rectangle *a, const Rectangle *b) {
return CheckCollisionRecs(*a, *b);
}
bool flan_rl_check_collision_circles(const Vector2 *c1, float r1,
const Vector2 *c2, float r2) {
return CheckCollisionCircles(*c1, r1, *c2, r2);
}
bool flan_rl_check_collision_circle_rec(const Vector2 *center, float radius,
const Rectangle *rec) {
return CheckCollisionCircleRec(*center, radius, *rec);
}
bool flan_rl_check_collision_circle_line(const Vector2 *center, float radius,
const Vector2 *p1, const Vector2 *p2) {
return CheckCollisionCircleLine(*center, radius, *p1, *p2);
}
bool flan_rl_check_collision_point_rec(const Vector2 *point, const Rectangle *rec) {
return CheckCollisionPointRec(*point, *rec);
}
bool flan_rl_check_collision_point_circle(const Vector2 *point,
const Vector2 *center, float radius) {
return CheckCollisionPointCircle(*point, *center, radius);
}
bool flan_rl_check_collision_point_triangle(const Vector2 *point, const Vector2 *a,
const Vector2 *b, const Vector2 *c) {
return CheckCollisionPointTriangle(*point, *a, *b, *c);
}
bool flan_rl_check_collision_point_line(const Vector2 *point, const Vector2 *p1,
const Vector2 *p2, int threshold) {
return CheckCollisionPointLine(*point, *p1, *p2, threshold);
}
/* A Flan slice arrives as ptr+len, the same shape a string does. raylib wants
* an int count, and a polygon with more than INT_MAX points is not a thing
* that happens; the clamp is there so the conversion is not silent. */
bool flan_rl_check_collision_point_poly(const Vector2 *point,
const Vector2 *points, long long n) {
if (n > INT_MAX) n = INT_MAX;
return CheckCollisionPointPoly(*point, points, (int)n);
}
bool flan_rl_check_collision_lines(const Vector2 *a1, const Vector2 *a2,
const Vector2 *b1, const Vector2 *b2,
Vector2 *out) {
return CheckCollisionLines(*a1, *a2, *b1, *b2, out);
}