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.
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
$ 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