Merge pull request #30 from paulcadman/bouncing_ball

Add bouncing ball example

lean/Examples.lean

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

lean/Examples/BouncingBall.lean

@@ -0,0 +1,92 @@
+import Raylean
+import ECS
+
+open Raylean
+open Raylean.Types
+open ECS
+
+namespace BouncingBall
+
+structure Position where
+  val : Vector2
+
+structure Velocity where
+  val : Vector2
+
+structure Config where
+  shapeRadius : Float
+  screenWidth : Float
+  screenHeight : Float
+  velocity : Vector2
+
+inductive Circle :=
+  | Circle
+
+-- Brings `World` and `initWorld` into scope
+makeWorldAndComponents Position Velocity Config Circle
+
+def init : System World Unit := do
+  let screenWidth := 800
+  let screenHeight := 600
+  set' global
+    { shapeRadius := 20
+    , screenWidth := screenWidth.toFloat
+    , screenHeight := screenHeight.toFloat
+    , velocity := ⟨300, 250⟩
+    : Config
+    }
+  initWindow screenWidth screenHeight "Bouncing ball"
+  setTargetFPS 120
+
+def newBall (p : Vector2) : System World Unit := do
+  let c : Config ← get global
+  newEntityAs_ (Position × Velocity × Circle) (⟨p⟩, ⟨c.velocity⟩, .Circle)
+
+def newSquare (p : Vector2) : System World Unit := do
+  let c : Config ← get global
+  newEntityAs_ (Position × Velocity × Not Circle) (⟨p⟩, ⟨c.velocity.mul (-1)⟩, .Not)
+
+def renderBall : Position × Circle → System World Unit
+  | (⟨p⟩, _) => do
+    let c : Config ← get global
+    drawCircleV p c.shapeRadius Color.Raylean.maroon
+
+def renderSquare : Position × Not Circle → System World Unit
+  | (⟨p⟩, _) => do
+    let c : Config ← get global
+    drawRectangleRec ⟨p.x - c.shapeRadius, p.y - c.shapeRadius, 2 * c.shapeRadius, 2 * c.shapeRadius⟩ Color.Raylean.green
+
+def updateShape (dt : Float) (c : Config) : Position × Velocity → Position × Velocity
+  | (⟨p⟩, ⟨v⟩) =>
+    let position := p.add (v.mul dt)
+    let velocity : Vector2 :=
+      ⟨
+        if position.x >= c.screenWidth - c.shapeRadius || position.x <= c.shapeRadius then v.x * (-1.0) else v.x,
+        if position.y >= c.screenHeight - c.shapeRadius || position.y <= c.shapeRadius then v.y * (-1.0) else v.y
+      ⟩
+    (⟨position⟩, ⟨velocity⟩)
+
+def removeAll (_ : Position) : Not Position := .Not
+
+def update : System World Unit := do
+  let c : Config ← get global
+  if (← isMouseButtonPressed MouseButton.left) then newBall (← getMousePosition)
+  if (← isMouseButtonPressed MouseButton.right) then newSquare (← getMousePosition)
+  if (← isKeyDown Key.space) then cmap removeAll
+  cmap (updateShape (← getFrameTime) c)
+
+def render : System World Unit := do
+  renderFrame do
+    clearBackground Color.white
+    cmapM_ renderBall
+    cmapM_ renderSquare
+
+def run : System World Unit := do
+  while not (← windowShouldClose) do
+    update
+    render
+
+def terminate : System World Unit := closeWindow
+
+def main : IO Unit := do
+  runSystem (init *> run *> terminate) (← initWorld)

lean/Examples/Selector.lean

@@ -17,6 +17,7 @@ inductive Demo where
   | inputKeys
   | basicECS
   | orbital
+  | bouncingBall
 
 def Demo.all := allElements Demo
 
@@ -29,6 +30,7 @@ def stringToDemo (s : String) : Option Demo :=
   | "inputkeys" => some .inputKeys
   | "basicecs" => some .basicECS
   | "orbital" => some .orbital
+  | "bouncingball" => some .bouncingBall
   | _ => none
 
 def screenWidth : Nat := 800
@@ -54,6 +56,7 @@ def mkDemoInfo : Demo -> DemoInfo
    | .jessica => {start := JessicaCantSwim.main, title := "Jessica can't swim"}
    | .basicECS => {start := BasicECS.main, title := "Basic ECS"}
    | .orbital => {start := Orbital.main, title := "Orbital"}
+   | .bouncingBall => {start := BouncingBall.main, title := "Bouncing Ball"}
 
 structure DemoRenderInfo where
   /-- The action that starts the demo --/