Skip to content

Commit

Permalink
Merge pull request #27 from paulcadman/orbital-vary-velocity
Browse files Browse the repository at this point in the history
Add option to vary the velocity of one of the orbits
  • Loading branch information
paulcadman authored Sep 6, 2024
2 parents f519e2b + 3a75ac3 commit 6ff3457
Show file tree
Hide file tree
Showing 2 changed files with 50 additions and 33 deletions.
75 changes: 46 additions & 29 deletions lean/Examples/Orbital.lean
Original file line number Diff line number Diff line change
Expand Up @@ -13,49 +13,66 @@ 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
def mkOrbitingBody (initPosition initVelocity : Vector2) (selected : Bool := false): System World Unit :=
newEntityAs_ (Position × Velocity × OrbitPath × Selectable) ⟨⟨initPosition⟩, ⟨initVelocity⟩, ⟨#[]⟩, ⟨selected⟩⟩

def mkStaticBody (position : Vector2) : System World Unit :=
newEntityAs_ (Position × Not Velocity) (⟨position⟩, .Not)

def init : System World Unit := do
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)⟩, ⟨#[]⟩⟩
mkStaticBody origin
mkOrbitingBody (selected := true) initPos initVel
mkOrbitingBody ⟨-4, 0⟩ (initVel.mul (-1))
mkOrbitingBody ⟨-0.8, -0.6⟩ (initVel.mul (-0.95))
mkOrbitingBody ⟨1, 1⟩ (initVel.mul (-1))

initWindow screenWidth screenHeight "Orbital"
setTargetFPS 60

def terminate : System World Unit := closeWindow

def updateOrbitingBody (dt : Float) : Position × Velocity × OrbitPath → Position × Velocity × OrbitPath
| (Position.mk p, Velocity.mk v, OrbitPath.mk o) =>
let pMag := p.length
let a := p |>.mul (-1 / pMag^3)
let vNew := v.add (a.mul dt)
let pNew := p.add (vNew.mul dt)
let oNew := o.push pNew
(⟨pNew⟩, ⟨vNew⟩, ⟨oNew⟩)

def changeSelectedVelocity (dv : Float) : Velocity × Selectable → Velocity
| (Velocity.mk v, Selectable.mk true) => ⟨v.add <| v.mul (dv / v.length)⟩
| (Velocity.mk v, Selectable.mk false) => ⟨v⟩

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)
if (← isKeyDown Key.right) then cmap (changeSelectedVelocity 0.01)
if (← isKeyDown Key.left) then cmap (changeSelectedVelocity (-0.01))
cmap (updateOrbitingBody (← getFrameTime))

/-- Convert a Position to a point on the screen --/
def toScreen (v : Vector2) : Vector2 :=
v.mul 100 |>.add center

def renderStaticBody (p : Position) : System World Unit :=
drawCircleV (p.val.add center) 30 Color.red

def renderOrbitingBody (p : Position) (s : Selectable) : System World Unit :=
drawCircleV (toScreen p.val) 10 (if s.selected then Color.green else Color.blue)

def renderOrbitPath (o : OrbitPath) : System World Unit :=
let arr := o.val
for (s, e) in arr.zip (arr.extract 1 arr.size) do
drawLineV (toScreen s) (toScreen e) Color.white

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
cmapM_ (cx := Position × Not Velocity) <| fun (p, _) => renderStaticBody p
cmapM_ (cx := Position × Velocity × Selectable) <| fun (p, _, s) => renderOrbitingBody p s
cmapM_ renderOrbitPath

def run : System World Unit := do
while not (← windowShouldClose) do
Expand Down
8 changes: 4 additions & 4 deletions lean/Examples/Orbital/Types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -7,9 +7,6 @@ open ECS

namespace Orbital

structure Camera where
val : Camera2D

structure Position where
val : Vector2

Expand All @@ -19,5 +16,8 @@ structure Velocity where
structure OrbitPath where
val : Array Vector2

structure Selectable where
selected : Bool

-- Brings `World` and `initWorld` into scope
makeWorldAndComponents Camera Position Velocity OrbitPath
makeWorldAndComponents Position Velocity OrbitPath Selectable

0 comments on commit 6ff3457

Please sign in to comment.