Quicksort on a List<Int> — Lomuto partition, recursive
Demonstrates: recursion with list slicing via helper, building result lists with push, and concatenating sublists. Pure / functional style: each call returns a fresh sorted list rather than mutating in place.
A Soma program from the algorithms part of the verified corpus: 42 lines, cells Quicksort, QuicksortTests. It passes soma check with soma 3.2.4.
How it is built
The cell Quicksort declares 1 signal in its face: sort(xs: List) -> List. Handlers: sort (line 14).
The file also holds 1 test cell (QuicksortTests) with 6 assertions, run by soma test.
The source
quicksort.cell
// Quicksort on a List<Int> — Lomuto partition, recursive.
// Demonstrates: recursion with list slicing via helper, building result lists
// with push, and concatenating sublists. Pure / functional style: each call
// returns a fresh sorted list rather than mutating in place.
//
// soma run examples/corpus/algorithms/quicksort.cell sort "[3,6,1,8,2,9,4]"
// soma test examples/corpus/algorithms/quicksort.cell
cell Quicksort {
face {
signal sort(xs: List) -> List
}
on sort(xs: List) {
if len(xs) <= 1 { return xs }
let pivot = xs[0]
let less = list()
let more = list()
for i in range(1, len(xs)) {
if xs[i] < pivot { less = push(less, xs[i]) }
else { more = push(more, xs[i]) }
}
let left = sort(less)
let right = sort(more)
// left ++ [pivot] ++ right
let out = push(left, pivot)
for v in right { out = push(out, v) }
return out
}
}
cell test QuicksortTests {
rules {
assert sort([3, 6, 1, 8, 2, 9, 4])[0] == 1
assert sort([3, 6, 1, 8, 2, 9, 4])[6] == 9
assert to_string(sort([5, 4, 3, 2, 1])) == to_string([1, 2, 3, 4, 5])
assert to_string(sort([2, 2, 1, 1, 3])) == to_string([1, 1, 2, 2, 3])
assert to_string(sort(list())) == to_string(list())
assert to_string(sort([42])) == to_string([42])
}
}What the toolchain says
$ soma check quicksort.cell
warning: inside Quicksort.sort, `sort(…)` with 1 argument(s) calls the handler ITSELF (recursion), not the builtin sort() — a handler shadows a builtin of the same name and arity. For an empty list write []
--> quicksort.cell:23:20
|
23 | let left = sort(less)
| ^
warning: inside Quicksort.sort, `sort(…)` with 1 argument(s) calls the handler ITSELF (recursion), not the builtin sort() — a handler shadows a builtin of the same name and arity. For an empty list write []
--> quicksort.cell:24:21
|
24 | let right = sort(more)
| ^
✓ 2 warning(s), no errors.$ soma test quicksort.cell
test QuicksortTests ...
✓ assert sort([3, 6, 1, 8, 2, 9, 4])[0] == 1
✓ assert sort([3, 6, 1, 8, 2, 9, 4])[6] == 9
✓ assert to_string(sort([5, 4, 3, 2, 1])) == to_string([1, 2, 3, 4, 5])
✓ assert to_string(sort([2, 2, 1, 1, 3])) == to_string([1, 1, 2, 2, 3])
✓ assert to_string(sort(list())) == to_string(list())
✓ assert to_string(sort([42])) == to_string([42])
6 tests: 6 passed, 0 failed$ soma verify quicksort.cell
Verifying quicksort.cell...
Quicksort/termination:
⚠ handler `sort`: recursive call without provable decreasing argument
0 passed, 1 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK$ soma run quicksort.cell sort "[3,6,1,8,2,9,4]"
[1, 2, 3, 4, 6, 8, 9]