monotonicity

A city-building and transport simulation game written in Lean

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
  81. 81
  82. 82
  83. 83
  84. 84
  85. 85
  86. 86
  87. 87
  88. 88
  89. 89
  90. 90
  91. 91
  92. 92
  93. 93
  94. 94
  95. 95
  96. 96
  97. 97
  98. 98
  99. 99
  100. 100
  101. 101
  102. 102
  103. 103
  104. 104
  105. 105
  106. 106
  107. 107
  108. 108
  109. 109
  110. 110
  111. 111
  112. 112
  113. 113
  114. 114
  115. 115
  116. 116
  117. 117
  118. 118
  119. 119
diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c
index 902a945..0750084 100644
--- a/c/raylib_bindings.c
+++ b/c/raylib_bindings.c
@@ -314,11 +314,11 @@ 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 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) {
@@ -336,6 +336,18 @@ lean_obj_res closeWindow(void) {
   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 +414,15 @@ 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 +437,13 @@ 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..23f03d9 100644
--- a/lean/Raylean/Core.lean
+++ b/lean/Raylean/Core.lean
@@ -15,6 +15,15 @@ opaque closeWindow : IO Unit
 @[extern "windowShouldClose"]
 opaque windowShouldClose : IO Bool
 
+@[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 +52,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"]
@@ -112,12 +124,18 @@ 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
 
 @[extern "drawCubeWires"]
 opaque drawCubeWires : (position : @& Vector3) → (width : Float) → (height : Float) → (length : Float) → (color : @& Color) -> IO Unit
 
+@[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