soma.cell

Singly linked list built from Node records whose next field is either another Node or () for the tail

Demonstrates a recursive record chain and folding over it without any list builtins.

A Soma program from the records part of the verified corpus: 74 lines, cells LinkedList, LinkedListTest. It passes soma check with soma 3.2.4.

How it is built

The cell LinkedList declares 5 signals in its face: chain() -> Map, length() -> Int, sum_all() -> Int, nth_value(i: Int) -> Int and to_list() -> List. Handlers: chain (line 15), length (line 22), sum_all (line 32), nth_value (line 42) and to_list (line 53).

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

Generated from soma describe on this file.

The source

linkedlist.cell

// Singly linked list built from Node records whose `next` field is either
// another Node or () for the tail. Demonstrates a recursive record chain
// and folding over it without any list builtins.

cell LinkedList {
    face {
        signal chain() -> Map
        signal length() -> Int
        signal sum_all() -> Int
        signal nth_value(i: Int) -> Int
        signal to_list() -> List
    }

    // 1 -> 2 -> 3 -> 4 -> ()
    on chain() {
        return Node { val: 1,
            next: Node { val: 2,
                next: Node { val: 3,
                    next: Node { val: 4, next: () } } } }
    }

    on length() {
        let n = chain()
        let count = 0
        while n != () {
            count = count + 1
            n = n.next
        }
        return count
    }

    on sum_all() {
        let n = chain()
        let acc = 0
        while n != () {
            acc = acc + n.val
            n = n.next
        }
        return acc
    }

    on nth_value(i: Int) {
        let n = chain()
        let k = 0
        while n != () && k < i {
            n = n.next
            k = k + 1
        }
        if n == () { return -1 }
        return n.val
    }

    on to_list() {
        let n = chain()
        let out = list()
        while n != () {
            out = push(out, n.val)
            n = n.next
        }
        return out
    }
}

cell test LinkedListTest {
    rules {
        assert length() == 4
        assert sum_all() == 10
        assert nth_value(2) == 3
        assert nth_value(9) == -1
        assert to_list()[0] == 1
        assert len(to_list()) == 4
    }
}

What the toolchain says

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

$ soma check linkedlist.cell
✓ All checks passed.
$ soma test linkedlist.cell
test LinkedListTest ...
  ✓ assert length() == 4
  ✓ assert sum_all() == 10
  ✓ assert nth_value(2) == 3
  ✓ assert nth_value(9) == -1
  ✓ assert to_list()[0] == 1
  ✓ assert len(to_list()) == 4

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

LinkedList/termination:

  ⚠ handler `length`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
  ⚠ handler `sum_all`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
  ⚠ handler `nth_value`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)
  ⚠ handler `to_list`: while-loop without provable termination bound (write `while [loop_bound(N)] cond { … }`, or a for-loop over a bounded range)

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

Builtins used

len, list, push

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