//! Property-based tests for JVMRS core components
//!
//! These tests verify that JVMRS properties hold true across
//! a wide range of randomly generated inputs.

use jvmrs::memory::{StackFrame, Value};
use jvmrs::interpreter::Interpreter;
use proptest::prelude::*;

/// Test that integer addition is commutative
proptest! {
    #[test]
    fn prop_iadd_commutative(a in any::<i32>(), b in any::<i32>()) {
        let mut frame = StackFrame::new(10, 10, "test".to_string());

        frame.push(Value::Int(a)).unwrap();
        frame.push(Value::Int(b)).unwrap();

        // Pop both and add
        let val_b = frame.pop().unwrap().as_int();
        let val_a = frame.pop().unwrap().as_int();
        let result1 = val_a.wrapping_add(val_b);

        // Reverse order
        frame.push(Value::Int(b)).unwrap();
        frame.push(Value::Int(a)).unwrap();
        let val_a2 = frame.pop().unwrap().as_int();
        let val_b2 = frame.pop().unwrap().as_int();
        let result2 = val_a2.wrapping_add(val_b2);

        prop_assert_eq!(result1, result2);
    }
}

/// Test that integer multiplication is associative
proptest! {
    #[test]
    fn prop_imul_associative(a in any::<i32>(), b in any::<i32>(), c in any::<i32>()) {
        let result1 = a.wrapping_mul(b).wrapping_mul(c);
        let result2 = a.wrapping_mul(b.wrapping_mul(c));

        prop_assert_eq!(result1, result2);
    }
}

/// Test that bitwise AND is idempotent
proptest! {
    #[test]
    fn prop_iand_idempotent(a in any::<i32>()) {
        let result = a & a;
        prop_assert_eq!(result, a);
    }
}

/// Test that bitwise XOR with zero is identity
proptest! {
    #[test]
    fn prop_ixor_zero_identity(a in any::<i32>()) {
        let result = a ^ 0;
        prop_assert_eq!(result, a);
    }
}

/// Test that shifts are within expected bounds
proptest! {
    #[test]
    fn prop_ishl_bounds(a in any::<i32>(), shift in any::<i32>()) {
        let masked_shift = shift & 0x1f; // JVM masks shift to 5 bits
        let result = a.wrapping_shl(masked_shift as u32);

        // Result should be consistent with masking
        prop_assert!(result == a.wrapping_shl((shift & 0x1f) as u32));
    }
}

/// Test that array operations preserve length
proptest! {
    #[test]
    fn prop_array_length_preserved(len in 0usize..1000) {
        let mut interpreter = Interpreter::new();

        // Create array
        let arr = interpreter.new_array_int(len as i32).unwrap();

        // Verify length
        let actual_len = interpreter.array_get_length(arr).unwrap();
        prop_assert_eq!(actual_len, len as i32);
    }
}

/// Test that array write/read preserves values
proptest! {
    #[test]
    fn prop_array_write_read(values in prop::collection::vec(any::<i32>(), 0..100)) {
        let mut interpreter = Interpreter::new();
        let len = values.len();

        // Create array
        let arr = interpreter.new_array_int(len as i32).unwrap();

        // Write values
        for (i, &val) in values.iter().enumerate() {
            interpreter.array_set_int(arr, i as i32, val).unwrap();
        }

        // Read values back
        for (i, &expected) in values.iter().enumerate() {
            let actual = interpreter.array_get_int(arr, i as i32).unwrap();
            prop_assert_eq!(actual, expected);
        }
    }
}

/// Test that stack push/pop is reversible
proptest! {
    #[test]
    fn prop_stack_push_pop(values in prop::collection::vec(any::<i32>(), 0..10)) {
        let mut frame = StackFrame::new(10, 10, "test".to_string());
        let original_len = values.len();

        // Push values
        for &val in &values {
            frame.push(Value::Int(val)).unwrap();
        }

        // Pop values in reverse
        let mut popped = Vec::new();
        while frame.stack.len() > 0 {
            popped.push(frame.pop().unwrap().as_int());
        }

        popped.reverse();

        // Should match original
        prop_assert_eq!(popped, values);
        prop_assert_eq!(frame.stack.len(), 0);
    }
}

/// Test that field get/set preserves values
// TODO: Implement field methods on Interpreter
/*
proptest! {
    #[test]
    fn prop_field_get_set(value in any::<i32>()) {
        let mut interpreter = Interpreter::new();

        // Create object
        let obj = interpreter.new_instance("java/lang/Object").unwrap();

        // Set field
        interpreter.set_field_value(obj, "value", Value::Int(value)).unwrap();

        // Get field
        let retrieved = interpreter.get_field_value(obj, "value").unwrap();

        prop_assert_eq!(retrieved, Value::Int(value));
    }
}
*/

/// Test that comparison operations are consistent
proptest! {
    #[test]
    fn prop_icmp_consistency(a in any::<i32>(), b in any::<i32>()) {
        // Test if_icmpeq
        let eq = if a == b { 1 } else { 0 };

        // Test if_icmpne
        let ne = if a != b { 1 } else { 0 };

        // Test if_icmplt
        let lt = if a < b { 1 } else { 0 };

        // Test if_icmpgt
        let gt = if a > b { 1 } else { 0 };

        // Consistency checks
        prop_assert_eq!((eq + ne), 1); // Either equal or not equal
        prop_assert_eq!((lt + gt + eq), 1); // Exactly one of less, greater, or equal
    }
}

/// Test that type conversions are lossless where appropriate
proptest! {
    #[test]
    fn prop_i2l_lossless(a in any::<i32>()) {
        let l = a as i64;
        let result = (l as i32);
        prop_assert_eq!(result, a);
    }
}

/// Test that float comparisons handle NaN correctly
proptest! {
    #[test]
    fn prop_fcmp_nan(_dummy in 0..1) {
        let nan: f32 = f32::NAN;
        let zero: f32 = 0.0;

        // fcmpl returns -1 for NaN
        let cmp_nan = if nan.is_nan() || zero.is_nan() { -1 } else { 0 };
        prop_assert_eq!(cmp_nan, -1);
    }
}

/// Test that string concatenation is associative
// TODO: Implement string methods on Interpreter
/*
proptest! {
    #[test]
    fn prop_string_concat_associative(a in ".*", b in ".*", c in ".*") {
        let mut interpreter = Interpreter::new();

        let sa = interpreter.new_string(a).unwrap();
        let sb = interpreter.new_string(b).unwrap();
        let sc = interpreter.new_string(c).unwrap();

        // (a + b) + c
        let ab = interpreter.string_concat(sa, sb).unwrap();
        let abc1 = interpreter.string_concat(ab, sc).unwrap();

        // a + (b + c)
        let bc = interpreter.string_concat(sb, sc).unwrap();
        let abc2 = interpreter.string_concat(sa, bc).unwrap();

        let s1 = interpreter.string_to_rust(abc1).unwrap();
        let s2 = interpreter.string_to_rust(abc2).unwrap();

        prop_assert_eq!(s1, s2);
    }
}
*/

/// Test that hash codes are consistent
// TODO: Implement hashcode method on Interpreter
/*
proptest! {
    #[test]
    fn prop_hashcode_consistent(a in ".*") {
        let mut interpreter = Interpreter::new();
        let s = interpreter.new_string(a).unwrap();

        let h1 = interpreter.hashcode(s).unwrap();
        let h2 = interpreter.hashcode(s).unwrap();

        prop_assert_eq!(h1, h2);
    }
}
*/

/// Test that GC preserves live objects
// TODO: Implement GC and array methods on Interpreter
/*
proptest! {
    #[test]
    fn prop_gc_preserves_live(values in prop::collection::vec(any::<i32>(), 1..10)) {
        let mut interpreter = Interpreter::new();
        let len = values.len();

        // Create array
        let arr = interpreter.new_array_int(len).unwrap();

        // Write values
        for (i, &val) in values.iter().enumerate() {
            interpreter.array_set_int(arr, i, val).unwrap();
        }

        // Run GC
        interpreter.gc();

        // Verify values preserved
        for (i, &expected) in values.iter().enumerate() {
            let actual = interpreter.array_get_int(arr, i).unwrap();
            prop_assert_eq!(actual, expected);
        }
    }
}
*/

/// Test that object identity is preserved
// TODO: Implement new_instance method
/*
proptest! {
    #[test]
    fn prop_object_identity() {
        let mut interpreter = Interpreter::new();

        let obj1 = interpreter.new_instance("java/lang/Object").unwrap();
        let obj2 = interpreter.new_instance("java/lang/Object").unwrap();

        // Different objects should have different identities
        prop_assert_ne!(obj1, obj2);

        // Same object should have same identity
        prop_assert_eq!(obj1, obj1);
    }
}
*/

/// Test that null handling is consistent
// Note: This test works as it only uses Value::Null
proptest! {
    #[test]
    fn prop_null_handling(_dummy in 0..1) {
        // Null is consistent
        let null1 = Value::Null;
        let null2 = Value::Null;
        prop_assert_eq!(null1, null2);

        // Null is not equal to any reference
        // TODO: Implement new_instance to test this properly
        // let obj = interpreter.new_instance("java/lang/Object").unwrap();
        // prop_assert_ne!(Value::Null, Value::Reference(obj));
    }
}

/// Test that method dispatch is consistent
// TODO: Implement invoke_method
/*
proptest! {
    #[test]
    fn prop_method_dispatch_consistent(a in any::<i32>(), b in any::<i32>()) {
        let mut interpreter = Interpreter::new();

        // Call static method twice with same arguments
        let result1 = interpreter.invoke_method(
            "java/lang/Math",
            "max",
            &[Value::Int(a), Value::Int(b)]
        ).unwrap();

        let result2 = interpreter.invoke_method(
            "java/lang/Math",
            "max",
            &[Value::Int(a), Value::Int(b)]
        ).unwrap();

        prop_assert_eq!(result1, result2);
    }
}
*/

/// Test that bitwise operations preserve properties
proptest! {
    #[test]
    fn prop_bitwise_properties(a in any::<i32>(), b in any::<i32>()) {
        // De Morgan's laws
        let not_a_and_b = !(a & b);
        let not_a_or_not_b = (!a) | (!b);
        prop_assert_eq!(not_a_and_b, not_a_or_not_b);

        let not_a_or_b = !(a | b);
        let not_a_and_not_b = (!a) & (!b);
        prop_assert_eq!(not_a_or_b, not_a_and_not_b);
    }
}

/// Test that array bounds checking works
// TODO: Implement array methods
/*
proptest! {
    #[test]
    fn prop_array_bounds(len in 0usize..100, valid_index in 0usize..100, invalid_index in 100usize..200) {
        let mut interpreter = Interpreter::new();
        let arr = interpreter.new_array_int(len).unwrap();

        // Valid access should succeed
        if valid_index < len {
            let result = interpreter.array_get_int(arr, valid_index);
            prop_assert!(result.is_ok());
        } else {
            let result = interpreter.array_get_int(arr, valid_index);
            prop_assert!(result.is_err());
        }

        // Invalid access should fail
        let result = interpreter.array_get_int(arr, invalid_index);
        prop_assert!(result.is_err());
    }
}
*/

/// Test that division by zero is handled correctly
proptest! {
    #[test]
    fn prop_division_by_zero(a in any::<i32>()) {
        let result = a.checked_div(0);
        prop_assert!(result.is_none());

        if a != 0 {
            let result = a.checked_div(a);
            prop_assert_eq!(result, Some(1));
        }
    }
}

/// Test that modulo operation properties hold
proptest! {
    #[test]
    fn prop_modulo_properties(a in any::<i32>(), b in any::<i32>()) {
        if b != 0 {
            let remainder = a % b;

            // Remainder has same sign as dividend
            if a >= 0 && b > 0 {
                prop_assert!(remainder >= 0);
            }

            // Remainder is less than divisor in magnitude
            prop_assert!(remainder.abs() < b.abs());
        }
    }
}

/// Test that negation properties hold
proptest! {
    #[test]
    fn prop_negation_properties(a in any::<i32>()) {
        // Double negation returns original
        prop_assert_eq!(-(-a), a);

        // Negation of zero is zero
        prop_assert_eq!(-0, 0);
    }
}

/// Test that shift operations preserve bits
proptest! {
    #[test]
    fn prop_shift_bit_preservation(a in any::<u32>()) {
        // Shifting by 0 should preserve value
        prop_assert_eq!(a >> 0, a);
        prop_assert_eq!(a << 0, a);

        // Note: Shifting by 32 or more causes overflow in debug mode
        // In release mode, it would wrap to shift by (shift_amount % 32)
    }
}
