brrr-lint 0.1.0

//! FST001: Duplicate type definition detection.
//!
//! Port of remove_fst_duplicate_types.py.
//!
//! When a type is fully defined (with = and body) in the .fsti interface file,
//! F* expects the .fst implementation file to NOT redefine it.
//!
//! Handles:
//! - Simple type aliases: type foo = nat
//! - noeq types: noeq type bar = { field : nat }
//! - unfold types: unfold type my_nat = nat
//! - inline_for_extraction types
//! - ADT types: type color = | Red | Green | Blue
//! - Record types: type person = { name: string; age: nat }
//! - Mutual recursion: type a = ... and b = ... and c = ...
//! - Attributes before types: [@...] type t = ...
//! - F* directives: #push-options, #pop-options, #set-options
//! - Type declarations (without =) in .fsti are NOT considered concrete
//! - Private types in .fst are NOT removed (implementation details)
//!
//! SAFETY FEATURES (Critical for autofix):
//! - Exact definition matching: Only offers fix if .fst and .fsti definitions are IDENTICAL
//! - Definition normalization: Strips comments and normalizes whitespace for comparison
//! - Preview support: Fix includes preview of what will be removed
//! - Validation: validate_fix function checks removal safety
//! - Reference detection: Warns about potential dependent code

use lazy_static::lazy_static;
use regex::Regex;
use std::collections::{HashMap, HashSet};
use std::path::PathBuf;

use super::rules::{Diagnostic, DiagnosticSeverity, Edit, Fix, FixSafetyLevel, Range, Rule, RuleCode};

lazy_static! {
    // All valid type modifiers that can precede 'type' keyword
    static ref TYPE_MODIFIERS: &'static [&'static str] = &[
        "inline_for_extraction",
        "noextract",
        "private",
        "abstract",
        "unfold",
        "noeq",
        "unopteq",
    ];

    // Build modifier pattern
    static ref MODIFIER_PATTERN: String = {
        let mods = TYPE_MODIFIERS.join("|");
        format!(r"(?:(?:{})\s+)*", mods)
    };

    // Pattern for detecting type definitions
    static ref TYPE_START_PATTERN: Regex = Regex::new(
        &format!(r"^{}type\s+([a-zA-Z_][a-zA-Z0-9_']*)", *MODIFIER_PATTERN)
    ).unwrap();

    // Pattern for 'and' continuation of mutual recursion
    static ref AND_TYPE_PATTERN: Regex = Regex::new(
        r"^and\s+([a-zA-Z_][a-zA-Z0-9_']*)"
    ).unwrap();

    // Pattern to check if a type line has 'private' modifier
    static ref PRIVATE_TYPE_PATTERN: Regex = Regex::new(
        &format!(r"^(?:(?:{})\s+)*private\s+(?:(?:{})\s+)*type\s+",
                 TYPE_MODIFIERS.join("|"), TYPE_MODIFIERS.join("|"))
    ).unwrap();

    // Pattern for F* directives that do NOT terminate type definitions
    static ref FST_DIRECTIVE_PATTERN: Regex = Regex::new(
        r"^#(push-options|pop-options|set-options|restart-solver)\b"
    ).unwrap();

    // Terminators: constructs that definitely end a type definition block
    static ref TERMINATORS: &'static [&'static str] = &[
        "val ",
        "let ",
        "let rec ",
        "unfold let ",
        "inline_for_extraction let ",
        "noextract let ",
        "assume val ",
        "friend ",
        "open ",
        "module ",
        "instance ",
        "class ",
        "effect ",
        "layered_effect ",
        "sub_effect ",
        "new_effect ",
        "total_effect ",
    ];

    // Pattern to strip block comments: (?s) makes . match newlines, .*? is non-greedy
    // This correctly handles comments like (* star * here *) unlike [^*]*
    static ref BLOCK_COMMENT_PATTERN: Regex = Regex::new(r"(?s)\(\*.*?\*\)").unwrap();

    // Pattern to strip line comments: (?m) makes $ match end-of-line, not just end-of-string
    // This fixes the bug where only the last // comment was removed
    static ref LINE_COMMENT_PATTERN: Regex = Regex::new(r"(?m)//.*$").unwrap();
}

/// A parsed type definition from F* code.
#[derive(Debug, Clone)]
pub struct TypeDefinition {
    pub name: String,
    pub block: String,
    pub start_line: usize, // 0-indexed
    pub end_line: usize,   // 0-indexed, inclusive
    pub is_private: bool,
    pub and_types: Vec<String>,
}

/// Check if line is a section header comment like (* ==== *).
fn is_section_header(line: &str) -> bool {
    let stripped = line.trim();
    (stripped.starts_with("(** ==") || stripped.starts_with("(* =="))
        || (stripped.starts_with("(*") && stripped.contains("===="))
}

/// Find the end of a type definition block starting at start_index.
/// Returns the index of the last line of the type block (inclusive).
fn find_type_block_end(lines: &[&str], start_index: usize) -> usize {
    let mut j = start_index + 1;

    while j < lines.len() {
        let curr_line = lines[j];
        let curr_stripped = curr_line.trim();

        // Skip empty lines
        if curr_stripped.is_empty() {
            j += 1;
            continue;
        }

        // F* directives don't terminate type definitions
        if FST_DIRECTIVE_PATTERN.is_match(curr_stripped) {
            j += 1;
            continue;
        }

        // Attributes don't terminate type definitions
        if curr_stripped.starts_with("[@") {
            j += 1;
            continue;
        }

        // Must be at column 0 (not indented) to be a terminator
        if !curr_line.is_empty() && !curr_line.starts_with(' ') && !curr_line.starts_with('\t') {
            // Check for 'and' continuation of mutual recursion
            if AND_TYPE_PATTERN.is_match(curr_stripped) {
                j += 1;
                continue;
            }

            // Check for terminators
            for term in TERMINATORS.iter() {
                if curr_stripped.starts_with(term) {
                    // Found terminator, go back to skip trailing blank lines
                    let mut end_line = j - 1;
                    while end_line > start_index && lines[end_line].trim().is_empty() {
                        end_line -= 1;
                    }
                    return end_line;
                }
            }

            // New type definition (not 'and')
            if TYPE_START_PATTERN.is_match(curr_stripped) {
                let mut end_line = j - 1;
                while end_line > start_index && lines[end_line].trim().is_empty() {
                    end_line -= 1;
                }
                return end_line;
            }

            // Section headers terminate
            if is_section_header(curr_line) {
                let mut end_line = j - 1;
                while end_line > start_index && lines[end_line].trim().is_empty() {
                    end_line -= 1;
                }
                return end_line;
            }
        }

        j += 1;
    }

    // Reached end of file
    let mut end_line = j - 1;
    while end_line > start_index && lines[end_line].trim().is_empty() {
        end_line -= 1;
    }
    end_line
}

/// Extract type names from 'and' continuations in a mutual recursion block.
fn extract_and_types(block: &str) -> Vec<String> {
    let mut and_types = Vec::new();
    for line in block.lines() {
        let stripped = line.trim();
        if let Some(caps) = AND_TYPE_PATTERN.captures(stripped) {
            if let Some(m) = caps.get(1) {
                and_types.push(m.as_str().to_string());
            }
        }
    }
    and_types
}

/// Check if a type block contains a private type definition.
fn is_private_type(block: &str) -> bool {
    let first_line = block.lines().next().map(|l| l.trim()).unwrap_or("");
    PRIVATE_TYPE_PATTERN.is_match(first_line)
}

/// Find the start of attribute prefix lines before a type definition.
fn find_attribute_prefix_lines(lines: &[&str], type_start: usize) -> usize {
    let mut actual_start = type_start;

    // Look backwards from type_start
    let mut j = type_start;
    while j > 0 {
        j -= 1;
        let line = lines[j];
        let stripped = line.trim();

        // Empty lines break the attribute chain
        if stripped.is_empty() {
            break;
        }

        // Attribute annotations
        if stripped.starts_with("[@") || stripped.starts_with("[@@") {
            actual_start = j;
            continue;
        }

        // Otherwise, not part of the type definition
        break;
    }

    actual_start
}

/// Find all type definitions with their line ranges.
/// Returns HashMap of type_name -> TypeDefinition
pub fn find_type_definitions(content: &str) -> HashMap<String, TypeDefinition> {
    let lines: Vec<&str> = content.lines().collect();
    let mut types: HashMap<String, TypeDefinition> = HashMap::new();

    let mut i = 0;
    while i < lines.len() {
        let line = lines[i];
        let stripped = line.trim();

        if let Some(caps) = TYPE_START_PATTERN.captures(stripped) {
            // Skip if this appears to be inside a comment
            if stripped.starts_with("(*") && stripped.contains("type ") {
                i += 1;
                continue;
            }

            if let Some(m) = caps.get(1) {
                let type_name = m.as_str().to_string();

                // Find attribute prefix
                let actual_start = find_attribute_prefix_lines(&lines, i);

                // Find the end of the type definition block
                let end_line = find_type_block_end(&lines, i);

                let block: String = lines[actual_start..=end_line].join("\n");
                let is_private = is_private_type(&block);
                let and_types = extract_and_types(&block);

                // Add main type
                types.insert(
                    type_name.clone(),
                    TypeDefinition {
                        name: type_name,
                        block: block.clone(),
                        start_line: actual_start,
                        end_line,
                        is_private,
                        and_types: and_types.clone(),
                    },
                );

                // Also add 'and' types as separate entries
                // They share the same block range and privacy
                for and_type in &and_types {
                    types.insert(
                        and_type.clone(),
                        TypeDefinition {
                            name: and_type.clone(),
                            block: block.clone(),
                            start_line: actual_start,
                            end_line,
                            is_private,
                            and_types: and_types.clone(),
                        },
                    );
                }

                i = end_line + 1;
                continue;
            }
        }

        i += 1;
    }

    types
}

/// Result of fix validation.
#[derive(Debug, Clone)]
pub struct FixValidation {
    /// Whether the fix is safe to apply.
    pub is_safe: bool,
    /// Detailed reason if not safe, or confirmation if safe.
    pub reason: String,
    /// Preview of the content that will be removed.
    pub removal_preview: String,
    /// List of potential issues (warnings even if safe).
    pub warnings: Vec<String>,
}

impl FixValidation {
    fn safe(preview: String) -> Self {
        Self {
            is_safe: true,
            reason: "Definitions match exactly; safe to remove".to_string(),
            removal_preview: preview,
            warnings: vec![],
        }
    }

    fn safe_with_warnings(preview: String, warnings: Vec<String>) -> Self {
        Self {
            is_safe: true,
            reason: "Definitions match; safe to remove with warnings".to_string(),
            removal_preview: preview,
            warnings,
        }
    }

    fn unsafe_mismatch(fst_def: &str, fsti_def: &str) -> Self {
        Self {
            is_safe: false,
            reason: format!(
                "Type definitions differ:\n  .fst:  {}\n  .fsti: {}",
                fst_def.lines().next().unwrap_or(""),
                fsti_def.lines().next().unwrap_or("")
            ),
            removal_preview: String::new(),
            warnings: vec![],
        }
    }

    fn unsafe_reason(reason: String) -> Self {
        Self {
            is_safe: false,
            reason,
            removal_preview: String::new(),
            warnings: vec![],
        }
    }
}

/// Normalize a type definition block for comparison.
///
/// This function:
/// 1. Removes all comments (block and line)
/// 2. Normalizes whitespace (collapses multiple spaces/newlines)
/// 3. Trims leading/trailing whitespace
/// 4. Removes attribute annotations ([@...]) for semantic comparison
///
/// The goal is to compare the SEMANTIC content of two type definitions,
/// ignoring formatting differences and comments.
fn normalize_type_definition(block: &str) -> String {
    // Step 1: Remove block comments
    let without_block_comments = BLOCK_COMMENT_PATTERN.replace_all(block, " ");

    // Step 2: Remove line comments
    let without_comments = LINE_COMMENT_PATTERN.replace_all(&without_block_comments, "");

    // Step 3: Normalize whitespace - replace all whitespace sequences with single space
    let normalized: String = without_comments
        .split_whitespace()
        .collect::<Vec<_>>()
        .join(" ");

    // Step 4: Remove attribute annotations for semantic comparison
    // Attributes like [@...] or [@@...] don't affect the type's semantic meaning
    lazy_static! {
        static ref ATTR_PATTERN: Regex = Regex::new(r"\[@+[^\]]*\]").unwrap();
    }
    let without_attrs = ATTR_PATTERN.replace_all(&normalized, "").to_string();

    // Final cleanup
    without_attrs.split_whitespace().collect::<Vec<_>>().join(" ")
}

/// Compare two type definition blocks for semantic equivalence.
///
/// Returns true if the definitions are semantically identical
/// (same type structure, ignoring comments and whitespace).
pub fn definitions_match(fst_block: &str, fsti_block: &str) -> bool {
    let norm_fst = normalize_type_definition(fst_block);
    let norm_fsti = normalize_type_definition(fsti_block);
    norm_fst == norm_fsti
}

/// Extract the core type signature from a block (type name + parameters + body).
///
/// This is a more lenient comparison that checks if the structural parts match.
fn extract_type_signature(block: &str) -> Option<String> {
    let normalized = normalize_type_definition(block);

    // Find the type keyword and extract everything after it
    if let Some(idx) = normalized.find("type ") {
        Some(normalized[idx..].to_string())
    } else {
        None
    }
}

/// Check if two type definitions have matching signatures.
///
/// This is a more lenient check than `definitions_match` that allows
/// for minor differences in modifiers (like `inline_for_extraction`).
pub fn signatures_match(fst_block: &str, fsti_block: &str) -> bool {
    match (extract_type_signature(fst_block), extract_type_signature(fsti_block)) {
        (Some(fst_sig), Some(fsti_sig)) => fst_sig == fsti_sig,
        _ => false,
    }
}

/// Detect potential references to a type within a file.
///
/// Returns a list of line numbers where the type name appears outside
/// of its own definition block.
fn find_type_references(content: &str, type_name: &str, def_start: usize, def_end: usize) -> Vec<usize> {
    let mut references = Vec::new();

    // Build a word-boundary pattern for the type name
    let pattern = format!(r"\b{}\b", regex::escape(type_name));
    let re = Regex::new(&pattern).unwrap();

    for (line_idx, line) in content.lines().enumerate() {
        // Skip lines within the definition block
        if line_idx >= def_start && line_idx <= def_end {
            continue;
        }

        // Skip comment-only lines
        let trimmed = line.trim();
        if trimmed.starts_with("//") || trimmed.starts_with("(*") {
            continue;
        }

        // Check if type name appears in this line
        if re.is_match(line) {
            references.push(line_idx + 1); // 1-indexed
        }
    }

    references
}

/// Validate whether a fix is safe to apply.
///
/// This function performs comprehensive safety checks:
/// 1. Verifies that the type definitions in .fst and .fsti match exactly
/// 2. Checks for references to the type in the .fst file
/// 3. Validates that removal won't break the file structure
///
/// Returns a FixValidation with detailed information about safety.
pub fn validate_fix(
    fst_content: &str,
    _fsti_content: &str,
    type_name: &str,
    fst_typedef: &TypeDefinition,
    fsti_typedef: &TypeDefinition,
) -> FixValidation {
    // Safety check 1: Verify definitions match exactly
    if !definitions_match(&fst_typedef.block, &fsti_typedef.block) {
        // Try more lenient signature matching
        if !signatures_match(&fst_typedef.block, &fsti_typedef.block) {
            return FixValidation::unsafe_mismatch(&fst_typedef.block, &fsti_typedef.block);
        }
        // Signatures match but full definitions don't - warn but allow
        let warnings = vec![
            "Definitions have minor differences (comments/attributes)".to_string(),
        ];
        let preview = create_removal_preview(&fst_typedef.block, fst_typedef.start_line);
        return FixValidation::safe_with_warnings(preview, warnings);
    }

    // Safety check 2: Check for references outside the definition
    let references = find_type_references(
        fst_content,
        type_name,
        fst_typedef.start_line,
        fst_typedef.end_line,
    );

    let preview = create_removal_preview(&fst_typedef.block, fst_typedef.start_line);

    if !references.is_empty() {
        // This is actually OK - the type will still be available from .fsti
        // But we warn the user about it
        let warnings = vec![format!(
            "Type `{}` is referenced at lines: {:?} (will use .fsti definition)",
            type_name, references
        )];
        return FixValidation::safe_with_warnings(preview, warnings);
    }

    FixValidation::safe(preview)
}

/// Create a preview of what will be removed.
fn create_removal_preview(block: &str, start_line: usize) -> String {
    let lines: Vec<&str> = block.lines().collect();
    let preview_lines = if lines.len() > 5 {
        format!(
            "Lines {}-{} ({} lines):\n  {}\n  {}\n  ...\n  {}",
            start_line + 1,
            start_line + lines.len(),
            lines.len(),
            lines[0],
            lines[1],
            lines[lines.len() - 1]
        )
    } else {
        format!(
            "Lines {}-{}:\n{}",
            start_line + 1,
            start_line + lines.len(),
            block
                .lines()
                .map(|l| format!("  {}", l))
                .collect::<Vec<_>>()
                .join("\n")
        )
    };
    preview_lines
}

/// Dry-run mode result for a single file pair.
#[derive(Debug, Clone)]
pub struct DryRunResult {
    /// File path for the .fst file.
    pub fst_file: PathBuf,
    /// File path for the .fsti file.
    pub fsti_file: PathBuf,
    /// List of fixes that would be applied, with validation info.
    pub proposed_fixes: Vec<(String, FixValidation)>,
    /// Total number of safe fixes.
    pub safe_count: usize,
    /// Total number of unsafe fixes (will not be applied).
    pub unsafe_count: usize,
}

/// Perform a dry-run of the duplicate type removal.
///
/// This function analyzes a .fst/.fsti pair and returns detailed information
/// about what fixes would be applied, including safety validation for each.
pub fn dry_run_check(
    fst_file: &PathBuf,
    fst_content: &str,
    fsti_file: &PathBuf,
    fsti_content: &str,
) -> DryRunResult {
    let fst_types = find_type_definitions(fst_content);
    let fsti_types = find_type_definitions(fsti_content);

    let mut proposed_fixes = Vec::new();
    let mut safe_count = 0;
    let mut unsafe_count = 0;

    // Find concrete types in .fsti
    let fsti_concrete: HashMap<&String, &TypeDefinition> = fsti_types
        .iter()
        .filter(|(_, typedef)| is_concrete_definition(&typedef.block))
        .collect();

    // Track processed ranges (for mutual recursion)
    let mut processed_ranges: HashSet<(usize, usize)> = HashSet::new();

    for (type_name, fst_typedef) in &fst_types {
        // Skip private types
        if fst_typedef.is_private {
            continue;
        }

        // Skip if already processed this range
        let range_key = (fst_typedef.start_line, fst_typedef.end_line);
        if processed_ranges.contains(&range_key) {
            continue;
        }

        if let Some(fsti_typedef) = fsti_concrete.get(type_name) {
            processed_ranges.insert(range_key);

            let validation = validate_fix(
                fst_content,
                fsti_content,
                type_name,
                fst_typedef,
                fsti_typedef,
            );

            if validation.is_safe {
                safe_count += 1;
            } else {
                unsafe_count += 1;
            }

            proposed_fixes.push((type_name.clone(), validation));
        }
    }

    DryRunResult {
        fst_file: fst_file.clone(),
        fsti_file: fsti_file.clone(),
        proposed_fixes,
        safe_count,
        unsafe_count,
    }
}

/// Check if a type block is a concrete definition (has bare `=` at depth 0).
///
/// Type declarations like `type foo` or `type foo : Type0` without `=`
/// are abstract -- they must be implemented in .fst.
///
/// The `=` that defines a type body always appears at bracket depth 0
/// (not inside parentheses, braces, or square brackets). An `=` inside
/// a refinement like `type t (x: int{x = 0}) : Type` is at depth > 0
/// and does NOT make the type concrete.
///
/// Additionally, `==`, `>=`, `<=`, `!=`, and `=>` are operators, not
/// type body definitions. Only a bare `=` counts.
fn is_concrete_definition(block: &str) -> bool {
    // Remove comments first to avoid matching = inside comments.
    let cleaned = BLOCK_COMMENT_PATTERN.replace_all(block, "");
    let cleaned = LINE_COMMENT_PATTERN.replace_all(&cleaned, "");

    let chars: Vec<char> = cleaned.chars().collect();
    let len = chars.len();

    // Track bracket depth: (, {, [ increase depth; ), }, ] decrease it.
    // Only a bare '=' at depth 0 counts as a type body definition.
    let mut depth: i32 = 0;
    let mut in_string = false;
    let mut i = 0;

    while i < len {
        let ch = chars[i];

        // Simple string literal tracking (F* uses double quotes)
        if ch == '"' && (i == 0 || chars[i - 1] != '\\') {
            in_string = !in_string;
            i += 1;
            continue;
        }
        if in_string {
            i += 1;
            continue;
        }

        match ch {
            '(' | '{' | '[' => depth += 1,
            ')' | '}' | ']' => {
                if depth > 0 {
                    depth -= 1;
                }
            }
            '=' if depth == 0 => {
                // Reject compound operators: ==, >=, <=, !=, =>
                let prev = if i > 0 { chars[i - 1] } else { ' ' };
                let next = if i + 1 < len { chars[i + 1] } else { ' ' };

                let is_compound = prev == '!' || prev == '<' || prev == '>'
                    || prev == '=' || next == '=' || next == '>';

                if !is_compound {
                    return true;
                }
            }
            _ => {}
        }
        i += 1;
    }

    false
}

/// FST001: Duplicate type definitions in .fst/.fsti pairs.
pub struct DuplicateTypesRule;

impl DuplicateTypesRule {
    pub fn new() -> Self {
        Self
    }
}

impl Default for DuplicateTypesRule {
    fn default() -> Self {
        Self::new()
    }
}

impl Rule for DuplicateTypesRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST001
    }

    fn check(&self, _file: &PathBuf, _content: &str) -> Vec<Diagnostic> {
        // This rule requires pair checking
        vec![]
    }

    fn requires_pair(&self) -> bool {
        true
    }

    /// Check for duplicate type definitions between .fst and .fsti files.
    ///
    /// Returns diagnostics with fixes to remove duplicate types from the .fst file.
    ///
    /// **SAFETY**: This function validates that type definitions match EXACTLY
    /// before offering an autofix. If definitions differ, no fix is offered
    /// (only a warning diagnostic).
    ///
    /// **Note**: After applying the generated fixes, the resulting content may have
    /// multiple consecutive blank lines. Use [`cleanup_consecutive_blanks`] as a
    /// post-processing step to normalize whitespace, or run a code formatter.
    fn check_pair(
        &self,
        fst_file: &PathBuf,
        fst_content: &str,
        _fsti_file: &PathBuf,
        fsti_content: &str,
    ) -> Vec<Diagnostic> {
        let fst_types = find_type_definitions(fst_content);
        let fsti_types = find_type_definitions(fsti_content);

        let mut diagnostics = Vec::new();

        // Find concrete types in .fsti (those with = sign)
        let fsti_concrete: HashMap<&String, &TypeDefinition> = fsti_types
            .iter()
            .filter(|(_, typedef)| is_concrete_definition(&typedef.block))
            .collect();

        // Track which ranges we've already marked for removal
        // (multiple types in mutual recursion share the same range)
        let mut removed_ranges: HashSet<(usize, usize)> = HashSet::new();

        for (type_name, fst_typedef) in &fst_types {
            // Skip private types - they are implementation details
            if fst_typedef.is_private {
                continue;
            }

            if let Some(fsti_typedef) = fsti_concrete.get(type_name) {
                let range_key = (fst_typedef.start_line, fst_typedef.end_line);
                if !removed_ranges.contains(&range_key) {
                    removed_ranges.insert(range_key);

                    // CRITICAL SAFETY: Validate the fix before offering it
                    let validation = validate_fix(
                        fst_content,
                        fsti_content,
                        type_name,
                        fst_typedef,
                        fsti_typedef,
                    );

                    // Build the diagnostic message
                    let mut message = format!(
                        "Type `{}` is defined in both .fst and .fsti.",
                        type_name
                    );

                    // Determine if we can offer a fix
                    let fix = if validation.is_safe {
                        // Add preview info to the message
                        if !validation.warnings.is_empty() {
                            message.push_str("\n\nWarnings:");
                            for warning in &validation.warnings {
                                message.push_str(&format!("\n  - {}", warning));
                            }
                        }
                        message.push_str("\n\nSafe to remove the duplicate from .fst.");

                        // Create fix with detailed message including preview
                        // Safety level depends on whether there are warnings:
                        // - No warnings + exact match = Safe (auto-apply)
                        // - Warnings present = Caution (show warning when applying)
                        let edits = vec![Edit {
                            file: fst_file.clone(),
                            // Convert 0-indexed to 1-indexed for Range
                            range: Range::new(
                                fst_typedef.start_line + 1,
                                1,
                                fst_typedef.end_line + 2, // +2 because end_line is inclusive and we want next line
                                1,
                            ),
                            new_text: String::new(),
                        }];

                        let fix = if validation.warnings.is_empty() {
                            // Definitions match exactly - safe to auto-apply
                            Fix::safe(
                                format!(
                                    "Remove duplicate type `{}` (definitions match exactly)\n\nPreview:\n{}",
                                    type_name, validation.removal_preview
                                ),
                                edits,
                            )
                            .with_reversible(false)  // Deletion is not easily reversible
                        } else {
                            // Definitions match with minor differences - caution
                            Fix::caution(
                                format!(
                                    "Remove duplicate type `{}` (definitions match with minor differences)\n\nPreview:\n{}",
                                    type_name, validation.removal_preview
                                ),
                                edits,
                            )
                            .with_reversible(false)
                            .with_requires_review(true)
                        };

                        Some(fix)
                    } else {
                        // Definitions don't match - DO NOT offer autofix
                        message.push_str(&format!(
                            "\n\nNO AUTOFIX: {}\n\nManual review required.",
                            validation.reason
                        ));
                        None
                    };

                    diagnostics.push(Diagnostic {
                        rule: RuleCode::FST001,
                        severity: DiagnosticSeverity::Warning,
                        file: fst_file.clone(),
                        range: Range::new(
                            fst_typedef.start_line + 1,
                            1,
                            fst_typedef.end_line + 1,
                            1,
                        ),
                        message,
                        fix,
                    });
                }
            }
        }

        diagnostics
    }
}

/// Clean up multiple consecutive blank lines in content, keeping at most one.
///
/// This function should be called after applying fixes that remove type blocks,
/// as the removal may leave behind multiple consecutive blank lines.
///
/// # Example
/// ```ignore
/// use fstar_lsp::lint::duplicate_types::cleanup_consecutive_blanks;
///
/// let content = "line1\n\n\n\nline2";
/// let cleaned = cleanup_consecutive_blanks(content);
/// assert_eq!(cleaned, "line1\n\nline2");
/// ```
pub fn cleanup_consecutive_blanks(content: &str) -> String {
    let mut result = Vec::new();
    let mut prev_blank = false;

    for line in content.lines() {
        let is_blank = line.trim().is_empty();
        if is_blank && prev_blank {
            // Skip consecutive blank line
            continue;
        }
        result.push(line);
        prev_blank = is_blank;
    }

    // Preserve trailing newline if original had one
    let mut output = result.join("\n");
    if content.ends_with('\n') {
        output.push('\n');
    }

    output
}

/// Find pairs of .fst and .fsti files.
pub fn find_fst_fsti_pairs(files: &[PathBuf]) -> Vec<(PathBuf, PathBuf)> {
    let mut pairs = Vec::new();
    let mut fst_files: HashMap<String, PathBuf> = HashMap::new();

    // Collect all .fst files by their base name
    for file in files {
        if let Some(ext) = file.extension() {
            if ext == "fst" {
                if let Some(stem) = file.file_stem() {
                    fst_files.insert(stem.to_string_lossy().to_string(), file.clone());
                }
            }
        }
    }

    // Find matching .fsti files
    for file in files {
        if let Some(ext) = file.extension() {
            if ext == "fsti" {
                if let Some(stem) = file.file_stem() {
                    let stem_str = stem.to_string_lossy().to_string();
                    let fst_path = file.with_extension("fst");
                    if let Some(fst) = fst_files.get(&stem_str) {
                        pairs.push((fst.clone(), file.clone()));
                    } else if fst_path.exists() {
                        pairs.push((fst_path, file.clone()));
                    }
                }
            }
        }
    }

    pairs
}

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

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

type mytype = int

let x = 1
"#;
        let types = find_type_definitions(content);
        assert!(types.contains_key("mytype"));
    }

    #[test]
    fn test_find_noeq_type() {
        let content = r#"
noeq type buffer (a: Type) = {
    content: seq a;
    length: nat
}
"#;
        let types = find_type_definitions(content);
        assert!(types.contains_key("buffer"));
    }

    #[test]
    fn test_find_mutual_recursion() {
        let content = r#"
type expr =
  | Var of string
  | App of expr * expr

and pattern =
  | PVar of string
  | PWild
"#;
        let types = find_type_definitions(content);
        assert!(types.contains_key("expr"));
        assert!(types.contains_key("pattern"));
        // Both should share the same block
        assert_eq!(types["expr"].start_line, types["pattern"].start_line);
    }

    #[test]
    fn test_private_type_detection() {
        let content = r#"
private type internal_state = {
    counter: nat
}
"#;
        let types = find_type_definitions(content);
        assert!(types.contains_key("internal_state"));
        assert!(types["internal_state"].is_private);
    }

    #[test]
    fn test_concrete_definition() {
        assert!(is_concrete_definition("type foo = int"));
        assert!(is_concrete_definition("noeq type bar = { x: int }"));
        assert!(!is_concrete_definition("type abstract_t"));
        assert!(!is_concrete_definition("type constrained : Type0"));
    }

    #[test]
    fn test_concrete_definition_with_comments() {
        // BUG FIX: Line comments with = should not be considered concrete
        assert!(!is_concrete_definition(
            "// Comment with = sign\n// Another comment = here\ntype abstract_t"
        ));

        // BUG FIX: Block comments with stars inside should be stripped correctly
        assert!(!is_concrete_definition(
            "(* Comment * with star and = inside *)\ntype abstract_t"
        ));

        // Still correctly identifies concrete types
        assert!(is_concrete_definition(
            "// Comment with = sign\ntype foo = int"
        ));
        assert!(is_concrete_definition("(* comment *) type bar = nat"));
    }

    #[test]
    fn test_cleanup_consecutive_blanks() {
        // Multiple consecutive blank lines should be reduced to one
        assert_eq!(
            cleanup_consecutive_blanks("line1\n\n\n\nline2"),
            "line1\n\nline2"
        );

        // Single blank line should be preserved
        assert_eq!(
            cleanup_consecutive_blanks("line1\n\nline2"),
            "line1\n\nline2"
        );

        // No blank lines should remain unchanged
        assert_eq!(cleanup_consecutive_blanks("line1\nline2"), "line1\nline2");

        // Trailing newline should be preserved
        assert_eq!(
            cleanup_consecutive_blanks("line1\n\n\nline2\n"),
            "line1\n\nline2\n"
        );

        // Empty content
        assert_eq!(cleanup_consecutive_blanks(""), "");

        // Only blank lines
        assert_eq!(cleanup_consecutive_blanks("\n\n\n"), "\n");

        // Mixed whitespace lines (tabs and spaces count as blank)
        assert_eq!(
            cleanup_consecutive_blanks("line1\n  \n\t\n\nline2"),
            "line1\n  \nline2"
        );
    }

    #[test]
    fn test_detect_duplicate() {
        let fst_content = r#"
module Test

type mytype = int

let foo x = x
"#;
        let fsti_content = r#"
module Test

type mytype = int

val foo: int -> int
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("Test.fst"),
            fst_content,
            &PathBuf::from("Test.fsti"),
            fsti_content,
        );

        assert!(!diagnostics.is_empty());
        assert!(diagnostics[0].message.contains("mytype"));
    }

    // ---- FALSE POSITIVE tests: abstract .fsti + concrete .fst is VALID ----

    #[test]
    fn test_no_false_positive_abstract_fsti_concrete_fst() {
        // Abstract type in .fsti, concrete in .fst => NOT a duplicate
        let fsti_content = "module Test\n\ntype t\n\nval foo: t -> int\n";
        let fst_content = "module Test\n\ntype t = int\n\nlet foo x = x\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("Test.fst"),
            fst_content,
            &PathBuf::from("Test.fsti"),
            fsti_content,
        );

        assert!(diagnostics.is_empty(), "Abstract .fsti + concrete .fst should NOT be flagged");
    }

    #[test]
    fn test_no_false_positive_abstract_with_kind() {
        // type t : Type0 in .fsti (abstract with kind annotation)
        let fsti_content = "module Test\n\ntype t : Type0\n\nval foo: t -> int\n";
        let fst_content = "module Test\n\ntype t = nat\n\nlet foo x = x\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("Test.fst"),
            fst_content,
            &PathBuf::from("Test.fsti"),
            fsti_content,
        );

        assert!(diagnostics.is_empty(), "Abstract type with kind annotation should NOT be flagged");
    }

    #[test]
    fn test_no_false_positive_abstract_eqtype() {
        // type t : eqtype in .fsti
        let fsti_content = "module Test\n\ntype t : eqtype\n";
        let fst_content = "module Test\n\ntype t = | A | B | C\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("Test.fst"),
            fst_content,
            &PathBuf::from("Test.fsti"),
            fsti_content,
        );

        assert!(diagnostics.is_empty(), "Abstract eqtype should NOT be flagged");
    }

    // ---- is_concrete_definition: depth-aware = detection ----

    #[test]
    fn test_concrete_equals_inside_refinement_not_concrete() {
        // type t (x: int{x = 0}) : Type  -- the = is inside braces, NOT a type body
        assert!(!is_concrete_definition(
            "type t (x: int{x = 0}) : Type"
        ));
    }

    #[test]
    fn test_concrete_equals_inside_parens_not_concrete() {
        // type t (x: int) (y: (z:int{z = x})) : Type
        assert!(!is_concrete_definition(
            "type t (x: int) (y: (z:int{z = x})) : Type"
        ));
    }

    #[test]
    fn test_concrete_multiline_abstract_with_refinement() {
        // Multi-line abstract type with = inside parameter refinement
        let block = "type my_type\n  (x: nat{x = 0})\n  : Type";
        assert!(!is_concrete_definition(block),
            "Abstract type with = inside refinement should NOT be concrete");
    }

    #[test]
    fn test_concrete_multiline_concrete_with_refinement() {
        // Multi-line concrete type: the = for the body is at depth 0
        let block = "type my_type\n  (x: nat{x = 0})\n  : Type =\n  | Mk : my_type";
        assert!(is_concrete_definition(block),
            "Concrete type with = at depth 0 should be detected");
    }

    #[test]
    fn test_concrete_double_equals_not_concrete() {
        // == is propositional equality, not a type body definition
        assert!(!is_concrete_definition(
            "type t (x: nat) : (y:Type{x == 0})"
        ));
    }

    #[test]
    fn test_concrete_operators_not_concrete() {
        // >=, <=, != should not be confused with =
        assert!(!is_concrete_definition("type t (x: nat{x >= 0}) : Type"));
        assert!(!is_concrete_definition("type t (x: nat{x <= 10}) : Type"));
        assert!(!is_concrete_definition("type t (x: nat{x != 0}) : Type"));
    }

    #[test]
    fn test_concrete_arrow_equals_not_concrete() {
        // => is match/implication arrow, not type body
        assert!(!is_concrete_definition("type t (x: nat{x > 0 ==> True}) : Type"));
    }

    #[test]
    fn test_concrete_adt_is_concrete() {
        // Standard ADT with = at depth 0
        assert!(is_concrete_definition("type color =\n  | Red\n  | Green\n  | Blue"));
    }

    #[test]
    fn test_concrete_record_is_concrete() {
        assert!(is_concrete_definition("noeq type rec = {\n  x: int;\n  y: int\n}"));
    }

    #[test]
    fn test_concrete_type_alias_is_concrete() {
        assert!(is_concrete_definition("type my_nat = nat"));
    }

    // ---- unopteq modifier support ----

    #[test]
    fn test_find_unopteq_type() {
        let content = "module Test\n\nunopteq type dtuple4\n  (a: Type) (b: a -> Type)\n  = | Mk : a -> dtuple4 a b\n";
        let types = find_type_definitions(content);
        assert!(types.contains_key("dtuple4"), "unopteq types should be detected");
    }

    #[test]
    fn test_detect_duplicate_unopteq() {
        let fsti_content = "module T\n\nunopteq type t = | A | B\n";
        let fst_content = "module T\n\nunopteq type t = | A | B\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert!(!diagnostics.is_empty(), "Duplicate unopteq types should be flagged");
    }

    // ---- TRUE DUPLICATE detection (should still work) ----

    #[test]
    fn test_true_duplicate_noeq_record() {
        let fsti_content = "module T\n\nnoeq type state = {\n  counter: nat;\n  data: list int\n}\n";
        let fst_content = "module T\n\nnoeq type state = {\n  counter: nat;\n  data: list int\n}\n\nlet init = { counter = 0; data = [] }\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert!(!diagnostics.is_empty(), "Identical noeq record in both files should be flagged");
    }

    #[test]
    fn test_true_duplicate_type_alias() {
        let fsti_content = "module T\n\ntype byte = UInt8.t\n";
        let fst_content = "module T\n\ntype byte = UInt8.t\n\nlet zero : byte = 0uy\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert!(!diagnostics.is_empty(), "Identical type alias in both files should be flagged");
    }

    // ---- Private types should NOT be flagged ----

    #[test]
    fn test_private_type_not_flagged() {
        let fsti_content = "module T\n\ntype t = int\n";
        let fst_content = "module T\n\ntype t = int\n\nprivate type internal = nat\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        // Should flag 't' but not 'internal'
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("t"));
    }

    // ---- Real-world pattern: multiline parameterized concrete type ----

    #[test]
    fn test_multiline_parameterized_concrete() {
        // Pattern from LowParse.Repr.fsti: multiline type with = on later line
        let block = "noeq inline_for_extraction\ntype field_accessor (#k1 #k2:strong_parser_kind)\n                    (#t1 #t2:Type)\n                    (p1 : LP.parser k1 t1)\n                    (p2 : LP.parser k2 t2) =\n  | FieldAccessor :\n     (acc:LP.accessor g) ->\n     field_accessor p1 p2";
        assert!(is_concrete_definition(block),
            "Multiline concrete type with = on later line should be detected");
    }

    // ---- Edge case: = inside string literal ----

    #[test]
    fn test_equals_in_string_not_concrete() {
        // Hypothetical: = inside a string in a type annotation
        assert!(!is_concrete_definition(
            "type t (x: string{x = \"hello = world\"}) : Type"
        ));
    }

    // ===========================================================================
    // SAFETY VALIDATION TESTS
    // ===========================================================================

    #[test]
    fn test_definitions_match_identical() {
        let fst_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";
        let fsti_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";

        assert!(definitions_match(fst_block, fsti_block));
    }

    #[test]
    fn test_definitions_match_with_whitespace_diff() {
        let fst_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";
        let fsti_block = "noeq type labeled_type = { base_type : brrr_type; label : sec_level; }";

        assert!(definitions_match(fst_block, fsti_block));
    }

    #[test]
    fn test_definitions_match_with_comment_diff() {
        let fst_block = "(** Labeled type *)\nnoeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";
        let fsti_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";

        assert!(definitions_match(fst_block, fsti_block));
    }

    #[test]
    fn test_definitions_dont_match_different_fields() {
        let fst_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n  extra     : nat;\n}";
        let fsti_block = "noeq type labeled_type = {\n  base_type : brrr_type;\n  label     : sec_level;\n}";

        assert!(!definitions_match(fst_block, fsti_block));
    }

    #[test]
    fn test_definitions_dont_match_different_types() {
        let fst_block = "type sec_level = | Public | Secret";
        let fsti_block = "type sec_level = | Public | Private | Secret";

        assert!(!definitions_match(fst_block, fsti_block));
    }

    #[test]
    fn test_no_autofix_when_definitions_differ() {
        // .fsti has a different definition than .fst
        let fsti_content = "module T\n\ntype color = | Red | Green | Blue\n";
        let fst_content = "module T\n\ntype color = | Red | Green\n"; // Missing Blue!

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        // Should produce a diagnostic but WITHOUT a fix
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_none(), "Should NOT offer autofix when definitions differ");
        assert!(diagnostics[0].message.contains("NO AUTOFIX"));
    }

    #[test]
    fn test_autofix_offered_when_definitions_match() {
        let fsti_content = "module T\n\ntype sec_level =\n  | Public\n  | Secret\n";
        let fst_content = "module T\n\ntype sec_level =\n  | Public\n  | Secret\n\nlet x = 1\n";

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some(), "Should offer autofix when definitions match");
        assert!(diagnostics[0].message.contains("Safe to remove"));
    }

    // ===========================================================================
    // REAL-WORLD PATTERNS FROM BrrrInformationFlow
    // ===========================================================================

    #[test]
    fn test_brrr_sec_level_type() {
        // Pattern from BrrrInformationFlow.fst/fsti
        let fsti_content = r#"module BrrrInformationFlow

type sec_level =
  | Public       : sec_level
  | Confidential : sec_level
  | Secret       : sec_level
  | TopSecret    : sec_level

val sec_leq (l1 l2: sec_level) : bool
"#;
        let fst_content = r#"module BrrrInformationFlow

type sec_level =
  | Public       : sec_level
  | Confidential : sec_level
  | Secret       : sec_level
  | TopSecret    : sec_level

let sec_leq (l1 l2: sec_level) : bool =
  match l1, l2 with
  | Public, _ -> true
  | _, TopSecret -> true
  | Secret, Secret -> true
  | Confidential, Confidential -> true
  | _, _ -> false
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("BrrrInformationFlow.fst"),
            fst_content,
            &PathBuf::from("BrrrInformationFlow.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some(), "Identical sec_level should have autofix");
    }

    #[test]
    fn test_brrr_labeled_type_noeq() {
        // Pattern from BrrrInformationFlow - noeq record type
        let fsti_content = r#"module BrrrInformationFlow

noeq type labeled_type = {
  base_type : brrr_type;
  label     : sec_level;
}

val label_type (t: brrr_type) (l: sec_level) : labeled_type
"#;
        let fst_content = r#"module BrrrInformationFlow

noeq type labeled_type = {
  base_type : brrr_type;
  label     : sec_level;
}

let label_type (t: brrr_type) (l: sec_level) : labeled_type =
  { base_type = t; label = l }
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("BrrrInformationFlow.fst"),
            fst_content,
            &PathBuf::from("BrrrInformationFlow.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some(), "Identical noeq record should have autofix");
    }

    #[test]
    fn test_brrr_sec_check_result_adt() {
        // Pattern from BrrrInformationFlow - ADT with multiple constructors
        let fsti_content = r#"module BrrrInformationFlow

noeq type sec_check_result =
  | SecOk  : labeled_type -> sec_ctx -> sec_check_result
  | SecErr : string -> sec_check_result

val check_flow (ctx: sec_ctx) (e: expr) : sec_check_result
"#;
        let fst_content = r#"module BrrrInformationFlow

noeq type sec_check_result =
  | SecOk  : labeled_type -> sec_ctx -> sec_check_result
  | SecErr : string -> sec_check_result

let check_flow (ctx: sec_ctx) (e: expr) : sec_check_result =
  SecOk (public_type TUnit) ctx
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("BrrrInformationFlow.fst"),
            fst_content,
            &PathBuf::from("BrrrInformationFlow.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some(), "Identical ADT should have autofix");
    }

    #[test]
    fn test_brrr_security_label_combined() {
        // Pattern from BrrrInformationFlow - combined confidentiality/integrity
        let fsti_content = r#"module BrrrInformationFlow

noeq type security_label = {
  confidentiality : sec_level;
  integrity       : integrity_level_full;
}

val security_label_leq (l1 l2: security_label) : bool
"#;
        let fst_content = r#"module BrrrInformationFlow

noeq type security_label = {
  confidentiality : sec_level;
  integrity       : integrity_level_full;
}

let security_label_leq (l1 l2: security_label) : bool =
  sec_leq l1.confidentiality l2.confidentiality &&
  integrity_leq_full l1.integrity l2.integrity
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("BrrrInformationFlow.fst"),
            fst_content,
            &PathBuf::from("BrrrInformationFlow.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_some());
    }

    #[test]
    fn test_no_autofix_modified_adt_variant() {
        // Modified ADT - should NOT offer autofix
        let fsti_content = r#"module T

type termination_behavior =
  | MustTerminate    : termination_behavior
  | MayDiverge       : termination_behavior
  | MustDiverge      : termination_behavior
"#;
        let fst_content = r#"module T

type termination_behavior =
  | MustTerminate    : termination_behavior
  | MayDiverge       : termination_behavior
  | Unknown          : termination_behavior
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_none(), "Different ADT variants should NOT have autofix");
    }

    #[test]
    fn test_no_autofix_modified_record_field() {
        // Modified record field type - should NOT offer autofix
        let fsti_content = r#"module T

noeq type declass_policy = {
  declass_name : string;
  allowed_patterns : list string;
  max_declass : option nat;
}
"#;
        let fst_content = r#"module T

noeq type declass_policy = {
  declass_name : string;
  allowed_patterns : list string;
  max_declass : nat;
}
"#;

        let rule = DuplicateTypesRule::new();
        let diagnostics = rule.check_pair(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].fix.is_none(), "Different field types should NOT have autofix");
    }

    // ===========================================================================
    // DRY-RUN TESTS
    // ===========================================================================

    #[test]
    fn test_dry_run_basic() {
        let fsti_content = "module T\n\ntype t = int\n";
        let fst_content = "module T\n\ntype t = int\n\nlet x = 1\n";

        let result = dry_run_check(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert_eq!(result.safe_count, 1);
        assert_eq!(result.unsafe_count, 0);
        assert_eq!(result.proposed_fixes.len(), 1);
        assert!(result.proposed_fixes[0].1.is_safe);
    }

    #[test]
    fn test_dry_run_mixed_safe_unsafe() {
        let fsti_content = "module T\n\ntype a = int\n\ntype b = | X | Y | Z\n";
        let fst_content = "module T\n\ntype a = int\n\ntype b = | X | Y\n"; // Missing Z!

        let result = dry_run_check(
            &PathBuf::from("T.fst"),
            fst_content,
            &PathBuf::from("T.fsti"),
            fsti_content,
        );

        assert_eq!(result.safe_count, 1);  // 'a' is safe
        assert_eq!(result.unsafe_count, 1); // 'b' is unsafe
    }

    // ===========================================================================
    // NORMALIZE DEFINITION TESTS
    // ===========================================================================

    #[test]
    fn test_normalize_removes_comments() {
        let block = "(* This is a comment *)\ntype t = int";
        let normalized = normalize_type_definition(block);
        assert!(!normalized.contains("comment"));
        assert!(normalized.contains("type t = int"));
    }

    #[test]
    fn test_normalize_removes_line_comments() {
        let block = "// Line comment\ntype t = int // trailing";
        let normalized = normalize_type_definition(block);
        assert!(!normalized.contains("comment"));
        assert!(!normalized.contains("trailing"));
    }

    #[test]
    fn test_normalize_removes_attributes() {
        let block = "[@attribute] [@@another]\ntype t = int";
        let normalized = normalize_type_definition(block);
        assert!(!normalized.contains("attribute"));
        assert!(normalized.contains("type t = int"));
    }

    #[test]
    fn test_normalize_whitespace_collapse() {
        let block = "type   t    =    int";
        let normalized = normalize_type_definition(block);
        assert_eq!(normalized, "type t = int");
    }

    // ===========================================================================
    // VALIDATE_FIX TESTS
    // ===========================================================================

    #[test]
    fn test_validate_fix_safe() {
        let fst_content = "module T\n\ntype t = int\n\nlet x = 1\n";
        let fsti_content = "module T\n\ntype t = int\n";

        let fst_types = find_type_definitions(fst_content);
        let fsti_types = find_type_definitions(fsti_content);

        let fst_typedef = fst_types.get("t").unwrap();
        let fsti_typedef = fsti_types.get("t").unwrap();

        let validation = validate_fix(fst_content, fsti_content, "t", fst_typedef, fsti_typedef);

        assert!(validation.is_safe);
        assert!(!validation.removal_preview.is_empty());
    }

    #[test]
    fn test_validate_fix_unsafe_mismatch() {
        let fst_content = "module T\n\ntype t = nat\n";
        let fsti_content = "module T\n\ntype t = int\n";

        let fst_types = find_type_definitions(fst_content);
        let fsti_types = find_type_definitions(fsti_content);

        let fst_typedef = fst_types.get("t").unwrap();
        let fsti_typedef = fsti_types.get("t").unwrap();

        let validation = validate_fix(fst_content, fsti_content, "t", fst_typedef, fsti_typedef);

        assert!(!validation.is_safe);
        assert!(validation.reason.contains("differ"));
    }

    #[test]
    fn test_validate_fix_with_references() {
        let fst_content = "module T\n\ntype t = int\n\nlet x : t = 0\nlet y : t = 1\n";
        let fsti_content = "module T\n\ntype t = int\n";

        let fst_types = find_type_definitions(fst_content);
        let fsti_types = find_type_definitions(fsti_content);

        let fst_typedef = fst_types.get("t").unwrap();
        let fsti_typedef = fsti_types.get("t").unwrap();

        let validation = validate_fix(fst_content, fsti_content, "t", fst_typedef, fsti_typedef);

        // Should still be safe (type available from .fsti) but with warnings
        assert!(validation.is_safe);
        assert!(!validation.warnings.is_empty(), "Should warn about references");
    }
}