Insertion sort and binary insertion sort on a List<Int>

insertion_sort.cell

// Insertion sort and binary insertion sort on a List<Int>.
// Demonstrates: the shift-right inner while loop, building a sorted prefix,
// and a variant that uses binary search to locate the insertion point.
//
//   soma run  examples/corpus/algorithms/insertion_sort.cell sort "[5,2,4,6,1,3]"
//   soma test examples/corpus/algorithms/insertion_sort.cell

cell InsertionSort {
    face {
        signal sort(xs: List) -> List
        signal insert_sorted(xs: List, v: Int) -> List
    }

    on sort(xs: List) {
        for i in range(1, len(xs)) {
            let key = xs[i]
            let j = i - 1
            while j >= 0 && xs[j] > key {
                xs[j + 1] = xs[j]
                j = j - 1
            }
            xs[j + 1] = key
        }
        return xs
    }

    // insert v into an already-sorted list, keeping it sorted
    on insert_sorted(xs: List, v: Int) {
        let lo = 0
        let hi = len(xs)
        while lo < hi {
            let mid = floor((lo + hi) / 2)
            if xs[mid] < v { lo = mid + 1 } else { hi = mid }
        }
        let out = list()
        for i in range(0, lo) { out = push(out, xs[i]) }
        out = push(out, v)
        for i in range(lo, len(xs)) { out = push(out, xs[i]) }
        return out
    }
}

cell test InsertionSortTests {
    rules {
        assert to_string(sort([5, 2, 4, 6, 1, 3])) == to_string([1, 2, 3, 4, 5, 6])
        assert to_string(sort([3, 1, 2])) == to_string([1, 2, 3])
        assert to_string(sort(list())) == to_string(list())
        assert to_string(insert_sorted([1, 3, 5], 4)) == to_string([1, 3, 4, 5])
        assert to_string(insert_sorted([1, 3, 5], 0)) == to_string([0, 1, 3, 5])
        assert to_string(insert_sorted(list(), 7)) == to_string([7])
    }
}