soma.cell

Binary search tree built from Node records with nested left/right children

Demonstrates trees-of-records, recursive handlers over a record shape, and unit () as the empty subtree.

A Soma program from the records part of the verified corpus: 68 lines, cells BST, BSTTest. It passes soma check with soma 3.2.4.

How it is built

The cell BST declares 4 signals in its face: sample() -> Map, has(n: Int) -> Bool, height() -> Int and in_order() -> List. Handlers: sample (line 18), has (line 28), height (line 39) and in_order (line 48). Private helpers: _has, _h and _walk.

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

Generated from soma describe on this file.

The source

bst.cell

// Binary search tree built from Node records with nested `left`/`right`
// children. Demonstrates trees-of-records, recursive handlers over a
// record shape, and unit () as the empty subtree.

cell BST {
    face {
        signal sample() -> Map
        signal has(n: Int) -> Bool
        signal height() -> Int
        signal in_order() -> List
    }

    // A hand-built tree:        8
    //                          / \
    //                         3   10
    //                        / \    \
    //                       1   6    14
    on sample() {
        return Node { v: 8,
            left:  Node { v: 3,
                left:  Node { v: 1, left: (), right: () },
                right: Node { v: 6, left: (), right: () } },
            right: Node { v: 10,
                left:  (),
                right: Node { v: 14, left: (), right: () } } }
    }

    on has(n: Int) {
        return _has(sample(), n)
    }

    on _has(t: Map, n: Int) {
        if t == () { return false }
        if n == t.v { return true }
        if n < t.v { return _has(t.left, n) }
        return _has(t.right, n)
    }

    on height() {
        return _h(sample())
    }

    on _h(t: Map) {
        if t == () { return 0 }
        return 1 + max(_h(t.left), _h(t.right))
    }

    on in_order() {
        return _walk(sample())
    }

    on _walk(t: Map) {
        if t == () { return list() }
        return list(_walk(t.left), list(t.v), _walk(t.right)) |> flatten()
    }
}

cell test BSTTest {
    rules {
        assert has(6) == true
        assert has(7) == false
        assert height() == 3
        assert in_order()[0] == 1
        assert in_order()[5] == 14
        assert len(in_order()) == 6
    }
}

What the toolchain says

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

$ soma check bst.cell
✓ All checks passed.
$ soma test bst.cell
test BSTTest ...
  ✓ assert has(6) == true
  ✓ assert has(7) == false
  ✓ assert height() == 3
  ✓ assert in_order()[0] == 1
  ✓ assert in_order()[5] == 14
  ✓ assert len(in_order()) == 6

6 tests: 6 passed, 0 failed
$ soma verify bst.cell
Verifying bst.cell...

BST/termination:

  ⚠ `has` calls `BST._has`, which may not terminate
  ⚠ handler `_has`: recursive call without provable decreasing argument
  ⚠ `height` calls `BST._h`, which may not terminate
  ⚠ handler `_h`: recursive call without provable decreasing argument
  ⚠ `in_order` calls `BST._walk`, which may not terminate
  ⚠ handler `_walk`: recursive call without provable decreasing argument

0 passed, 6 warnings, 0 failures
Temporal: 0 passed, 0 failed
VERIFY OK

Builtins used

flatten, len, list, max

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