lib/algo/tests/builtins.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, CASE_NAMES
from algo.props import (
    algo_is_index_perm, algo_is_max_pos, algo_is_min_pos, algo_is_permutation, algo_is_sorted,
    algo_is_sorted_by, algo_is_sorted_total, algo_is_stable_by, algo_is_stable_values,
)

#| builtin_sort: the `sort` builtin
def algo_t_builtin_sort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ builtin_sort", CASE_NAMES[kind], n)
    R = copy(X)
    sort(R)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_permutation(R, X)
    p1 = algo_is_sorted_total(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))
}

#| phrase_sorted: the phrase `take V sorted` (phrases.rs: take(V, argsort(V), 0))
def algo_t_phrase_sorted(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ phrase_sorted", CASE_NAMES[kind], n)
    R = take X sorted
    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)
    p3 = algo_is_sorted_total(R)
    print("?", p0, p1, p2, p3)
    return inside == 0 or ((p0 or skip[0] == 1) and (p1 or skip[1] == 1) and (p2 or skip[2] == 1))
}

#| builtin_argsort: the `argsort` builtin
def algo_t_builtin_argsort(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ builtin_argsort", CASE_NAMES[kind], n)
    P = argsort(X)
    print("= X", fmt(X))
    print("= P", fmt(P))
    p0 = algo_is_index_perm(P, len(X))
    p1 = algo_is_sorted_by(P, X)
    p2 = algo_is_stable_by(P, 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))
}

#| builtin_argsort_key: `argsort(a, key=...)`, which parser.rs lowers to a merge sort in Viv
def algo_t_builtin_argsort_key(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ builtin_argsort_key", CASE_NAMES[kind], n)
    P = argsort(X, key=fn(x) -> x)
    print("= X", fmt(X))
    print("= P", fmt(P))
    p0 = algo_is_index_perm(P, len(X))
    p1 = algo_is_sorted_by(P, X)
    p2 = algo_is_stable_by(P, 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))
}

#| builtin_argmin: the `argmin` builtin
def algo_t_builtin_argmin(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ builtin_argmin", CASE_NAMES[kind], n)
    R = argmin(X)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_min_pos(R, X)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

#| builtin_argmax: the `argmax` builtin
def algo_t_builtin_argmax(kind, n, inside, skip: Arr) -> Bool {
    X = algo_case(kind, n, 1 + 97 * kind + n)
    print("@ builtin_argmax", CASE_NAMES[kind], n)
    R = argmax(X)
    print("= X", fmt(X))
    print("= R", fmt(R))
    p0 = algo_is_max_pos(R, X)
    print("?", p0)
    return inside == 0 or ((p0 or skip[0] == 1))
}

algo_t_ok_builtin_sort = true
algo_t_kinds_builtin_sort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_builtin_sort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_builtin_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_builtin_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_builtin_sort) {
    for algo_t_s to len(algo_t_sizes_builtin_sort) {
        algo_t_r = algo_t_builtin_sort(algo_t_kinds_builtin_sort[algo_t_k], algo_t_sizes_builtin_sort[algo_t_s], algo_t_inside_builtin_sort[algo_t_k], algo_t_skip_builtin_sort[algo_t_k * 2:(algo_t_k + 1) * 2])
        algo_t_ok_builtin_sort = algo_t_ok_builtin_sort and algo_t_r
    }
}

algo_t_ok_phrase_sorted = true
algo_t_kinds_phrase_sorted = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_phrase_sorted = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_phrase_sorted = [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_phrase_sorted = [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_phrase_sorted) {
    for algo_t_s to len(algo_t_sizes_phrase_sorted) {
        algo_t_r = algo_t_phrase_sorted(algo_t_kinds_phrase_sorted[algo_t_k], algo_t_sizes_phrase_sorted[algo_t_s], algo_t_inside_phrase_sorted[algo_t_k], algo_t_skip_phrase_sorted[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_phrase_sorted = algo_t_ok_phrase_sorted and algo_t_r
    }
}

algo_t_ok_builtin_argsort = true
algo_t_kinds_builtin_argsort = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_builtin_argsort = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_builtin_argsort = [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_builtin_argsort = [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_builtin_argsort) {
    for algo_t_s to len(algo_t_sizes_builtin_argsort) {
        algo_t_r = algo_t_builtin_argsort(algo_t_kinds_builtin_argsort[algo_t_k], algo_t_sizes_builtin_argsort[algo_t_s], algo_t_inside_builtin_argsort[algo_t_k], algo_t_skip_builtin_argsort[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_builtin_argsort = algo_t_ok_builtin_argsort and algo_t_r
    }
}

algo_t_ok_builtin_argsort_key = true
algo_t_kinds_builtin_argsort_key = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_builtin_argsort_key = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_builtin_argsort_key = [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_builtin_argsort_key = [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_builtin_argsort_key) {
    for algo_t_s to len(algo_t_sizes_builtin_argsort_key) {
        algo_t_r = algo_t_builtin_argsort_key(algo_t_kinds_builtin_argsort_key[algo_t_k], algo_t_sizes_builtin_argsort_key[algo_t_s], algo_t_inside_builtin_argsort_key[algo_t_k], algo_t_skip_builtin_argsort_key[algo_t_k * 3:(algo_t_k + 1) * 3])
        algo_t_ok_builtin_argsort_key = algo_t_ok_builtin_argsort_key and algo_t_r
    }
}

algo_t_ok_builtin_argmin = true
algo_t_kinds_builtin_argmin = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_builtin_argmin = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_builtin_argmin = [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_builtin_argmin = [0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 0.0, 1.0]
for algo_t_k to len(algo_t_kinds_builtin_argmin) {
    for algo_t_s to len(algo_t_sizes_builtin_argmin) {
        algo_t_r = algo_t_builtin_argmin(algo_t_kinds_builtin_argmin[algo_t_k], algo_t_sizes_builtin_argmin[algo_t_s], algo_t_inside_builtin_argmin[algo_t_k], algo_t_skip_builtin_argmin[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_builtin_argmin = algo_t_ok_builtin_argmin and algo_t_r
    }
}

algo_t_ok_builtin_argmax = true
algo_t_kinds_builtin_argmax = [0.0, 1.0, 2.0, 3.0, 4.0, 5.0, 6.0, 7.0, 8.0, 9.0]
algo_t_inside_builtin_argmax = [1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0, 1.0]
algo_t_sizes_builtin_argmax = [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_builtin_argmax = [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_builtin_argmax) {
    for algo_t_s to len(algo_t_sizes_builtin_argmax) {
        algo_t_r = algo_t_builtin_argmax(algo_t_kinds_builtin_argmax[algo_t_k], algo_t_sizes_builtin_argmax[algo_t_s], algo_t_inside_builtin_argmax[algo_t_k], algo_t_skip_builtin_argmax[algo_t_k * 1:(algo_t_k + 1) * 1])
        algo_t_ok_builtin_argmax = algo_t_ok_builtin_argmax and algo_t_r
    }
}

test "builtin_sort: permutation R X, ordered-total R (kinds random dups sorted reversed equal organ sawtooth nearly zeros special)" {
    assert_true(algo_t_ok_builtin_sort)
}

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

test "builtin_argsort: index-perm P X, ordered-by P X, stable-by P X (kinds random dups sorted reversed equal organ sawtooth nearly zeros special)" {
    assert_true(algo_t_ok_builtin_argsort)
}

test "builtin_argsort_key: index-perm P X, ordered-by P X, stable-by P X (kinds random dups sorted reversed equal organ sawtooth nearly zeros special)" {
    assert_true(algo_t_ok_builtin_argsort_key)
}

test "builtin_argmin: min-pos R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros special)" {
    assert_true(algo_t_ok_builtin_argmin)
}

test "builtin_argmax: max-pos R X (kinds random dups sorted reversed equal organ sawtooth nearly zeros special)" {
    assert_true(algo_t_ok_builtin_argmax)
}