brrr-lint 0.1.0

//! Fix validation engine for F* linting autofixes.
//!
//! This module provides centralized validation for all autofix rules to ensure
//! fixes are safe to apply and don't break working code.
//!
//! # Safety guarantees
//!
//! Before any fix is applied, it must pass validation checks:
//! - Content preservation (no unintended deletions)
//! - Declaration count consistency
//! - No orphaned references
//! - Basic F* syntax validation
//!
//! # Usage
//!
//! All fixable rules (FST001, FST002, FST004, FST005, FST010, FST012, FST013)
//! should use this validator before creating Fix instances.

use std::collections::{HashMap, HashSet};
use std::hash::{Hash, Hasher};
use std::path::Path;

use lazy_static::lazy_static;
use regex::Regex;

lazy_static! {
    /// Pattern to extract F* declarations for counting.
    /// Matches: val, let, type, class, instance, effect, exception, assume val
    static ref DECLARATION_PATTERN: Regex = Regex::new(
        r"(?m)^(?:private\s+)?(?:inline_for_extraction\s+)?(?:noextract\s+)?(?:unfold\s+)?(?:ghost\s+)?(?:noeq\s+)?(?:abstract\s+)?(val|let(?:\s+rec)?|type|class|instance|(?:layered_)?effect|exception|assume\s+val)\s+([a-zA-Z_][a-zA-Z0-9_']*)"
    ).unwrap();

    /// Pattern to extract identifier references from code.
    /// Excludes F* keywords and common built-in types.
    static ref IDENTIFIER_PATTERN: Regex = Regex::new(
        r"\b([a-zA-Z_][a-zA-Z0-9_']*)\b"
    ).unwrap();

    /// F* keywords that should not be counted as references.
    static ref FSTAR_KEYWORDS: HashSet<&'static str> = {
        let mut s = HashSet::new();
        for kw in &[
            // Declaration keywords
            "val", "let", "rec", "type", "noeq", "and", "with", "match",
            "module", "open", "friend", "include",
            "effect", "layered_effect", "new_effect", "sub_effect", "total_effect",
            "class", "instance", "exception",
            "assume", "private", "abstract", "unfold", "irreducible",
            "inline_for_extraction", "noextract", "opaque_to_smt", "ghost",
            // Control flow
            "if", "then", "else", "begin", "end",
            "fun", "function", "return", "yield",
            "in", "of", "when", "as", "try",
            // Logic
            "forall", "exists", "True", "False", "true", "false",
            "not", "mod", "div", "land", "lor", "lxor",
            // Types
            "prop", "Type", "Type0", "Type1", "eqtype", "squash",
            "Tot", "GTot", "Lemma", "Pure", "Ghost", "ST", "Dv", "Div", "Exn",
            "requires", "ensures", "returns", "decreases", "modifies",
            "assert", "admit", "calc",
            // Built-ins
            "unit", "bool", "int", "nat", "pos", "string", "char",
            "option", "list", "either", "ref", "seq", "set", "map",
            // Common constructors
            "Some", "None", "Cons", "Nil", "Inl", "Inr",
            // Module prefixes
            "FStar", "Prims",
        ] {
            s.insert(*kw);
        }
        s
    };

    /// Pattern to detect unclosed block comments.
    static ref COMMENT_OPEN: Regex = Regex::new(r"\(\*").unwrap();
    static ref COMMENT_CLOSE: Regex = Regex::new(r"\*\)").unwrap();

    /// Pattern to detect unclosed string literals (simplified).
    static ref STRING_LITERAL: Regex = Regex::new(r#""(?:[^"\\]|\\.)*""#).unwrap();

    /// Pattern to detect common F* syntax errors.
    static ref SYNTAX_ERROR_PATTERNS: Vec<(&'static str, Regex)> = vec![
        ("Unclosed parenthesis", Regex::new(r"\([^)]*$").unwrap()),
        ("Unclosed brace", Regex::new(r"\{[^}]*$").unwrap()),
        ("Unclosed bracket", Regex::new(r"\[[^\]]*$").unwrap()),
        ("Double semicolon", Regex::new(r";;").unwrap()),
        ("Empty type definition", Regex::new(r"(?m)^type\s+\w+\s*$").unwrap()),
    ];
}

/// Result of fix validation.
#[derive(Debug, Clone)]
pub struct FixValidation {
    /// Whether the fix is considered safe to apply.
    pub is_safe: bool,
    /// Confidence level from 0.0 (no confidence) to 1.0 (full confidence).
    pub confidence: f64,
    /// Warning messages about potential issues.
    pub warnings: Vec<String>,
    /// Whether semantic content is preserved (excluding whitespace).
    pub content_preserved: bool,
    /// Details about what changed in declarations.
    pub declaration_changes: DeclarationChanges,
    /// List of potentially orphaned references.
    pub orphaned_refs: Vec<String>,
}

impl FixValidation {
    /// Create a validation result indicating a safe fix.
    pub fn safe(confidence: f64) -> Self {
        Self {
            is_safe: true,
            confidence,
            warnings: Vec::new(),
            content_preserved: true,
            declaration_changes: DeclarationChanges::default(),
            orphaned_refs: Vec::new(),
        }
    }

    /// Create a validation result indicating an unsafe fix.
    pub fn unsafe_fix(reason: impl Into<String>) -> Self {
        Self {
            is_safe: false,
            confidence: 0.0,
            warnings: vec![reason.into()],
            content_preserved: false,
            declaration_changes: DeclarationChanges::default(),
            orphaned_refs: Vec::new(),
        }
    }

    /// Add a warning to the validation result.
    pub fn with_warning(mut self, warning: impl Into<String>) -> Self {
        self.warnings.push(warning.into());
        self
    }

    /// Reduce confidence by a factor.
    pub fn reduce_confidence(mut self, factor: f64) -> Self {
        self.confidence *= factor;
        self
    }

    /// Check if this fix should be auto-applied based on validation.
    /// Requires is_safe=true and confidence >= threshold.
    pub fn can_auto_apply(&self, threshold: f64) -> bool {
        self.is_safe && self.confidence >= threshold
    }
}

impl Default for FixValidation {
    fn default() -> Self {
        Self {
            is_safe: true,
            confidence: 1.0,
            warnings: Vec::new(),
            content_preserved: true,
            declaration_changes: DeclarationChanges::default(),
            orphaned_refs: Vec::new(),
        }
    }
}

/// Tracks changes in declarations between original and fixed content.
#[derive(Debug, Clone, Default)]
pub struct DeclarationChanges {
    /// Declarations that were removed.
    pub removed: Vec<String>,
    /// Declarations that were added.
    pub added: Vec<String>,
    /// Declarations that were modified (same name, different content).
    pub modified: Vec<String>,
    /// Net change in declaration count (positive = more, negative = fewer).
    pub net_change: i32,
}

/// Validate a fix before applying it.
///
/// Performs comprehensive checks:
/// 1. Content preservation (semantic content excluding whitespace)
/// 2. Declaration counting (no unexpected removals)
/// 3. Reference integrity (no orphaned references)
/// 4. Basic syntax validation
///
/// # Arguments
/// * `original` - The original file content
/// * `fixed` - The proposed fixed content
/// * `_file_path` - Path to the file (for context-specific validation)
///
/// # Returns
/// A `FixValidation` struct with detailed validation results.
pub fn validate_fix(original: &str, fixed: &str, _file_path: &Path) -> FixValidation {
    let mut validation = FixValidation::default();

    // Check 1: Content hash comparison (excluding whitespace)
    let original_hash = content_hash(original);
    let fixed_hash = content_hash(fixed);
    validation.content_preserved = original_hash != fixed_hash; // Different is expected for a fix

    // Check 2: Declaration counting
    let original_decls = count_declarations(original);
    let fixed_decls = count_declarations(fixed);
    validation.declaration_changes = compare_declarations(&original_decls, &fixed_decls);

    // Unexpected declaration removals reduce confidence
    if !validation.declaration_changes.removed.is_empty() {
        let removed_count = validation.declaration_changes.removed.len();
        validation.warnings.push(format!(
            "Fix removes {} declaration(s): {}",
            removed_count,
            validation.declaration_changes.removed.join(", ")
        ));
        // Reduce confidence based on number of removals
        validation.confidence *= 0.8_f64.powi(removed_count as i32);
    }

    // Unexpected declaration additions are suspicious
    if !validation.declaration_changes.added.is_empty() {
        validation.warnings.push(format!(
            "Fix adds new declaration(s): {}",
            validation.declaration_changes.added.join(", ")
        ));
        validation.confidence *= 0.9;
    }

    // Check 3: Orphaned references
    let orphaned = find_undefined_references(fixed, &fixed_decls);
    if !orphaned.is_empty() {
        validation.orphaned_refs = orphaned.clone();
        validation.warnings.push(format!(
            "Potential undefined references after fix: {}",
            orphaned.into_iter().take(5).collect::<Vec<_>>().join(", ")
        ));
        validation.confidence *= 0.7;
    }

    // Check 4: Syntax validation
    if let Err(syntax_errors) = validate_fstar_syntax(fixed) {
        validation.is_safe = false;
        validation.warnings.extend(syntax_errors);
        validation.confidence = 0.0;
    }

    // Check 5: Comment balance
    if !check_comment_balance(fixed) {
        validation.warnings.push("Unbalanced comments detected in fixed content".to_string());
        validation.confidence *= 0.5;
    }

    // Final safety determination
    // A fix is safe if:
    // - No syntax errors
    // - Confidence remains above 0.5
    // - Not removing more than expected
    if validation.confidence < 0.5 {
        validation.is_safe = false;
    }

    validation
}

/// Compute a semantic hash of content, ignoring whitespace differences.
///
/// This hash is used to check if content has changed semantically,
/// not just in formatting.
///
/// # Algorithm
/// 1. Strip all whitespace
/// 2. Remove comments
/// 3. Compute FNV-1a hash of remaining content
pub fn content_hash(text: &str) -> u64 {
    use std::collections::hash_map::DefaultHasher;

    let normalized = normalize_content(text);
    let mut hasher = DefaultHasher::new();
    normalized.hash(&mut hasher);
    hasher.finish()
}

/// Normalize content by removing whitespace and comments.
fn normalize_content(text: &str) -> String {
    // Remove block comments
    let without_block_comments = strip_block_comments(text);
    // Remove line comments
    let without_comments = strip_line_comments(&without_block_comments);
    // Normalize whitespace
    without_comments
        .split_whitespace()
        .collect::<Vec<_>>()
        .join(" ")
}

/// Strip F* block comments (* ... *).
fn strip_block_comments(text: &str) -> String {
    let mut result = String::new();
    let mut depth = 0;
    let chars: Vec<char> = text.chars().collect();
    let mut i = 0;

    while i < chars.len() {
        if i + 1 < chars.len() && chars[i] == '(' && chars[i + 1] == '*' {
            depth += 1;
            i += 2;
            continue;
        }
        if i + 1 < chars.len() && chars[i] == '*' && chars[i + 1] == ')' && depth > 0 {
            depth -= 1;
            i += 2;
            continue;
        }
        if depth == 0 {
            result.push(chars[i]);
        }
        i += 1;
    }

    result
}

/// Strip F* line comments (// ...).
fn strip_line_comments(text: &str) -> String {
    text.lines()
        .map(|line| {
            if let Some(pos) = line.find("//") {
                &line[..pos]
            } else {
                line
            }
        })
        .collect::<Vec<_>>()
        .join("\n")
}

/// Verify basic F* syntax in content.
///
/// Checks for common syntax errors that would make the fixed code invalid.
/// This is a heuristic check, not a full parser.
///
/// # Returns
/// - `Ok(())` if no obvious syntax errors
/// - `Err(Vec<String>)` with error descriptions if issues found
pub fn validate_fstar_syntax(content: &str) -> Result<(), Vec<String>> {
    let mut errors = Vec::new();

    // Check bracket balance
    let paren_balance = count_char_balance(content, '(', ')');
    if paren_balance != 0 {
        errors.push(format!(
            "Unbalanced parentheses: {} extra {}",
            paren_balance.abs(),
            if paren_balance > 0 { "open" } else { "close" }
        ));
    }

    let brace_balance = count_char_balance(content, '{', '}');
    if brace_balance != 0 {
        errors.push(format!(
            "Unbalanced braces: {} extra {}",
            brace_balance.abs(),
            if brace_balance > 0 { "open" } else { "close" }
        ));
    }

    let bracket_balance = count_char_balance(content, '[', ']');
    if bracket_balance != 0 {
        errors.push(format!(
            "Unbalanced brackets: {} extra {}",
            bracket_balance.abs(),
            if bracket_balance > 0 { "open" } else { "close" }
        ));
    }

    // Check for specific error patterns
    for (name, pattern) in SYNTAX_ERROR_PATTERNS.iter() {
        if pattern.is_match(content) {
            errors.push(format!("Syntax issue: {}", name));
        }
    }

    // Check string literal balance (simplified)
    let quote_count = content.chars().filter(|&c| c == '"').count();
    if quote_count % 2 != 0 {
        errors.push("Unbalanced string quotes".to_string());
    }

    if errors.is_empty() {
        Ok(())
    } else {
        Err(errors)
    }
}

/// Count character balance (opens - closes), accounting for strings and comments.
fn count_char_balance(content: &str, open: char, close: char) -> i32 {
    let clean = strip_block_comments(content);
    let clean = strip_line_comments(&clean);
    // Also strip string literals to avoid counting brackets inside strings
    let clean = strip_string_literals(&clean);

    let opens = clean.chars().filter(|&c| c == open).count() as i32;
    let closes = clean.chars().filter(|&c| c == close).count() as i32;
    opens - closes
}

/// Strip string literals from content.
fn strip_string_literals(text: &str) -> String {
    STRING_LITERAL.replace_all(text, "\"\"").to_string()
}

/// Check if block comments are balanced.
fn check_comment_balance(content: &str) -> bool {
    let opens = COMMENT_OPEN.find_iter(content).count();
    let closes = COMMENT_CLOSE.find_iter(content).count();
    opens == closes
}

/// Count declarations in F* content by category.
///
/// Returns a map from declaration name to declaration kind.
pub fn count_declarations(content: &str) -> HashMap<String, String> {
    let mut decls = HashMap::new();

    for caps in DECLARATION_PATTERN.captures_iter(content) {
        let kind = caps.get(1).map(|m| m.as_str()).unwrap_or("unknown");
        let name = caps.get(2).map(|m| m.as_str()).unwrap_or("");

        if !name.is_empty() {
            decls.insert(name.to_string(), kind.to_string());
        }
    }

    decls
}

/// Compare declaration counts between original and fixed.
fn compare_declarations(
    original: &HashMap<String, String>,
    fixed: &HashMap<String, String>,
) -> DeclarationChanges {
    let mut changes = DeclarationChanges::default();

    // Find removed declarations
    for name in original.keys() {
        if !fixed.contains_key(name) {
            changes.removed.push(name.clone());
        }
    }

    // Find added declarations
    for name in fixed.keys() {
        if !original.contains_key(name) {
            changes.added.push(name.clone());
        }
    }

    // Find modified declarations (same name, could have different implementation)
    // We can't easily detect this without deeper analysis, so we skip for now

    changes.net_change = fixed.len() as i32 - original.len() as i32;
    changes
}

/// Find potentially undefined references in content.
///
/// Returns identifiers that are used but not declared in the content.
/// Note: This has false positives for imports from other modules.
pub fn find_undefined_references(
    content: &str,
    declarations: &HashMap<String, String>,
) -> Vec<String> {
    let mut undefined = Vec::new();
    let declared_names: HashSet<&str> = declarations.keys().map(|s| s.as_str()).collect();

    // Extract all identifier usages
    for caps in IDENTIFIER_PATTERN.captures_iter(content) {
        let ident = caps.get(1).map(|m| m.as_str()).unwrap_or("");

        // Skip keywords, declared names, and common patterns
        if FSTAR_KEYWORDS.contains(ident) {
            continue;
        }
        if declared_names.contains(ident) {
            continue;
        }
        // Skip uppercase identifiers (likely module names or constructors)
        if ident.chars().next().map(|c| c.is_uppercase()).unwrap_or(false) {
            continue;
        }
        // Skip underscored names (often parameters)
        if ident.starts_with('_') {
            continue;
        }

        // This is a potential undefined reference
        // But it could also be imported from another module
        // We track it but don't necessarily fail on it
        if !undefined.contains(&ident.to_string()) {
            undefined.push(ident.to_string());
        }
    }

    // Limit to first 20 to avoid noise
    undefined.truncate(20);
    undefined
}

/// Validate that a fix preserves expected declarations.
///
/// Use this for fixes that should only modify, not remove, declarations.
pub fn validate_no_removals(original: &str, fixed: &str) -> Result<(), String> {
    let orig_decls = count_declarations(original);
    let fixed_decls = count_declarations(fixed);

    for name in orig_decls.keys() {
        if !fixed_decls.contains_key(name) {
            return Err(format!("Fix would remove declaration: {}", name));
        }
    }

    Ok(())
}

/// Validate that a fix only removes specified declarations.
///
/// Use this for fixes that intentionally remove specific declarations
/// (e.g., removing duplicate types).
pub fn validate_expected_removals(
    original: &str,
    fixed: &str,
    expected_removals: &[&str],
) -> FixValidation {
    let orig_decls = count_declarations(original);
    let fixed_decls = count_declarations(fixed);
    let mut validation = FixValidation::safe(1.0);

    let expected_set: HashSet<&str> = expected_removals.iter().copied().collect();

    for name in orig_decls.keys() {
        if !fixed_decls.contains_key(name) {
            if !expected_set.contains(name.as_str()) {
                validation.warnings.push(format!(
                    "Unexpected removal of declaration: {}",
                    name
                ));
                validation.confidence *= 0.5;
            }
            validation.declaration_changes.removed.push(name.clone());
        }
    }

    for name in fixed_decls.keys() {
        if !orig_decls.contains_key(name) {
            validation.declaration_changes.added.push(name.clone());
            validation.warnings.push(format!("Unexpected addition: {}", name));
            validation.confidence *= 0.8;
        }
    }

    validation.declaration_changes.net_change =
        fixed_decls.len() as i32 - orig_decls.len() as i32;

    if validation.confidence < 0.5 {
        validation.is_safe = false;
    }

    validation
}

/// Quick validation for whitespace-only fixes.
///
/// These are always safe since they don't change semantics.
pub fn validate_whitespace_only_fix(original: &str, fixed: &str) -> FixValidation {
    let orig_normalized = normalize_content(original);
    let fixed_normalized = normalize_content(fixed);

    if orig_normalized == fixed_normalized {
        FixValidation::safe(1.0)
    } else {
        FixValidation::unsafe_fix("Fix changes more than whitespace")
    }
}

/// Validate a line deletion fix.
///
/// Checks that only the specified lines are removed and nothing else changes.
pub fn validate_line_deletion(
    original: &str,
    _start_line: usize,
    _end_line: usize,
    deleted_content: &str,
) -> FixValidation {
    let mut validation = FixValidation::safe(0.9);

    // Check what's being deleted
    let decls_in_deleted = count_declarations(deleted_content);
    if !decls_in_deleted.is_empty() {
        validation.declaration_changes.removed =
            decls_in_deleted.keys().cloned().collect();
        validation.warnings.push(format!(
            "Deleting {} declaration(s): {}",
            decls_in_deleted.len(),
            decls_in_deleted.keys().cloned().collect::<Vec<_>>().join(", ")
        ));
        validation.confidence *= 0.7;
    }

    // Check for references in deleted content that might be used elsewhere
    let refs_in_deleted: Vec<String> = IDENTIFIER_PATTERN
        .captures_iter(deleted_content)
        .filter_map(|c| c.get(1))
        .map(|m| m.as_str().to_string())
        .filter(|s| !FSTAR_KEYWORDS.contains(s.as_str()))
        .collect();

    if !refs_in_deleted.is_empty() {
        // Check if these references exist elsewhere in original
        let remaining_content = original.replace(deleted_content, "");
        for ref_name in &refs_in_deleted {
            if remaining_content.contains(ref_name) {
                // Reference exists elsewhere, might be the definition
                // This is expected for deletion fixes
            }
        }
    }

    validation
}

#[cfg(test)]
mod tests {
    use super::*;
    use std::path::PathBuf;

    #[test]
    fn test_content_hash_ignores_whitespace() {
        let content1 = "let foo x = x + 1";
        let content2 = "let   foo   x   =   x   +   1";
        let content3 = "let foo x =\n  x + 1";

        assert_eq!(content_hash(content1), content_hash(content2));
        assert_eq!(content_hash(content1), content_hash(content3));
    }

    #[test]
    fn test_content_hash_ignores_comments() {
        let content1 = "let foo x = x + 1";
        let content2 = "(* comment *) let foo x = x + 1";
        let content3 = "let foo x = x + 1 // comment";

        assert_eq!(content_hash(content1), content_hash(content2));
        assert_eq!(content_hash(content1), content_hash(content3));
    }

    #[test]
    fn test_content_hash_different_for_different_content() {
        let content1 = "let foo x = x + 1";
        let content2 = "let foo x = x + 2";

        assert_ne!(content_hash(content1), content_hash(content2));
    }

    #[test]
    fn test_count_declarations() {
        let content = r#"
module Test

val foo : int -> int
let foo x = x + 1

type mytype = nat

let bar y = y * 2
"#;
        let decls = count_declarations(content);

        assert!(decls.contains_key("foo"));
        assert!(decls.contains_key("mytype"));
        assert!(decls.contains_key("bar"));
        assert_eq!(decls.len(), 3); // foo appears twice but same name
    }

    #[test]
    fn test_validate_fstar_syntax_balanced() {
        let content = "let foo (x: int) = { field = x }";
        assert!(validate_fstar_syntax(content).is_ok());
    }

    #[test]
    fn test_validate_fstar_syntax_unbalanced_parens() {
        let content = "let foo (x: int = x + 1";
        let result = validate_fstar_syntax(content);
        assert!(result.is_err());
        let errors = result.unwrap_err();
        assert!(errors.iter().any(|e| e.contains("parentheses")));
    }

    #[test]
    fn test_validate_fstar_syntax_unbalanced_braces() {
        let content = "let foo x = { field = x";
        let result = validate_fstar_syntax(content);
        assert!(result.is_err());
        let errors = result.unwrap_err();
        assert!(errors.iter().any(|e| e.contains("braces")));
    }

    #[test]
    fn test_find_undefined_references() {
        let content = r#"
let foo x = bar x + baz
"#;
        let decls = count_declarations(content);
        let undefined = find_undefined_references(content, &decls);

        // bar and baz should be flagged as potentially undefined
        // (though they might be imported)
        assert!(undefined.contains(&"bar".to_string()) || undefined.contains(&"baz".to_string()));
    }

    #[test]
    fn test_validate_fix_safe() {
        let original = r#"
module Test
let foo x = x + 1
let bar y = y * 2
"#;
        let fixed = r#"
module Test
let foo x = x + 1
let bar y = y * 3
"#;
        let path = PathBuf::from("test.fst");
        let validation = validate_fix(original, fixed, &path);

        assert!(validation.is_safe);
        assert!(validation.confidence > 0.5);
    }

    #[test]
    fn test_validate_fix_removes_declaration() {
        let original = r#"
module Test
let foo x = x + 1
let bar y = y * 2
"#;
        let fixed = r#"
module Test
let foo x = x + 1
"#;
        let path = PathBuf::from("test.fst");
        let validation = validate_fix(original, fixed, &path);

        // Should detect the removal
        assert!(validation.declaration_changes.removed.contains(&"bar".to_string()));
        assert!(!validation.warnings.is_empty());
    }

    #[test]
    fn test_validate_expected_removals() {
        let original = r#"
module Test
type foo = nat
let bar x = x
"#;
        let fixed = r#"
module Test
let bar x = x
"#;
        let validation = validate_expected_removals(original, fixed, &["foo"]);

        assert!(validation.is_safe);
        assert!(validation.confidence > 0.8);
    }

    #[test]
    fn test_validate_unexpected_removal() {
        let original = r#"
module Test
type foo = nat
let bar x = x
"#;
        let fixed = r#"
module Test
"#;
        let validation = validate_expected_removals(original, fixed, &["foo"]);

        // bar was removed unexpectedly - this should trigger warnings
        // and reduce confidence significantly
        assert!(validation.warnings.iter().any(|w| w.contains("bar")));
        // Confidence should be reduced due to unexpected removal
        assert!(validation.confidence < 1.0, "Confidence should be reduced: {}", validation.confidence);
    }

    #[test]
    fn test_validate_whitespace_only() {
        let original = "let foo x = x + 1";
        let fixed = "let  foo  x  =  x  +  1";

        let validation = validate_whitespace_only_fix(original, fixed);
        assert!(validation.is_safe);
        assert_eq!(validation.confidence, 1.0);
    }

    #[test]
    fn test_validate_not_whitespace_only() {
        let original = "let foo x = x + 1";
        let fixed = "let foo x = x + 2";

        let validation = validate_whitespace_only_fix(original, fixed);
        assert!(!validation.is_safe);
    }

    #[test]
    fn test_strip_block_comments() {
        let content = "let (* comment *) foo = 1";
        let stripped = strip_block_comments(content);
        assert_eq!(stripped, "let  foo = 1");
    }

    #[test]
    fn test_strip_nested_block_comments() {
        let content = "let (* outer (* inner *) *) foo = 1";
        let stripped = strip_block_comments(content);
        assert_eq!(stripped, "let  foo = 1");
    }

    #[test]
    fn test_check_comment_balance() {
        assert!(check_comment_balance("(* comment *)"));
        assert!(check_comment_balance("(* outer (* inner *) *)"));
        assert!(!check_comment_balance("(* unclosed"));
        assert!(!check_comment_balance("extra close *)"));
    }

    #[test]
    fn test_fix_validation_can_auto_apply() {
        let validation = FixValidation::safe(0.9);
        assert!(validation.can_auto_apply(0.8));
        assert!(!validation.can_auto_apply(0.95));

        let unsafe_validation = FixValidation::unsafe_fix("reason");
        assert!(!unsafe_validation.can_auto_apply(0.0));
    }

    #[test]
    fn test_declaration_pattern_matches() {
        let test_cases = vec![
            ("val foo : int -> int", Some("foo")),
            ("let foo x = x + 1", Some("foo")),
            ("let rec factorial n = ...", Some("factorial")),
            ("type mytype = nat", Some("mytype")),
            ("private let internal x = 1", Some("internal")),
            ("inline_for_extraction let fast x = x", Some("fast")),
            ("class myclass a = { ... }", Some("myclass")),
            ("instance myinst : myclass int = { ... }", Some("myinst")),
            ("exception MyExn", Some("MyExn")),
            ("assume val axiom : prop", Some("axiom")),
        ];

        for (input, expected_name) in test_cases {
            let decls = count_declarations(input);
            if let Some(name) = expected_name {
                assert!(
                    decls.contains_key(name),
                    "Expected to find '{}' in '{}'",
                    name,
                    input
                );
            }
        }
    }

    // =========================================================================
    // F*-SPECIFIC PATTERN TESTS
    // =========================================================================

    #[test]
    fn test_fstar_refinement_types() {
        let content = r#"
val bounded_nat : (n:nat{n < 100}) -> int
let bounded_nat n = n + 1
"#;
        let result = validate_fstar_syntax(content);
        assert!(result.is_ok(), "Refinement types should be valid syntax");
    }

    #[test]
    fn test_fstar_lemma_declarations() {
        let content = r#"
val lemma_add_comm : x:int -> y:int -> Lemma (x + y == y + x)
let lemma_add_comm x y = ()
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("lemma_add_comm"));
    }

    #[test]
    fn test_fstar_ghost_bindings() {
        let content = r#"
ghost let ghost_val : int = 42
let normal_val : int = 1
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("ghost_val"));
        assert!(decls.contains_key("normal_val"));
    }

    #[test]
    fn test_fstar_noextract_bindings() {
        let content = r#"
noextract let proof_only : int = 1
inline_for_extraction noextract let also_proof : int = 2
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("proof_only"));
        assert!(decls.contains_key("also_proof"));
    }

    #[test]
    fn test_fstar_noeq_types() {
        let content = r#"
noeq type myrecord = {
  field1: int;
  field2: string
}
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("myrecord"));
    }

    #[test]
    fn test_fstar_effect_declarations() {
        let content = r#"
effect MyEffect (a:Type) = Tot a
layered_effect PURE = ...
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("MyEffect"));
        assert!(decls.contains_key("PURE"));
    }

    #[test]
    fn test_validate_fix_preserves_open_statements() {
        let original = r#"
module Test
open FStar.List.Tot

let use_list x = List.hd x
"#;
        let fixed = r#"
module Test
open FStar.List.Tot

let use_list x = List.head x
"#;
        let path = PathBuf::from("test.fst");
        let validation = validate_fix(original, fixed, &path);

        // Should be safe - only implementation changed
        assert!(validation.is_safe);
        assert!(validation.declaration_changes.removed.is_empty());
    }

    #[test]
    fn test_validate_fix_detects_removed_open() {
        let original = r#"
module Test
open FStar.List.Tot
open FStar.Seq

let use_list x = List.hd x
"#;
        let fixed = r#"
module Test
open FStar.List.Tot

let use_list x = List.hd x
"#;
        let path = PathBuf::from("test.fst");
        let validation = validate_fix(original, fixed, &path);

        // Open removal doesn't show up in declaration changes
        // but should still be safe
        assert!(validation.is_safe);
    }

    #[test]
    fn test_fstar_mutual_recursion() {
        let content = r#"
type expr =
  | Const : int -> expr
  | Add : expr -> expr -> expr

and stmt =
  | Assign : string -> expr -> stmt
  | Seq : stmt -> stmt -> stmt
"#;
        let result = validate_fstar_syntax(content);
        assert!(result.is_ok(), "Mutual recursion should be valid syntax");
    }

    #[test]
    fn test_fstar_attributes() {
        let content = r#"
[@@ "opaque_to_smt"]
val hidden_impl : int -> int

[@ "inline_let"]
let inlined x = x + 1
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("hidden_impl"));
        assert!(decls.contains_key("inlined"));
    }

    #[test]
    fn test_validate_line_deletion_empty() {
        let original = r#"
module Test

let foo x = x

let bar y = y
"#;
        let deleted = "\nlet bar y = y\n";
        let validation = validate_line_deletion(original, 5, 6, deleted);

        assert!(validation.declaration_changes.removed.contains(&"bar".to_string()));
    }

    // =========================================================================
    // EDGE CASE TESTS
    // =========================================================================

    #[test]
    fn test_empty_content() {
        let decls = count_declarations("");
        assert!(decls.is_empty());

        let result = validate_fstar_syntax("");
        assert!(result.is_ok());
    }

    #[test]
    fn test_comment_only_content() {
        let content = "(* This is just a comment *)";
        let decls = count_declarations(content);
        assert!(decls.is_empty());
    }

    #[test]
    fn test_nested_brackets_in_strings() {
        let content = r#"let msg = "({[}])" in msg"#;
        let result = validate_fstar_syntax(content);
        // String literals should be stripped, so brackets inside don't count
        assert!(result.is_ok());
    }

    #[test]
    fn test_validation_with_warnings_still_safe() {
        let validation = FixValidation::safe(0.9)
            .with_warning("Minor issue detected");

        assert!(validation.is_safe);
        assert!(!validation.warnings.is_empty());
        assert!(validation.can_auto_apply(0.8));
    }

    #[test]
    fn test_confidence_reduction() {
        let validation = FixValidation::safe(1.0)
            .reduce_confidence(0.5)
            .reduce_confidence(0.5);

        assert_eq!(validation.confidence, 0.25);
    }

    #[test]
    fn test_validate_no_removals_success() {
        let original = "let foo x = x\nlet bar y = y";
        let fixed = "let foo x = x + 1\nlet bar y = y * 2";

        let result = validate_no_removals(original, fixed);
        assert!(result.is_ok());
    }

    #[test]
    fn test_validate_no_removals_failure() {
        let original = "let foo x = x\nlet bar y = y";
        let fixed = "let foo x = x + 1";

        let result = validate_no_removals(original, fixed);
        assert!(result.is_err());
        assert!(result.unwrap_err().contains("bar"));
    }

    #[test]
    fn test_declaration_changes_default() {
        let changes = DeclarationChanges::default();
        assert!(changes.removed.is_empty());
        assert!(changes.added.is_empty());
        assert!(changes.modified.is_empty());
        assert_eq!(changes.net_change, 0);
    }

    #[test]
    fn test_fix_validation_default() {
        let validation = FixValidation::default();
        assert!(validation.is_safe);
        assert_eq!(validation.confidence, 1.0);
        assert!(validation.warnings.is_empty());
        assert!(validation.content_preserved);
    }

    #[test]
    fn test_multiline_string_handling() {
        // F* doesn't have multiline strings, but we should handle gracefully
        let content = r#"let x = "line1
line2""#;
        // This is actually invalid F* but we test robustness
        let _ = validate_fstar_syntax(content);
    }

    #[test]
    fn test_unicode_identifiers() {
        // F* supports unicode in strings but not in identifiers
        let content = r#"let msg = "Hello, World!" in msg"#;
        let result = validate_fstar_syntax(content);
        assert!(result.is_ok());
    }

    #[test]
    fn test_complex_fstar_file() {
        let content = r#"
module ComplexTest

open FStar.List.Tot
open FStar.Seq

(** Documentation for foo *)
val foo : #a:Type -> list a -> nat
let foo #a l = length l

private let helper x = x + 1

type config = {
  debug: bool;
  level: nat
}

let rec factorial (n:nat) : Tot nat (decreases n) =
  if n = 0 then 1
  else n * factorial (n - 1)
"#;
        let decls = count_declarations(content);
        assert!(decls.contains_key("foo"));
        assert!(decls.contains_key("helper"));
        assert!(decls.contains_key("config"));
        assert!(decls.contains_key("factorial"));

        let result = validate_fstar_syntax(content);
        assert!(result.is_ok());
    }
}