An an implementation of an Entity Component System

[paulcadman]

You can write something like, using the command makeWorldAndComponents to generate all of the boilerplate.

structure Position where
  position : Vector2

structure Velocity where
  velocity : Vector2

makeWorldAndComponents Position Velocity

def update (pv : Position × Velocity) : Position :=
  let (p, v) := pv
  {position := p.position.add v.velocity}

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})")

def game : System World Unit := do
  newEntity_ ({position := ⟨0,0⟩ : Position}, {velocity := ⟨10,11⟩ : Velocity})
  newEntity_ ({position := ⟨1,0⟩ : Position}, {velocity := ⟨-5,-2⟩ : Velocity})
  dumpState
  cmap update
  dumpState

def main : IO Unit := do
  runSystem game (← initWorld)

And run:

$ just run-ecs-example
DUMP STATE
position : (0.000000, 0.000000) velocity : (10.000000, 11.000000)
position : (1.000000, 0.000000) velocity : (-5.000000, -2.000000)
DUMP STATE
position : (10.000000, 11.000000) velocity : (10.000000, 11.000000)
position : (-4.000000, -2.000000) velocity : (-5.000000, -2.000000)