brrr-lint 0.1.0

//! FST015: Module dependency analyzer.
//!
//! Analyzes F* module dependencies from open/friend/include statements:
//! - Detects self-dependencies (module depending on itself)
//! - Warns when module has too many dependencies (>15)
//! - Detects circular dependencies using Tarjan's SCC algorithm
//! - Generates DOT graph output for visualization
//! - Calculates dependency depth for each module
//! - Computes optimal verification order via topological sort

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

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

lazy_static! {
    /// Matches top-level module declaration: `module Foo.Bar`
    /// Must NOT have `=` after the name (that would be a module abbreviation).
    static ref MODULE_DECL: Regex = Regex::new(r"^module\s+([A-Z][\w.]*)\s*$").unwrap();
    /// Matches module abbreviation: `module L = FStar.List.Tot`
    /// The RHS module name is a dependency.
    static ref MODULE_ABBREV: Regex =
        Regex::new(r"^module\s+[A-Za-z_][\w]*\s*=\s*([A-Z][\w.]*)").unwrap();
    /// Matches `open Foo.Bar` at the start of a (trimmed) line.
    static ref OPEN_STMT: Regex = Regex::new(r"^open\s+([A-Z][\w.]*)").unwrap();
    /// Matches `let open Foo.Bar` (scoped open inside expressions).
    static ref LET_OPEN_STMT: Regex =
        Regex::new(r"let\s+open\s+([A-Z][\w.]*)").unwrap();
    static ref FRIEND_STMT: Regex = Regex::new(r"^friend\s+([A-Z][\w.]*)").unwrap();
    static ref INCLUDE_STMT: Regex = Regex::new(r"^include\s+([A-Z][\w.]*)").unwrap();
}

/// Module dependency information extracted from source.
#[derive(Debug, Clone)]
pub struct ModuleDeps {
    /// Module name from `module X.Y.Z` declaration.
    pub name: String,
    /// Modules from `open X` statements.
    pub opens: Vec<String>,
    /// Modules from `friend X` statements.
    pub friends: Vec<String>,
    /// Modules from `include X` statements.
    pub includes: Vec<String>,
    /// Modules from `module Alias = X` abbreviations (these are dependencies).
    pub abbreviations: Vec<String>,
}

impl ModuleDeps {
    /// Get all dependencies as a single vector.
    pub fn all_deps(&self) -> Vec<&str> {
        self.opens
            .iter()
            .chain(self.friends.iter())
            .chain(self.includes.iter())
            .chain(self.abbreviations.iter())
            .map(|s| s.as_str())
            .collect()
    }

    /// Total number of dependencies.
    pub fn total_deps(&self) -> usize {
        self.opens.len() + self.friends.len() + self.includes.len() + self.abbreviations.len()
    }

    /// Number of unique dependencies (deduplicated).
    pub fn unique_dep_count(&self) -> usize {
        let deps: HashSet<&str> = self.all_deps().into_iter().collect();
        deps.len()
    }
}

/// Tarjan's Strongly Connected Components algorithm for cycle detection.
///
/// Finds all strongly connected components in a directed graph.
/// An SCC with more than one node indicates a circular dependency.
///
/// Time complexity: O(V + E) where V = nodes, E = edges
/// Space complexity: O(V)
pub struct TarjanSCC {
    /// Current DFS index counter
    index: usize,
    /// Stack of nodes in current DFS path
    stack: Vec<String>,
    /// Set for O(1) stack membership check
    on_stack: HashSet<String>,
    /// DFS discovery index for each node
    indices: HashMap<String, usize>,
    /// Lowest reachable index for each node
    low_links: HashMap<String, usize>,
    /// Resulting strongly connected components
    sccs: Vec<Vec<String>>,
}

impl TarjanSCC {
    /// Create a new Tarjan SCC finder.
    pub fn new() -> Self {
        Self {
            index: 0,
            stack: Vec::new(),
            on_stack: HashSet::new(),
            indices: HashMap::new(),
            low_links: HashMap::new(),
            sccs: Vec::new(),
        }
    }

    /// Find all cycles (SCCs with more than one node) in the dependency graph.
    ///
    /// Returns a vector of cycles, where each cycle is a vector of module names.
    pub fn find_cycles(&mut self, graph: &HashMap<String, Vec<String>>) -> Vec<Vec<String>> {
        // Run Tarjan's algorithm on all unvisited nodes
        for node in graph.keys() {
            if !self.indices.contains_key(node) {
                self.strongconnect(node, graph);
            }
        }

        // Filter to only SCCs with more than one node (actual cycles)
        // A single-node SCC is not a cycle unless it has a self-edge
        self.sccs
            .iter()
            .filter(|scc| scc.len() > 1)
            .cloned()
            .collect()
    }

    /// Find all SCCs including single-node components.
    pub fn find_all_sccs(&mut self, graph: &HashMap<String, Vec<String>>) -> Vec<Vec<String>> {
        for node in graph.keys() {
            if !self.indices.contains_key(node) {
                self.strongconnect(node, graph);
            }
        }
        std::mem::take(&mut self.sccs)
    }

    /// Core Tarjan's algorithm: depth-first search with lowlink computation.
    fn strongconnect(&mut self, v: &str, graph: &HashMap<String, Vec<String>>) {
        // Set the depth index for v to the smallest unused index
        self.indices.insert(v.to_string(), self.index);
        self.low_links.insert(v.to_string(), self.index);
        self.index += 1;
        self.stack.push(v.to_string());
        self.on_stack.insert(v.to_string());

        // Consider successors of v
        if let Some(successors) = graph.get(v) {
            for w in successors {
                if !self.indices.contains_key(w) {
                    // Successor w has not been visited; recurse on it
                    self.strongconnect(w, graph);
                    let low_v = self.low_links[v];
                    let low_w = self.low_links[w];
                    self.low_links
                        .insert(v.to_string(), std::cmp::min(low_v, low_w));
                } else if self.on_stack.contains(w) {
                    // Successor w is on stack, hence in current SCC
                    // Update v's lowlink to w's index (not lowlink!)
                    let low_v = self.low_links[v];
                    let idx_w = self.indices[w];
                    self.low_links
                        .insert(v.to_string(), std::cmp::min(low_v, idx_w));
                }
            }
        }

        // If v is a root node, pop the stack and generate an SCC
        if self.low_links[v] == self.indices[v] {
            let mut scc = Vec::new();
            loop {
                let w = self.stack.pop().expect("Stack should not be empty");
                self.on_stack.remove(&w);
                scc.push(w.clone());
                if w == v {
                    break;
                }
            }
            self.sccs.push(scc);
        }
    }

    /// Reset the state for reuse.
    pub fn reset(&mut self) {
        self.index = 0;
        self.stack.clear();
        self.on_stack.clear();
        self.indices.clear();
        self.low_links.clear();
        self.sccs.clear();
    }
}

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

/// Edge type for DOT graph visualization.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum DependencyType {
    Open,
    Friend,
    Include,
}

/// Generate DOT format graph for module dependency visualization.
///
/// Output can be rendered with graphviz: `dot -Tpng deps.dot -o deps.png`
///
/// Features:
/// - Different edge styles for open/friend/include
/// - Cycle nodes highlighted in red
/// - Leaf nodes (no dependencies) in green
pub fn generate_dot_graph(modules: &[ModuleDeps]) -> String {
    generate_dot_graph_with_options(modules, true, true)
}

/// Generate DOT graph with configurable options.
///
/// Arguments:
/// - `modules`: Module dependency data
/// - `highlight_cycles`: If true, nodes in cycles are colored red
/// - `highlight_leaves`: If true, nodes with no deps are colored green
pub fn generate_dot_graph_with_options(
    modules: &[ModuleDeps],
    highlight_cycles: bool,
    highlight_leaves: bool,
) -> String {
    let mut dot = String::new();
    dot.push_str("digraph ModuleDependencies {\n");
    dot.push_str("    rankdir=TB;\n");
    dot.push_str("    node [shape=box, fontname=\"Helvetica\"];\n");
    dot.push_str("    edge [fontname=\"Helvetica\", fontsize=10];\n\n");

    // Build graph for cycle detection
    let graph = build_dependency_graph(modules);

    // Find cycles if highlighting is enabled
    let cycle_nodes: HashSet<String> = if highlight_cycles {
        let mut tarjan = TarjanSCC::new();
        let cycles = tarjan.find_cycles(&graph);
        cycles.into_iter().flatten().collect()
    } else {
        HashSet::new()
    };

    // Find leaf nodes (no outgoing dependencies)
    let leaf_nodes: HashSet<&str> = if highlight_leaves {
        modules
            .iter()
            .filter(|m| m.total_deps() == 0)
            .map(|m| m.name.as_str())
            .collect()
    } else {
        HashSet::new()
    };

    // Node definitions with styling
    for module in modules {
        let node_name = sanitize_dot_name(&module.name);

        let style = if cycle_nodes.contains(&module.name) {
            "fillcolor=\"#ffcccc\", style=filled"
        } else if leaf_nodes.contains(module.name.as_str()) {
            "fillcolor=\"#ccffcc\", style=filled"
        } else {
            ""
        };

        if !style.is_empty() {
            dot.push_str(&format!(
                "    {} [label=\"{}\", {}];\n",
                node_name, module.name, style
            ));
        } else {
            dot.push_str(&format!("    {} [label=\"{}\"];\n", node_name, module.name));
        }
    }

    dot.push('\n');

    // Edge definitions
    for module in modules {
        let src_name = sanitize_dot_name(&module.name);

        for dep in &module.opens {
            let dst_name = sanitize_dot_name(dep);
            dot.push_str(&format!(
                "    {} -> {} [label=\"open\"];\n",
                src_name, dst_name
            ));
        }

        for dep in &module.friends {
            let dst_name = sanitize_dot_name(dep);
            dot.push_str(&format!(
                "    {} -> {} [label=\"friend\", style=dashed];\n",
                src_name, dst_name
            ));
        }

        for dep in &module.includes {
            let dst_name = sanitize_dot_name(dep);
            dot.push_str(&format!(
                "    {} -> {} [label=\"include\", style=dotted];\n",
                src_name, dst_name
            ));
        }

        for dep in &module.abbreviations {
            let dst_name = sanitize_dot_name(dep);
            dot.push_str(&format!(
                "    {} -> {} [label=\"module\", style=bold];\n",
                src_name, dst_name
            ));
        }
    }

    dot.push_str("}\n");
    dot
}

/// Sanitize module name for DOT node identifier.
/// Replaces dots with underscores and ensures valid identifier.
fn sanitize_dot_name(name: &str) -> String {
    name.replace('.', "_").replace('-', "_")
}

/// Build adjacency list graph from module dependencies.
///
/// Only includes edges to modules that are present in the input list (internal deps).
/// External dependencies (e.g. FStar.*, LowStar.*) are excluded from the graph
/// since they cannot participate in cycles within the project.
pub fn build_dependency_graph(modules: &[ModuleDeps]) -> HashMap<String, Vec<String>> {
    let known_modules: HashSet<&str> = modules.iter().map(|m| m.name.as_str()).collect();
    let mut graph: HashMap<String, Vec<String>> = HashMap::new();

    for module in modules {
        let deps: Vec<String> = module
            .all_deps()
            .into_iter()
            .filter(|dep| known_modules.contains(dep))
            .map(|s| s.to_string())
            .collect();
        graph.insert(module.name.clone(), deps);
    }

    graph
}

/// Calculate dependency depth for each module.
///
/// Depth is the longest chain of internal dependencies a module has.
/// External dependencies (not in the module list) are ignored.
/// A module with no internal dependencies has depth 0.
/// A module that only depends on depth-0 modules has depth 1, etc.
/// Modules in cycles have depth set to usize::MAX.
///
/// Returns a map from module name to depth.
pub fn calculate_dependency_depths(modules: &[ModuleDeps]) -> HashMap<String, usize> {
    let graph = build_dependency_graph(modules);

    // Check for cycles first
    let mut tarjan = TarjanSCC::new();
    let cycles = tarjan.find_cycles(&graph);
    let cycle_nodes: HashSet<String> = cycles.into_iter().flatten().collect();

    let mut depths: HashMap<String, usize> = HashMap::new();

    // Nodes in cycles get MAX depth
    for node in &cycle_nodes {
        depths.insert(node.clone(), usize::MAX);
    }

    // Root nodes (no internal dependencies, not in cycle) start at depth 0
    for (name, deps) in &graph {
        if deps.is_empty() && !cycle_nodes.contains(name) {
            depths.insert(name.clone(), 0);
        }
    }

    // Iteratively compute depths until fixed point
    // A module's depth is 1 + max depth of its internal dependencies
    let mut changed = true;
    while changed {
        changed = false;
        for (name, deps) in &graph {
            if cycle_nodes.contains(name) || deps.is_empty() {
                continue;
            }

            // Compute max depth of internal dependencies
            let mut max_dep_depth: Option<usize> = Some(0);
            for dep in deps {
                if cycle_nodes.contains(dep) {
                    max_dep_depth = None;
                    break;
                }
                if let Some(dep_depth) = depths.get(dep) {
                    if *dep_depth == usize::MAX {
                        max_dep_depth = None;
                        break;
                    }
                    if let Some(current_max) = max_dep_depth {
                        max_dep_depth = Some(std::cmp::max(current_max, *dep_depth));
                    }
                } else {
                    // Internal dependency depth not yet computed; retry next iteration
                    max_dep_depth = None;
                    break;
                }
            }

            if let Some(max_d) = max_dep_depth {
                let new_depth = max_d + 1;
                let current = depths.get(name).copied();
                if current != Some(new_depth) {
                    depths.insert(name.clone(), new_depth);
                    changed = true;
                }
            }
        }
    }

    depths
}

/// Compute optimal verification order using topological sort.
///
/// Returns modules in order such that internal dependencies come before dependents.
/// External dependencies (modules not in the input list) are ignored.
/// If cycles exist among internal modules, returns None.
pub fn compute_verification_order(modules: &[ModuleDeps]) -> Option<Vec<String>> {
    // Build the internal-only dependency graph
    let graph = build_dependency_graph(modules);

    // Kahn's algorithm: count internal dependencies per module
    let mut remaining_deps: HashMap<String, usize> = HashMap::new();
    for (name, deps) in &graph {
        remaining_deps.insert(name.clone(), deps.len());
    }

    // Start with nodes that have no internal dependencies
    let mut queue: Vec<String> = remaining_deps
        .iter()
        .filter(|(_, &d)| d == 0)
        .map(|(n, _)| n.clone())
        .collect();
    queue.sort();

    let mut result: Vec<String> = Vec::new();
    let processed: &mut HashSet<String> = &mut HashSet::new();

    while let Some(node) = queue.pop() {
        if processed.contains(&node) {
            continue;
        }
        result.push(node.clone());
        processed.insert(node.clone());

        // Decrement remaining_deps for modules that depend on this node
        for (name, deps) in &graph {
            if deps.contains(&node) {
                if let Some(deg) = remaining_deps.get_mut(name) {
                    *deg = deg.saturating_sub(1);
                    if *deg == 0 && !processed.contains(name) {
                        queue.push(name.clone());
                        queue.sort();
                    }
                }
            }
        }
    }

    if result.len() != modules.len() {
        None
    } else {
        Some(result)
    }
}

/// Find all cycles in a dependency graph using Tarjan's algorithm.
pub fn find_dependency_cycles(modules: &[ModuleDeps]) -> Vec<Vec<String>> {
    let graph = build_dependency_graph(modules);
    let mut tarjan = TarjanSCC::new();
    tarjan.find_cycles(&graph)
}

/// Extract module dependencies from F* source content.
///
/// Parses module declaration, open/friend/include statements,
/// module abbreviations (`module L = FStar.List`), and scoped
/// opens (`let open FStar.UInt32 in`).
///
/// Does not perform semantic analysis - purely syntactic extraction.
pub fn extract_dependencies(content: &str) -> ModuleDeps {
    let mut deps = ModuleDeps {
        name: String::new(),
        opens: Vec::new(),
        friends: Vec::new(),
        includes: Vec::new(),
        abbreviations: Vec::new(),
    };

    for line in content.lines() {
        let stripped = line.trim();

        // Module abbreviation: `module L = FStar.List.Tot` (must check BEFORE MODULE_DECL)
        if let Some(caps) = MODULE_ABBREV.captures(stripped) {
            deps.abbreviations
                .push(caps.get(1).unwrap().as_str().to_string());
        } else if let Some(caps) = MODULE_DECL.captures(stripped) {
            // Top-level module declaration: `module Foo.Bar` (no `=` sign)
            // Only set name if not already set (first declaration wins).
            if deps.name.is_empty() {
                deps.name = caps.get(1).unwrap().as_str().to_string();
            }
        } else if let Some(caps) = OPEN_STMT.captures(stripped) {
            deps.opens.push(caps.get(1).unwrap().as_str().to_string());
        } else if let Some(caps) = LET_OPEN_STMT.captures(stripped) {
            // Scoped open: `let open FStar.UInt32 in`
            deps.opens.push(caps.get(1).unwrap().as_str().to_string());
        } else if let Some(caps) = FRIEND_STMT.captures(stripped) {
            deps.friends.push(caps.get(1).unwrap().as_str().to_string());
        } else if let Some(caps) = INCLUDE_STMT.captures(stripped) {
            deps.includes
                .push(caps.get(1).unwrap().as_str().to_string());
        }
    }

    deps
}

/// Detect if a module depends on itself (circular self-reference).
///
/// Returns error message if self-dependency found.
pub fn detect_self_dependency(deps: &ModuleDeps) -> Option<String> {
    let all: HashSet<&str> = deps.all_deps().into_iter().collect();

    if all.contains(deps.name.as_str()) {
        Some(format!("Module `{}` depends on itself", deps.name))
    } else {
        None
    }
}

/// FST015: Module dependency analyzer rule.
pub struct ModuleDepsRule;

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

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

impl Rule for ModuleDepsRule {
    fn code(&self) -> RuleCode {
        RuleCode::FST015
    }

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

        // Skip if no module declaration found
        if deps.name.is_empty() {
            return diagnostics;
        }

        // Check for self-dependency
        if let Some(msg) = detect_self_dependency(&deps) {
            diagnostics.push(Diagnostic {
                rule: RuleCode::FST015,
                severity: DiagnosticSeverity::Error,
                file: file.clone(),
                range: Range::point(1, 1),
                message: msg,
                fix: None,
            });
        }

        // Check for too many unique dependencies (>10 is a code smell in F*)
        let total_deps = deps.unique_dep_count();
        if total_deps > 10 {
            diagnostics.push(Diagnostic {
                rule: RuleCode::FST015,
                severity: DiagnosticSeverity::Warning,
                file: file.clone(),
                range: Range::point(1, 1),
                message: format!(
                    "Module has {} dependencies - consider splitting into smaller modules",
                    total_deps
                ),
                fix: None,
            });
        }

        diagnostics
    }
}

/// Multi-file cycle detection rule.
///
/// This requires analyzing multiple files together to detect cycles.
/// Use `check_multi_file` instead of the single-file `check` method.
pub struct MultiFileCycleDetector;

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

    /// Check multiple files for circular dependencies.
    ///
    /// Returns diagnostics for each cycle found.
    pub fn check_multi_file(&self, modules: &[ModuleDeps]) -> Vec<Diagnostic> {
        let cycles = find_dependency_cycles(modules);

        cycles
            .into_iter()
            .map(|cycle| {
                let cycle_str = cycle.join(" -> ");
                Diagnostic {
                    rule: RuleCode::FST015,
                    severity: DiagnosticSeverity::Error,
                    file: PathBuf::new(),
                    range: Range::point(1, 1),
                    message: format!(
                        "Circular dependency detected: {} -> {}",
                        cycle_str, cycle[0]
                    ),
                    fix: None,
                }
            })
            .collect()
    }
}

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

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

    /// Helper to create a ModuleDeps with only opens (reduces test boilerplate).
    fn make_deps(name: &str, opens: &[&str]) -> ModuleDeps {
        ModuleDeps {
            name: name.to_string(),
            opens: opens.iter().map(|s| s.to_string()).collect(),
            friends: vec![],
            includes: vec![],
            abbreviations: vec![],
        }
    }

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

open FStar.List
open FStar.Seq
friend MyModule.Helper
include MyModule.Base
"#;
        let deps = extract_dependencies(content);
        assert_eq!(deps.name, "MyModule.Test");
        assert_eq!(deps.opens, vec!["FStar.List", "FStar.Seq"]);
        assert_eq!(deps.friends, vec!["MyModule.Helper"]);
        assert_eq!(deps.includes, vec!["MyModule.Base"]);
        assert!(deps.abbreviations.is_empty());
    }

    #[test]
    fn test_extract_module_abbreviation() {
        let content = r#"
module Vale.Interop.X64

open FStar.Mul
module B = LowStar.Buffer
module HS = FStar.HyperStack
"#;
        let deps = extract_dependencies(content);
        assert_eq!(deps.name, "Vale.Interop.X64");
        assert_eq!(deps.opens, vec!["FStar.Mul"]);
        assert_eq!(deps.abbreviations, vec!["LowStar.Buffer", "FStar.HyperStack"]);
    }

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

let foo x =
  let open FStar.UInt32 in
  let open FStar.Int.Cast in
  x
"#;
        let deps = extract_dependencies(content);
        assert_eq!(deps.name, "MyModule");
        assert_eq!(deps.opens, vec!["FStar.UInt32", "FStar.Int.Cast"]);
    }

    #[test]
    fn test_module_abbreviation_does_not_corrupt_name() {
        let content = r#"
module Real.Module.Name

open FStar.Mul
module L = FStar.List.Tot
module S = FStar.Seq
"#;
        let deps = extract_dependencies(content);
        // The module name must be the top-level declaration, NOT the abbreviation alias
        assert_eq!(deps.name, "Real.Module.Name");
        assert_eq!(deps.abbreviations, vec!["FStar.List.Tot", "FStar.Seq"]);
    }

    #[test]
    fn test_self_dependency() {
        let deps = ModuleDeps {
            name: "MyModule".to_string(),
            opens: vec!["MyModule".to_string()],
            friends: vec![],
            includes: vec![],
            abbreviations: vec![],
        };
        assert!(detect_self_dependency(&deps).is_some());
    }

    #[test]
    fn test_no_self_dependency() {
        let deps = ModuleDeps {
            name: "MyModule".to_string(),
            opens: vec!["OtherModule".to_string()],
            friends: vec![],
            includes: vec![],
            abbreviations: vec![],
        };
        assert!(detect_self_dependency(&deps).is_none());
    }

    #[test]
    fn test_tarjan_no_cycles() {
        // A -> B -> C (no cycles)
        let mut graph: HashMap<String, Vec<String>> = HashMap::new();
        graph.insert("A".to_string(), vec!["B".to_string()]);
        graph.insert("B".to_string(), vec!["C".to_string()]);
        graph.insert("C".to_string(), vec![]);

        let mut tarjan = TarjanSCC::new();
        let cycles = tarjan.find_cycles(&graph);
        assert!(cycles.is_empty());
    }

    #[test]
    fn test_tarjan_simple_cycle() {
        // A -> B -> A (cycle)
        let mut graph: HashMap<String, Vec<String>> = HashMap::new();
        graph.insert("A".to_string(), vec!["B".to_string()]);
        graph.insert("B".to_string(), vec!["A".to_string()]);

        let mut tarjan = TarjanSCC::new();
        let cycles = tarjan.find_cycles(&graph);
        assert_eq!(cycles.len(), 1);
        assert_eq!(cycles[0].len(), 2);
        assert!(cycles[0].contains(&"A".to_string()));
        assert!(cycles[0].contains(&"B".to_string()));
    }

    #[test]
    fn test_tarjan_complex_cycle() {
        // A -> B -> C -> A (3-node cycle)
        // D -> E (no cycle)
        let mut graph: HashMap<String, Vec<String>> = HashMap::new();
        graph.insert("A".to_string(), vec!["B".to_string()]);
        graph.insert("B".to_string(), vec!["C".to_string()]);
        graph.insert("C".to_string(), vec!["A".to_string()]);
        graph.insert("D".to_string(), vec!["E".to_string()]);
        graph.insert("E".to_string(), vec![]);

        let mut tarjan = TarjanSCC::new();
        let cycles = tarjan.find_cycles(&graph);
        assert_eq!(cycles.len(), 1);
        assert_eq!(cycles[0].len(), 3);
    }

    #[test]
    fn test_tarjan_multiple_cycles() {
        // A -> B -> A (cycle 1)
        // C -> D -> C (cycle 2)
        let mut graph: HashMap<String, Vec<String>> = HashMap::new();
        graph.insert("A".to_string(), vec!["B".to_string()]);
        graph.insert("B".to_string(), vec!["A".to_string()]);
        graph.insert("C".to_string(), vec!["D".to_string()]);
        graph.insert("D".to_string(), vec!["C".to_string()]);

        let mut tarjan = TarjanSCC::new();
        let cycles = tarjan.find_cycles(&graph);
        assert_eq!(cycles.len(), 2);
    }

    #[test]
    fn test_dot_graph_generation() {
        let modules = vec![
            ModuleDeps {
                name: "A.Module".to_string(),
                opens: vec!["B.Module".to_string()],
                friends: vec![],
                includes: vec![],
                abbreviations: vec![],
            },
            ModuleDeps {
                name: "B.Module".to_string(),
                opens: vec![],
                friends: vec!["C.Module".to_string()],
                includes: vec![],
                abbreviations: vec![],
            },
        ];

        let dot = generate_dot_graph(&modules);
        assert!(dot.contains("digraph ModuleDependencies"));
        assert!(dot.contains("A_Module -> B_Module"));
        assert!(dot.contains("B_Module -> C_Module"));
        assert!(dot.contains("label=\"open\""));
        assert!(dot.contains("label=\"friend\""));
    }

    #[test]
    fn test_dot_cycle_highlighting() {
        let modules = vec![
            make_deps("A", &["B"]),
            make_deps("B", &["A"]),
        ];

        let dot = generate_dot_graph_with_options(&modules, true, false);
        assert!(dot.contains("fillcolor=\"#ffcccc\""));
    }

    #[test]
    fn test_dependency_depths() {
        // Linear chain: C -> B -> A
        let modules = vec![
            make_deps("A", &[]),
            make_deps("B", &["A"]),
            make_deps("C", &["B"]),
        ];

        let depths = calculate_dependency_depths(&modules);
        assert_eq!(depths.get("A"), Some(&0));
        assert_eq!(depths.get("B"), Some(&1));
        assert_eq!(depths.get("C"), Some(&2));
    }

    #[test]
    fn test_verification_order_no_cycles() {
        let modules = vec![
            make_deps("C", &["B"]),
            make_deps("B", &["A"]),
            make_deps("A", &[]),
        ];

        let order = compute_verification_order(&modules);
        assert!(order.is_some());
        let order = order.unwrap();
        // A should come before B, B should come before C
        let a_pos = order.iter().position(|x| x == "A").unwrap();
        let b_pos = order.iter().position(|x| x == "B").unwrap();
        let c_pos = order.iter().position(|x| x == "C").unwrap();
        assert!(a_pos < b_pos);
        assert!(b_pos < c_pos);
    }

    #[test]
    fn test_verification_order_with_cycle() {
        let modules = vec![
            make_deps("A", &["B"]),
            make_deps("B", &["A"]),
        ];

        let order = compute_verification_order(&modules);
        assert!(order.is_none());
    }

    #[test]
    fn test_find_dependency_cycles() {
        let modules = vec![
            make_deps("A", &["B"]),
            make_deps("B", &["C"]),
            make_deps("C", &["A"]),
        ];

        let cycles = find_dependency_cycles(&modules);
        assert_eq!(cycles.len(), 1);
        assert_eq!(cycles[0].len(), 3);
    }

    #[test]
    fn test_multi_file_cycle_detector() {
        let modules = vec![
            make_deps("A", &["B"]),
            make_deps("B", &["A"]),
        ];

        let detector = MultiFileCycleDetector::new();
        let diagnostics = detector.check_multi_file(&modules);
        assert_eq!(diagnostics.len(), 1);
        assert!(diagnostics[0].message.contains("Circular dependency"));
    }

    #[test]
    fn test_module_deps_all_deps() {
        let deps = ModuleDeps {
            name: "Test".to_string(),
            opens: vec!["A".to_string(), "B".to_string()],
            friends: vec!["C".to_string()],
            includes: vec!["D".to_string()],
            abbreviations: vec!["E".to_string()],
        };

        let all = deps.all_deps();
        assert_eq!(all.len(), 5);
        assert!(all.contains(&"A"));
        assert!(all.contains(&"B"));
        assert!(all.contains(&"C"));
        assert!(all.contains(&"D"));
        assert!(all.contains(&"E"));
    }

    #[test]
    fn test_unique_dep_count_deduplicates() {
        let deps = ModuleDeps {
            name: "Test".to_string(),
            opens: vec!["A".to_string(), "B".to_string()],
            friends: vec![],
            includes: vec![],
            abbreviations: vec!["A".to_string()],
        };
        assert_eq!(deps.total_deps(), 3);
        assert_eq!(deps.unique_dep_count(), 2);
    }

    #[test]
    fn test_verification_order_with_external_deps() {
        // Modules depend on external FStar.List which is NOT in the module list.
        // The old code would incorrectly report a cycle here.
        let modules = vec![
            ModuleDeps {
                name: "C".to_string(),
                opens: vec!["B".to_string(), "FStar.List".to_string()],
                friends: vec![],
                includes: vec![],
                abbreviations: vec![],
            },
            ModuleDeps {
                name: "B".to_string(),
                opens: vec!["A".to_string(), "FStar.Seq".to_string()],
                friends: vec![],
                includes: vec![],
                abbreviations: vec![],
            },
            make_deps("A", &[]),
        ];

        let order = compute_verification_order(&modules);
        assert!(
            order.is_some(),
            "Should not report cycle when external deps are present"
        );
    }

    #[test]
    fn test_dependency_depths_with_external_deps() {
        let modules = vec![
            make_deps("A", &[]),
            ModuleDeps {
                name: "B".to_string(),
                opens: vec!["A".to_string(), "FStar.List".to_string()],
                friends: vec![],
                includes: vec![],
                abbreviations: vec![],
            },
        ];

        let depths = calculate_dependency_depths(&modules);
        assert_eq!(depths.get("A"), Some(&0));
        assert_eq!(depths.get("B"), Some(&1));
    }

    #[test]
    fn test_build_graph_filters_external_deps() {
        let modules = vec![
            ModuleDeps {
                name: "A".to_string(),
                opens: vec!["B".to_string(), "FStar.List".to_string()],
                friends: vec![],
                includes: vec![],
                abbreviations: vec!["FStar.Seq".to_string()],
            },
            make_deps("B", &[]),
        ];

        let graph = build_dependency_graph(&modules);
        assert_eq!(graph["A"], vec!["B".to_string()]);
    }

    #[test]
    fn test_extract_real_vale_file() {
        let content = r#"
module Vale.Interop.X64

open FStar.Mul
open Vale.Interop.Base
module B = LowStar.Buffer
module BS = Vale.X64.Machine_Semantics_s
module HS = FStar.HyperStack

let foo x =
  let open FStar.UInt32 in
  x
"#;
        let deps = extract_dependencies(content);
        assert_eq!(deps.name, "Vale.Interop.X64");
        assert_eq!(
            deps.opens,
            vec!["FStar.Mul", "Vale.Interop.Base", "FStar.UInt32"]
        );
        assert_eq!(
            deps.abbreviations,
            vec![
                "LowStar.Buffer",
                "Vale.X64.Machine_Semantics_s",
                "FStar.HyperStack"
            ]
        );
        assert_eq!(deps.total_deps(), 6);
    }

    #[test]
    fn test_sanitize_dot_name() {
        assert_eq!(sanitize_dot_name("FStar.List"), "FStar_List");
        assert_eq!(sanitize_dot_name("A.B.C"), "A_B_C");
        assert_eq!(sanitize_dot_name("Simple"), "Simple");
        assert_eq!(sanitize_dot_name("My-Module"), "My_Module");
    }
}