soma.cell

Entity-Component shape: each Entity record carries a bag of components

(position, velocity, health) as nested records. Demonstrates an entity-component data model, nested dot-mutation, and a physics "tick".

A Soma program from the records part of the verified corpus: 60 lines, cells ECS, ECSTest. It passes soma check with soma 3.2.4.

How it is built

The cell ECS declares 4 signals in its face: world() -> List, tick() -> List, alive_count() -> Int and damage(id: String, amount: Int) -> Map. Handlers: world (line 13), tick (line 27), alive_count (line 36) and damage (line 40).

The file also holds 1 test cell (ECSTest) with 7 assertions, run by soma test.

Generated from soma describe on this file.

The source

ecs.cell

// Entity-Component shape: each Entity record carries a bag of components
// (position, velocity, health) as nested records. Demonstrates an
// entity-component data model, nested dot-mutation, and a physics "tick".

cell ECS {
    face {
        signal world() -> List
        signal tick() -> List
        signal alive_count() -> Int
        signal damage(id: String, amount: Int) -> Map
    }

    on world() {
        return list(
            Entity { id: "player",
                pos: Vec2 { x: 0,  y: 0 },
                vel: Vec2 { x: 1,  y: 2 },
                hp:  Health { cur: 100, max: 100 } },
            Entity { id: "enemy",
                pos: Vec2 { x: 10, y: 5 },
                vel: Vec2 { x: -1, y: 0 },
                hp:  Health { cur: 30,  max: 30 } }
        )
    }

    // Integrate one step: pos += vel for every entity.
    on tick() {
        let es = world()
        for i in range(0, len(es)) {
            es[i].pos.x = es[i].pos.x + es[i].vel.x
            es[i].pos.y = es[i].pos.y + es[i].vel.y
        }
        return es
    }

    on alive_count() {
        return world() |> count(e => e.hp.cur > 0)
    }

    on damage(id: String, amount: Int) {
        let es = world()
        let e = es |> find(x => x.id == id)
        if e == () { return map("error", "no entity") }
        e.hp.cur = max(0, e.hp.cur - amount)
        return map("id", id, "hp", e.hp.cur, "dead", e.hp.cur == 0)
    }
}

cell test ECSTest {
    rules {
        assert tick()[0].pos.x == 1
        assert tick()[0].pos.y == 2
        assert tick()[1].pos.x == 9
        assert alive_count() == 2
        assert damage("enemy", 50).hp == 0
        assert damage("enemy", 50).dead == true
        assert damage("player", 10).hp == 90
    }
}

What the toolchain says

Run on a fresh copy of the program at build time; the outputs are pasted unedited.

$ soma check ecs.cell
✓ All checks passed.
$ soma test ecs.cell
test ECSTest ...
  ✓ assert tick()[0].pos.x == 1
  ✓ assert tick()[0].pos.y == 2
  ✓ assert tick()[1].pos.x == 9
  ✓ assert alive_count() == 2
  ✓ assert damage("enemy", 50).hp == 0
  ✓ assert damage("enemy", 50).dead == true
  ✓ assert damage("player", 10).hp == 90

7 tests: 7 passed, 0 failed
$ soma verify ecs.cell
Verifying ecs.cell...
No state machine in this program: nothing to prove beyond `soma check` (invariants and lifecycles are what verify proves).
VERIFY OK (vacuous — no state machine)

Builtins used

count, find, len, list, map, max, range

Source file: /corpus/records/ecs.cell · examples/corpus/records/ecs.cell