lib/algo/legacy/tests/ta_sorting.viv

# Generated by tools/algo/check.py from lib/algo/algo.spec: do not edit.
# Each case prints its input (= X), its results, and the verdict of each postcondition
# (? ...) as lib/algo/props.viv computes it; check.py checks them again in Python.
from algo.cases import algo_case, algo_needles, CASE_NAMES
from algo.props import (
    algo_all_first_or_none, algo_all_lower_bounds, algo_is_permutation, algo_is_sorted,
    algo_is_stable_values,
)
from algo.legacy.ta_sorting import (
    binary_search, binary_search_by_recursion, bisect_left, heap_sort, insertion_sort,
    merge_sort, quick_sort,
)

#| ta_merge_sort: TheAlgorithms merge_sort (study/idioms/thealgorithms-python/sorting.viv)
def algo_t_ta_merge_sort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_merge_sort", CASE_NAMES[kind], n)
    R = merge_sort(X)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted(R)
    p2 = algo_is_stable_values(R, X)
    print("?", p0, p1, p2)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1) and (p2 or skip[2] == 1))
}

#| ta_quick_sort: TheAlgorithms quick_sort: random pivot, three lists
def algo_t_ta_quick_sort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_quick_sort", CASE_NAMES[kind], n)
    R = quick_sort(X)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted(R)
    p2 = algo_is_stable_values(R, X)
    print("?", p0, p1, p2)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1) and (p2 or skip[2] == 1))
}

#| ta_heap_sort: TheAlgorithms heap_sort
def algo_t_ta_heap_sort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_heap_sort", CASE_NAMES[kind], n)
    R = heap_sort(copy(X))
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted(R)
    p2 = algo_is_stable_values(R, X)
    print("?", p0, p1, p2)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1))
}

#| ta_insertion_sort: TheAlgorithms insertion_sort
def algo_t_ta_insertion_sort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_insertion_sort", CASE_NAMES[kind], n)
    R = insertion_sort(copy(X))
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted(R)
    p2 = algo_is_stable_values(R, X)
    print("?", p0, p1, p2)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1) and (p2 or skip[2] == 1))
}

#| ta_binary_search: TheAlgorithms binary_search: the leftmost index of x, or -1
def algo_t_ta_binary_search(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_binary_search", CASE_NAMES[kind], n)
    V = copy(X)
    sort(V)
    Q = algo_needles(V)
    RS = zeros(len(Q))
    for k to len(Q) {
        RS[k] = binary_search(V, Q[k])
    }
    print("= X", fmt(X))
    print("= RS", fmt(RS))
    print("= V", fmt(V))
    print("= Q", fmt(Q))
    p0 = algo_all_first_or_none(RS, V, Q)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

#| ta_bisect_left: TheAlgorithms bisect_left
def algo_t_ta_bisect_left(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_bisect_left", CASE_NAMES[kind], n)
    V = copy(X)
    sort(V)
    Q = algo_needles(V)
    RS = zeros(len(Q))
    for k to len(Q) {
        RS[k] = bisect_left(V, Q[k])
    }
    print("= X", fmt(X))
    print("= RS", fmt(RS))
    print("= V", fmt(V))
    print("= Q", fmt(Q))
    p0 = algo_all_lower_bounds(RS, V, Q)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

#| ta_binary_search_rec: TheAlgorithms binary_search_by_recursion
def algo_t_ta_binary_search_rec(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ ta_binary_search_rec", CASE_NAMES[kind], n)
    V = copy(X)
    sort(V)
    Q = algo_needles(V)
    RS = zeros(len(Q))
    for k to len(Q) {
        RS[k] = binary_search_by_recursion(V, Q[k])
    }
    print("= X", fmt(X))
    print("= RS", fmt(RS))
    print("= V", fmt(V))
    print("= Q", fmt(Q))
    p0 = algo_all_first_or_none(RS, V, Q)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

algo_t_ok_ta_merge_sort = true
algo_t_kinds_ta_merge_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_merge_sort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_merge_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_merge_sort = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_merge_sort) {
    for algo_t_s to len(algo_t_sizes_ta_merge_sort) {
        algo_t_r = algo_t_ta_merge_sort(algo_t_kinds_ta_merge_sort[algo_t_k], algo_t_sizes_ta_merge_sort[algo_t_s], algo_t_inside_ta_merge_sort[algo_t_k], algo_t_skip_ta_merge_sort[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_ta_merge_sort = algo_t_ok_ta_merge_sort and algo_t_r
    }
}

algo_t_ok_ta_quick_sort = true
algo_t_kinds_ta_quick_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_quick_sort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_quick_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_quick_sort = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_quick_sort) {
    for algo_t_s to len(algo_t_sizes_ta_quick_sort) {
        algo_t_r = algo_t_ta_quick_sort(algo_t_kinds_ta_quick_sort[algo_t_k], algo_t_sizes_ta_quick_sort[algo_t_s], algo_t_inside_ta_quick_sort[algo_t_k], algo_t_skip_ta_quick_sort[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_ta_quick_sort = algo_t_ok_ta_quick_sort and algo_t_r
    }
}

algo_t_ok_ta_heap_sort = true
algo_t_kinds_ta_heap_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_heap_sort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_heap_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_heap_sort = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_heap_sort) {
    for algo_t_s to len(algo_t_sizes_ta_heap_sort) {
        algo_t_r = algo_t_ta_heap_sort(algo_t_kinds_ta_heap_sort[algo_t_k], algo_t_sizes_ta_heap_sort[algo_t_s], algo_t_inside_ta_heap_sort[algo_t_k], algo_t_skip_ta_heap_sort[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_ta_heap_sort = algo_t_ok_ta_heap_sort and algo_t_r
    }
}

algo_t_ok_ta_insertion_sort = true
algo_t_kinds_ta_insertion_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_insertion_sort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_insertion_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_insertion_sort = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_insertion_sort) {
    for algo_t_s to len(algo_t_sizes_ta_insertion_sort) {
        algo_t_r = algo_t_ta_insertion_sort(algo_t_kinds_ta_insertion_sort[algo_t_k], algo_t_sizes_ta_insertion_sort[algo_t_s], algo_t_inside_ta_insertion_sort[algo_t_k], algo_t_skip_ta_insertion_sort[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_ta_insertion_sort = algo_t_ok_ta_insertion_sort and algo_t_r
    }
}

algo_t_ok_ta_binary_search = true
algo_t_kinds_ta_binary_search = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_binary_search = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_binary_search = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_binary_search = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_binary_search) {
    for algo_t_s to len(algo_t_sizes_ta_binary_search) {
        algo_t_r = algo_t_ta_binary_search(algo_t_kinds_ta_binary_search[algo_t_k], algo_t_sizes_ta_binary_search[algo_t_s], algo_t_inside_ta_binary_search[algo_t_k], algo_t_skip_ta_binary_search[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_ta_binary_search = algo_t_ok_ta_binary_search and algo_t_r
    }
}

algo_t_ok_ta_bisect_left = true
algo_t_kinds_ta_bisect_left = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_bisect_left = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_bisect_left = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_bisect_left = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_bisect_left) {
    for algo_t_s to len(algo_t_sizes_ta_bisect_left) {
        algo_t_r = algo_t_ta_bisect_left(algo_t_kinds_ta_bisect_left[algo_t_k], algo_t_sizes_ta_bisect_left[algo_t_s], algo_t_inside_ta_bisect_left[algo_t_k], algo_t_skip_ta_bisect_left[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_ta_bisect_left = algo_t_ok_ta_bisect_left and algo_t_r
    }
}

algo_t_ok_ta_binary_search_rec = true
algo_t_kinds_ta_binary_search_rec = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_ta_binary_search_rec = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 0.0]
algo_t_sizes_ta_binary_search_rec = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 7.0, 8.0, 9.0, 15.0, 16.0, 17.0, 31.0, 32.0, 33.0, 63.0, 64.0, 65.0, 129.0, 257.0]
algo_t_skip_ta_binary_search_rec = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0]
for algo_t_k to len(algo_t_kinds_ta_binary_search_rec) {
    for algo_t_s to len(algo_t_sizes_ta_binary_search_rec) {
        algo_t_r = algo_t_ta_binary_search_rec(algo_t_kinds_ta_binary_search_rec[algo_t_k], algo_t_sizes_ta_binary_search_rec[algo_t_s], algo_t_inside_ta_binary_search_rec[algo_t_k], algo_t_skip_ta_binary_search_rec[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_ta_binary_search_rec = algo_t_ok_ta_binary_search_rec and algo_t_r
    }
}

test "ta_merge_sort: permutation R X, ordered R, stable-values R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_merge_sort)
}

test "ta_quick_sort: permutation R X, ordered R, stable-values R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_quick_sort)
}

test "ta_heap_sort: permutation R X, ordered R (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_heap_sort)
}

test "ta_insertion_sort: permutation R X, ordered R, stable-values R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_insertion_sort)
}

test "ta_binary_search: first-or-none RS V Q (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_binary_search)
}

test "ta_bisect_left: lower-bounds RS V Q (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_bisect_left)
}

test "ta_binary_search_rec: first-or-none RS V Q (kinds random dups sorted reversed equal organ sawtooth nearly zeros)" {
    assert_true(algo_t_ok_ta_binary_search_rec)
}