From 94be94425518cc52c220f0ca43aa6f6c3a7e3525 Mon Sep 17 00:00:00 2001 From: Anthony Wang Date: Wed, 1 Jul 2026 03:54:44 -0400 Subject: [PATCH] Add more bindings, arithmetic instances for Vector2 and Vector3 --- c/raylib_bindings.c | 42 +++++++++++++++++++++++++++++++++++------ lean/Raylean/Core.lean | 35 +++++++++++++++++++++++++++++----- lean/Raylean/Math.lean | 43 +++++++++++++++++++++++++++++++++++++++++- 3 files changed, 108 insertions(+), 12 deletions(-) diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c index 902a945..a869c03 100644 --- a/c/raylib_bindings.c +++ b/c/raylib_bindings.c @@ -314,12 +314,6 @@ static inline Camera2D camera2D_of_arg(lean_obj_arg camera) { return (Camera2D){offset, target, rotation, zoom}; } -lean_obj_res getRandomValue(uint32_t min, uint32_t max) - __attribute__((optnone)) { - // BUG: This always seems to return `min` - return lean_io_result_mk_ok(lean_box_uint32(GetRandomValue(min, max))); -} - lean_obj_res initWindow(lean_obj_arg width, lean_obj_arg height, b_lean_obj_arg title) { InitWindow(lean_uint32_of_nat_mk(width), lean_uint32_of_nat_mk(height), @@ -336,6 +330,23 @@ lean_obj_res closeWindow(void) { return IO_UNIT; } +lean_obj_res maximizeWindow(void) { + MaximizeWindow(); + return IO_UNIT; +} + +lean_obj_res getScreenWidth(void) { + return lean_io_result_mk_ok(lean_uint32_to_nat(GetScreenWidth())); +} + +lean_obj_res getScreenHeight(void) { + return lean_io_result_mk_ok(lean_uint32_to_nat(GetScreenHeight())); +} + +lean_obj_res getWindowScaleDPI(void) { + return lean_io_result_mk_ok(vector2_obj_mk(GetWindowScaleDPI())); +} + lean_obj_res beginDrawing(void) { BeginDrawing(); return IO_UNIT; @@ -402,6 +413,17 @@ lean_obj_res beginMode3D(lean_obj_arg camera) { return IO_UNIT; } +lean_obj_res getWorldToScreen (lean_obj_arg position, lean_obj_arg camera) { + return lean_io_result_mk_ok(vector2_obj_mk(GetWorldToScreen(vector3_of_arg(position), + camera3D_of_arg(camera)))); +} + +lean_obj_res drawLine3D(lean_obj_arg startPos, lean_obj_arg endPos, + lean_obj_arg color) { + DrawLine3D(vector3_of_arg(startPos), vector3_of_arg(endPos), color_of_arg(color)); + return IO_UNIT; +} + lean_obj_res drawCube(lean_obj_arg position, double width, double height, double length, lean_obj_arg color) { DrawCube(vector3_of_arg(position), width, height, length, @@ -416,6 +438,14 @@ lean_obj_res drawCubeWires(lean_obj_arg position, double width, double height, return IO_UNIT; } +lean_obj_res drawCylinderEx(lean_obj_arg startPos, lean_obj_arg endPos, + double startRadius, double endRadius, + lean_obj_arg sides, lean_obj_arg color) { + DrawCylinderEx(vector3_of_arg(startPos), vector3_of_arg(endPos), startRadius, + endRadius, lean_uint32_of_nat_mk(sides), color_of_arg(color)); + return IO_UNIT; +} + lean_obj_res drawGrid(lean_obj_arg slices, double spacing) { DrawGrid(lean_uint32_of_nat_mk(slices), spacing); return IO_UNIT; diff --git a/lean/Raylean/Core.lean b/lean/Raylean/Core.lean index e0818b6..b1aa7ac 100644 --- a/lean/Raylean/Core.lean +++ b/lean/Raylean/Core.lean @@ -15,6 +15,18 @@ opaque closeWindow : IO Unit @[extern "windowShouldClose"] opaque windowShouldClose : IO Bool +@[extern "maximizeWindow"] +opaque maximizeWindow : IO Unit + +@[extern "getScreenWidth"] +opaque getScreenWidth : IO Nat + +@[extern "getScreenHeight"] +opaque getScreenHeight : IO Nat + +@[extern "getWindowScaleDPI"] +opaque getWindowScaleDPI : IO Vector2 + /- Cursor-related functions -/ @[extern "disableCursor"] @@ -43,6 +55,9 @@ opaque beginMode3D : (camera : @& Camera3D) → IO Unit @[extern "endMode3D"] opaque endMode3D : IO Unit +@[extern "getWorldToScreen"] +opaque getWorldToScreen : (position : @& Vector3) → (camera : @& Camera3D) → IO Vector2 + /- Timing-related functions -/ @[extern "setTargetFPS"] @@ -51,11 +66,6 @@ opaque setTargetFPS : (fps : Nat) → IO Unit @[extern "getFrameTime"] opaque getFrameTime : IO Float -/- Random values generation functions -/ - -@[extern "getRandomValue"] -opaque getRandomValue : UInt32 → UInt32 → IO UInt32 - /- Input-related functions: keyboard -/ @[extern "isKeyDown"] @@ -112,12 +122,25 @@ opaque drawText : (text : @& String) → (posX : Nat) → (posY : Nat) → (font /- Basic geometric 3D shapes drawing functions -/ +@[extern "drawLine3D"] +opaque drawLine3D : (startPos : @& Vector3) → (endPos : @& Vector3) → (color : @& Color) → IO Unit + @[extern "drawCube"] opaque drawCube : (position : @& Vector3) → (width : Float) → (height : Float) → (length : Float) → (color : @& Color) -> IO Unit +-- This is also in Raylib but it's easier to just reimplement it here +def drawCubeV (position size : Vector3) (color : Color) := + drawCube position size.x size.y size.z color + @[extern "drawCubeWires"] opaque drawCubeWires : (position : @& Vector3) → (width : Float) → (height : Float) → (length : Float) → (color : @& Color) -> IO Unit +def drawCubeWiresV (position size : Vector3) (color : Color) := + drawCubeWires position size.x size.y size.z color + +@[extern "drawCylinderEx"] +opaque drawCylinderEx : (startPos : @& Vector3) → (endPos : @& Vector3) → (startRadius : Float) → (endRadius : Float) → (sides : Nat) → (color : @& Color) -> IO Unit + @[extern "drawGrid"] opaque drawGrid : (slices : Nat) → (spacing : Float) → IO Unit @@ -151,6 +174,8 @@ opaque setWindowState : (flags : UInt64) -> IO Unit namespace Flags +def windowResizable : UInt64 := 0x00000004 def vsyncHint : UInt64 := 0x00000040 +def windowHighdpi : UInt64 := 0x00002000 end Flags diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean index ce5e654..8ea5b0f 100644 --- a/lean/Raylean/Math.lean +++ b/lean/Raylean/Math.lean @@ -9,7 +9,7 @@ namespace Vector2 open Raylean.Types def add (v1 : Vector2) (v2 : Vector2) : Vector2 := - { x := v1.x + v2.x, y := v1.y + v2.y : Vector2 } + { x := v1.x + v2.x, y := v1.y + v2.y } def length (v : Vector2) : Float := Float.sqrt (v.x ^ 2 + v.y ^ 2) @@ -19,6 +19,47 @@ def sub (v1 : Vector2) (v2 : Vector2) : Vector2 := def mul (v : Vector2) (s : Float) : Vector2 := { x := s * v.x, y := s * v.y } +def div (v : Vector2) (s : Float) : Vector2 := + { x := v.x / s, y := v.y / s } + def dot (v1 v2 : Vector2) : Vector2 := ⟨v1.x * v2.x, v1.y * v2.y⟩ +instance : Add Vector2 := ⟨add⟩ + +instance : Sub Vector2 := ⟨sub⟩ + +instance : HMul Float Vector2 Vector2 := ⟨flip mul⟩ + +instance : HMul Vector2 Float Vector2 := ⟨mul⟩ + +instance : HDiv Vector2 Float Vector2 := ⟨div⟩ + end Vector2 + +namespace Vector3 + +def add (v1 : Vector3) (v2 : Vector3) : Vector3 := + { x := v1.x + v2.x, y := v1.y + v2.y, z := v1.z + v2.z } + +def length (v : Vector3) : Float := Float.sqrt (v.x ^ 2 + v.y ^ 2 + v.z ^ 2) + +def sub (v1 : Vector3) (v2 : Vector3) : Vector3 := + { x := v1.x - v2.x, y := v1.y - v2.y, z := v1.z - v2.z } + +def mul (v : Vector3) (s : Float) : Vector3 := + { x := s * v.x, y := s * v.y, z := s * v.z } + +def div (v : Vector3) (s : Float) : Vector3 := + { x := v.x / s, y := v.y / s, z := v.z / s } + +instance : Add Vector3 := ⟨add⟩ + +instance : Sub Vector3 := ⟨sub⟩ + +instance : HMul Float Vector3 Vector3 := ⟨flip mul⟩ + +instance : HMul Vector3 Float Vector3 := ⟨mul⟩ + +instance : HDiv Vector3 Float Vector3 := ⟨div⟩ + +end Vector3