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/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..e72b96a --- /dev/null +++ b/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) diff --git a/lean/Examples/Orbital/Types.lean b/lean/Examples/Orbital/Types.lean new file mode 100644 index 0000000..3cefc11 --- /dev/null +++ b/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 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 --/ 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 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