Skip to content

Commit

Permalink
Merge pull request #36 from paulcadman/ecs-entity-component
Browse files Browse the repository at this point in the history
ECS: Add Entity component
  • Loading branch information
paulcadman authored Sep 17, 2024
2 parents 1aa26bd + c7dfd84 commit ef761d9
Show file tree
Hide file tree
Showing 2 changed files with 29 additions and 0 deletions.
23 changes: 23 additions & 0 deletions lean/ECS/Components.lean
Original file line number Diff line number Diff line change
Expand Up @@ -217,3 +217,26 @@ instance : @ExplSet Unit Unit _ where

instance : ExplDestroy Unit where
explDestroy _ _ := return ()

/-- A pseudostore used to produce components of type `Entity`.
It always returns `true` for `explExists`, and echoes back the entity argument for `explGet`.
It can be used in e.g. `cmap $ fun (a, ety : Entity) -> b` to access the current entity.
--/
inductive EntityStore where
| EntityStore

axiom ElemEntityStore : ElemFam EntityStore = Entity
instance : FamilyDef ElemFam EntityStore Entity := ⟨ElemEntityStore⟩

axiom StorageEntity : StorageFam Entity = EntityStore
instance : FamilyDef StorageFam Entity EntityStore := ⟨StorageEntity⟩

instance : @Component Entity EntityStore Entity _ _ where
constraint := rfl

instance : @Has w Entity EntityStore _ where
getStore := return .EntityStore

instance : @ExplGet EntityStore Entity _ where
explGet _ ety := return ety
explExists _ _ := return true
6 changes: 6 additions & 0 deletions lean/Examples/BouncingBall.lean
Original file line number Diff line number Diff line change
Expand Up @@ -73,6 +73,12 @@ def deleteAt (pos : Vector2) (radius : Float) : Position → System World (Optio
(← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
then return none else return (some ⟨p⟩)

/-- An alternative to `deleteAt` that explicitly deletes an entity --/
def deleteAt' (pos : Vector2) (radius : Float) : Position × Entity → System World Unit
| (⟨p⟩, e) => do if
(← checkCollisionPointRec pos {x := p.x - radius, y := p.y - radius, width := 2 * radius, height := 2 * radius : Rectangle})
then destroy (Position × Velocity) e else return ()

def update : System World Unit := do
let c : Config ← get global
if (← isMouseButtonPressed MouseButton.left) then
Expand Down

0 comments on commit ef761d9

Please sign in to comment.