brrr-lint 0.1.0

//! FST008: Import optimization.
//!
//! Detects import patterns that can be improved for better verification performance
//! and code clarity. This rule focuses on optimizing module imports in F* source files.
//!
//! # Detection Categories
//!
//! - **FST008-A**: Broad import when selective would suffice (`open M` when only 1-3 names used)
//! - **FST008-B**: Unused import (redundant with FST004 but provides additional context)
//! - **FST008-C**: Qualified names preferred over open for infrequently used modules
//! - **FST008-D**: Circular import detection (module A opens B which opens A)
//! - **FST008-E**: Unnecessary transitive import (opening module that re-exports another)
//! - **FST008-H**: Heavy module import warning (Tactics, Reflection)
//!
//! Note: FST008-F (import ordering) was removed. The "Core > Pure > Effect > Project"
//! categorization produced false positives because it did not match actual F* conventions.
//! Many FStar.* modules were miscategorized, and no community standard for import ordering
//! exists in the F* ecosystem.
//!
//! # Heavy Modules
//!
//! Some F* modules are known to significantly slow down verification when imported:
//! - `FStar.Tactics.V2` and `FStar.Tactics` - Full tactics machinery
//! - `FStar.Reflection.V2` and `FStar.Reflection` - Reflection capabilities
//!
//! These should be imported selectively or avoided when not necessary.

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

use super::rules::{Diagnostic, DiagnosticSeverity, Edit, Fix, Range, Rule, RuleCode};
use super::unused_opens::{analyze_opens, OpenStatement};

lazy_static! {
    /// Pattern for simple open statements: `open Module.Path`
    static ref OPEN_PATTERN: Regex = Regex::new(r"^open\s+([A-Z][\w.]*)").unwrap();

    /// Pattern for include statements: `include Module.Path`
    static ref INCLUDE_PATTERN: Regex = Regex::new(r"^include\s+([A-Z][\w.]*)").unwrap();

    /// Pattern for qualified identifier usage: `Module.identifier`
    static ref QUALIFIED_USE_PATTERN: Regex = Regex::new(r"\b([A-Z][\w.]*)\.([\w']+)").unwrap();

    /// Heavy modules that significantly slow verification when imported.
    /// These should be imported selectively or with caution.
    static ref HEAVY_MODULES: HashSet<&'static str> = {
        let mut set = HashSet::new();
        set.insert("FStar.Tactics.V2");
        set.insert("FStar.Tactics");
        set.insert("FStar.Reflection.V2");
        set.insert("FStar.Reflection");
        set.insert("FStar.Tactics.V2.Derived");
        set.insert("FStar.Tactics.V2.SyntaxCoercions");
        set.insert("FStar.Tactics.CanonCommMonoid");
        set.insert("FStar.Tactics.CanonCommSemiring");
        set
    };

    /// Modules that are idiomatically opened in their entirety in F* code.
    /// These provide operators, types, or pervasive definitions that are
    /// designed to be used unqualified. Opening them is standard practice
    /// and should never trigger FST008-A or FST008-C warnings.
    static ref WHITELISTED_OPENS: HashSet<&'static str> = {
        let mut set = HashSet::new();
        // Operator modules - bring arithmetic operators into scope
        set.insert("FStar.Mul");                // op_Star for natural number multiplication (*)
        set.insert("FStar.Pervasives");         // Core pervasives
        set.insert("FStar.Pervasives.Native");  // Native tuples etc.
        // Commonly opened effect/memory modules
        set.insert("FStar.HyperStack");         // mem, contains, etc.
        set.insert("FStar.HyperStack.ST");      // Stack effect, push/pop_frame
        set.insert("FStar.HyperStack.All");     // Combined HyperStack effect
        set.insert("FStar.ST");                 // State effect
        set.insert("FStar.Ghost");              // Ghost/erased types
        // Buffer/memory modules - provide many unqualified names
        set.insert("Lib.Buffer");               // HACL* buffer operations
        set.insert("Lib.IntTypes");             // Integer types and operators
        set.insert("Lib.Sequence");             // Sequence operations
        set.insert("Lib.ByteBuffer");           // Byte buffer operations
        set.insert("Lib.ByteSequence");         // Byte sequence operations
        set.insert("Lib.LoopCombinators");      // Loop combinators
        set.insert("Lib.IntVector");            // SIMD vector types
        set.insert("Lib.NTuple");               // N-tuples
        set.insert("Lib.MultiBuffer");          // Multi-buffer operations
        set.insert("LowStar.Buffer");           // Low* buffer operations
        set.insert("LowStar.BufferOps");        // Low* buffer operators (!*, *=)
        set.insert("LowStar.Monotonic.Buffer"); // Monotonic buffer
        // Common spec/math modules
        set.insert("FStar.Math.Lemmas");        // Math lemma helpers
        set.insert("FStar.Classical");          // Classical reasoning
        set.insert("FStar.Calc");               // Calculation proofs
        set
    };

    /// Modules that re-export other modules (transitive imports).
    /// Maps re-exporting module to what it re-exports.
    static ref TRANSITIVE_EXPORTS: HashMap<&'static str, Vec<&'static str>> = {
        let mut map = HashMap::new();
        map.insert("FStar.All", vec!["FStar.Exn", "FStar.ST"]);
        map.insert("FStar.HyperStack.All", vec!["FStar.HyperStack.ST", "FStar.HyperStack"]);
        map.insert("FStar.Tactics.V2", vec!["FStar.Tactics.V2.Derived", "FStar.Tactics.V2.SyntaxHelpers"]);
        map
    };

    /// Known module exports - maps module name to commonly used exports.
    /// Used to suggest selective imports when only a few names are used.
    static ref KNOWN_EXPORTS: HashMap<&'static str, Vec<&'static str>> = {
        let mut map = HashMap::new();
        map.insert("FStar.List.Tot", vec![
            "length", "hd", "tl", "nth", "index", "rev", "append",
            "map", "mapi", "fold_left", "fold_right", "filter", "mem",
            "for_all", "existsb", "find", "assoc", "split", "concatMap",
        ]);
        map.insert("FStar.Seq", vec![
            "seq", "length", "index", "create", "upd", "append", "slice",
            "init", "head", "tail", "last", "cons", "snoc", "equal",
        ]);
        map.insert("FStar.Set", vec![
            "set", "empty", "singleton", "union", "intersect", "complement",
            "mem", "equal", "subset", "disjoint",
        ]);
        map.insert("FStar.Map", vec![
            "map", "sel", "upd", "const", "concat", "restrict", "contains",
            "domain", "equal",
        ]);
        // Note: FStar.Mul and Lib.IntTypes are in WHITELISTED_OPENS and excluded
        // from KNOWN_EXPORTS. FStar.Mul provides op_Star (the * operator) which
        // is not detectable as an identifier. Lib.IntTypes provides operators,
        // type abbreviations, and coercions that are pervasive in HACL* code.
        map.insert("FStar.UInt32", vec![
            "t", "v", "uint_to_t", "add", "sub", "mul", "div",
            "add_mod", "sub_mod", "mul_mod", "logand", "logor", "logxor",
        ]);
        map.insert("FStar.UInt64", vec![
            "t", "v", "uint_to_t", "add", "sub", "mul", "div",
            "add_mod", "sub_mod", "mul_mod", "logand", "logor", "logxor",
        ]);
        map
    };

    /// Threshold for suggesting selective import (if using <= this many names, suggest selective)
    static ref SELECTIVE_THRESHOLD: usize = 3;
}

/// Subcategory for FST008 diagnostics.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum ImportCategory {
    /// FST008-A: Broad import when selective would suffice
    BroadImport,
    /// FST008-B: Unused import
    UnusedImport,
    /// FST008-C: Qualified names preferred
    PreferQualified,
    /// FST008-D: Circular import detected (self-import or parent-child cycle)
    CircularImport,
    /// FST008-E: Unnecessary transitive import
    TransitiveImport,
    /// Heavy module import warning
    HeavyModule,
}

impl ImportCategory {
    /// Returns the subcategory code suffix.
    pub fn code_suffix(&self) -> &'static str {
        match self {
            ImportCategory::BroadImport => "A",
            ImportCategory::UnusedImport => "B",
            ImportCategory::PreferQualified => "C",
            ImportCategory::CircularImport => "D",
            ImportCategory::TransitiveImport => "E",
            ImportCategory::HeavyModule => "H",
        }
    }
}

/// Information about how a module's exports are used in the file.
#[derive(Debug, Default, Clone)]
struct ModuleUsage {
    /// Names from this module that are used unqualified
    unqualified_names: HashSet<String>,
    /// Times this module is used with qualified access (e.g., Module.foo)
    qualified_uses: usize,
    /// The open statement for this module (if any)
    open_line: Option<usize>,
}

/// Import optimization analysis result.
#[derive(Debug)]
struct ImportAnalysis {
    /// Open statements in the file
    opens: Vec<OpenStatement>,
    /// Module usage information
    module_usage: HashMap<String, ModuleUsage>,
    /// All identifiers used in the file
    used_identifiers: HashSet<String>,
    /// Modules used via qualified access
    qualified_modules: HashSet<String>,
    /// Current module name (from module declaration)
    current_module: Option<String>,
}

/// Analyze imports and their usage in the file.
fn analyze_imports(content: &str) -> ImportAnalysis {
    let open_analysis = analyze_opens(content);
    let mut module_usage: HashMap<String, ModuleUsage> = HashMap::new();

    // Extract current module name
    let current_module = extract_current_module(content);

    // Track open statements
    for open in &open_analysis.opens {
        let usage = module_usage.entry(open.module_path.clone()).or_default();
        usage.open_line = Some(open.line);
    }

    // Track qualified uses
    let qualified_modules = extract_qualified_modules(content);
    for module in &qualified_modules {
        let usage = module_usage.entry(module.clone()).or_default();
        usage.qualified_uses += 1;
    }

    // Track unqualified identifier usage per module (for modules with known exports)
    for (module, exports) in KNOWN_EXPORTS.iter() {
        let usage = module_usage.entry(module.to_string()).or_default();
        for export in exports.iter() {
            if open_analysis.used_identifiers.contains(*export) {
                usage.unqualified_names.insert(export.to_string());
            }
        }
    }

    ImportAnalysis {
        opens: open_analysis.opens,
        module_usage,
        used_identifiers: open_analysis.used_identifiers,
        qualified_modules,
        current_module,
    }
}

/// Extract the current module name from the module declaration.
fn extract_current_module(content: &str) -> Option<String> {
    lazy_static! {
        static ref MODULE_DECL: Regex = Regex::new(r"^module\s+([A-Z][\w.]*)\s*$").unwrap();
    }

    for line in content.lines() {
        let trimmed = line.trim();
        if let Some(caps) = MODULE_DECL.captures(trimmed) {
            return Some(caps.get(1).unwrap().as_str().to_string());
        }
    }
    None
}

/// Extract modules used via qualified access.
///
/// Filters out declaration lines (open, module, friend, include) so that
/// qualified module paths appearing in those lines are not mistakenly counted
/// as "qualified usage". For example, `open FStar.HyperStack.ST` should not
/// cause `FStar.HyperStack` to appear as a qualified use of that module.
fn extract_qualified_modules(content: &str) -> HashSet<String> {
    let mut modules = HashSet::new();

    // Filter out declaration lines before analysis to avoid false positives.
    // Without this, `open FStar.HyperStack.ST` would make the regex extract
    // `FStar.HyperStack` as a qualified use, causing FST008-C to fire on
    // `open FStar.HyperStack` (claiming it's "only accessed via qualified names").
    let filtered: String = content
        .lines()
        .filter(|line| {
            let trimmed = line.trim();
            !trimmed.starts_with("open ")
                && !trimmed.starts_with("module ")
                && !trimmed.starts_with("friend ")
                && !trimmed.starts_with("include ")
        })
        .collect::<Vec<_>>()
        .join("\n");

    let clean = strip_comments_and_strings(&filtered);

    for caps in QUALIFIED_USE_PATTERN.captures_iter(&clean) {
        if let Some(m) = caps.get(1) {
            modules.insert(m.as_str().to_string());
        }
    }

    modules
}

/// Strip comments and string literals for accurate analysis.
fn strip_comments_and_strings(content: &str) -> String {
    let mut result = String::with_capacity(content.len());
    let chars: Vec<char> = content.chars().collect();
    let n = chars.len();
    let mut i = 0;
    let mut comment_depth = 0;
    let mut in_line_comment = false;

    while i < n {
        // Handle line comments
        if i + 1 < n && chars[i] == '/' && chars[i + 1] == '/' {
            in_line_comment = true;
            i += 2;
            continue;
        }

        if in_line_comment {
            if chars[i] == '\n' {
                in_line_comment = false;
                result.push('\n');
            }
            i += 1;
            continue;
        }

        // Handle block comment start
        if i + 1 < n && chars[i] == '(' && chars[i + 1] == '*' {
            comment_depth += 1;
            i += 2;
            continue;
        }

        // Handle block comment end
        if i + 1 < n && chars[i] == '*' && chars[i + 1] == ')' && comment_depth > 0 {
            comment_depth -= 1;
            i += 2;
            continue;
        }

        if comment_depth > 0 {
            if chars[i] == '\n' {
                result.push('\n');
            }
            i += 1;
            continue;
        }

        // Handle string literals
        if chars[i] == '"' {
            i += 1;
            while i < n && chars[i] != '"' {
                if chars[i] == '\\' && i + 1 < n {
                    i += 2;
                } else {
                    i += 1;
                }
            }
            if i < n {
                i += 1;
            }
            continue;
        }

        result.push(chars[i]);
        i += 1;
    }

    result
}

/// Result of circular import analysis.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum CircularImportType {
    /// Module imports itself (A opens A)
    SelfImport,
    /// Child module imports parent (A.B opens A) - may cause dependency cycle
    ChildImportsParent,
    /// Parent module imports child (A opens A.B) - unusual but sometimes valid
    ParentImportsChild,
    /// No circular dependency detected
    None,
}

impl CircularImportType {
    /// Returns the severity for this type of circular import.
    pub fn severity(&self) -> DiagnosticSeverity {
        match self {
            CircularImportType::SelfImport => DiagnosticSeverity::Error,
            CircularImportType::ChildImportsParent => DiagnosticSeverity::Warning,
            CircularImportType::ParentImportsChild => DiagnosticSeverity::Info,
            CircularImportType::None => DiagnosticSeverity::Hint,
        }
    }

    /// Returns a descriptive message for this type of circular import.
    pub fn message(&self, current: &str, imported: &str) -> String {
        match self {
            CircularImportType::SelfImport => {
                format!("[FST008-D] Self-import: module `{}` opens itself", current)
            }
            CircularImportType::ChildImportsParent => {
                format!(
                    "[FST008-D] Parent import: module `{}` opens parent `{}` - may cause circular dependency",
                    current, imported
                )
            }
            CircularImportType::ParentImportsChild => {
                format!(
                    "[FST008-D] Child import: module `{}` opens child `{}` - unusual pattern, ensure no dependency cycle",
                    current, imported
                )
            }
            CircularImportType::None => String::new(),
        }
    }
}

/// Analyze circular import relationship between current module and imported module.
fn analyze_circular_import(current_module: &Option<String>, imported: &str) -> CircularImportType {
    if let Some(current) = current_module {
        // Direct circular: A opens A
        if current == imported {
            return CircularImportType::SelfImport;
        }

        // Child imports parent: A.B.C opens A.B or A
        // Check if current module starts with imported module (current is a child of imported)
        if current.starts_with(&format!("{}.", imported)) {
            return CircularImportType::ChildImportsParent;
        }

        // Parent imports child: A opens A.B or A.B.C
        // Check if imported module starts with current module (imported is a child of current)
        if imported.starts_with(&format!("{}.", current)) {
            return CircularImportType::ParentImportsChild;
        }
    }
    CircularImportType::None
}

/// Check if a module path indicates circular dependency with current module.
/// Returns true for any form of circular dependency (self, parent, or child).
#[allow(dead_code)]
fn is_circular_import(current_module: &Option<String>, imported: &str) -> bool {
    analyze_circular_import(current_module, imported) != CircularImportType::None
}

/// Generate a fix to convert broad open to selective open.
fn generate_selective_fix(
    open: &OpenStatement,
    used_names: &HashSet<String>,
    file: &PathBuf,
) -> Option<Fix> {
    if used_names.is_empty() {
        return None;
    }

    let names: Vec<_> = used_names.iter().cloned().collect();
    let selective_import = format!("open {} {{ {} }}", open.module_path, names.join(", "));

    Some(Fix::new(
        format!(
            "Convert to selective import: only {} name{} used",
            names.len(),
            if names.len() == 1 { "" } else { "s" }
        ),
        vec![Edit {
            file: file.clone(),
            range: Range::new(open.line, 1, open.line + 1, 1),
            new_text: format!("{}\n", selective_import),
        }],
    ))
}

/// Generate a fix to use qualified access instead of open.
fn generate_qualified_fix(open: &OpenStatement, file: &PathBuf) -> Fix {
    Fix::new(
        format!(
            "Remove open and use qualified access: `{}.name`",
            open.module_path
        ),
        vec![Edit {
            file: file.clone(),
            range: Range::new(open.line, 1, open.line + 1, 1),
            new_text: String::new(),
        }],
    )
}

/// FST008: Import Optimizer rule.
///
/// Detects import patterns that can be improved for better verification
/// performance and code clarity.
pub struct ImportOptimizerRule {
    /// Threshold for suggesting selective import.
    /// If a module is opened but only N or fewer names are used, suggest selective import.
    selective_threshold: usize,
}

impl ImportOptimizerRule {
    /// Create a new ImportOptimizerRule with default settings.
    pub fn new() -> Self {
        Self {
            selective_threshold: *SELECTIVE_THRESHOLD,
        }
    }

    /// Create with custom selective threshold.
    pub fn with_threshold(threshold: usize) -> Self {
        Self {
            selective_threshold: threshold,
        }
    }

    /// Check for heavy module imports that may slow verification.
    fn check_heavy_modules(&self, open: &OpenStatement, file: &PathBuf) -> Option<Diagnostic> {
        if HEAVY_MODULES.contains(open.module_path.as_str()) {
            Some(Diagnostic {
                rule: RuleCode::FST008,
                severity: DiagnosticSeverity::Info,
                file: file.clone(),
                range: Range::new(
                    open.line,
                    open.col,
                    open.line,
                    open.col + open.line_text.trim().len(),
                ),
                message: format!(
                    "[FST008-H] Heavy import: `{}` may significantly slow verification. \
                     Consider selective import or ensure it's necessary.",
                    open.module_path
                ),
                fix: None,
            })
        } else {
            None
        }
    }

    /// Check for broad imports where selective would suffice.
    fn check_broad_import(
        &self,
        open: &OpenStatement,
        usage: &ModuleUsage,
        file: &PathBuf,
    ) -> Option<Diagnostic> {
        // Skip if already selective
        if open.selective.is_some() {
            return None;
        }

        // Skip whitelisted modules - they are designed to be opened entirely
        // (e.g., FStar.Mul for operators, Lib.IntTypes for integer types)
        if WHITELISTED_OPENS.contains(open.module_path.as_str()) {
            return None;
        }

        // Check if we have known exports for this module
        if let Some(_exports) = KNOWN_EXPORTS.get(open.module_path.as_str()) {
            let used_count = usage.unqualified_names.len();

            // If only a few names are used, suggest selective import
            if used_count > 0 && used_count <= self.selective_threshold {
                let fix = generate_selective_fix(open, &usage.unqualified_names, file);

                return Some(Diagnostic {
                    rule: RuleCode::FST008,
                    severity: DiagnosticSeverity::Info,
                    file: file.clone(),
                    range: Range::new(
                        open.line,
                        open.col,
                        open.line,
                        open.col + open.line_text.trim().len(),
                    ),
                    message: format!(
                        "[FST008-A] Broad import: `open {}` but only {} name{} used ({}). \
                         Consider selective import.",
                        open.module_path,
                        used_count,
                        if used_count == 1 { "" } else { "s" },
                        usage
                            .unqualified_names
                            .iter()
                            .cloned()
                            .collect::<Vec<_>>()
                            .join(", ")
                    ),
                    fix,
                });
            }
        }

        None
    }

    /// Check for imports where qualified access would be clearer.
    ///
    /// Only emits a diagnostic when we can reliably determine that the module
    /// is not used unqualified. This requires the module to be in KNOWN_EXPORTS
    /// so we can check which names it provides. For modules not in KNOWN_EXPORTS,
    /// we cannot know what names the open brings into scope, so we skip the check
    /// to avoid false positives.
    fn check_prefer_qualified(
        &self,
        open: &OpenStatement,
        usage: &ModuleUsage,
        file: &PathBuf,
    ) -> Option<Diagnostic> {
        // Skip whitelisted modules - they are designed to be opened entirely
        // and may bring operators or types not trackable by identifier scanning
        if WHITELISTED_OPENS.contains(open.module_path.as_str()) {
            return None;
        }

        // Only emit FST008-C for modules in KNOWN_EXPORTS where we can reliably
        // determine unqualified usage. For unknown modules, we have no way to know
        // what names the open brings into scope, so emitting a warning would be
        // a false positive in most cases.
        if !KNOWN_EXPORTS.contains_key(open.module_path.as_str()) {
            return None;
        }

        // If module is only used via qualified access anyway, the open is redundant
        if usage.qualified_uses > 0 && usage.unqualified_names.is_empty() {
            return Some(Diagnostic {
                rule: RuleCode::FST008,
                severity: DiagnosticSeverity::Hint,
                file: file.clone(),
                range: Range::new(
                    open.line,
                    open.col,
                    open.line,
                    open.col + open.line_text.trim().len(),
                ),
                message: format!(
                    "[FST008-C] Unnecessary open: `{}` is only accessed via qualified names. \
                     Consider removing the open statement.",
                    open.module_path
                ),
                fix: Some(generate_qualified_fix(open, file)),
            });
        }

        None
    }

    /// Check for circular imports with differentiated severity.
    ///
    /// Only reports truly problematic circular imports:
    /// - Self-import (Error): Module opens itself -- always a bug
    /// - Child imports parent (Warning): `A.B` opens `A` -- may cause dependency cycle
    ///
    /// Parent-imports-child (`A` opens `A.B`) is suppressed because it is a
    /// completely normal pattern in F*. Parent modules routinely open their
    /// child sub-modules to compose functionality, and F* resolves this via
    /// interface files (.fsti).
    fn check_circular_import(
        &self,
        open: &OpenStatement,
        current_module: &Option<String>,
        file: &PathBuf,
    ) -> Option<Diagnostic> {
        let circular_type = analyze_circular_import(current_module, &open.module_path);

        // Only report self-import and child-imports-parent.
        // ParentImportsChild is a normal F* pattern, not a code smell.
        if circular_type == CircularImportType::None
            || circular_type == CircularImportType::ParentImportsChild
        {
            return None;
        }

        let current = current_module.as_deref().unwrap_or("<unknown>");
        Some(Diagnostic {
            rule: RuleCode::FST008,
            severity: circular_type.severity(),
            file: file.clone(),
            range: Range::new(
                open.line,
                open.col,
                open.line,
                open.col + open.line_text.trim().len(),
            ),
            message: circular_type.message(current, &open.module_path),
            fix: None,
        })
    }

    /// Check for unnecessary transitive imports.
    fn check_transitive_import(
        &self,
        open: &OpenStatement,
        analysis: &ImportAnalysis,
        file: &PathBuf,
    ) -> Option<Diagnostic> {
        // Check if this module re-exports something else that's also imported
        if let Some(reexports) = TRANSITIVE_EXPORTS.get(open.module_path.as_str()) {
            for reexported in reexports {
                // Check if the re-exported module is also directly imported
                if analysis.opens.iter().any(|o| o.module_path == *reexported) {
                    return Some(Diagnostic {
                        rule: RuleCode::FST008,
                        severity: DiagnosticSeverity::Info,
                        file: file.clone(),
                        range: Range::new(
                            open.line,
                            open.col,
                            open.line,
                            open.col + open.line_text.trim().len(),
                        ),
                        message: format!(
                            "[FST008-E] Potentially redundant import: `{}` re-exports `{}`, \
                             which is also directly imported.",
                            open.module_path, reexported
                        ),
                        fix: None,
                    });
                }
            }
        }

        None
    }

}

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

impl Rule for ImportOptimizerRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST008
    }

    fn check(&self, file: &PathBuf, content: &str) -> Vec<Diagnostic> {
        let analysis = analyze_imports(content);
        let mut diagnostics = Vec::new();

        for open in &analysis.opens {
            // Get usage info for this module
            let usage = analysis
                .module_usage
                .get(&open.module_path)
                .cloned()
                .unwrap_or_default();

            // Check for heavy module imports (always check first)
            if let Some(diag) = self.check_heavy_modules(open, file) {
                diagnostics.push(diag);
            }

            // Check for circular imports (with differentiated severity)
            if let Some(diag) = self.check_circular_import(open, &analysis.current_module, file) {
                diagnostics.push(diag);
            }

            // Check for transitive imports
            if let Some(diag) = self.check_transitive_import(open, &analysis, file) {
                diagnostics.push(diag);
            }

            // Check for broad imports (only if not already flagged as heavy)
            if !HEAVY_MODULES.contains(open.module_path.as_str()) {
                if let Some(diag) = self.check_broad_import(open, &usage, file) {
                    diagnostics.push(diag);
                }
            }

            // Check for prefer qualified access
            if let Some(diag) = self.check_prefer_qualified(open, &usage, file) {
                diagnostics.push(diag);
            }
        }

        diagnostics
    }
}

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

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

open FStar.Tactics.V2

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        assert!(!diagnostics.is_empty());
        assert!(diagnostics[0].message.contains("FST008-H"));
        assert!(diagnostics[0].message.contains("Heavy import"));
    }

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

open FStar.List.Tot

let x = length [1; 2; 3]
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        // Should detect that only "length" is used from FStar.List.Tot
        let broad = diagnostics.iter().find(|d| d.message.contains("FST008-A"));
        assert!(broad.is_some(), "Should detect broad import");
    }

    #[test]
    fn test_circular_import_detection() {
        let content = r#"module Test.Sub

open Test.Sub

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("Test/Sub.fst"), content);

        let circular = diagnostics.iter().find(|d| d.message.contains("FST008-D"));
        assert!(circular.is_some(), "Should detect circular import");
    }

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

open FStar.List.Tot { length }

let x = length [1; 2; 3]
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        // Selective import should not trigger FST008-A
        let broad = diagnostics.iter().find(|d| d.message.contains("FST008-A"));
        assert!(
            broad.is_none(),
            "Selective import should not trigger broad import warning"
        );
    }

    #[test]
    fn test_strip_comments() {
        let content = r#"
(* open FStar.Unused *)
let x = List.map (* comment *) f xs
// open Another.Unused
let y = 1
"#;
        let stripped = strip_comments_and_strings(content);
        assert!(!stripped.contains("FStar.Unused"));
        assert!(!stripped.contains("Another.Unused"));
        assert!(stripped.contains("List.map"));
    }

    #[test]
    fn test_extract_current_module() {
        let content = r#"module MyProject.Utils.Helper

open FStar.All

let helper x = x + 1
"#;
        let module_name = extract_current_module(content);
        assert_eq!(module_name, Some("MyProject.Utils.Helper".to_string()));
    }

    #[test]
    fn test_parent_child_circular() {
        // Module opening its parent
        let content = r#"module Test.Sub.Child

open Test.Sub

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let circular = diagnostics.iter().find(|d| d.message.contains("FST008-D"));
        assert!(
            circular.is_some(),
            "Should detect parent-child circular dependency"
        );
        // Should be a warning for child importing parent
        assert!(
            circular.unwrap().message.contains("Parent import"),
            "Should identify as parent import"
        );
    }

    #[test]
    fn test_self_import_detection() {
        let content = r#"module MyModule

open MyModule

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let circular = diagnostics.iter().find(|d| d.message.contains("FST008-D"));
        assert!(circular.is_some(), "Should detect self-import");
        assert!(
            circular.unwrap().message.contains("Self-import"),
            "Should identify as self-import"
        );
        // Self-import should be an error
        assert_eq!(
            circular.unwrap().severity,
            DiagnosticSeverity::Error,
            "Self-import should be Error severity"
        );
    }

    #[test]
    fn test_parent_imports_child_suppressed() {
        // Parent module opening child is a normal F* pattern and should NOT
        // produce a diagnostic. Parent modules routinely open child sub-modules
        // to compose functionality.
        let content = r#"module Parent

open Parent.Child

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let circular = diagnostics.iter().find(|d| d.message.contains("FST008-D"));
        assert!(
            circular.is_none(),
            "Parent importing child should NOT trigger FST008-D (normal F* pattern)"
        );
    }

    #[test]
    fn test_deep_parent_import() {
        // Deep child module opening parent
        let content = r#"module A.B.C.D

open A.B

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let circular = diagnostics.iter().find(|d| d.message.contains("FST008-D"));
        assert!(circular.is_some(), "Should detect deep parent import");
        assert!(
            circular.unwrap().message.contains("Parent import"),
            "Should identify as parent import"
        );
    }

    #[test]
    fn test_no_fst008f_import_order() {
        // FST008-F was removed: import ordering (Core > Pure > Effect > Project)
        // produces false positives because:
        // 1. FStar.Ghost was wrongly categorized as "Effect" (it's pure erasure types)
        // 2. Many FStar.* modules (Calc, Squash, Tactics, etc.) fell through to "Project"
        // 3. No F* community convention for this ordering exists
        // 4. Real F* codebases (hacl-star, everparse) don't follow this ordering
        let content = r#"module Test

open MyProject.Utils
open FStar.Pervasives
open FStar.ST
open FStar.List.Tot
open FStar.Ghost
open FStar.Calc
open Hacl.Impl.SHA256

let x = 1
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let order_issues: Vec<_> = diagnostics
            .iter()
            .filter(|d| d.message.contains("FST008-F"))
            .collect();
        assert!(
            order_issues.is_empty(),
            "FST008-F import ordering should not be emitted"
        );
    }

    #[test]
    fn test_circular_import_type_messages() {
        let self_msg = CircularImportType::SelfImport.message("A", "A");
        assert!(self_msg.contains("Self-import"));
        assert!(self_msg.contains("opens itself"));

        let parent_msg = CircularImportType::ChildImportsParent.message("A.B", "A");
        assert!(parent_msg.contains("Parent import"));
        assert!(parent_msg.contains("may cause circular"));

        let child_msg = CircularImportType::ParentImportsChild.message("A", "A.B");
        assert!(child_msg.contains("Child import"));
        assert!(child_msg.contains("unusual pattern"));
    }

    #[test]
    fn test_analyze_circular_import() {
        // Self-import
        assert_eq!(
            analyze_circular_import(&Some("Test".to_string()), "Test"),
            CircularImportType::SelfImport
        );

        // Child imports parent
        assert_eq!(
            analyze_circular_import(&Some("A.B.C".to_string()), "A.B"),
            CircularImportType::ChildImportsParent
        );
        assert_eq!(
            analyze_circular_import(&Some("A.B".to_string()), "A"),
            CircularImportType::ChildImportsParent
        );

        // Parent imports child
        assert_eq!(
            analyze_circular_import(&Some("A".to_string()), "A.B"),
            CircularImportType::ParentImportsChild
        );
        assert_eq!(
            analyze_circular_import(&Some("A.B".to_string()), "A.B.C"),
            CircularImportType::ParentImportsChild
        );

        // No circular
        assert_eq!(
            analyze_circular_import(&Some("A".to_string()), "B"),
            CircularImportType::None
        );
        assert_eq!(
            analyze_circular_import(&Some("A.B".to_string()), "C.D"),
            CircularImportType::None
        );
        assert_eq!(
            analyze_circular_import(&None, "A"),
            CircularImportType::None
        );
    }

    #[test]
    fn test_no_false_positive_similar_names() {
        // "AModule" should not be considered parent of "AModuleExtended"
        assert_eq!(
            analyze_circular_import(&Some("AModuleExtended".to_string()), "AModule"),
            CircularImportType::None
        );

        // "Test" should not match "Testing" as parent
        assert_eq!(
            analyze_circular_import(&Some("Testing.Sub".to_string()), "Test"),
            CircularImportType::None
        );
    }

    // ========================================================================
    // FALSE POSITIVE PREVENTION TESTS
    // ========================================================================

    #[test]
    fn test_whitelisted_module_no_broad_import_warning() {
        // FStar.Mul is whitelisted - opening it should never trigger FST008-A
        // even though the linter cannot detect op_Star usage (written as `*`)
        let content = r#"module Test

open FStar.Mul

let x = 2 * 3
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let broad = diagnostics.iter().find(|d| d.message.contains("FST008-A"));
        assert!(
            broad.is_none(),
            "Whitelisted module FStar.Mul should not trigger FST008-A"
        );
    }

    #[test]
    fn test_whitelisted_module_no_prefer_qualified_warning() {
        // Lib.IntTypes is whitelisted - should not trigger FST008-C even if
        // qualified access like Lib.IntTypes.Intrinsics.foo exists
        let content = r#"module Test

open Lib.IntTypes

let x = Lib.IntTypes.Intrinsics.add_carry 0uy 1ul 2ul out
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let prefer_qual = diagnostics.iter().find(|d| d.message.contains("FST008-C"));
        assert!(
            prefer_qual.is_none(),
            "Whitelisted module Lib.IntTypes should not trigger FST008-C"
        );
    }

    #[test]
    fn test_no_fst008c_for_unknown_modules() {
        // Modules not in KNOWN_EXPORTS should not trigger FST008-C because
        // we cannot reliably determine what names they bring into scope.
        // This was the #1 source of false positives.
        let content = r#"module Test

open Hacl.Bignum.Definitions

let x = Hacl.Bignum.Definitions.bn_v h b
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let prefer_qual = diagnostics.iter().find(|d| d.message.contains("FST008-C"));
        assert!(
            prefer_qual.is_none(),
            "Unknown module should not trigger FST008-C"
        );
    }

    #[test]
    fn test_no_false_qualified_use_from_open_lines() {
        // When a file has `open FStar.HyperStack` and `open FStar.HyperStack.ST`,
        // the second open line should NOT cause FStar.HyperStack to appear as a
        // "qualified use". This was the main source of false FST008-C warnings.
        let content = r#"module Test

open FStar.HyperStack
open FStar.HyperStack.ST

let f (h: mem) = h
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let prefer_qual = diagnostics.iter().find(|d| d.message.contains("FST008-C"));
        assert!(
            prefer_qual.is_none(),
            "open FStar.HyperStack.ST should not make FStar.HyperStack appear as qualified use"
        );
    }

    #[test]
    fn test_extract_qualified_modules_filters_declarations() {
        // Verify that extract_qualified_modules does not pick up module
        // paths from open/module/friend/include declaration lines
        let content = r#"module Test

open FStar.HyperStack
open FStar.HyperStack.ST
module S = Hacl.Spec.Bignum

let x = S.bn_v h b
"#;
        let modules = extract_qualified_modules(content);

        // S should be found (used in code)
        assert!(
            modules.contains("S"),
            "Should find S as qualified module from `S.bn_v`"
        );

        // FStar.HyperStack should NOT be found (only appears in open lines)
        assert!(
            !modules.contains("FStar.HyperStack"),
            "Should not extract FStar.HyperStack from `open FStar.HyperStack.ST` line"
        );

        // Hacl.Spec should NOT be found (only appears in module alias line)
        assert!(
            !modules.contains("Hacl.Spec"),
            "Should not extract Hacl.Spec from module alias declaration"
        );
    }

    #[test]
    fn test_hacl_star_typical_file_no_false_positives() {
        // Simulate a typical HACL* file header - should produce zero warnings
        // from FST008-A, FST008-C
        let content = r#"module Hacl.Bignum.Base

open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Mul

open Lib.IntTypes
open Lib.Buffer
open Hacl.Bignum.Definitions

module LSeq = Lib.Sequence

let addcarry_st c_in a b out =
  Lib.IntTypes.Intrinsics.add_carry c_in a b out

let x = LSeq.index (as_seq h out) 0
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("Hacl/Bignum/Base.fst"), content);

        let a_warnings: Vec<_> = diagnostics
            .iter()
            .filter(|d| d.message.contains("FST008-A"))
            .collect();
        let c_warnings: Vec<_> = diagnostics
            .iter()
            .filter(|d| d.message.contains("FST008-C"))
            .collect();

        assert!(
            a_warnings.is_empty(),
            "Typical HACL* file should not trigger FST008-A, got: {:?}",
            a_warnings.iter().map(|d| &d.message).collect::<Vec<_>>()
        );
        assert!(
            c_warnings.is_empty(),
            "Typical HACL* file should not trigger FST008-C, got: {:?}",
            c_warnings.iter().map(|d| &d.message).collect::<Vec<_>>()
        );
    }

    #[test]
    fn test_fst008c_still_fires_for_known_exports_modules() {
        // FST008-C should still fire for modules in KNOWN_EXPORTS that are
        // NOT whitelisted, when they are only used qualified.
        let content = r#"module Test

open FStar.List.Tot

let x = FStar.List.Tot.length [1; 2; 3]
"#;
        let rule = ImportOptimizerRule::new();
        let diagnostics = rule.check(&PathBuf::from("test.fst"), content);

        let prefer_qual = diagnostics.iter().find(|d| d.message.contains("FST008-C"));
        assert!(
            prefer_qual.is_some(),
            "FST008-C should still fire for KNOWN_EXPORTS module used only qualified"
        );
    }

    #[test]
    fn test_whitelisted_modules_comprehensive() {
        // Verify all critical whitelisted modules are covered
        let critical_modules = vec![
            "FStar.Mul",
            "FStar.HyperStack",
            "FStar.HyperStack.ST",
            "Lib.IntTypes",
            "Lib.Buffer",
            "LowStar.Buffer",
            "LowStar.BufferOps",
        ];

        for module in critical_modules {
            assert!(
                WHITELISTED_OPENS.contains(module),
                "Module {} should be in WHITELISTED_OPENS",
                module
            );
        }
    }
}