// Property-Based Testing Library for Lux
//
// This module provides generators and helper functions for property-based testing.
//
// Usage:
//   Use the generator functions (genInt, genIntList, genString, etc.) in your
//   property tests to generate random test data.
//
// Example:
//   fn testReverseInvolutive(n: Int): Unit with {Console, Test, Random} = {
//       if n <= 0 then
//           Console.print("  PASS reverse(reverse(xs)) == xs")
//       else {
//           let xs = genIntList(0, 100, 20)
//           if List.reverse(List.reverse(xs)) == xs then
//               testReverseInvolutive(n - 1)
//           else
//               Test.fail("Property failed")
//       }
//   }

// ============================================================
// Generator Module
// ============================================================

// Character set for string generation
let GEN_CHARS = "abcdefghijklmnopqrstuvwxyz"
let GEN_ALPHANUM = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789"

// Generate a random integer in a range
fn genInt(min: Int, max: Int): Int with {Random} =
    Random.int(min, max)

// Generate a random integer from 0 to max
fn genIntUpTo(max: Int): Int with {Random} =
    Random.int(0, max)

// Generate a random positive integer
fn genPositiveInt(max: Int): Int with {Random} =
    Random.int(1, max)

// Generate a random boolean
fn genBool(): Bool with {Random} =
    Random.bool()

// Generate a random character (lowercase letter)
fn genChar(): String with {Random} = {
    let idx = Random.int(0, 25)
    String.substring(GEN_CHARS, idx, idx + 1)
}

// Generate a random alphanumeric character
fn genAlphaNum(): String with {Random} = {
    let idx = Random.int(0, 61)
    String.substring(GEN_ALPHANUM, idx, idx + 1)
}

// Generate a random string of given max length
fn genString(maxLen: Int): String with {Random} = {
    let len = Random.int(0, maxLen)
    genStringOfLength(len)
}

// Generate a random string of exact length
fn genStringOfLength(len: Int): String with {Random} = {
    if len <= 0 then
        ""
    else
        genChar() + genStringOfLength(len - 1)
}

// Generate a random list of integers
fn genIntList(min: Int, max: Int, maxLen: Int): List<Int> with {Random} = {
    let len = Random.int(0, maxLen)
    genIntListOfLength(min, max, len)
}

// Generate a random list of integers with exact length
fn genIntListOfLength(min: Int, max: Int, len: Int): List<Int> with {Random} = {
    if len <= 0 then
        []
    else
        List.concat([Random.int(min, max)], genIntListOfLength(min, max, len - 1))
}

// Generate a random list of booleans
fn genBoolList(maxLen: Int): List<Bool> with {Random} = {
    let len = Random.int(0, maxLen)
    genBoolListOfLength(len)
}

fn genBoolListOfLength(len: Int): List<Bool> with {Random} = {
    if len <= 0 then
        []
    else
        List.concat([Random.bool()], genBoolListOfLength(len - 1))
}

// Generate a random list of strings
fn genStringList(maxStrLen: Int, maxLen: Int): List<String> with {Random} = {
    let len = Random.int(0, maxLen)
    genStringListOfLength(maxStrLen, len)
}

fn genStringListOfLength(maxStrLen: Int, len: Int): List<String> with {Random} = {
    if len <= 0 then
        []
    else
        List.concat([genString(maxStrLen)], genStringListOfLength(maxStrLen, len - 1))
}

// ============================================================
// Shrinking Module
// ============================================================

// Shrink an integer towards zero
fn shrinkInt(n: Int): List<Int> = {
    if n == 0 then
        []
    else if n > 0 then
        [0, n / 2, n - 1]
    else
        [0, n / 2, n + 1]
}

// Shrink a list by removing elements
fn shrinkList<T>(xs: List<T>): List<List<T>> = {
    let len = List.length(xs)
    if len == 0 then
        []
    else if len == 1 then
        [[]]
    else {
        // Return: empty list, first half, second half
        let half = len / 2
        let firstHalf = List.take(xs, half)
        let secondHalf = List.drop(xs, half)
        [[], firstHalf, secondHalf]
    }
}

// Shrink a string by removing characters
fn shrinkString(s: String): List<String> = {
    let len = String.length(s)
    if len == 0 then
        []
    else if len == 1 then
        [""]
    else {
        let half = len / 2
        ["", String.substring(s, 0, half), String.substring(s, half, len)]
    }
}

// ============================================================
// Common Properties
// ============================================================

// Check that a list is sorted
fn isSorted(xs: List<Int>): Bool = {
    match List.head(xs) {
        None => true,
        Some(first) => {
            match List.tail(xs) {
                None => true,
                Some(rest) => isSortedHelper(first, rest)
            }
        }
    }
}

fn isSortedHelper(prev: Int, xs: List<Int>): Bool = {
    match List.head(xs) {
        None => true,
        Some(curr) => {
            if prev <= curr then {
                match List.tail(xs) {
                    None => true,
                    Some(rest) => isSortedHelper(curr, rest)
                }
            } else
                false
        }
    }
}

// Check that two lists have the same elements (ignoring order)
fn sameElements(xs: List<Int>, ys: List<Int>): Bool = {
    List.length(xs) == List.length(ys) &&
    List.all(xs, fn(x) => List.contains(ys, x)) &&
    List.all(ys, fn(y) => List.contains(xs, y))
}