soma.cell

A stack (LIFO) backed by a List, used to check balanced brackets

Demonstrates: list-as-stack with push + index-based pop, a String scan, match over bracket characters, and an early-out on mismatch.

A Soma program from the algorithms part of the verified corpus: 69 lines, cells Brackets, BracketsTests. It passes soma check with soma 3.2.4.

How it is built

The cell Brackets declares 3 signals in its face: balanced(s: String) -> Bool, closes(open: String, close: String) -> Bool and pop(xs: List) -> List. Handlers: pop (line 16), closes (line 22) and balanced (line 31).

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

Generated from soma describe on this file.

The source

stack.cell

// A stack (LIFO) backed by a List, used to check balanced brackets.
// Demonstrates: list-as-stack with push + index-based pop, a String scan,
// match over bracket characters, and an early-out on mismatch.
//
//   soma run  examples/corpus/algorithms/stack.cell balanced "{[()]}"
//   soma test examples/corpus/algorithms/stack.cell

cell Brackets {
    face {
        signal balanced(s: String) -> Bool
        signal closes(open: String, close: String) -> Bool
        signal pop(xs: List) -> List
    }

    // pop = the list without its last element (the classic stack pop)
    on pop(xs: List) {
        let out = list()
        for i in range(0, len(xs) - 1) { out = push(out, xs[i]) }
        return out
    }

    on closes(open: String, close: String) {
        return match open {
            "(" -> close == ")"
            "[" -> close == "]"
            "{" -> close == "}"
            _   -> false
        }
    }

    on balanced(s: String) {
        let stack = list()
        let ok = true
        for ch in split(s, "") {
            if ch == "(" || ch == "[" || ch == "{" {
                stack = push(stack, ch)
            } else if ch == ")" || ch == "]" || ch == "}" {
                let n = len(stack)
                if n == 0 {
                    ok = false
                    break
                }
                let top = stack[n - 1]
                if !closes(top, ch) {
                    ok = false
                    break
                }
                stack = pop(stack)
            }
        }
        return ok && len(stack) == 0
    }
}

cell test BracketsTests {
    rules {
        assert balanced("{[()]}")
        assert balanced("()[]{}")
        assert balanced("")
        assert !balanced("(]")
        assert !balanced("([)]")
        assert !balanced("(((")
        assert !balanced("))")
        assert closes("(", ")")
        assert !closes("(", "]")
        assert to_string(pop([1, 2, 3])) == to_string([1, 2])
    }
}

What the toolchain says

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

$ soma check stack.cell
✓ All checks passed.
$ soma test stack.cell
test BracketsTests ...
  ✓ assert balanced("{[()]}")
  ✓ assert balanced("()[]{}")
  ✓ assert balanced("")
  ✓ assert !balanced("(]")
  ✓ assert !balanced("([)]")
  ✓ assert !balanced("(((")
  ✓ assert !balanced("))")
  ✓ assert closes("(", ")")
  ✓ assert !closes("(", "]")
  ✓ assert to_string(pop([1, 2, 3])) == to_string([1, 2])

10 tests: 10 passed, 0 failed
$ soma verify stack.cell
Verifying stack.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)
$ soma run stack.cell balanced "{[()]}"
true

Builtins used

len, list, push, range, split, to_string

Source file: /corpus/algorithms/stack.cell · examples/corpus/algorithms/stack.cell