// Property-Based Testing Example
//
// This example demonstrates property-based testing in Lux,
// where we verify properties hold for randomly generated inputs.
//
// Run with: lux examples/property_testing.lux

// ============================================================
// Generator Functions (using Random effect)
// ============================================================

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)
}

// ============================================================
// Test Runner State
// ============================================================

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)
}

// ============================================================
// Property Tests
// ============================================================

// Test: List reverse is involutive
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
        }
    }
}

// Test: List reverse preserves length
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
        }
    }
}

// Test: List map preserves length
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
        }
    }
}

// Test: List concat length is sum
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
        }
    }
}

// Test: Addition is commutative
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
        }
    }
}

// Test: Multiplication is associative
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
        }
    }
}

// Test: String concat length is sum
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
        }
    }
}

// Test: Zero is identity for addition
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
        }
    }
}

// Test: Filter reduces or maintains length
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
        }
    }
}

// Test: Empty list is identity for concat
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
        }
    }
}

// ============================================================
// Main
// ============================================================

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 {}