lux/examples/property_testing.lux

let CHARS = "abcdefghijklmnopqrstuvwxyz"

fn genInt(min: Int, max: Int): Int with {Random} = Random.int(min, max)

fn genIntList(min: Int, max: Int, maxLen: Int): List<Int> with {Random} = {
    let len = Random.int(0, maxLen)
    genIntListHelper(min, max, len)
}

fn genIntListHelper(min: Int, max: Int, len: Int): List<Int> with {Random} = {
    if len <= 0 then [] else List.concat([Random.int(min, max)], genIntListHelper(min, max, len - 1))
}

fn genChar(): String with {Random} = {
    let idx = Random.int(0, 25)
    String.substring(CHARS, idx, idx + 1)
}

fn genString(maxLen: Int): String with {Random} = {
    let len = Random.int(0, maxLen)
    genStringHelper(len)
}

fn genStringHelper(len: Int): String with {Random} = {
    if len <= 0 then "" else genChar() + genStringHelper(len - 1)
}

fn printResult(name: String, passed: Bool, count: Int): Unit with {Console} = {
    if passed then Console.print("  PASS " + name + " (" + toString(count) + " tests)") else Console.print("  FAIL " + name)
}

fn testReverseInvolutive(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("reverse(reverse(xs)) == xs", true, count)
    true
} else {
    let xs = genIntList(0, 100, 20)
    if List.reverse(List.reverse(xs)) == xs then testReverseInvolutive(n - 1, count) else {
    printResult("reverse(reverse(xs)) == xs", false, count - n + 1)
    false
}
}
}

fn testReverseLength(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("length(reverse(xs)) == length(xs)", true, count)
    true
} else {
    let xs = genIntList(0, 100, 20)
    if List.length(List.reverse(xs)) == List.length(xs) then testReverseLength(n - 1, count) else {
    printResult("length(reverse(xs)) == length(xs)", false, count - n + 1)
    false
}
}
}

fn testMapLength(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("length(map(xs, f)) == length(xs)", true, count)
    true
} else {
    let xs = genIntList(0, 100, 20)
    if List.length(List.map(xs, fn(x: _) => x * 2)) == List.length(xs) then testMapLength(n - 1, count) else {
    printResult("length(map(xs, f)) == length(xs)", false, count - n + 1)
    false
}
}
}

fn testConcatLength(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("length(xs ++ ys) == length(xs) + length(ys)", true, count)
    true
} else {
    let xs = genIntList(0, 50, 10)
    let ys = genIntList(0, 50, 10)
    if List.length(List.concat(xs, ys)) == List.length(xs) + List.length(ys) then testConcatLength(n - 1, count) else {
    printResult("length(xs ++ ys) == length(xs) + length(ys)", false, count - n + 1)
    false
}
}
}

fn testAddCommutative(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("a + b == b + a", true, count)
    true
} else {
    let a = genInt(-1000, 1000)
    let b = genInt(-1000, 1000)
    if a + b == b + a then testAddCommutative(n - 1, count) else {
    printResult("a + b == b + a", false, count - n + 1)
    false
}
}
}

fn testMulAssociative(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("(a * b) * c == a * (b * c)", true, count)
    true
} else {
    let a = genInt(-100, 100)
    let b = genInt(-100, 100)
    let c = genInt(-100, 100)
    if a * b * c == a * b * c then testMulAssociative(n - 1, count) else {
    printResult("(a * b) * c == a * (b * c)", false, count - n + 1)
    false
}
}
}

fn testStringConcatLength(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("length(s1 + s2) == length(s1) + length(s2)", true, count)
    true
} else {
    let s1 = genString(10)
    let s2 = genString(10)
    if String.length(s1 + s2) == String.length(s1) + String.length(s2) then testStringConcatLength(n - 1, count) else {
    printResult("length(s1 + s2) == length(s1) + length(s2)", false, count - n + 1)
    false
}
}
}

fn testAddIdentity(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("x + 0 == x && 0 + x == x", true, count)
    true
} else {
    let x = genInt(-10000, 10000)
    if x + 0 == x && 0 + x == x then testAddIdentity(n - 1, count) else {
    printResult("x + 0 == x && 0 + x == x", false, count - n + 1)
    false
}
}
}

fn testFilterLength(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("length(filter(xs, p)) <= length(xs)", true, count)
    true
} else {
    let xs = genIntList(0, 100, 20)
    if List.length(List.filter(xs, fn(x: _) => x > 50)) <= List.length(xs) then testFilterLength(n - 1, count) else {
    printResult("length(filter(xs, p)) <= length(xs)", false, count - n + 1)
    false
}
}
}

fn testConcatIdentity(n: Int, count: Int): Bool with {Console, Random} = {
    if n <= 0 then {
    printResult("concat(xs, []) == xs && concat([], xs) == xs", true, count)
    true
} else {
    let xs = genIntList(0, 100, 10)
    if List.concat(xs, []) == xs && List.concat([], xs) == xs then testConcatIdentity(n - 1, count) else {
    printResult("concat(xs, []) == xs && concat([], xs) == xs", false, count - n + 1)
    false
}
}
}

fn main(): Unit with {Console, Random} = {
    Console.print("========================================")
    Console.print("  Property-Based Testing Demo")
    Console.print("========================================")
    Console.print("")
    Console.print("Running 100 iterations per property...")
    Console.print("")
    testReverseInvolutive(100, 100)
    testReverseLength(100, 100)
    testMapLength(100, 100)
    testConcatLength(100, 100)
    testAddCommutative(100, 100)
    testMulAssociative(100, 100)
    testStringConcatLength(100, 100)
    testAddIdentity(100, 100)
    testFilterLength(100, 100)
    testConcatIdentity(100, 100)
    Console.print("")
    Console.print("========================================")
    Console.print("  All property tests completed!")
    Console.print("========================================")
}

let result = run main() with {}