diff --git a/lean/Examples/ECS.lean b/lean/Examples/ECS.lean index c41f1b6..a79e521 100644 --- a/lean/Examples/ECS.lean +++ b/lean/Examples/ECS.lean @@ -10,6 +10,9 @@ structure Position where structure Velocity where velocity : Vector2 +structure Magic where + magic : Nat + axiom StoragePosition : StorageFam Position = MapStorage Position instance : FamilyDef StorageFam Position (MapStorage Position) := ⟨StoragePosition⟩ @@ -22,9 +25,16 @@ instance : FamilyDef StorageFam Velocity (MapStorage Velocity) := ⟨StorageVelo instance : @Component Velocity (MapStorage Velocity) Velocity _ _ where constraint := rfl +axiom StorageMagic : StorageFam Magic = MapStorage Magic +instance : FamilyDef StorageFam Magic (MapStorage Magic) := ⟨StorageMagic⟩ + +instance : @Component Magic (MapStorage Magic) Magic _ _ where + constraint := rfl + structure World where positionStore : MapStorage Position velocityStore : MapStorage Velocity + magicStore : MapStorage Magic entityStore : GlobalStorage EntityCounter instance : @Has World Position (MapStorage Position) _ where @@ -33,14 +43,18 @@ instance : @Has World Position (MapStorage Position) _ where instance : @Has World Velocity (MapStorage Velocity) _ where getStore := (·.velocityStore) <$> read +instance : @Has World Magic (MapStorage Magic) _ where + getStore := (·.magicStore) <$> read + instance : @Has World EntityCounter (GlobalStorage EntityCounter) _ where getStore := (·.entityStore) <$> read def initWorld : IO World := do let positionStore : MapStorage Position ← ExplInit.explInit let velocityStore : MapStorage Velocity ← ExplInit.explInit + let magicStore : MapStorage Magic ← ExplInit.explInit let entityStore : GlobalStorage EntityCounter ← ExplInit.explInit - pure {positionStore,velocityStore,entityStore} + pure {positionStore,velocityStore,magicStore,entityStore} def update (pv : Position × Velocity) : Position := let (p, v) := pv @@ -48,13 +62,15 @@ def update (pv : Position × Velocity) : Position := def dumpState : System World Unit := do IO.println "DUMP STATE" - cmapM_ (fun ((p, v) : Position × Velocity) => - IO.println s!"position : ({p.position.x}, {p.position.y}) velocity : ({v.velocity.x}, {v.velocity.y})") + let globalPosition : Position ← get global + cmapM_ (fun ((p, v, m) : Position × Velocity × Magic) => + IO.println s!"global pos: {globalPosition.position.x} position : ({p.position.x}, {p.position.y}) velocity : ({v.velocity.x}, {v.velocity.y}) magic : {m.magic}") def game : System World Unit := do newEntityAs_ (Position × Velocity) (⟨0,0⟩, ⟨10,11⟩) newEntityAs_ (Position × Velocity) (⟨1,0⟩, ⟨-5,-2⟩) - set' global {position := ⟨0,0⟩ : Position} + newEntityAs_ (Position × Velocity × Magic) (⟨1,0⟩, ⟨-5,-2⟩, ⟨1⟩) + set' global {position := ⟨999,0⟩ : Position} dumpState cmap update dumpState