From 6e2fdf8aeebbf677e59c82cd0aa60f3b9d9f8542 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 6 Sep 2024 15:13:14 +0100 Subject: [PATCH 1/4] Setup orbital example --- lean/Examples.lean | 1 + lean/Examples/Orbital.lean | 43 +++++++++++++++++++++++++++++++++++++ lean/Examples/Selector.lean | 3 +++ 3 files changed, 47 insertions(+) create mode 100644 lean/Examples/Orbital.lean diff --git a/lean/Examples.lean b/lean/Examples.lean index b1a2fca..f46a167 100644 --- a/lean/Examples.lean +++ b/lean/Examples.lean @@ -4,3 +4,4 @@ import «Examples».Camera3D import «Examples».Camera2DPlatformer import «Examples».JessicaCantSwim import «Examples».BasicECS +import «Examples».Orbital diff --git a/lean/Examples/Orbital.lean b/lean/Examples/Orbital.lean new file mode 100644 index 0000000..ddeb18d --- /dev/null +++ b/lean/Examples/Orbital.lean @@ -0,0 +1,43 @@ +import Raylean +import ECS + +open Raylean +open Raylean.Types +open ECS + +namespace Orbital + +structure Camera where + camera : Camera2D + +structure Position where + val : Vector2 + +structure Velocity where + val : Vector2 + +inductive Dynamic := + | Dynamic + +-- Brings `World` and `initWorld` into scope +makeWorldAndComponents Camera Position Velocity Dynamic + +def init : System World Unit := do + initWindow 1920 1080 "Orbital" + setTargetFPS 60 + +def terminate : System World Unit := closeWindow + +def update : System World Unit := return () + +def render : System World Unit := + renderFrame do + clearBackground Color.black + +def run : System World Unit := do + while not (← windowShouldClose) do + update + render + +def main : IO Unit := do + runSystem (init *> run *> terminate) (← initWorld) diff --git a/lean/Examples/Selector.lean b/lean/Examples/Selector.lean index 8dfe921..694fd0a 100644 --- a/lean/Examples/Selector.lean +++ b/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 --/ From 2af1e1e70c2a89999b08edbfd655bb9b79a6d01a Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 6 Sep 2024 19:45:40 +0100 Subject: [PATCH 2/4] Add orbital simulation --- lean/Examples/Orbital.lean | 47 ++++++++++++++++++++++---------- lean/Examples/Orbital/Types.lean | 20 ++++++++++++++ lean/Raylean/Math.lean | 3 ++ 3 files changed, 55 insertions(+), 15 deletions(-) create mode 100644 lean/Examples/Orbital/Types.lean diff --git a/lean/Examples/Orbital.lean b/lean/Examples/Orbital.lean index ddeb18d..148f451 100644 --- a/lean/Examples/Orbital.lean +++ b/lean/Examples/Orbital.lean @@ -1,5 +1,6 @@ import Raylean import ECS +import Examples.Orbital.Types open Raylean open Raylean.Types @@ -7,32 +8,48 @@ open ECS namespace Orbital -structure Camera where - camera : Camera2D +def screenWidth : Nat := 1920 +def screenHeight : Nat := 1080 +def center : Vector2 := ⟨screenWidth.toFloat / 2, screenHeight.toFloat / 2⟩ +def origin : Vector2 := ⟨0,0⟩ -structure Position where - val : Vector2 - -structure Velocity where - val : Vector2 - -inductive Dynamic := - | Dynamic +def init : System World Unit := do + let camera : Camera := ⟨center, center, 0, 1⟩ + set' global camera --- Brings `World` and `initWorld` into scope -makeWorldAndComponents Camera Position Velocity Dynamic + let initPos : Vector2 := ⟨5,0⟩ + let initVel : Vector2 := ⟨0, 1.0 / initPos.length |>.sqrt⟩ -def init : System World Unit := do - initWindow 1920 1080 "Orbital" + newEntityAs_ (Position × Not Velocity) (⟨origin⟩, .Not) + newEntityAs_ (Position × Velocity) ⟨⟨initPos⟩, ⟨initVel⟩⟩ + newEntityAs_ (Position × Velocity) ⟨⟨-4, 0⟩, ⟨initVel.mul (-1)⟩⟩ + newEntityAs_ (Position × Velocity) ⟨⟨2, 2⟩, ⟨initVel.mul (-1)⟩⟩ + initWindow screenWidth screenHeight "Orbital" setTargetFPS 60 def terminate : System World Unit := closeWindow -def update : System World Unit := return () +def update : System World Unit := do + let dt ← getFrameTime + cmap (cx := Position × Velocity) <| fun (p, v) => + 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⟩ + (pNew, vNew) 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 def run : System World Unit := do while not (← windowShouldClose) do diff --git a/lean/Examples/Orbital/Types.lean b/lean/Examples/Orbital/Types.lean new file mode 100644 index 0000000..868805b --- /dev/null +++ b/lean/Examples/Orbital/Types.lean @@ -0,0 +1,20 @@ +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 + +-- Brings `World` and `initWorld` into scope +makeWorldAndComponents Camera Position Velocity diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean index a64184c..633ba67 100644 --- a/lean/Raylean/Math.lean +++ b/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 From 73c20f3fd8eb04a535a20c558af54ae6b9edce64 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 6 Sep 2024 20:19:28 +0100 Subject: [PATCH 3/4] Add binding for DrawLineV --- c/raylib_bindings.c | 8 ++++++++ lean/Raylean/Core.lean | 3 +++ 2 files changed, 11 insertions(+) diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c index 42bea9f..8b9fc72 100644 --- a/c/raylib_bindings.c +++ b/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; +} diff --git a/lean/Raylean/Core.lean b/lean/Raylean/Core.lean index 48aaf65..8f86359 100644 --- a/lean/Raylean/Core.lean +++ b/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 From d1d4e555370bb162986e10414540238f99284550 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Fri, 6 Sep 2024 20:19:45 +0100 Subject: [PATCH 4/4] Add smore more orbiting bodies and traces --- lean/Examples/Orbital.lean | 16 +++++++++++----- lean/Examples/Orbital/Types.lean | 5 ++++- 2 files changed, 15 insertions(+), 6 deletions(-) diff --git a/lean/Examples/Orbital.lean b/lean/Examples/Orbital.lean index 148f451..e72b96a 100644 --- a/lean/Examples/Orbital.lean +++ b/lean/Examples/Orbital.lean @@ -21,9 +21,10 @@ def init : System World Unit := do let initVel : Vector2 := ⟨0, 1.0 / initPos.length |>.sqrt⟩ newEntityAs_ (Position × Not Velocity) (⟨origin⟩, .Not) - newEntityAs_ (Position × Velocity) ⟨⟨initPos⟩, ⟨initVel⟩⟩ - newEntityAs_ (Position × Velocity) ⟨⟨-4, 0⟩, ⟨initVel.mul (-1)⟩⟩ - newEntityAs_ (Position × Velocity) ⟨⟨2, 2⟩, ⟨initVel.mul (-1)⟩⟩ + 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 @@ -31,7 +32,7 @@ def terminate : System World Unit := closeWindow def update : System World Unit := do let dt ← getFrameTime - cmap (cx := Position × Velocity) <| fun (p, v) => + cmap (cx := Position × Velocity × OrbitPath) <| fun (p, v, o) => let pv := p.val let pMag := pv.length let a := pv |>.mul (-1 / pMag^3) @@ -40,7 +41,8 @@ def update : System World Unit := do let pvNew := pv.add (vvNew.mul dt) let pNew : Position := ⟨pvNew⟩ let vNew : Velocity := ⟨vvNew⟩ - (pNew, vNew) + let oNew : OrbitPath := ⟨o.val.push pvNew⟩ + (pNew, vNew, oNew) def render : System World Unit := renderFrame do @@ -50,6 +52,10 @@ def render : System World Unit := 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 diff --git a/lean/Examples/Orbital/Types.lean b/lean/Examples/Orbital/Types.lean index 868805b..3cefc11 100644 --- a/lean/Examples/Orbital/Types.lean +++ b/lean/Examples/Orbital/Types.lean @@ -16,5 +16,8 @@ structure Position where structure Velocity where val : Vector2 +structure OrbitPath where + val : Array Vector2 + -- Brings `World` and `initWorld` into scope -makeWorldAndComponents Camera Position Velocity +makeWorldAndComponents Camera Position Velocity OrbitPath