Improve API for global entity

lean/ECS/EntityCounter.lean

@@ -4,13 +4,9 @@ import ECS.System
 
 namespace ECS
 
-def global : Entity := ⟨0⟩
-
 structure EntityCounter where
   getCounter : Nat
-
-instance : Inhabited EntityCounter where
-  default := ⟨1⟩
+  deriving Inhabited
 
 axiom StorageEntityCounter : StorageFam EntityCounter = GlobalStorage EntityCounter
 instance : FamilyDef StorageFam EntityCounter (GlobalStorage EntityCounter) := ⟨StorageEntityCounter⟩
@@ -19,28 +15,18 @@ instance : @Component EntityCounter (GlobalStorage EntityCounter) EntityCounter
   constraint := rfl
 
 def nextEntity
-  [FamilyDef StorageFam EntityCounter s]
-  [FamilyDef ElemFam s t]
-  [@Component EntityCounter s t _ _]
-  [@Has w EntityCounter s _]
-  [@ExplGet s t _]
-  [@ExplSet s t _]
+  [@Has w EntityCounter (GlobalStorage EntityCounter) _]
   : System w Entity := do
-  let g : EntityCounter ← get global
-  set' global (EntityCounter.mk (g.getCounter + 1))
+  let g : EntityCounter ← getGlobal
+  setGlobal (EntityCounter.mk (g.getCounter + 1))
   return ⟨g.getCounter⟩
 
 def newEntity
   [FamilyDef StorageFam c s]
   [FamilyDef ElemFam s t]
-  [FamilyDef StorageFam EntityCounter se]
-  [FamilyDef ElemFam se te]
   [@Component c s t _ _]
-  [@Component EntityCounter se te _ _]
-  [@Has w EntityCounter se _]
+  [@Has w EntityCounter (GlobalStorage EntityCounter) _]
   [@Has w c s _]
-  [@ExplGet se te _]
-  [@ExplSet se te _]
   [@ExplSet s t _]
   (x : c) : System w Entity := do
   let ety ← nextEntity
@@ -50,14 +36,9 @@ def newEntity
 def newEntity_
   [FamilyDef StorageFam c s]
   [FamilyDef ElemFam s t]
-  [FamilyDef StorageFam EntityCounter se]
-  [FamilyDef ElemFam se te]
   [@Component c s t _ _]
-  [@Component EntityCounter se te _ _]
-  [@Has w EntityCounter se _]
+  [@Has w EntityCounter (GlobalStorage EntityCounter) _]
   [@Has w c s _]
-  [@ExplGet se te _]
-  [@ExplSet se te _]
   [@ExplSet s t _]
   (x : c) : System w Unit := do
   let ety ← nextEntity
@@ -67,14 +48,9 @@ def newEntityAs_
   (c : Type)
   [FamilyDef StorageFam c s]
   [FamilyDef ElemFam s t]
-  [FamilyDef StorageFam EntityCounter se]
-  [FamilyDef ElemFam se te]
   [@Component c s t _ _]
-  [@Component EntityCounter se te _ _]
-  [@Has w EntityCounter se _]
+  [@Has w EntityCounter (GlobalStorage EntityCounter) _]
   [@Has w c s _]
-  [@ExplGet se te _]
-  [@ExplSet se te _]
   [@ExplSet s t _]
   (x : c) : System w Unit := do
   let ety ← nextEntity

lean/ECS/System.lean

@@ -1,12 +1,17 @@
 import ECS.Basic
+import ECS.Store
 
 namespace ECS
 
 /-- Run a system in a game world --/
 def runSystem (s : System w α) (world : w) : IO α := s.run world
 
+/-- The entity used in `getGlobal` and `setGlobal`.-/
+def global : Entity := ⟨0⟩
+
 /-- Read a component --/
 def get
+  {w c s t : Type}
   [FamilyDef StorageFam c s]
   [FamilyDef ElemFam s t]
   [comp : @Component c s t _ _]
@@ -16,10 +21,17 @@ def get
     let s ← Has.getStore c
     comp.constraint.mp <$> e.explGet s ety
 
+def getGlobal
+  {w c : Type}
+  [FamilyDef StorageFam c (GlobalStorage c)]
+  [@Component c (GlobalStorage c) c _ _]
+  [@Has w c (GlobalStorage c) _]
+  [@ExplGet (GlobalStorage c) c _] : System w c := get global
+
 -- TODO: I want to call this `set` but it conflicts with a Prelude function
 /-- Writes a component to the given entity. Will overwrite existing components --/
 def set'
-  {c s t : Type}
+  {w c s t : Type}
   [FamilyDef StorageFam c s]
   [FamilyDef ElemFam s t]
   [comp : @Component c s t _ _]
@@ -30,6 +42,13 @@ def set'
     let s ← Has.getStore c
     e.explSet s ety (comp.constraint.symm.mp x)
 
+def setGlobal
+  {w c : Type}
+  [FamilyDef StorageFam c (GlobalStorage c)]
+  [@Component c (GlobalStorage c) c _ _]
+  [@Has w c (GlobalStorage c) _]
+  (x : c) : System w Unit := set' global x
+
 /-- Returns whether the given entity has component c --/
 def exists?
   (c : Type)

lean/Examples/BouncingBall.lean

@@ -26,35 +26,38 @@ inductive Circle :=
 -- Brings `World` and `initWorld` into scope
 makeWorldAndComponents [Position, Velocity, Circle] [Config] []
 
-def init : System World Unit := do
-  let screenWidth := 800
-  let screenHeight := 600
-  set' global
+def screenWidth := 800
+def screenHeight := 600
+
+def initConfig  : Config :=
     { shapeRadius := 20
     , screenWidth := screenWidth.toFloat
     , screenHeight := screenHeight.toFloat
     , velocity := ⟨300, 250⟩
     : Config
     }
+
+def init : System World Unit := do
   initWindow screenWidth screenHeight "Bouncing ball"
+  setGlobal initConfig
   setTargetFPS 120
 
 def newBall (p : Vector2) : System World Unit := do
-  let c : Config ← get global
+  let c : Config ← getGlobal
   newEntityAs_ (Position × Velocity × Circle) (⟨p⟩, ⟨c.velocity⟩, .Circle)
 
 def newSquare (p : Vector2) : System World Unit := do
-  let c : Config ← get global
+  let c : Config ← getGlobal
   newEntityAs_ (Position × Velocity × Not Circle) (⟨p⟩, ⟨c.velocity.mul (-1)⟩, .Not)
 
 def renderBall : Position × Circle → System World Unit
   | (⟨p⟩, _) => do
-    let c : Config ← get global
+    let c : Config ← getGlobal
     drawCircleV p c.shapeRadius Color.Raylean.maroon
 
 def renderSquare : Position × Not Circle → System World Unit
   | (⟨p⟩, _) => do
-    let c : Config ← get global
+    let c : Config ← getGlobal
     drawRectangleRec ⟨p.x - c.shapeRadius, p.y - c.shapeRadius, 2 * c.shapeRadius, 2 * c.shapeRadius⟩ Color.Raylean.green
 
 def updateShape (dt : Float) (c : Config) : Position × Velocity → Position × Velocity
@@ -87,7 +90,7 @@ def deleteAt'' (pos : Vector2) (radius : Float) : Position → System World (Uni
     then return .inr .Not else return .inl ()
 
 def update : System World Unit := do
-  let c : Config ← get global
+  let c : Config ← getGlobal
   if (← isMouseButtonPressed MouseButton.left) then
     if (← isKeyDown Key.r) then cmapM (deleteAt (← getMousePosition) c.shapeRadius)
                            else newBall (← getMousePosition)

lean/Raylean/Graphics2D/Render.lean

@@ -49,11 +49,11 @@ partial def renderPicture' : (picture : Picture) → ReaderT RenderContext IO Un
   | .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 (fun s =>
+  | .color c p  => ReaderT.local (set color c) (renderPicture' p)
+  | .translate v p => ReaderT.local (fun s =>
     over translate (·.add (v.dot s.scale)) s
-  )
-  | .scale v p => renderPicture'  p |>.local (over scale (·.dot v))
+  ) (renderPicture' p)
+  | .scale v p => ReaderT.local (over scale (·.dot v)) (renderPicture' p)
   | .pictures ps => (fun _ => ()) <$> ps.mapM renderPicture'
 
 def renderPicture (width height : Float) (picture : Picture) : IO Unit :=