Skip to content

Commit

Permalink
Merge pull request #33 from paulcadman/ecs-option-component
Browse files Browse the repository at this point in the history
ECS: Make Option c into a component
  • Loading branch information
paulcadman authored Sep 17, 2024
2 parents d8e037f + a07616e commit 503d93f
Show file tree
Hide file tree
Showing 2 changed files with 56 additions and 1 deletion.
48 changes: 48 additions & 0 deletions lean/ECS/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -177,3 +177,51 @@ instance
explSet sa ety _ := do
let (NotStore.mk st) := sa
ExplDestroy.explDestroy st ety

/-- A pseudostore used to produce values of type `Option a`. It will always return `true` for `explExists`.
Writing can both set and delete a component using `some` and `none` respectively.
--/
structure OptionStore (α : Type) where
val : α

axiom ElemOptionStore {s es : Type} [FamilyDef ElemFam s es] : ElemFam (OptionStore s) = Option es
instance [FamilyDef ElemFam s es] : FamilyDef ElemFam (OptionStore s) (Option es) := ⟨ElemOptionStore⟩

axiom StorageOption {c s : Type} [FamilyDef StorageFam c s] : StorageFam (Option c) = OptionStore s
instance [FamilyDef StorageFam c s] : FamilyDef StorageFam (Option c) (OptionStore s) := ⟨StorageOption⟩

instance
[FamilyDef StorageFam c s]
[FamilyDef ElemFam s es]
[ca : @Component c s es _ _]
: @Component (Option c) (OptionStore s) (Option es) _ _ where
constraint := congrArg Option ca.constraint

instance
[FamilyDef StorageFam c s]
[@Has w c s _]
: @Has w (Option c) (OptionStore s) _ where
getStore := OptionStore.mk <$> Has.getStore c

instance
[FamilyDef ElemFam s e]
[@ExplGet s e _]
: @ExplGet (OptionStore s) (Option e) _ where
explGet sa ety := do
let (OptionStore.mk st) := sa
if (← ExplGet.explExists st ety)
then some <$> ExplGet.explGet st ety
else return none

explExists _ _ := return true

instance
[FamilyDef ElemFam s e]
[ExplDestroy s]
[@ExplSet s e _]
: @ExplSet (OptionStore s) (Option e) _ where
explSet sa ety mv := do
let (OptionStore.mk st) := sa
match mv with
| none => ExplDestroy.explDestroy st ety
| some x => ExplSet.explSet st ety x
9 changes: 8 additions & 1 deletion lean/Examples/BouncingBall.lean
Original file line number Diff line number Diff line change
Expand Up @@ -68,9 +68,16 @@ def updateShape (dt : Float) (c : Config) : Position × Velocity → Position ×

def removeAll (_ : Position) : Not Position := .Not

def deleteAt (pos : Vector2) (radius : Float) : Position → System World (Option Position)
| ⟨p⟩ => do if
(← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
then return none else return (some ⟨p⟩)

def update : System World Unit := do
let c : Config ← get global
if (← isMouseButtonPressed MouseButton.left) then newBall (← getMousePosition)
if (← isMouseButtonPressed MouseButton.left) then
if (← isKeyDown Key.r) then cmapM (deleteAt (← getMousePosition) c.shapeRadius)
else newBall (← getMousePosition)
if (← isMouseButtonPressed MouseButton.right) then newSquare (← getMousePosition)
if (← isKeyDown Key.space) then cmap removeAll
cmap (updateShape (← getFrameTime) c)
Expand Down

0 comments on commit 503d93f

Please sign in to comment.