Add orbtial game

c/raylib_bindings.c

@@ -497,3 +497,11 @@ lean_obj_res drawTexturePro(b_lean_obj_arg texture_arg,
   DrawTexturePro(*texture, source, dest, origin, rotation, tint);
   return IO_UNIT;
 }
+
+lean_obj_res drawLineV(lean_obj_arg startPos_arg, lean_obj_arg endPos_arg, lean_obj_arg color_arg) {
+  Vector2 startPos = vector2_of_arg(startPos_arg);
+  Vector2 endPos = vector2_of_arg(endPos_arg);
+  Color color = color_of_arg(color_arg);
+  DrawLineV(startPos, endPos, color);
+  return IO_UNIT;
+}

lean/Examples.lean

@@ -4,3 +4,4 @@ import «Examples».Camera3D
 import «Examples».Camera2DPlatformer
 import «Examples».JessicaCantSwim
 import «Examples».BasicECS
+import «Examples».Orbital

lean/Examples/Orbital.lean

@@ -0,0 +1,66 @@
+import Raylean
+import ECS
+import Examples.Orbital.Types
+
+open Raylean
+open Raylean.Types
+open ECS
+
+namespace Orbital
+
+def screenWidth : Nat := 1920
+def screenHeight : Nat := 1080
+def center : Vector2 := ⟨screenWidth.toFloat / 2, screenHeight.toFloat / 2⟩
+def origin : Vector2 := ⟨0,0⟩
+
+def init : System World Unit := do
+  let camera : Camera := ⟨center, center, 0, 1⟩
+  set' global camera
+
+  let initPos : Vector2 := ⟨5,0⟩
+  let initVel : Vector2 := ⟨0, 1.0 / initPos.length |>.sqrt⟩
+
+  newEntityAs_ (Position × Not Velocity) (⟨origin⟩, .Not)
+  newEntityAs_ (Position × Velocity × OrbitPath) ⟨⟨initPos⟩, ⟨initVel⟩, ⟨#[]⟩⟩
+  newEntityAs_ (Position × Velocity × OrbitPath) ⟨⟨-4, 0⟩, ⟨initVel.mul (-1)⟩, ⟨#[]⟩⟩
+  newEntityAs_ (Position × Velocity × OrbitPath) ⟨⟨-0.8, -0.6⟩, ⟨initVel.mul (-0.9)⟩, ⟨#[]⟩⟩
+  newEntityAs_ (Position × Velocity × OrbitPath) ⟨⟨1, 1⟩, ⟨initVel.mul (-1)⟩, ⟨#[]⟩⟩
+  initWindow screenWidth screenHeight "Orbital"
+  setTargetFPS 60
+
+def terminate : System World Unit := closeWindow
+
+def update : System World Unit := do
+  let dt ← getFrameTime
+  cmap (cx := Position × Velocity × OrbitPath) <| fun (p, v, o) =>
+    let pv := p.val
+    let pMag := pv.length
+    let a := pv |>.mul (-1 / pMag^3)
+    let vv := v.val
+    let vvNew := vv.add (a.mul dt)
+    let pvNew := pv.add (vvNew.mul dt)
+    let pNew : Position := ⟨pvNew⟩
+    let vNew : Velocity := ⟨vvNew⟩
+    let oNew : OrbitPath := ⟨o.val.push pvNew⟩
+    (pNew, vNew, oNew)
+
+def render : System World Unit :=
+  renderFrame do
+    drawFPS 10 20
+    clearBackground Color.black
+    cmapM_ (cx := Position × Not Velocity) <| fun (p, _) => do
+      drawCircleV (p.val.add center) 30 Color.red
+    cmapM_ (cx := Position × Velocity) <| fun (p, _) => do
+      drawCircleV (p.val.mul 100 |>.add center) 10 Color.blue
+    cmapM_ (cx := OrbitPath) <| fun o => do
+      let arr := o.val
+      for (s, e) in arr.zip (arr.extract 1 arr.size) do
+        drawLineV (s.mul 100 |>.add center) (e.mul 100 |>.add center) Color.white
+
+def run : System World Unit := do
+  while not (← windowShouldClose) do
+    update
+    render
+
+def main : IO Unit := do
+  runSystem (init *> run *> terminate) (← initWorld)

lean/Examples/Orbital/Types.lean

@@ -0,0 +1,23 @@
+import Raylean
+import ECS
+
+open Raylean
+open Raylean.Types
+open ECS
+
+namespace Orbital
+
+structure Camera where
+  val : Camera2D
+
+structure Position where
+  val : Vector2
+
+structure Velocity where
+  val : Vector2
+
+structure OrbitPath where
+  val : Array Vector2
+
+-- Brings `World` and `initWorld` into scope
+makeWorldAndComponents Camera Position Velocity OrbitPath

lean/Examples/Selector.lean

@@ -16,6 +16,7 @@ inductive Demo where
   | cube3d
   | inputKeys
   | basicECS
+  | orbital
 
 def Demo.all := allElements Demo
 
@@ -27,6 +28,7 @@ def stringToDemo (s : String) : Option Demo :=
   | "cube3d" => some .cube3d
   | "inputkeys" => some .inputKeys
   | "basicecs" => some .basicECS
+  | "orbital" => some .orbital
   | _ => none
 
 def screenWidth : Nat := 800
@@ -51,6 +53,7 @@ def mkDemoInfo : Demo -> DemoInfo
    | .inputKeys => {start := InputKeys.inputKeys, title := "Input keys"}
    | .jessica => {start := JessicaCantSwim.main, title := "Jessica can't swim"}
    | .basicECS => {start := BasicECS.main, title := "Basic ECS"}
+   | .orbital => {start := Orbital.main, title := "Orbital"}
 
 structure DemoRenderInfo where
   /-- The action that starts the demo --/

lean/Raylean/Core.lean

@@ -82,6 +82,9 @@ opaque updateCamera : (camera : Camera3D) → (mode : CameraMode) → IO Camera3
 @[extern "drawCircleV"]
 opaque drawCircleV : (center : Vector2) → (radius : Float) → (color : Color) → IO Unit
 
+@[extern "drawLineV"]
+opaque drawLineV : (startPos : Vector2) → (endPos : Vector2) → (color : Color) → IO Unit
+
 @[extern "drawRectangleRec"]
 opaque drawRectangleRec : (rectangle : Rectangle) → (color : Color) → IO Unit
 

lean/Raylean/Math.lean

@@ -16,4 +16,7 @@ def length (v : Vector2) : Float := Float.sqrt (v.x ^ 2 + v.y ^ 2)
 def sub (v1 : Vector2) (v2 : Vector2) : Vector2 :=
   { x := v1.x - v2.x, y := v1.y - v2.y  }
 
+def mul (v : Vector2) (s : Float) : Vector2 :=
+  { x := s * v.x, y := s * v.y }
+
 end Vector2