From 10a153f343641752d8bcf69f517765679dc76e19 Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 17 Sep 2024 16:34:34 +0100 Subject: [PATCH 1/3] ECS Add EntityStore for accessing Entities in a cmap --- lean/ECS/Components.lean | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/lean/ECS/Components.lean b/lean/ECS/Components.lean index 6b0b845..60f5aee 100644 --- a/lean/ECS/Components.lean +++ b/lean/ECS/Components.lean @@ -217,3 +217,23 @@ 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 : @Has w Entity EntityStore _ where + getStore := return .EntityStore + +instance : @ExplGet EntityStore Entity _ where + explGet _ ety := return ety + explExists _ _ := return true From 7028de0a589e45e2b63ec2ec798852373d5a423d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 17 Sep 2024 16:54:42 +0100 Subject: [PATCH 2/3] ECS: Make Entity a component --- lean/ECS/Components.lean | 3 +++ 1 file changed, 3 insertions(+) diff --git a/lean/ECS/Components.lean b/lean/ECS/Components.lean index 60f5aee..2e68fb0 100644 --- a/lean/ECS/Components.lean +++ b/lean/ECS/Components.lean @@ -231,6 +231,9 @@ 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 From c7dfd8470fb8c2ee18cadfc586574782dd21153d Mon Sep 17 00:00:00 2001 From: Paul Cadman Date: Tue, 17 Sep 2024 16:56:36 +0100 Subject: [PATCH 3/3] ECS: Demo deleting an entity explicitly using Entity component --- lean/Examples/BouncingBall.lean | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/lean/Examples/BouncingBall.lean b/lean/Examples/BouncingBall.lean index 25f6748..3b85a1a 100644 --- a/lean/Examples/BouncingBall.lean +++ b/lean/Examples/BouncingBall.lean @@ -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