Merge pull request #39 from paulcadman/2d-graphics

Add 2D Graphics library

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;
+}

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) #[]

lean/Examples/Camera2DPlatformer/Types.lean

@@ -4,6 +4,7 @@ import Lens
 namespace Types
 
 open Raylean.Types
+open Lens
 
 structure Player where
   position : Vector2

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

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,14 @@ 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 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
+      renderPicture screenWidth.toFloat screenHeight.toFloat p
       clearBackground Color.Raylean.gold
       drawFPS 100 100
       let c := match (← IO.rand 0 6) with

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 }

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}"
 

lean/Raylean.lean

@@ -2,3 +2,4 @@ import «Raylean».Core
 import «Raylean».Math
 import «Raylean».Types
 import «Raylean».Frame
+import «Raylean».Graphics2D

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
 

lean/Raylean/Graphics2D.lean

@@ -0,0 +1,2 @@
+import Raylean.Graphics2D.Basic
+import Raylean.Graphics2D.Render

lean/Raylean/Graphics2D/Basic.lean

@@ -0,0 +1,25 @@
+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)
+  | color : Color → Picture → Picture
+  | translate : Vector2 → Picture → Picture
+  | scale : Vector2 → 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]

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 RenderContext where
+  scale : Vector2
+  color : Color
+  translate : Vector2
+  center : 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⟩
+
+/-- 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⟩
+
+abbrev getContext : ReaderT RenderContext IO RenderContext := read
+
+makeLenses RenderContext
+
+open RenderContext.Lens
+
+def renderLine (points : Array Vector2) : ReaderT RenderContext IO Unit := do
+  let ctx ← getContext
+  drawLineStrip (points.map ctx.toScreen) ctx.color
+
+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 := 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
+
+-- 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
+  | .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'
+
+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

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

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