//! Property-based tests for verifying compiler invariants

#![allow(clippy::unnecessary_wraps)] // Property tests often need Result for the test framework

use crate::backend::Transpiler;

use crate::frontend::ast::{BinaryOp, Expr, ExprKind, Literal, StringPart, UnaryOp};

use crate::frontend::{Parser, RecoveryParser};

#[allow(unused_imports)]

use crate::testing::generators::{arb_expr, arb_well_typed_expr};

use proptest::prelude::*;

use proptest::test_runner::TestCaseError;

/// Property: Parser should never panic on any input

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_parser_never_panics(input: &str) -> Result<(), TestCaseError> {

    let mut parser = Parser::new(input);

    // Parser should either succeed or return an error, never panic

    let _ = parser.parse();

    Ok(())

}

/// Property: Recovery parser should always produce some AST

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_recovery_parser_always_produces_ast(input: &str) -> Result<(), TestCaseError> {

    let mut parser = RecoveryParser::new(input);

    let result = parser.parse_with_recovery();

    // For non-empty input, we should get some AST or errors

    if !input.trim().is_empty() {

        prop_assert!(

            result.ast.is_some() || 
!result.errors.is_empty()0
,

            "Recovery parser should produce AST or errors for non-empty input"

        );

    }

    Ok(())

}

/// Property: Transpilation preserves expression structure

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_transpilation_preserves_structure(expr: &Expr) -> Result<(), TestCaseError> {

    let transpiler = Transpiler::new();

    // Transpilation should either succeed or fail cleanly

    if let Ok(rust_code) = transpiler.transpile(expr) {

        // The generated Rust code should not be empty

        let code_str = rust_code.to_string();

        prop_assert!(!code_str.is_empty(), 
"Transpiled code should not be empty"0
);

    } else {

        // Transpilation errors are acceptable for some ASTs

    }

    Ok(())

}

/// Property: String interpolation transpiles correctly

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_string_interpolation_transpiles(parts: &[StringPart]) -> Result<(), TestCaseError> {

    let transpiler = Transpiler::new();

    let result = transpiler.transpile_string_interpolation(parts);

    // Should either succeed or fail cleanly, never panic

    if let Ok(tokens) = result {

        let code = tokens.to_string();

        // Should either be a format! call or a simple string literal

        prop_assert!(

            code.contains("format!") || code.starts_with('"') || code == "()",

            "String interpolation should produce format! call or string literal"

        );

    }

    // Transpilation errors are acceptable for malformed parts

    Ok(())

}

/// Property: Parse-print roundtrip

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_parse_print_roundtrip(expr: &Expr) -> Result<(), TestCaseError> {

    // This would require a pretty-printer, which we'll implement later

    // For now, just check that we can transpile and the result is valid

    let transpiler = Transpiler::new();

    if let Ok(rust_code) = transpiler.transpile(expr) {

        // Check that the Rust code contains expected elements based on expr type

        let code_str = rust_code.to_string();

        match &expr.kind {

            ExprKind::Literal(Literal::Integer(n)) => {

                // Integer literals are transpiled with type suffixes (e.g., "42 i32")

                prop_assert!(

                    code_str.contains(&n.to_string()),

                    "Integer literal {n} not found in transpiled code"

                );

            }

            ExprKind::Literal(Literal::Bool(b)) => {

                prop_assert!(

                    code_str.contains(&b.to_string()),

                    "Bool literal {b} not found in transpiled code"

                );

            }

            ExprKind::Binary {

                op: BinaryOp::Add, ..

            } => {

                prop_assert!(

                    code_str.contains('+'),

                    "Addition operator not found in transpiled code"

                );

            }

            _ => {

                // Other cases are more complex to verify

            }

        }

    }

    Ok(())

}

/// Property: Well-typed expressions should always transpile successfully

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_well_typed_always_transpiles(expr: &Expr) -> Result<(), TestCaseError> {

    let transpiler = Transpiler::new();

    // Check if this is a simple, well-typed expression

    if is_well_typed(expr) {

        match transpiler.transpile(expr) {

            Ok(_) => Ok(()),

            Err(e) => {

                prop_assert!(

                    false,

                    "Well-typed expression failed to transpile: {:?}\nError: {}",

                    expr,

                    e

                );

                Ok(())

            }

        }

    } else {

        // Complex expressions may fail, which is acceptable

        Ok(())

    }

}

/// Property: Error recovery should handle truncated input gracefully

///

/// # Errors

///

/// Returns an error if the property test fails

pub fn prop_recovery_handles_truncation(input: &str) -> Result<(), TestCaseError> {

    if input.is_empty() {

        return Ok(());

    }

    // Try parsing truncated versions of the input

    for i in 0..
input33
.
len33
() {

        let truncated = &input[..i];

        let mut parser = RecoveryParser::new(truncated);

        let result = parser.parse_with_recovery();

        // Should not panic, and should produce something

        if !truncated.trim().is_empty() {

            prop_assert!(

                result.ast.is_some() || 
!result.errors.is_empty()0
,

                "Recovery parser should handle truncated input at position {i}"

            );

        }

    }

    Ok(())

}

/// Helper to check if an expression is well-typed (simplified)

fn is_well_typed(expr: &Expr) -> bool {

    match &expr.kind {

        ExprKind::Literal(_) | ExprKind::Identifier(_) => true,

        ExprKind::Binary { left, right, op } => {

            match op {

                BinaryOp::Add | BinaryOp::Subtract | BinaryOp::Multiply | BinaryOp::Divide => {

                    is_numeric(left) && is_numeric(right)

                }

                BinaryOp::And | BinaryOp::Or => is_boolean(left) && is_boolean(right),

                BinaryOp::Equal | BinaryOp::NotEqual => {

                    // Equality can work on many types

                    is_well_typed(left) && is_well_typed(right)

                }

                _ => is_well_typed(left) && is_well_typed(right),

            }

        }

        ExprKind::Unary { operand, op } => match op {

            UnaryOp::Not => is_boolean(operand),

            UnaryOp::Negate | UnaryOp::BitwiseNot => is_numeric(operand),

            UnaryOp::Reference => true, // Reference can be applied to any type

        },

        ExprKind::If {

            condition,

            then_branch,

            else_branch,

        } => {

            is_boolean(condition)

                && is_well_typed(then_branch)

                && else_branch.as_ref().is_none_or(|e| is_well_typed(e))

        }

        _ => false, // Conservative for complex expressions

    }

}

fn is_numeric(expr: &Expr) -> bool {

    matches!(

        &expr.kind,

        ExprKind::Literal(Literal::Integer(_) | Literal::Float(_))

    )

}

fn is_boolean(expr: &Expr) -> bool {

    matches!(&expr.kind, ExprKind::Literal(Literal::Bool(_)))

}

#[cfg(test)]

#[allow(clippy::unwrap_used, clippy::panic)]

mod tests {

    use super::*;

    proptest! {

        #[test]

        fn test_parser_never_panics(input in ".*") {

            prop_parser_never_panics(&input)?;

        }

        #[test]

        fn test_recovery_parser_always_produces_ast(input in ".*") {

            prop_recovery_parser_always_produces_ast(&input)?;

        }

        #[test]

        fn test_transpilation_preserves_structure(expr in arb_expr()) {

            prop_transpilation_preserves_structure(&expr)?;

        }

        #[test]

        fn test_well_typed_always_transpiles(expr in arb_well_typed_expr()) {

            prop_well_typed_always_transpiles(&expr)?;

        }

        #[test]

        fn test_recovery_handles_truncation(input in "[a-zA-Z0-9 +\\-*/()]+") {

            prop_recovery_handles_truncation(&input)?;

        }

        #[test]

        fn test_parse_print_roundtrip(expr in arb_well_typed_expr()) {

            prop_parse_print_roundtrip(&expr)?;

        }

    }

    #[test]

    #[ignore = "This test hangs due to infinite loop in recovery parser"]

    fn test_specific_recovery_cases() {

        // Test specific error recovery scenarios

        let cases = vec![

            ("let x =", "Missing value in let binding"),

            ("if x >", "Missing right operand"),

            ("fun foo(", "Missing closing paren"),

            ("[1, 2,", "Missing closing bracket"),

            ("1 + + 2", "Double operator"),

        ];

        for (input, _description) in cases {

            let mut parser = RecoveryParser::new(input);

            let result = parser.parse_with_recovery();

            assert!(

                result.ast.is_some() || !result.errors.is_empty(),

                "Failed to handle: {input}"

            );

        }

    }

}