From 377e18ac33ac70d31d16a7d7cb05e94482f497fc Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 25 Sep 2024 00:03:06 +0100
Subject: [PATCH 1/8] Add Lens namespace

---
 lean/Examples/Camera2DPlatformer/Types.lean |  1 +
 lean/Lens/Basic.lean                        | 11 ++++++++---
 lean/Lens/Elab.lean                         |  8 +++++---
 3 files changed, 14 insertions(+), 6 deletions(-)

diff --git a/lean/Examples/Camera2DPlatformer/Types.lean b/lean/Examples/Camera2DPlatformer/Types.lean
index 8ec69da..c466130 100644
--- a/lean/Examples/Camera2DPlatformer/Types.lean
+++ b/lean/Examples/Camera2DPlatformer/Types.lean
@@ -4,6 +4,7 @@ import Lens
 namespace Types
 
 open Raylean.Types
+open Lens
 
 structure Player where
   position : Vector2
diff --git a/lean/Lens/Basic.lean b/lean/Lens/Basic.lean
index 29f24fd..1e51801 100644
--- a/lean/Lens/Basic.lean
+++ b/lean/Lens/Basic.lean
@@ -4,6 +4,8 @@ open Const
 def Lens (s t a b : Type) :=
   ∀ {f : Type → Type} [Functor f], (a → f b) → s → f t
 
+namespace Lens
+
 def view {s a : Type} (l : Lens s s a a) (x : s) : a :=
   (l (fun y => (y : Const a a)) x : Const a s)
 
@@ -15,7 +17,10 @@ def over {s t a b : Type} (l : Lens s t a b) (f : a → b) (x : s) : t :=
 
 infixl:50 " ^. " => flip view
 
+end Lens
+
 namespace Example
+open Lens
 
 structure Name where
   firstname : String
@@ -25,7 +30,7 @@ structure Person where
   name : Name
   age : Nat
 
-namespace Lens
+namespace Example.Lens
 
 def firstname : Lens Name Name String String :=
   fun {f} [Functor f] g p =>
@@ -35,9 +40,9 @@ def name : Lens Person Person Name Name :=
   fun {f} [Functor f] g p =>
     Functor.map (fun newName => { p with name := newName }) (g p.name)
 
-end Lens
+end Example.Lens
 
-open Lens
+open Example.Lens
 
 def exampleView : IO Unit :=
   let person : Person := { name := {firstname := "Alice", surname := "H"}, age := 30 }
diff --git a/lean/Lens/Elab.lean b/lean/Lens/Elab.lean
index a6a523f..9d9c1bc 100644
--- a/lean/Lens/Elab.lean
+++ b/lean/Lens/Elab.lean
@@ -2,7 +2,7 @@ import Lens.Basic
 
 import Lean
 
-namespace Elab
+namespace Lens
 
 /-
 makeLenses T` creates a lens for each field of the structure `T`.
@@ -42,10 +42,12 @@ elab "makeLenses" structIdent:ident : command => do
     elabCommand d
   elabCommand (← `(end $lensNs))
 
-end Elab
+end Lens
 
 namespace Example
 
+open Lens
+
 structure P where
   name : Nat
 
@@ -76,7 +78,7 @@ def exampleView' : IO Unit :=
   IO.println s!"Name: {personName}"
 
 def exampleSet' : IO Unit :=
-  let person := { name := { firstname := "Alice", surname := "H"}, age := 30 }
+  let person : Person' := { name := { firstname := "Alice", surname := "H"}, age := 30 }
   let updatedPerson := set (name ∘ firstname) "Bob" person
   IO.println s!"Updated name: {updatedPerson.name.firstname}"
 

From f8ac433e530c15b93f34aea61f05f87123b900f9 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Wed, 25 Sep 2024 00:04:34 +0100
Subject: [PATCH 2/8] Add 2D graphics library

---
 lean/Examples/Window.lean           |  5 +++
 lean/Raylean.lean                   |  1 +
 lean/Raylean/Graphics2D.lean        |  2 +
 lean/Raylean/Graphics2D/Basic.lean  | 29 ++++++++++++++
 lean/Raylean/Graphics2D/Render.lean | 61 +++++++++++++++++++++++++++++
 lean/Raylean/Lean.lean              |  3 ++
 lean/Raylean/Math.lean              |  2 +
 7 files changed, 103 insertions(+)
 create mode 100644 lean/Raylean/Graphics2D.lean
 create mode 100644 lean/Raylean/Graphics2D/Basic.lean
 create mode 100644 lean/Raylean/Graphics2D/Render.lean
 create mode 100644 lean/Raylean/Lean.lean

diff --git a/lean/Examples/Window.lean b/lean/Examples/Window.lean
index ddef911..f0bfa8c 100644
--- a/lean/Examples/Window.lean
+++ b/lean/Examples/Window.lean
@@ -3,6 +3,7 @@ import «Raylean»
 namespace Window
 
 open Raylean.Types
+open Raylean.Graphics2D
 open Raylean
 
 def screenWidth : Nat := 800
@@ -24,9 +25,13 @@ def render : IO Unit := do
     }
   let origin : Vector2 := ⟨0, 0⟩
   let rotation : Float := 0
+  let rectangle := .rectangle 10 10 |> .color Color.red |> .scale ⟨20,20⟩
+  let circle := (.circle 100 |> .color Color.blue |> .scale ⟨0.5, 0.5⟩)
+  let p := rectangle ++ circle |> .translate ⟨250, -50⟩ |> .scale ⟨1, 2⟩
 
   while not (← windowShouldClose) do
     renderFrame do
+      renderPicture screenWidth.toFloat screenHeight.toFloat p
       clearBackground Color.Raylean.gold
       drawFPS 100 100
       let c := match (← IO.rand 0 6) with
diff --git a/lean/Raylean.lean b/lean/Raylean.lean
index 8c5921b..725d6fb 100644
--- a/lean/Raylean.lean
+++ b/lean/Raylean.lean
@@ -2,3 +2,4 @@ import «Raylean».Core
 import «Raylean».Math
 import «Raylean».Types
 import «Raylean».Frame
+import «Raylean».Graphics2D
diff --git a/lean/Raylean/Graphics2D.lean b/lean/Raylean/Graphics2D.lean
new file mode 100644
index 0000000..abb252b
--- /dev/null
+++ b/lean/Raylean/Graphics2D.lean
@@ -0,0 +1,2 @@
+import Raylean.Graphics2D.Basic
+import Raylean.Graphics2D.Render
diff --git a/lean/Raylean/Graphics2D/Basic.lean b/lean/Raylean/Graphics2D/Basic.lean
new file mode 100644
index 0000000..4e1ec49
--- /dev/null
+++ b/lean/Raylean/Graphics2D/Basic.lean
@@ -0,0 +1,29 @@
+import Raylean.Types
+
+open Raylean.Types
+
+namespace Raylean.Graphics2D
+
+inductive Picture : Type where
+  | blank : Picture
+  | line (path : Array Vector2) : Picture
+  | circle (radius : Float) : Picture
+  | rectangle (width : Float) (height : Float)
+  | image : Image → Picture
+  | imageSelection (subsection : Rectangle) : Image → Picture
+  | text : String → Picture
+  | color : Color → Picture → Picture
+  | translate : Vector2 → Picture → Picture
+  | scale : Vector2 → Picture → Picture
+  | rotate : Float → Picture → Picture
+  | pictures : Array Picture → Picture
+
+instance : Inhabited Picture where
+  default := .blank
+
+instance : Append Picture where
+  append : Picture → Picture → Picture
+   | (.pictures ps1), (.pictures ps2) => .pictures <| ps1 ++ ps2
+   | (.pictures ps), p => .pictures <| ps.push p
+   | p, (.pictures ps) => .pictures <| #[p] ++ ps
+   | p1, p2 => .pictures #[p1, p2]
diff --git a/lean/Raylean/Graphics2D/Render.lean b/lean/Raylean/Graphics2D/Render.lean
new file mode 100644
index 0000000..c1e1063
--- /dev/null
+++ b/lean/Raylean/Graphics2D/Render.lean
@@ -0,0 +1,61 @@
+import Raylean.Core
+import Raylean.Types
+import Raylean.Math
+import Raylean.Graphics2D.Basic
+import Lens
+import Raylean.Lean
+
+open Raylean.Types
+open Lens
+
+namespace Raylean.Graphics2D
+
+structure RenderState where
+  scale : Vector2
+  color : Color
+  translate : Vector2
+  center : Vector2
+
+def RenderState.doTranslate (s : RenderState) (v : Vector2) : Vector2 :=
+  ⟨v.x + s.translate.x, v.y - s.translate.y⟩
+
+def RenderState.toScreen (s : RenderState) (v : Vector2) : Vector2 :=
+  s.doTranslate ⟨s.center.x + s.scale.x * v.x, s.center.y - s.scale.y * v.y⟩
+
+makeLenses RenderState
+
+open RenderState.Lens
+
+def renderLine (points : Array Vector2) : ReaderT RenderState IO Unit :=
+  for (startPoint, endPoint) in points.zip (points.extract 1 points.size) do
+    let s ← read
+    drawLineV (s.toScreen startPoint) (s.toScreen endPoint) s.color
+
+def renderCircle (radius : Float) : ReaderT RenderState IO Unit := do
+  let s ← read
+  drawCircleV (s.doTranslate s.center) (radius * (max 0 (max s.scale.x s.scale.y))) s.color
+
+def renderRectangle (width height : Float) : ReaderT RenderState IO Unit := do
+  let s ← read
+  let topLeft : Vector2 := ⟨-width / 2, height / 2⟩
+  let p := s.toScreen topLeft
+  let r : Rectangle := {x := p.x, y := p.y, width := s.scale.x * width, height := s.scale.y * height}
+  drawRectangleRec r s.color
+
+partial def renderPicture' : (picture : Picture) → ReaderT RenderState IO Unit
+  | .blank => return ()
+  | .line ps => renderLine ps
+  | .circle radius => renderCircle radius
+  | .rectangle width height => renderRectangle width height
+  | .color c p  => renderPicture' p |>.local (set color c)
+  | .translate v p => renderPicture' p |>.local (over translate (·.add v))
+  | .scale v p => renderPicture'  p |>.local (over scale (·.dot v))
+  | .pictures ps => (fun _ => ()) <$> ps.mapM renderPicture'
+  | .rotate _ _ => return ()
+  | .text _ => return ()
+  | .image _ => return ()
+  | .imageSelection _ _ => return ()
+
+def renderPicture (width height : Float) (picture : Picture) : IO Unit :=
+  let initState := {scale := ⟨1,1⟩, color := Color.transparent, translate := ⟨0,0⟩, center := ⟨width / 2, height / 2⟩}
+  renderPicture' picture |>.run initState
diff --git a/lean/Raylean/Lean.lean b/lean/Raylean/Lean.lean
new file mode 100644
index 0000000..265f6a1
--- /dev/null
+++ b/lean/Raylean/Lean.lean
@@ -0,0 +1,3 @@
+
+/-- Execute a computation in a modified environment --/
+def ReaderT.local {ρ : Type u} (f : ρ → ρ) (r : ReaderT ρ m α) : ReaderT ρ m α := r.run ∘ f
diff --git a/lean/Raylean/Math.lean b/lean/Raylean/Math.lean
index 633ba67..ce5e654 100644
--- a/lean/Raylean/Math.lean
+++ b/lean/Raylean/Math.lean
@@ -19,4 +19,6 @@ def sub (v1 : Vector2) (v2 : Vector2) : Vector2 :=
 def mul (v : Vector2) (s : Float) : Vector2 :=
   { x := s * v.x, y := s * v.y }
 
+def dot (v1 v2 : Vector2) : Vector2 := ⟨v1.x * v2.x, v1.y * v2.y⟩
+
 end Vector2

From adcf107c52ff13f03c9fe19f2f784025c64c4122 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 20:57:22 +0100
Subject: [PATCH 3/8] Add cfold and collect system functions

---
 lean/ECS/System.lean | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

diff --git a/lean/ECS/System.lean b/lean/ECS/System.lean
index 69d680b..1711822 100644
--- a/lean/ECS/System.lean
+++ b/lean/ECS/System.lean
@@ -143,3 +143,26 @@ def cmapM_
   for ety in sl do
     let x ← getX.explGet stx ety
     sys (compX.constraint.mp x)
+
+def cfold
+  [FamilyDef StorageFam cx sx]
+  [FamilyDef ElemFam sx tx]
+  [compX : @Component cx sx tx _ _]
+  [@Has w cx sx _]
+  [getX : @ExplGet sx tx _]
+  [mX : ExplMembers sx]
+  (f : a → cx → a) (accInit : a) : System w a := do
+  let stx ← Has.getStore cx
+  let sl ← mX.explMembers stx
+  sl.foldlM (fun a e => (f a ∘ compX.constraint.mp) <$> getX.explGet stx e) accInit
+
+/-- collect matching components into an array using the specified test/process function -/
+def collect
+  [FamilyDef StorageFam cx sx]
+  [FamilyDef ElemFam sx tx]
+  [@Component cx sx tx _ _]
+  [@Has w cx sx _]
+  [@ExplGet sx tx _]
+  [ExplMembers sx]
+  (f : cx → Option a) : System w (Array a) :=
+    cfold (fun acc e => f e |>.elim acc acc.push) #[]

From a79b33d60e588a83e5f2446150e52e7f18a6d351 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 20:57:50 +0100
Subject: [PATCH 4/8] Add binding for drawLineStrip

---
 c/raylib_bindings.c    | 11 +++++++++++
 lean/Raylean/Core.lean |  3 +++
 2 files changed, 14 insertions(+)

diff --git a/c/raylib_bindings.c b/c/raylib_bindings.c
index 8b9fc72..e4963a9 100644
--- a/c/raylib_bindings.c
+++ b/c/raylib_bindings.c
@@ -505,3 +505,14 @@ lean_obj_res drawLineV(lean_obj_arg startPos_arg, lean_obj_arg endPos_arg, lean_
   DrawLineV(startPos, endPos, color);
   return IO_UNIT;
 }
+
+lean_obj_res drawLineStrip(b_lean_obj_arg points_arg, lean_obj_arg color_arg) {
+  size_t pointCount = lean_array_size(points_arg);
+  Vector2* points = malloc(pointCount * sizeof(Vector2));
+  for (size_t i = 0; i < pointCount; i++) {
+    points[i] = vector2_of_arg(lean_array_get_core(points_arg, i));
+  }
+  DrawLineStrip(points, pointCount, color_of_arg(color_arg));
+  free(points);
+  return IO_UNIT;
+}
diff --git a/lean/Raylean/Core.lean b/lean/Raylean/Core.lean
index 89640d0..61a5491 100644
--- a/lean/Raylean/Core.lean
+++ b/lean/Raylean/Core.lean
@@ -85,6 +85,9 @@ opaque drawCircleV : (center : @& Vector2) → (radius : Float) → (color : @&
 @[extern "drawLineV"]
 opaque drawLineV : (startPos : @& Vector2) → (endPos : @& Vector2) → (color : @& Color) → IO Unit
 
+@[extern "drawLineStrip"]
+opaque drawLineStrip : (points : @& Array Vector2) → (color : @& Color) → IO Unit
+
 @[extern "drawRectangleRec"]
 opaque drawRectangleRec : (rectangle : @& Rectangle) → (color : @& Color) → IO Unit
 

From 2cdedff8a4c85601ade4c9a7a92e6eb331daa8e4 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 20:58:34 +0100
Subject: [PATCH 5/8] Remove unused 2d graphics constructors for now

---
 lean/Raylean/Graphics2D/Basic.lean  | 4 ----
 lean/Raylean/Graphics2D/Render.lean | 4 ----
 2 files changed, 8 deletions(-)

diff --git a/lean/Raylean/Graphics2D/Basic.lean b/lean/Raylean/Graphics2D/Basic.lean
index 4e1ec49..e28e796 100644
--- a/lean/Raylean/Graphics2D/Basic.lean
+++ b/lean/Raylean/Graphics2D/Basic.lean
@@ -9,13 +9,9 @@ inductive Picture : Type where
   | line (path : Array Vector2) : Picture
   | circle (radius : Float) : Picture
   | rectangle (width : Float) (height : Float)
-  | image : Image → Picture
-  | imageSelection (subsection : Rectangle) : Image → Picture
-  | text : String → Picture
   | color : Color → Picture → Picture
   | translate : Vector2 → Picture → Picture
   | scale : Vector2 → Picture → Picture
-  | rotate : Float → Picture → Picture
   | pictures : Array Picture → Picture
 
 instance : Inhabited Picture where
diff --git a/lean/Raylean/Graphics2D/Render.lean b/lean/Raylean/Graphics2D/Render.lean
index c1e1063..b3b63b5 100644
--- a/lean/Raylean/Graphics2D/Render.lean
+++ b/lean/Raylean/Graphics2D/Render.lean
@@ -51,10 +51,6 @@ partial def renderPicture' : (picture : Picture) → ReaderT RenderState IO Unit
   | .translate v p => renderPicture' p |>.local (over translate (·.add v))
   | .scale v p => renderPicture'  p |>.local (over scale (·.dot v))
   | .pictures ps => (fun _ => ()) <$> ps.mapM renderPicture'
-  | .rotate _ _ => return ()
-  | .text _ => return ()
-  | .image _ => return ()
-  | .imageSelection _ _ => return ()
 
 def renderPicture (width height : Float) (picture : Picture) : IO Unit :=
   let initState := {scale := ⟨1,1⟩, color := Color.transparent, translate := ⟨0,0⟩, center := ⟨width / 2, height / 2⟩}

From ca9363bcacc070dffe83859cf2e5b6e5ebaf5b36 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 20:59:53 +0100
Subject: [PATCH 6/8] Rename RenderState to RenderContext

---
 lean/Raylean/Graphics2D/Render.lean | 42 ++++++++++++++++-------------
 1 file changed, 23 insertions(+), 19 deletions(-)

diff --git a/lean/Raylean/Graphics2D/Render.lean b/lean/Raylean/Graphics2D/Render.lean
index b3b63b5..09336c8 100644
--- a/lean/Raylean/Graphics2D/Render.lean
+++ b/lean/Raylean/Graphics2D/Render.lean
@@ -10,39 +10,43 @@ open Lens
 
 namespace Raylean.Graphics2D
 
-structure RenderState where
+structure RenderContext where
   scale : Vector2
   color : Color
   translate : Vector2
   center : Vector2
 
-def RenderState.doTranslate (s : RenderState) (v : Vector2) : Vector2 :=
+/-- Translate a point in screen coordinates -/
+def RenderContext.screenTranslate (s : RenderContext) (v : Vector2) : Vector2 :=
   ⟨v.x + s.translate.x, v.y - s.translate.y⟩
 
-def RenderState.toScreen (s : RenderState) (v : Vector2) : Vector2 :=
-  s.doTranslate ⟨s.center.x + s.scale.x * v.x, s.center.y - s.scale.y * v.y⟩
+/-- Convert a point in Picture coordinates to a point in screen coordinates -/
+def RenderContext.toScreen (s : RenderContext) (v : Vector2) : Vector2 :=
+  s.screenTranslate ⟨s.center.x + s.scale.x * v.x, s.center.y - s.scale.y * v.y⟩
 
-makeLenses RenderState
+abbrev getContext : ReaderT RenderContext IO RenderContext := read
 
-open RenderState.Lens
+makeLenses RenderContext
 
-def renderLine (points : Array Vector2) : ReaderT RenderState IO Unit :=
-  for (startPoint, endPoint) in points.zip (points.extract 1 points.size) do
-    let s ← read
-    drawLineV (s.toScreen startPoint) (s.toScreen endPoint) s.color
+open RenderContext.Lens
 
-def renderCircle (radius : Float) : ReaderT RenderState IO Unit := do
-  let s ← read
-  drawCircleV (s.doTranslate s.center) (radius * (max 0 (max s.scale.x s.scale.y))) s.color
+def renderLine (points : Array Vector2) : ReaderT RenderContext IO Unit := do
+  let ctx ← getContext
+  drawLineStrip (points.map ctx.toScreen) ctx.color
 
-def renderRectangle (width height : Float) : ReaderT RenderState IO Unit := do
-  let s ← read
+def renderCircle (radius : Float) : ReaderT RenderContext IO Unit := do
+  let ctx ← getContext
+  drawCircleV (ctx.screenTranslate ctx.center) (radius * (max 0 (max ctx.scale.x ctx.scale.y))) ctx.color
+
+def renderRectangle (width height : Float) : ReaderT RenderContext IO Unit := do
+  let ctx ← getContext
   let topLeft : Vector2 := ⟨-width / 2, height / 2⟩
-  let p := s.toScreen topLeft
-  let r : Rectangle := {x := p.x, y := p.y, width := s.scale.x * width, height := s.scale.y * height}
-  drawRectangleRec r s.color
+  let p := ctx.toScreen topLeft
+  let r : Rectangle := {x := p.x, y := p.y, width := ctx.scale.x * width, height := ctx.scale.y * height}
+  drawRectangleRec r ctx.color
 
-partial def renderPicture' : (picture : Picture) → ReaderT RenderState IO Unit
+-- This function is partial because lean cannot prove termination
+partial def renderPicture' : (picture : Picture) → ReaderT RenderContext IO Unit
   | .blank => return ()
   | .line ps => renderLine ps
   | .circle radius => renderCircle radius

From 7c30035a947db86a07cead42d0b582f00c61bdf2 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 21:00:26 +0100
Subject: [PATCH 7/8] Update Window 2d graphics example

---
 lean/Examples/Window.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lean/Examples/Window.lean b/lean/Examples/Window.lean
index f0bfa8c..2137239 100644
--- a/lean/Examples/Window.lean
+++ b/lean/Examples/Window.lean
@@ -27,7 +27,8 @@ def render : IO Unit := do
   let rotation : Float := 0
   let rectangle := .rectangle 10 10 |> .color Color.red |> .scale ⟨20,20⟩
   let circle := (.circle 100 |> .color Color.blue |> .scale ⟨0.5, 0.5⟩)
-  let p := rectangle ++ circle |> .translate ⟨250, -50⟩ |> .scale ⟨1, 2⟩
+  let line :=  .line #[⟨100, 100⟩, ⟨200, 200⟩] |> .color Color.black
+  let p : Picture := line ++ (rectangle ++ circle |> .translate ⟨250, -50⟩ |> .scale ⟨1, 2⟩)
 
   while not (← windowShouldClose) do
     renderFrame do

From f19f216e5fbfef68d2f2eccbadb27ae1b9ea20c6 Mon Sep 17 00:00:00 2001
From: Paul Cadman <git@paulcadman.dev>
Date: Sat, 12 Oct 2024 21:00:53 +0100
Subject: [PATCH 8/8] Update orbital to use Graphics2D

---
 lean/Examples/Orbital.lean | 63 +++++++++++++++++++++-----------------
 1 file changed, 35 insertions(+), 28 deletions(-)

diff --git a/lean/Examples/Orbital.lean b/lean/Examples/Orbital.lean
index 4f33c32..c93165d 100644
--- a/lean/Examples/Orbital.lean
+++ b/lean/Examples/Orbital.lean
@@ -1,19 +1,19 @@
 import Raylean
 import ECS
 import Examples.Orbital.Types
+import Raylean.Graphics2D
 
 open Raylean
 open Raylean.Types
 open ECS
+open Raylean.Graphics2D
 
 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 initPos : Vector2 := ⟨5,0⟩
-def initVel : Vector2 := ⟨0, 1.0 / initPos.length |>.sqrt⟩
+def initVel : Vector2 := ⟨0, 1.0 / initPos.length |>.sqrt |>.neg⟩
 
 def mkOrbitingBody (initPosition initVelocity : Vector2) : System World Unit :=
   newEntityAs_ (Position × Velocity × OrbitPath) ⟨⟨initPosition⟩, ⟨initVelocity⟩, ⟨#[]⟩⟩
@@ -26,20 +26,18 @@ def mkStaticBody (mass : Float) (position : Vector2) : System World Unit :=
 
 def init : System World Unit := do
 
-  mkStaticBody 1 origin
-  mkStaticBody 0.5 (origin.add ⟨3, 3⟩)
-  mkStaticBody 0.5 (origin.add ⟨-1, 3⟩)
-  mkStaticBody 0.5 (origin.add ⟨-4, -4⟩)
+  mkStaticBody 1 ⟨0,0⟩
+  mkStaticBody 0.5 ⟨3, -3⟩
+  mkStaticBody 0.5 ⟨-1, -3⟩
+  mkStaticBody 0.5 ⟨-4, 4⟩
   mkPlayer initPos initVel
   mkOrbitingBody ⟨-4, 0⟩ (initVel.mul (-1))
-  mkOrbitingBody ⟨-0.8, -0.6⟩ (initVel.mul (-0.95))
-  mkOrbitingBody ⟨1, 1⟩ (initVel.mul (-1))
+  mkOrbitingBody ⟨-0.8, 0.6⟩ (initVel.mul (-0.95))
+  mkOrbitingBody ⟨1, 1⟩ initVel
 
   initWindow screenWidth screenHeight "Orbital"
   setTargetFPS 60
 
-def terminate : System World Unit := closeWindow
-
 def updateWithStatic (dt : Float) (staticBodies : Array (Mass × Position)) : Position × Velocity × OrbitPath → Position × Velocity × OrbitPath
   | ⟨⟨po⟩, ⟨v⟩, ⟨o⟩⟩ => Id.run do
     -- compute the new velocity from contributions from each static body
@@ -74,34 +72,43 @@ def resetPlayer : Position × Velocity × OrbitPath × Player → Position × Ve
 def update : System World Unit := do
   if (← isKeyDown Key.up) then cmap (changeVelocity 0.01)
   if (← isKeyDown Key.down) then cmap (changeVelocity (-0.01))
-  if (← isKeyDown Key.right) then cmap (changePerpVelocity (0.01))
-  if (← isKeyDown Key.left) then cmap (changePerpVelocity (-0.01))
+  if (← isKeyDown Key.right) then cmap (changePerpVelocity (-0.01))
+  if (← isKeyDown Key.left) then cmap (changePerpVelocity (0.01))
   if (← isKeyDown Key.space) then cmap resetOrbitPath
   if (← isKeyDown Key.r) then cmap resetPlayer
   updateOrbitingBody (← getFrameTime)
 
-/-- Convert a Position to a point on the screen --/
-def toScreen (v : Vector2) : Vector2 :=
-  v.mul 100 |>.add center
+def translateScale (v : Vector2) : Vector2 :=
+  v.mul 100
+
+def bodyScale (mass : Mass) : Float := mass.val * 30
 
-def renderStaticBody (mass : Mass) (p : Position) : System World Unit :=
-    drawCircleV (toScreen p.val) (mass.val * 30) Color.red
+def staticBody (mass : Mass) (p : Position) : Picture :=
+  .circle (bodyScale mass) |>
+  .color .red |>
+  .translate (translateScale p.val)
 
-def renderOrbitingBody (p : Position) (c : Color) : System World Unit :=
-  drawCircleV (toScreen p.val) 10 c
+def orbitingBody (p : Position) (c : Color) : Picture :=
+  .circle 10 |>
+  .color c |>
+  .translate (translateScale p.val)
 
-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 orbitPath (o : OrbitPath) : Picture :=
+  .line (o.val.map (translateScale ·)) |> .color .white
+
+def gamePicture : System World Picture := do
+  let staticBodies ← collect (cx := Mass × Position × Not Velocity) <| fun (m, p, _) => staticBody m p |> some
+  let playerOrbitingBody ← collect (cx := Player × Position × Velocity) <| fun (_, p, _) => orbitingBody p .green |> some
+  let orbitingBodies ← collect (cx := Position × Velocity × Not Player) <| fun (p, _, _) => orbitingBody p .blue |> some
+  let orbitPaths ← collect <| fun o => orbitPath o |> some
+  return (.pictures (staticBodies ++ playerOrbitingBody ++ orbitingBodies ++ orbitPaths))
 
 def render : System World Unit :=
   renderFrame do
     clearBackground Color.black
-    cmapM_ (cx := Mass × Position × Not Velocity) <| fun (m, p, _) => renderStaticBody m p
-    cmapM_ (cx := Position × Velocity × Player) <| fun (p, _, _) => renderOrbitingBody p Color.green
-    cmapM_ (cx := Position × Velocity × Not Player) <| fun (p, _, _) => renderOrbitingBody p Color.blue
-    cmapM_ renderOrbitPath
+    renderPicture screenWidth.toFloat screenHeight.toFloat (← gamePicture)
+
+def terminate : System World Unit := closeWindow
 
 def run : System World Unit := do
   while not (← windowShouldClose) do