Add more bindings, arithmetic instances for Vector2 and Vector3

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;

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

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